Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 5 additions & 6 deletions library/kani/src/models/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ mod test {
}

#[repr(simd)]
#[derive(Clone, Debug)]
#[derive(Copy, Clone, Debug)]
struct CustomMask<T, const LANES: usize>([T; LANES]);

/// Check that the bitmask model can handle odd size SIMD arrays.
Expand Down Expand Up @@ -276,15 +276,14 @@ mod test {
/// Compare the value returned by our model and the simd_bitmask intrinsic.
fn check_bitmask<T, U, E, const LANES: usize>(mask: T)
where
T: Clone,
T: Clone + Copy,
U: PartialEq + Debug,
E: kani_intrinsic::MaskElement,
[u8; kani_intrinsic::mask_len(LANES)]: Sized,
{
assert_eq!(
unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) },
unsafe { simd_bitmask::<T, U>(mask) }
);
assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask) }, unsafe {
simd_bitmask::<T, U>(mask)
});
}

/// Similar to portable simd_harness.
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2025-07-21"
channel = "nightly-2025-07-24"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/simd-arith-overflows/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
#[derive(Clone, Copy)]
pub struct i8x2([i8; 2]);

#[kani::proof]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,27 +8,33 @@ use std::intrinsics::simd::simd_eq;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct u64x2([u64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct u32x4([u32; 4]);

impl u32x4 {
fn into_array(self) -> [u32; 4] {
unsafe { std::mem::transmute(self) }
}
}

#[kani::proof]
fn main() {
let x = u64x2([0, 0]);
let y = u64x2([0, 1]);

unsafe {
let invalid_simd: u32x4 = simd_eq(x, y);
assert!(invalid_simd == u32x4([u32::MAX, u32::MAX, 0, 0]));
assert!(invalid_simd.into_array() == u32x4([u32::MAX, u32::MAX, 0, 0]).into_array());
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
// error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected
Expand Down
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/simd-div-div-zero/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_div;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

#[kani::proof]
Expand Down
4 changes: 2 additions & 2 deletions tests/expected/intrinsics/simd-div-rem-overflow/expected
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
FAILURE\
attempt to compute simd_div which would overflow
UNREACHABLE\
assertion failed: quotients.0[0] == quotients.0[1]
assertion failed: quotients.into_array()[0] == quotients.into_array()[1]
FAILURE\
attempt to compute simd_rem which would overflow
UNREACHABLE\
assertion failed: remainders.0[0] == remainders.0[1]
assertion failed: remainders.into_array()[0] == remainders.into_array()[1]
12 changes: 9 additions & 3 deletions tests/expected/intrinsics/simd-div-rem-overflow/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,15 @@ use std::intrinsics::simd::{simd_div, simd_rem};

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

impl i32x2 {
fn into_array(self) -> [i32; 2] {
unsafe { std::mem::transmute(self) }
}
}

unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
simd_div(dividends, divisors)
}
Expand All @@ -25,7 +31,7 @@ fn test_simd_div_overflow() {
let divisor = -1;
let divisors = i32x2([divisor, divisor]);
let quotients = unsafe { do_simd_div(dividends, divisors) };
assert_eq!(quotients.0[0], quotients.0[1]);
assert_eq!(quotients.into_array()[0], quotients.into_array()[1]);
}

#[kani::proof]
Expand All @@ -35,5 +41,5 @@ fn test_simd_rem_overflow() {
let divisor = -1;
let divisors = i32x2([divisor, divisor]);
let remainders = unsafe { do_simd_rem(dividends, divisors) };
assert_eq!(remainders.0[0], remainders.0[1]);
assert_eq!(remainders.into_array()[0], remainders.into_array()[1]);
}
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use std::intrinsics::simd::simd_extract;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[kani::proof]
Expand Down
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/simd-insert-wrong-type/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use std::intrinsics::simd::simd_insert;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[kani::proof]
Expand Down
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/simd-rem-div-zero/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_rem;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

#[kani::proof]
Expand Down
16 changes: 11 additions & 5 deletions tests/expected/intrinsics/simd-result-type-is-float/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,32 +8,38 @@ use std::intrinsics::simd::simd_eq;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct u64x2([u64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct u32x4([u32; 4]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
#[derive(Clone, Copy)]
pub struct f32x2([f32; 2]);

impl f32x2 {
fn into_array(self) -> [f32; 2] {
unsafe { std::mem::transmute(self) }
}
}

#[kani::proof]
fn main() {
let x = u64x2([0, 0]);
let y = u64x2([0, 1]);

unsafe {
let invalid_simd: f32x2 = simd_eq(x, y);
assert!(invalid_simd == f32x2([0.0, -1.0]));
assert!(invalid_simd.into_array() == f32x2([0.0, -1.0]).into_array());
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
// error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected return type with integer elements, found `f32x2` with non-integer `f32`
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shl;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

#[kani::proof]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shl;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

#[kani::proof]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shr;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

#[kani::proof]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::intrinsics::simd::simd_shr;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

#[kani::proof]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use std::intrinsics::simd::simd_shuffle;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,12 @@ use std::intrinsics::simd::simd_shuffle;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x4([i64; 4]);

#[repr(simd)]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,12 @@ use std::intrinsics::simd::simd_shuffle;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
#[derive(Clone, Copy)]
pub struct f64x2([f64; 2]);

#[repr(simd)]
Expand Down
14 changes: 10 additions & 4 deletions tests/kani/Intrinsics/SIMD/Compare/float.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,23 +7,29 @@ use std::intrinsics::simd::*;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
#[derive(Clone, Copy)]
pub struct f64x2([f64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
#[derive(Clone, Copy)]
pub struct i32x2([i32; 2]);

impl i32x2 {
fn into_array(self) -> [i32; 2] {
unsafe { std::mem::transmute(self) }
}
}

macro_rules! assert_cmp {
($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
let $res_cmp: i32x2 = $simd_cmp($x, $y);
assert!($res_cmp == i32x2($($res),+))
assert!($res_cmp.into_array() == i32x2($($res),+).into_array())
};
}

Expand Down
22 changes: 17 additions & 5 deletions tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,29 +8,41 @@ use std::intrinsics::simd::simd_eq;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

impl i64x2 {
fn into_array(self) -> [i64; 2] {
unsafe { std::mem::transmute(self) }
}
}

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct u64x2([u64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct u32x2([u32; 2]);

impl u32x2 {
fn into_array(self) -> [u32; 2] {
unsafe { std::mem::transmute(self) }
}
}

#[kani::proof]
fn main() {
let x = u64x2([0, 0]);
let y = u64x2([0, 1]);

unsafe {
let w: i64x2 = simd_eq(x, y);
assert!(w == i64x2([-1, 0]));
assert!(w.into_array() == i64x2([-1, 0]).into_array());

let z: u32x2 = simd_eq(x, y);
assert!(z == u32x2([u32::MAX, 0]));
assert!(z.into_array() == u32x2([u32::MAX, 0]).into_array());
}
}
10 changes: 8 additions & 2 deletions tests/kani/Intrinsics/SIMD/Compare/signed.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,19 @@ use std::intrinsics::simd::*;

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
#[derive(Clone, Copy)]
pub struct i64x2([i64; 2]);

impl i64x2 {
fn into_array(self) -> [i64; 2] {
unsafe { std::mem::transmute(self) }
}
}

macro_rules! assert_cmp {
($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
let $res_cmp: i64x2 = $simd_cmp($x, $y);
assert!($res_cmp == i64x2($($res),+))
assert!($res_cmp.into_array() == i64x2($($res),+).into_array())
};
}

Expand Down
Loading
Loading