From fa92da29f014ffe1e26fe759c2c67d0257bc5b25 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 7 Dec 2023 22:22:50 +0000
Subject: [PATCH] Add more tests (`simd_shuffle`/`simd_swizzle`)

---
 library/kani/src/models/mod.rs             |  4 +--
 tests/kani/Intrinsics/SIMD/Shuffle/main.rs | 10 +++++++
 tests/kani/SIMD/portable_simd.rs           |  1 -
 tests/kani/SIMD/swizzle.rs                 | 31 ++++++++++++++++++++++
 4 files changed, 43 insertions(+), 3 deletions(-)
 create mode 100644 tests/kani/SIMD/swizzle.rs

diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs
index 26a1c4563c54..194f220595c0 100644
--- a/library/kani/src/models/mod.rs
+++ b/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);
     }
-
 }
diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
index b3b0d41f0dff..6d822a18bdc1 100644
--- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
+++ b/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) };
+    }
+}
diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs
index 0a0b6d435d46..64cfb4b1fcf3 100644
--- a/tests/kani/SIMD/portable_simd.rs
+++ b/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]);
-
 }
diff --git a/tests/kani/SIMD/swizzle.rs b/tests/kani/SIMD/swizzle.rs
new file mode 100644
index 000000000000..26781743dbfa
--- /dev/null
+++ b/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]);
+}