Fix more tests

model-checking · Sep 18, 2024 · d1ab704 · d1ab704
1 parent 30252df
commit d1ab704
Show file tree

Hide file tree

Showing 16 changed files with 58 additions and 58 deletions.
diff --git a/tests/expected/intrinsics/simd-arith-overflows/main.rs b/tests/expected/intrinsics/simd-arith-overflows/main.rs
@@ -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);

diff --git a/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs
@@ -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

diff --git a/tests/expected/intrinsics/simd-div-div-zero/main.rs b/tests/expected/intrinsics/simd-div-div-zero/main.rs
@@ -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) };
 }
diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/expected b/tests/expected/intrinsics/simd-div-rem-overflow/expected
@@ -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]
diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs
@@ -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)
@@ -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]);
 }
diff --git a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs b/tests/expected/intrinsics/simd-extract-wrong-type/main.rs
@@ -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:
     // ```

diff --git a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs b/tests/expected/intrinsics/simd-insert-wrong-type/main.rs
@@ -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:
     // ```

diff --git a/tests/expected/intrinsics/simd-rem-div-zero/main.rs b/tests/expected/intrinsics/simd-rem-div-zero/main.rs
@@ -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) };
 }
diff --git a/tests/expected/intrinsics/simd-result-type-is-float/main.rs b/tests/expected/intrinsics/simd-result-type-is-float/main.rs
@@ -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`

diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs
@@ -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) };
 }
diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
@@ -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) };
 }
diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs
@@ -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) };
 }
diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
@@ -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) };
 }
diff --git a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
@@ -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) };

diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs
@@ -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:

diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs
@@ -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: