Restore support for bitwise SIMD intrinsics (rust-lang#1893)

Author: adpaco-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -609,7 +609,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_add" => {
                 unstable_codegen!(codegen_simd_with_overflow_check!(plus, add_overflow_p))
             }
-            "simd_and" => unstable_codegen!(codegen_intrinsic_binop!(bitand)),
+            "simd_and" => codegen_intrinsic_binop!(bitand),
             "simd_div" => unstable_codegen!(codegen_intrinsic_binop!(div)),
             "simd_eq" => self.codegen_simd_cmp(Expr::vector_eq, fargs, p, span, farg_types, ret_ty),
             "simd_extract" => {
@@ -628,7 +628,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_ne" => {
                 self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty)
             }
-            "simd_or" => unstable_codegen!(codegen_intrinsic_binop!(bitor)),
+            "simd_or" => codegen_intrinsic_binop!(bitor),
             "simd_rem" => unstable_codegen!(codegen_intrinsic_binop!(rem)),
             "simd_shl" => unstable_codegen!(codegen_intrinsic_binop!(shl)),
             "simd_shr" => {
@@ -643,7 +643,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             // "simd_shuffle#" => handled in an `if` preceding this match
             "simd_sub" => unstable_codegen!(codegen_simd_with_overflow_check!(sub, sub_overflow_p)),
-            "simd_xor" => unstable_codegen!(codegen_intrinsic_binop!(bitxor)),
+            "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => codegen_intrinsic_const!(),
             "size_of_val" => codegen_size_align!(size),
             "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),

tests/kani/Intrinsics/SIMD/Operators/bitwise.rs

@@ -0,0 +1,104 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that the following SIMD intrinsics are supported:
+//!  * `simd_and`
+//!  * `simd_or`
+//!  * `simd_xor`
+//! This is done by initializing vectors with the contents of 2-member tuples
+//! with symbolic values. The result of using each of the intrinsics is compared
+//! against the result of using the associated bitwise operator on the tuples.
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i8x2(i8, i8);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i16x2(i16, i16);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i32x2(i32, i32);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i64x2(i64, i64);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct u8x2(u8, u8);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct u16x2(u16, u16);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct u32x2(u32, u32);
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct u64x2(u64, u64);
+
+extern "platform-intrinsic" {
+    fn simd_and<T>(x: T, y: T) -> T;
+    fn simd_or<T>(x: T, y: T) -> T;
+    fn simd_xor<T>(x: T, y: T) -> T;
+}
+macro_rules! compare_simd_op_with_normal_op {
+    ($simd_op: ident, $normal_op: tt, $simd_type: ident) => {
+        let tup_x = (kani::any(), kani::any());
+        let tup_y = (kani::any(), kani::any());
+        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);
+    };
+}
+
+#[kani::proof]
+fn test_simd_and() {
+    compare_simd_op_with_normal_op!(simd_and, &, i8x2);
+    compare_simd_op_with_normal_op!(simd_and, &, i16x2);
+    compare_simd_op_with_normal_op!(simd_and, &, i32x2);
+    compare_simd_op_with_normal_op!(simd_and, &, i64x2);
+    compare_simd_op_with_normal_op!(simd_and, &, u8x2);
+    compare_simd_op_with_normal_op!(simd_and, &, u16x2);
+    compare_simd_op_with_normal_op!(simd_and, &, u32x2);
+    compare_simd_op_with_normal_op!(simd_and, &, u64x2);
+}
+
+#[kani::proof]
+fn test_simd_or() {
+    compare_simd_op_with_normal_op!(simd_or, |, i8x2);
+    compare_simd_op_with_normal_op!(simd_or, |, i16x2);
+    compare_simd_op_with_normal_op!(simd_or, |, i32x2);
+    compare_simd_op_with_normal_op!(simd_or, |, i64x2);
+    compare_simd_op_with_normal_op!(simd_or, |, u8x2);
+    compare_simd_op_with_normal_op!(simd_or, |, u16x2);
+    compare_simd_op_with_normal_op!(simd_or, |, u32x2);
+    compare_simd_op_with_normal_op!(simd_or, |, u64x2);
+}
+
+#[kani::proof]
+fn test_simd_xor() {
+    compare_simd_op_with_normal_op!(simd_xor, ^, i8x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, i16x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, i32x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, i64x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, u8x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, u16x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, u32x2);
+    compare_simd_op_with_normal_op!(simd_xor, ^, u64x2);
+}

tests/kani/Intrinsics/SIMD/Operators/main_fixme.rs

@@ -17,11 +17,6 @@ extern "platform-intrinsic" {
     fn simd_mul<T>(x: T, y: T) -> T;
     fn simd_div<T>(x: T, y: T) -> T;
     fn simd_rem<T>(x: T, y: T) -> T;
-    fn simd_shl<T>(x: T, y: T) -> T;
-    fn simd_shr<T>(x: T, y: T) -> T;
-    fn simd_and<T>(x: T, y: T) -> T;
-    fn simd_or<T>(x: T, y: T) -> T;
-    fn simd_xor<T>(x: T, y: T) -> T;
 }
 
 macro_rules! assert_op {
@@ -46,10 +41,5 @@ fn main() {
         assert_op!(res_mul, simd_mul, y, z, 0, 2);
         assert_op!(res_div, simd_div, v, z, 1, 1);
         assert_op!(res_rem, simd_rem, v, z, 0, 1);
-        assert_op!(res_shl, simd_shl, z, z, 2, 8);
-        assert_op!(res_shr, simd_shr, z, y, 1, 1);
-        assert_op!(res_and, simd_and, y, v, 0, 1);
-        assert_op!(res_or, simd_or, x, y, 0, 1);
-        assert_op!(res_xor, simd_xor, x, y, 0, 1);
     }
 }