Add more tests (simd_shuffle/simd_swizzle)

library/kani/src/models/mod.rs

@@ -223,8 +223,8 @@ mod test {
         let bitmask = mask.to_bitmask();
         assert_eq!(bitmask, 0b1010);
 
-        let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) };
+        let kani_mask =
+            unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) };
         assert_eq!(kani_mask, bitmask);
     }
-
 }

tests/kani/Intrinsics/SIMD/Shuffle/main.rs

@@ -45,3 +45,13 @@ fn main() {
         assert!(c == i64x4(2, 4, 6, 8));
     }
 }
+
+#[kani::proof]
+fn check_shuffle() {
+    {
+        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) };
+    }
+}

tests/kani/SIMD/portable_simd.rs

@@ -29,5 +29,4 @@ fn check_resize() {
     let x = u32x4::from_array([0, 1, 2, 3]);
     assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]);
     assert_eq!(x.resize::<2>(9).to_array(), [0, 1]);
-
 }

tests/kani/SIMD/swizzle.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Ensure we can safely swizzle between SIMD types of different sizes.
+#![feature(portable_simd)]
+
+use std::simd::{simd_swizzle, u32x4, u32x8};
+
+#[kani::proof]
+fn harness_from_u32x4_to_u32x4() {
+    let a = u32x4::from_array([0, 1, 2, 3]);
+    let b = u32x4::from_array([4, 5, 6, 7]);
+    let r: u32x4 = simd_swizzle!(a, b, [0, 1, 6, 7]);
+    assert_eq!(r.to_array(), [0, 1, 6, 7]);
+}
+
+#[kani::proof]
+fn harness_from_u32x4_to_u32x8() {
+    let a = u32x4::from_array([0, 1, 2, 3]);
+    let b = u32x4::from_array([4, 5, 6, 7]);
+    let r: u32x8 = simd_swizzle!(a, b, [0, 1, 2, 3, 4, 5, 6, 7]);
+    assert_eq!(r.to_array(), [0, 1, 2, 3, 4, 5, 6, 7]);
+}
+
+#[kani::proof]
+fn harness_from_u32x8_to_u32x4() {
+    let a = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]);
+    let b = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]);
+    let r: u32x4 = simd_swizzle!(a, b, [0, 1, 2, 3]);
+    assert_eq!(r.to_array(), [0, 1, 2, 3]);
+}