diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 1b4c0174d5ed..4b66d60e735b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1243,35 +1243,27 @@ impl<'tcx> GotocCtx<'tcx> { /// 1. `simd_shuffleN`, where `N` is a number which is part of the name /// (e.g., `simd_shuffle4`). /// 2. `simd_shuffle`, where `N` isn't specified and must be computed from - /// the length of the indexes array (the third argument). + /// the length of the indexes SIMD vector (the third argument). fn simd_shuffle_length(&mut self, stripped: &str, farg_types: &[Ty], span: Span) -> u64 { let n = if stripped.is_empty() { - // Make sure that this is an array, since only the + // Make sure that this is an SIMD vector, since only the // length-suffixed version of `simd_shuffle` (e.g., // `simd_shuffle4`) is type-checked - match farg_types[2].kind() { - TyKind::RigidTy(RigidTy::Array(ty, len)) - if matches!(ty.kind(), TyKind::RigidTy(RigidTy::Uint(UintTy::U32))) => - { - len.eval_target_usize().unwrap_or_else(|err| { - utils::span_err( - self.tcx, - span, - format!("could not evaluate shuffle index array length: {err}"), - ); - // Return a dummy value - u64::MIN - }) - } - _ => { - let err_msg = format!( - "simd_shuffle index must be an array of `u32`, got `{}`", - self.pretty_ty(farg_types[2]) - ); - utils::span_err(self.tcx, span, err_msg); - // Return a dummy value - u64::MIN - } + if farg_types[2].kind().is_simd() + && matches!( + self.simd_size_and_type(farg_types[2]).1.kind(), + TyKind::RigidTy(RigidTy::Uint(UintTy::U32)) + ) + { + self.simd_size_and_type(farg_types[2]).0 + } else { + let err_msg = format!( + "simd_shuffle index must be a SIMD vector of `u32`, got `{}`", + self.pretty_ty(farg_types[2]) + ); + utils::span_err(self.tcx, span, err_msg); + // Return a dummy value + u64::MIN } } else { stripped.parse().unwrap_or_else(|_| { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 668713f66b4a..d87b063bfd23 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-14" +channel = "nightly-2024-09-15" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs index b89f40369853..a9da5c773743 100644 --- a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs @@ -11,11 +11,14 @@ use std::intrinsics::simd::simd_shuffle; #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x2([i64; 2]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { 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]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([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 3fe534f3bc08..3936f39ed318 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 @@ -16,11 +16,14 @@ pub struct i64x2([i64; 2]); #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x4([i64; 4]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 4] = [1, 2, 1, 2]; + const I: SimdShuffleIdx<4> = SimdShuffleIdx([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 8c7cd5245cbe..7f8c511a96e5 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 @@ -16,11 +16,14 @@ pub struct i64x2([i64; 2]); #[derive(Clone, Copy, PartialEq)] pub struct f64x2([f64; 2]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 2] = [1, 2]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([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/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index a105a3b1d81e..b20c16be5877 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -16,12 +16,15 @@ pub struct i64x2([i64; 2]); #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x4([i64; 4]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 2] = [1, 2]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]); let x: i64x2 = unsafe { simd_shuffle(y, z, I) }; assert!(x.0[0] == 1); assert!(x.0[1] == 1); @@ -29,7 +32,7 @@ fn main() { { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 2] = [1, 2]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]); let x: i64x2 = unsafe { simd_shuffle(y, z, I) }; assert!(x.0[0] == 1); assert!(x.0[1] == 1); @@ -37,7 +40,7 @@ fn main() { { let a = i64x4([1, 2, 3, 4]); let b = i64x4([5, 6, 7, 8]); - const I: [u32; 4] = [1, 3, 5, 7]; + const I: SimdShuffleIdx<4> = SimdShuffleIdx([1, 3, 5, 7]); let c: i64x4 = unsafe { simd_shuffle(a, b, I) }; assert!(c == i64x4([2, 4, 6, 8])); } @@ -48,7 +51,7 @@ fn check_shuffle() { { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 4] = [1, 2, 0, 3]; + const I: SimdShuffleIdx<4> = SimdShuffleIdx([1, 2, 0, 3]); let _x: i64x4 = unsafe { simd_shuffle(y, z, I) }; } }