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
42 changes: 17 additions & 25 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(|_| {
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-2024-09-14"
channel = "nightly-2024-09-15"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,14 @@ use std::intrinsics::simd::simd_shuffle;
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2([i64; 2]);

#[repr(simd)]
struct SimdShuffleIdx<const LEN: usize>([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) };
}
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,14 @@ pub struct i64x2([i64; 2]);
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x4([i64; 4]);

#[repr(simd)]
struct SimdShuffleIdx<const LEN: usize>([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:
// ```
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,14 @@ pub struct i64x2([i64; 2]);
#[derive(Clone, Copy, PartialEq)]
pub struct f64x2([f64; 2]);

#[repr(simd)]
struct SimdShuffleIdx<const LEN: usize>([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:
// ```
Expand Down
11 changes: 7 additions & 4 deletions tests/kani/Intrinsics/SIMD/Shuffle/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,28 +16,31 @@ pub struct i64x2([i64; 2]);
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x4([i64; 4]);

#[repr(simd)]
struct SimdShuffleIdx<const LEN: usize>([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);
}
{
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);
}
{
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]));
}
Expand All @@ -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) };
}
}