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
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-2024-09-11"
channel = "nightly-2024-09-12"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-arith-overflows/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct i8x2(i8, i8);
pub struct i8x2([i8; 2]);

#[kani::proof]
fn main() {
let a = kani::any();
let b = kani::any();
let simd_a = i8x2(a, a);
let simd_b = i8x2(b, b);
let simd_a = i8x2([a, a]);
let simd_b = i8x2([b, b]);

unsafe {
let _ = simd_add(simd_a, simd_b);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,26 +9,26 @@ use std::intrinsics::simd::simd_eq;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

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

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

#[kani::proof]
fn main() {
let x = u64x2(0, 0);
let y = u64x2(0, 1);
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 == u32x4([u32::MAX, u32::MAX, 0, 0]));
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
// error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected
Expand Down
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-div-div-zero/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_div;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_div() {
let dividend = kani::any();
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = 0;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let _ = unsafe { simd_div(dividends, divisors) };
}
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 == quotients.1
assertion failed: quotients.0[0] == quotients.0[1]
FAILURE\
attempt to compute simd_rem which would overflow
UNREACHABLE\
assertion failed: remainders.0 == remainders.1
assertion failed: remainders.0[0] == remainders.0[1]
14 changes: 7 additions & 7 deletions tests/expected/intrinsics/simd-div-rem-overflow/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use std::intrinsics::simd::{simd_div, simd_rem};
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
simd_div(dividends, divisors)
Expand All @@ -21,19 +21,19 @@ unsafe fn do_simd_rem(dividends: i32x2, divisors: i32x2) -> i32x2 {
#[kani::proof]
fn test_simd_div_overflow() {
let dividend = i32::MIN;
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = -1;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let quotients = unsafe { do_simd_div(dividends, divisors) };
assert_eq!(quotients.0, quotients.1);
assert_eq!(quotients.0[0], quotients.0[1]);
}

#[kani::proof]
fn test_simd_rem_overflow() {
let dividend = i32::MIN;
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = -1;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let remainders = unsafe { do_simd_rem(dividends, divisors) };
assert_eq!(remainders.0, remainders.1);
assert_eq!(remainders.0[0], remainders.0[1]);
}
4 changes: 2 additions & 2 deletions tests/expected/intrinsics/simd-extract-wrong-type/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_extract;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let y = i64x2([0, 1]);
let res: i32 = unsafe { simd_extract(y, 1) };
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
Expand Down
4 changes: 2 additions & 2 deletions tests/expected/intrinsics/simd-insert-wrong-type/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_insert;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let y = i64x2([0, 1]);
let _ = unsafe { simd_insert(y, 0, 1) };
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
Expand Down
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-rem-div-zero/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_rem;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_rem() {
let dividend = kani::any();
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = 0;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let _ = unsafe { simd_rem(dividends, divisors) };
}
14 changes: 7 additions & 7 deletions tests/expected/intrinsics/simd-result-type-is-float/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,31 +9,31 @@ use std::intrinsics::simd::simd_eq;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

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

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

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

#[kani::proof]
fn main() {
let x = u64x2(0, 0);
let y = u64x2(0, 1);
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 == f32x2([0.0, -1.0]));
// ^^^^ 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
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shl-shift-negative/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift < 32);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shl(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift >= 0);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shl(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shr-shift-negative/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shr;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shr() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift < 32);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shr(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shr;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shr() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift >= 0);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shr(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@ use std::intrinsics::simd::simd_shuffle;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let z = i64x2(1, 2);
let y = i64x2([0, 1]);
let z = i64x2([1, 2]);
// Only [0, 3] are valid indexes, 4 is out of bounds
const I: [u32; 2] = [1, 4];
let _: i64x2 = unsafe { simd_shuffle(y, z, I) };
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,17 @@ use std::intrinsics::simd::simd_shuffle;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

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

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let z = i64x2(1, 2);
let y = i64x2([0, 1]);
let z = i64x2([1, 2]);
const I: [u32; 4] = [1, 2, 1, 2];
let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
// ^^^^ The code above fails to type-check in Rust with the error:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,17 @@ use std::intrinsics::simd::simd_shuffle;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

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

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let z = i64x2(1, 2);
let y = i64x2([0, 1]);
let z = i64x2([1, 2]);
const I: [u32; 2] = [1, 2];
let x: f64x2 = unsafe { simd_shuffle(y, z, I) };
// ^^^^ The code above fails to type-check in Rust with the error:
Expand Down
34 changes: 17 additions & 17 deletions tests/kani/Intrinsics/SIMD/Compare/float.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,17 @@ use std::intrinsics::simd::*;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct f64x2(f64, f64);
pub struct f64x2([f64; 2]);

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

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

macro_rules! assert_cmp {
($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
Expand All @@ -29,21 +29,21 @@ macro_rules! assert_cmp {

#[kani::proof]
fn main() {
let x = f64x2(0.0, 0.0);
let y = f64x2(0.0, 1.0);
let x = f64x2([0.0, 0.0]);
let y = f64x2([0.0, 1.0]);

unsafe {
assert_cmp!(res_eq, simd_eq, x, x, -1, -1);
assert_cmp!(res_eq, simd_eq, x, y, -1, 0);
assert_cmp!(res_ne, simd_ne, x, x, 0, 0);
assert_cmp!(res_ne, simd_ne, x, y, 0, -1);
assert_cmp!(res_lt, simd_lt, x, x, 0, 0);
assert_cmp!(res_lt, simd_lt, x, y, 0, -1);
assert_cmp!(res_le, simd_le, x, x, -1, -1);
assert_cmp!(res_le, simd_le, x, y, -1, -1);
assert_cmp!(res_gt, simd_gt, x, x, 0, 0);
assert_cmp!(res_gt, simd_gt, x, y, 0, 0);
assert_cmp!(res_ge, simd_ge, x, x, -1, -1);
assert_cmp!(res_ge, simd_ge, x, y, -1, 0);
assert_cmp!(res_eq, simd_eq, x, x, [-1, -1]);
assert_cmp!(res_eq, simd_eq, x, y, [-1, 0]);
assert_cmp!(res_ne, simd_ne, x, x, [0, 0]);
assert_cmp!(res_ne, simd_ne, x, y, [0, -1]);
assert_cmp!(res_lt, simd_lt, x, x, [0, 0]);
assert_cmp!(res_lt, simd_lt, x, y, [0, -1]);
assert_cmp!(res_le, simd_le, x, x, [-1, -1]);
assert_cmp!(res_le, simd_le, x, y, [-1, -1]);
assert_cmp!(res_gt, simd_gt, x, x, [0, 0]);
assert_cmp!(res_gt, simd_gt, x, y, [0, 0]);
assert_cmp!(res_ge, simd_ge, x, x, [-1, -1]);
assert_cmp!(res_ge, simd_ge, x, y, [-1, 0]);
}
}
Loading