From d2051b77437a0032120f0513e0e9c3c4766d8562 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 18 Sep 2024 02:54:13 -0500 Subject: [PATCH] Upgrade toolchain to 2024-09-12 (#3524) Relevant upstream PR: https://github.com/rust-lang/rust/commit/d2309c2a9d Ban non-array SIMD Resolves https://github.com/model-checking/kani/issues/3521 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- rust-toolchain.toml | 2 +- .../intrinsics/simd-arith-overflows/main.rs | 6 ++-- .../simd-cmp-result-type-is-diff-size/main.rs | 12 +++---- .../intrinsics/simd-div-div-zero/main.rs | 6 ++-- .../intrinsics/simd-div-rem-overflow/expected | 4 +-- .../intrinsics/simd-div-rem-overflow/main.rs | 14 ++++---- .../simd-extract-wrong-type/main.rs | 4 +-- .../intrinsics/simd-insert-wrong-type/main.rs | 4 +-- .../intrinsics/simd-rem-div-zero/main.rs | 6 ++-- .../simd-result-type-is-float/main.rs | 14 ++++---- .../simd-shl-shift-negative/main.rs | 6 ++-- .../simd-shl-shift-too-large/main.rs | 6 ++-- .../simd-shr-shift-negative/main.rs | 6 ++-- .../simd-shr-shift-too-large/main.rs | 6 ++-- .../simd-shuffle-indexes-out/main.rs | 6 ++-- .../main.rs | 8 ++--- .../main.rs | 8 ++--- tests/kani/Intrinsics/SIMD/Compare/float.rs | 34 +++++++++---------- .../SIMD/Compare/result_type_is_same_size.rs | 14 ++++---- tests/kani/Intrinsics/SIMD/Compare/signed.rs | 30 ++++++++-------- .../kani/Intrinsics/SIMD/Compare/unsigned.rs | 30 ++++++++-------- .../kani/Intrinsics/SIMD/Construction/main.rs | 16 ++++----- tests/kani/Intrinsics/SIMD/Operators/arith.rs | 10 +++--- .../Intrinsics/SIMD/Operators/bitshift.rs | 22 ++++++------ .../kani/Intrinsics/SIMD/Operators/bitwise.rs | 24 ++++++------- .../Intrinsics/SIMD/Operators/division.rs | 14 ++++---- .../SIMD/Operators/division_float.rs | 6 ++-- tests/kani/Intrinsics/SIMD/Shuffle/main.rs | 30 ++++++++-------- tests/kani/SIMD/generic_access.rs | 8 ++--- tests/kani/SIMD/multi_field_simd.rs | 12 +++---- 30 files changed, 184 insertions(+), 184 deletions(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 1177a1ec6809..934515867187 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"] diff --git a/tests/expected/intrinsics/simd-arith-overflows/main.rs b/tests/expected/intrinsics/simd-arith-overflows/main.rs index fc710645fd66..28be8e309774 100644 --- 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 index f84cf1d8b9aa..fd4dd40b17b8 100644 --- 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 index 148ae62a252c..0765e0fd0755 100644 --- 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 index 156854c7dcdc..9c1a0aa96774 100644 --- 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 \ No newline at end of file +assertion failed: remainders.0[0] == remainders.0[1] \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs index 5f49e7db6154..117fd6bffe95 100644 --- 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 index b8fb5a3ffc6f..9af6b5279ec6 100644 --- 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 index 6c4946a051b6..8a0853cc7945 100644 --- 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 index 4393808ac039..7ed9bd2968cd 100644 --- 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 index 01286de9cdd8..2d7892a1a537 100644 --- 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 index 2b7b2a418e19..f18a9ba14190 100644 --- 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 index dada7a5a8b84..75b73a5b81f1 100644 --- 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 index dc38955099a2..f46a91b37c21 100644 --- 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 index 70ae0ad0da45..cdcfce0cf755 100644 --- 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 index 0f7c42d2d46c..b89f40369853 100644 --- 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 index 6345f5516101..3fe534f3bc08 100644 --- 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 index 81f176700152..8c7cd5245cbe 100644 --- 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: diff --git a/tests/kani/Intrinsics/SIMD/Compare/float.rs b/tests/kani/Intrinsics/SIMD/Compare/float.rs index cc5765ef226b..6c69d142ff7d 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/float.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/float.rs @@ -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),+) => { @@ -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]); } } diff --git a/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs b/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs index d3582057fd00..584a5e07876a 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs @@ -9,28 +9,28 @@ 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 u32x2(u32, u32); +pub struct u32x2([u32; 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 w: i64x2 = simd_eq(x, y); - assert!(w == i64x2(-1, 0)); + assert!(w == i64x2([-1, 0])); let z: u32x2 = simd_eq(x, y); - assert!(z == u32x2(u32::MAX, 0)); + assert!(z == u32x2([u32::MAX, 0])); } } diff --git a/tests/kani/Intrinsics/SIMD/Compare/signed.rs b/tests/kani/Intrinsics/SIMD/Compare/signed.rs index cfd781fa64c7..671078bad2d4 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/signed.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/signed.rs @@ -8,7 +8,7 @@ use std::intrinsics::simd::*; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct i64x2(i64, i64); +pub struct i64x2([i64; 2]); macro_rules! assert_cmp { ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => { @@ -23,21 +23,21 @@ macro_rules! assert_cmp { // * No bits set (e.g., 0 in signed integers) if the result is true #[kani::proof] fn main() { - let x = i64x2(0, 0); - let y = i64x2(0, 1); + let x = i64x2([0, 0]); + let y = i64x2([0, 1]); 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]); } } diff --git a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs index ee39f750c8a2..b2943b36ab71 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs @@ -8,7 +8,7 @@ use std::intrinsics::simd::*; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct u64x2(u64, u64); +pub struct u64x2([u64; 2]); macro_rules! assert_cmp { ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => { @@ -23,21 +23,21 @@ macro_rules! assert_cmp { // * No bits set (e.g., 0 in signed integers) if the result is true #[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 { - assert_cmp!(res_eq, simd_eq, x, x, u64::MAX, u64::MAX); - assert_cmp!(res_eq, simd_eq, x, y, u64::MAX, 0); - assert_cmp!(res_ne, simd_ne, x, x, 0, 0); - assert_cmp!(res_ne, simd_ne, x, y, 0, u64::MAX); - assert_cmp!(res_lt, simd_lt, x, x, 0, 0); - assert_cmp!(res_lt, simd_lt, x, y, 0, u64::MAX); - assert_cmp!(res_le, simd_le, x, x, u64::MAX, u64::MAX); - assert_cmp!(res_le, simd_le, x, y, u64::MAX, u64::MAX); - 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, u64::MAX, u64::MAX); - assert_cmp!(res_ge, simd_ge, x, y, u64::MAX, 0); + assert_cmp!(res_eq, simd_eq, x, x, [u64::MAX, u64::MAX]); + assert_cmp!(res_eq, simd_eq, x, y, [u64::MAX, 0]); + assert_cmp!(res_ne, simd_ne, x, x, [0, 0]); + assert_cmp!(res_ne, simd_ne, x, y, [0, u64::MAX]); + assert_cmp!(res_lt, simd_lt, x, x, [0, 0]); + assert_cmp!(res_lt, simd_lt, x, y, [0, u64::MAX]); + assert_cmp!(res_le, simd_le, x, x, [u64::MAX, u64::MAX]); + assert_cmp!(res_le, simd_le, x, y, [u64::MAX, u64::MAX]); + 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, [u64::MAX, u64::MAX]); + assert_cmp!(res_ge, simd_ge, x, y, [u64::MAX, 0]); } } diff --git a/tests/kani/Intrinsics/SIMD/Construction/main.rs b/tests/kani/Intrinsics/SIMD/Construction/main.rs index 5de3ae20d868..92c5a167dc15 100644 --- a/tests/kani/Intrinsics/SIMD/Construction/main.rs +++ b/tests/kani/Intrinsics/SIMD/Construction/main.rs @@ -9,16 +9,16 @@ use std::intrinsics::simd::{simd_extract, 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 z = i64x2(1, 2); + let y = i64x2([0, 1]); + let z = i64x2([1, 2]); // Indexing into the vectors - assert!(z.0 == 1); - assert!(z.1 == 2); + assert!(z.0[0] == 1); + assert!(z.0[1] == 2); { // Intrinsic indexing @@ -31,9 +31,9 @@ fn main() { // Intrinsic updating let m = unsafe { simd_insert(y, 0, 1_i64) }; let n = unsafe { simd_insert(y, 1, 5_i64) }; - assert!(m.0 == 1 && m.1 == 1); - assert!(n.0 == 0 && n.1 == 5); + assert!(m.0[0] == 1 && m.0[1] == 1); + assert!(n.0[0] == 0 && n.0[1] == 5); // Original unchanged - assert!(y.0 == 0 && y.1 == 1); + assert!(y.0[0] == 0 && y.0[1] == 1); } } diff --git a/tests/kani/Intrinsics/SIMD/Operators/arith.rs b/tests/kani/Intrinsics/SIMD/Operators/arith.rs index d9f442a659ba..33a8ba65b538 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/arith.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/arith.rs @@ -9,7 +9,7 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub}; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct i8x2(i8, i8); +pub struct i8x2([i8; 2]); macro_rules! verify_no_overflow { ($cf: ident, $uf: ident) => {{ @@ -17,11 +17,11 @@ macro_rules! verify_no_overflow { let b: i8 = kani::any(); let checked = a.$cf(b); kani::assume(checked.is_some()); - let simd_a = i8x2(a, a); - let simd_b = i8x2(b, b); + let simd_a = i8x2([a, a]); + let simd_b = i8x2([b, b]); let unchecked: i8x2 = unsafe { $uf(simd_a, simd_b) }; - assert!(checked.unwrap() == unchecked.0); - assert!(checked.unwrap() == unchecked.1); + assert!(checked.unwrap() == unchecked.0[0]); + assert!(checked.unwrap() == unchecked.0[1]); }}; } diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs index fa2cd3c52cd6..09a19fa7b29a 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs @@ -9,47 +9,47 @@ use std::intrinsics::simd::{simd_shl, simd_shr}; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct i32x2(i32, i32); +pub struct i32x2([i32; 2]); #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct u32x2(u32, u32); +pub struct u32x2([u32; 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); kani::assume(shift < 32); - let shifts = i32x2(shift, shift); + let shifts = i32x2([shift, shift]); let normal_result = value << shift; let simd_result = unsafe { simd_shl(values, shifts) }; - assert_eq!(normal_result, simd_result.0); + assert_eq!(normal_result, simd_result.0[0]); } #[kani::proof] fn test_simd_shr_signed() { let value = kani::any(); - let values = i32x2(value, value); + let values = i32x2([value, value]); let shift = kani::any(); kani::assume(shift >= 0); kani::assume(shift < 32); - let shifts = i32x2(shift, shift); + let shifts = i32x2([shift, shift]); let normal_result = value >> shift; let simd_result = unsafe { simd_shr(values, shifts) }; - assert_eq!(normal_result, simd_result.0); + assert_eq!(normal_result, simd_result.0[0]); } #[kani::proof] fn test_simd_shr_unsigned() { let value = kani::any(); - let values = u32x2(value, value); + let values = u32x2([value, value]); let shift = kani::any(); kani::assume(shift < 32); - let shifts = u32x2(shift, shift); + let shifts = u32x2([shift, shift]); let normal_result = value >> shift; let simd_result = unsafe { simd_shr(values, shifts) }; - assert_eq!(normal_result, simd_result.0); + assert_eq!(normal_result, simd_result.0[0]); } diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs index b18410088f18..a9aaa96f75e5 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs @@ -14,52 +14,52 @@ use std::intrinsics::simd::{simd_and, simd_or, simd_xor}; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct i8x2(i8, i8); +pub struct i8x2([i8; 2]); #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct i16x2(i16, i16); +pub struct i16x2([i16; 2]); #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct i32x2(i32, i32); +pub struct i32x2([i32; 2]); #[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 u8x2(u8, u8); +pub struct u8x2([u8; 2]); #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct u16x2(u16, u16); +pub struct u16x2([u16; 2]); #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct u32x2(u32, u32); +pub struct u32x2([u32; 2]); #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] -pub struct u64x2(u64, u64); +pub struct u64x2([u64; 2]); macro_rules! compare_simd_op_with_normal_op { ($simd_op: ident, $normal_op: tt, $simd_type: ident) => { let tup_x: (_,_) = kani::any(); let tup_y: (_,_) = kani::any(); - let x = $simd_type(tup_x.0, tup_x.1); - let y = $simd_type(tup_y.0, tup_y.1); + let x = $simd_type([tup_x.0, tup_x.1]); + let y = $simd_type([tup_y.0, tup_y.1]); let res_and = unsafe { $simd_op(x, y) }; - assert_eq!(tup_x.0 $normal_op tup_y.0, res_and.0); - assert_eq!(tup_x.1 $normal_op tup_y.1, res_and.1); + assert_eq!(tup_x.0 $normal_op tup_y.0, res_and.0[0]); + assert_eq!(tup_x.1 $normal_op tup_y.1, res_and.0[1]); }; } diff --git a/tests/kani/Intrinsics/SIMD/Operators/division.rs b/tests/kani/Intrinsics/SIMD/Operators/division.rs index e1e8dab39cca..d48968342ca4 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/division.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/division.rs @@ -9,32 +9,32 @@ 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]); #[kani::proof] fn test_simd_div() { let dividend = kani::any(); - let dividends = i32x2(dividend, dividend); + let dividends = i32x2([dividend, dividend]); let divisor = kani::any(); // Narrow down the divisor interval so the operation doesn't overflow and // the test finishes in a short time kani::assume(divisor > 0 && divisor < 5); - let divisors = i32x2(divisor, divisor); + let divisors = i32x2([divisor, divisor]); let normal_result = dividend / divisor; let simd_result = unsafe { simd_div(dividends, divisors) }; - assert_eq!(normal_result, simd_result.0); + assert_eq!(normal_result, simd_result.0[0]); } #[kani::proof] fn test_simd_rem() { let dividend = kani::any(); - let dividends = i32x2(dividend, dividend); + let dividends = i32x2([dividend, dividend]); let divisor = kani::any(); // Narrow down the divisor interval so the operation doesn't overflow and // the test finishes in a short time kani::assume(divisor > 0 && divisor < 5); - let divisors = i32x2(divisor, divisor); + let divisors = i32x2([divisor, divisor]); let normal_result = dividend % divisor; let simd_result = unsafe { simd_rem(dividends, divisors) }; - assert_eq!(normal_result, simd_result.0); + assert_eq!(normal_result, simd_result.0[0]); } diff --git a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs index 711b67b87116..d61bd81f1f87 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs @@ -8,15 +8,15 @@ use std::intrinsics::simd::simd_div; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, kani::Arbitrary)] -pub struct f32x2(f32, f32); +pub struct f32x2([f32; 2]); impl f32x2 { fn new_with(f: impl Fn() -> f32) -> Self { - f32x2(f(), f()) + f32x2([f(), f()]) } fn non_simd_div(self, divisors: Self) -> Self { - f32x2(self.0 / divisors.0, self.1 / divisors.1) + f32x2([self.0[0] / divisors.0[0], self.0[1] / divisors.0[1]]) } } diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index 9b6870e40004..a105a3b1d81e 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -9,45 +9,45 @@ 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; 2] = [1, 2]; let x: i64x2 = unsafe { simd_shuffle(y, z, I) }; - assert!(x.0 == 1); - assert!(x.1 == 1); + assert!(x.0[0] == 1); + assert!(x.0[1] == 1); } { - 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: i64x2 = unsafe { simd_shuffle(y, z, I) }; - assert!(x.0 == 1); - assert!(x.1 == 1); + assert!(x.0[0] == 1); + assert!(x.0[1] == 1); } { - let a = i64x4(1, 2, 3, 4); - let b = i64x4(5, 6, 7, 8); + let a = i64x4([1, 2, 3, 4]); + let b = i64x4([5, 6, 7, 8]); const I: [u32; 4] = [1, 3, 5, 7]; let c: i64x4 = unsafe { simd_shuffle(a, b, I) }; - assert!(c == i64x4(2, 4, 6, 8)); + assert!(c == i64x4([2, 4, 6, 8])); } } #[kani::proof] fn check_shuffle() { { - 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, 0, 3]; let _x: i64x4 = unsafe { simd_shuffle(y, z, I) }; } diff --git a/tests/kani/SIMD/generic_access.rs b/tests/kani/SIMD/generic_access.rs index 280175a781c6..805eeaa403ea 100644 --- a/tests/kani/SIMD/generic_access.rs +++ b/tests/kani/SIMD/generic_access.rs @@ -31,20 +31,20 @@ mod fields_based { use super::*; #[repr(simd)] - struct CustomSimd(T, T); + struct CustomSimd([T; 2]); fn check_fields( simd: CustomSimd, expected: [T; LANES], ) { - assert_eq!(simd.0, expected[0]); - assert_eq!(simd.1, expected[1]) + assert_eq!(simd.0[0], expected[0]); + assert_eq!(simd.0[1], expected[1]) } #[kani::proof] fn check_field_access() { let data: [u8; 16] = kani::any(); - let vec = CustomSimd(data[0], data[1]); + let vec = CustomSimd([data[0], data[1]]); check_fields(vec, data); } } diff --git a/tests/kani/SIMD/multi_field_simd.rs b/tests/kani/SIMD/multi_field_simd.rs index d54cf1a07bdb..c8cdd848c69e 100644 --- a/tests/kani/SIMD/multi_field_simd.rs +++ b/tests/kani/SIMD/multi_field_simd.rs @@ -10,19 +10,19 @@ #[repr(simd)] #[derive(PartialEq, Eq, PartialOrd, kani::Arbitrary)] -pub struct i64x2(i64, i64); +pub struct i64x2([i64; 2]); #[kani::proof] fn check_diff() { - let x = i64x2(1, 2); - let y = i64x2(3, 4); + let x = i64x2([1, 2]); + let y = i64x2([3, 4]); assert!(x != y); } #[kani::proof] fn check_ge() { let x: i64x2 = kani::any(); - kani::assume(x.0 > 0); - kani::assume(x.1 > 0); - assert!(x > i64x2(0, 0)); + kani::assume(x.0[0] > 0); + kani::assume(x.0[1] > 0); + assert!(x > i64x2([0, 0])); }