Restore support for some SIMD arithmetic intrinsics (rust-lang#1931)

Author: adpaco-aws

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

@@ -274,40 +274,6 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
-        // Intrinsics which encode a SIMD arithmetic operation with overflow check.
-        // We expand the overflow check because CBMC overflow operations don't accept array as
-        // argument.
-        macro_rules! _codegen_simd_with_overflow_check {
-            ($op:ident, $overflow:ident) => {{
-                let a = fargs.remove(0);
-                let b = fargs.remove(0);
-                let mut check = Expr::bool_false();
-                if let Type::Vector { size, .. } = a.typ() {
-                    let a_size = size;
-                    if let Type::Vector { size, .. } = b.typ() {
-                        let b_size = size;
-                        assert_eq!(a_size, b_size, "Expected same length vectors",);
-                        for i in 0..*a_size {
-                            // create expression
-                            let index = Expr::int_constant(i, Type::ssize_t());
-                            let v_a = a.clone().index_array(index.clone());
-                            let v_b = b.clone().index_array(index);
-                            check = check.or(v_a.$overflow(v_b));
-                        }
-                    }
-                }
-                let check_stmt = self.codegen_assert(
-                    check.not(),
-                    PropertyClass::ArithmeticOverflow,
-                    format!("attempt to compute {} which would overflow", intrinsic).as_str(),
-                    loc,
-                );
-                let res = a.$op(b);
-                let expr_place = self.codegen_expr_to_place(p, res);
-                Stmt::block(vec![expr_place, check_stmt], loc)
-            }};
-        }
-
         // Intrinsics which encode a simple wrapping arithmetic operation
         macro_rules! codegen_wrapping_op {
             ($f:ident) => {{ codegen_intrinsic_binop!($f) }};
@@ -606,9 +572,14 @@ impl<'tcx> GotocCtx<'tcx> {
             "saturating_sub" => codegen_intrinsic_binop_with_mm!(saturating_sub),
             "sinf32" => codegen_simple_intrinsic!(Sinf),
             "sinf64" => codegen_simple_intrinsic!(Sin),
-            "simd_add" => {
-                unstable_codegen!(codegen_simd_with_overflow_check!(plus, add_overflow_p))
-            }
+            "simd_add" => self.codegen_simd_op_with_overflow(
+                Expr::plus,
+                Expr::add_overflow_p,
+                fargs,
+                intrinsic,
+                p,
+                loc,
+            ),
             "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),
@@ -624,7 +595,14 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "simd_le" => self.codegen_simd_cmp(Expr::vector_le, fargs, p, span, farg_types, ret_ty),
             "simd_lt" => self.codegen_simd_cmp(Expr::vector_lt, fargs, p, span, farg_types, ret_ty),
-            "simd_mul" => unstable_codegen!(codegen_simd_with_overflow_check!(mul, mul_overflow_p)),
+            "simd_mul" => self.codegen_simd_op_with_overflow(
+                Expr::mul,
+                Expr::mul_overflow_p,
+                fargs,
+                intrinsic,
+                p,
+                loc,
+            ),
             "simd_ne" => {
                 self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty)
             }
@@ -642,7 +620,14 @@ 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_sub" => self.codegen_simd_op_with_overflow(
+                Expr::sub,
+                Expr::sub_overflow_p,
+                fargs,
+                intrinsic,
+                p,
+                loc,
+            ),
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => codegen_intrinsic_const!(),
             "size_of_val" => codegen_size_align!(size),
@@ -1432,6 +1417,44 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_expr_to_place(p, e)
     }
 
+    /// Intrinsics which encode a SIMD arithmetic operation with overflow check.
+    /// We expand the overflow check because CBMC overflow operations don't accept array as
+    /// argument.
+    fn codegen_simd_op_with_overflow<F: FnOnce(Expr, Expr) -> Expr, G: Fn(Expr, Expr) -> Expr>(
+        &mut self,
+        op_fun: F,
+        overflow_fun: G,
+        mut fargs: Vec<Expr>,
+        intrinsic: &str,
+        p: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let a = fargs.remove(0);
+        let b = fargs.remove(0);
+
+        let a_size = a.typ().len().unwrap();
+        let b_size = b.typ().len().unwrap();
+        assert_eq!(a_size, b_size, "expected same length vectors");
+
+        let mut check = Expr::bool_false();
+        for i in 0..a_size {
+            // create expression
+            let index = Expr::int_constant(i, Type::ssize_t());
+            let v_a = a.clone().index_array(index.clone());
+            let v_b = b.clone().index_array(index);
+            check = check.or(overflow_fun(v_a, v_b));
+        }
+        let check_stmt = self.codegen_assert_assume(
+            check.not(),
+            PropertyClass::ArithmeticOverflow,
+            format!("attempt to compute {} which would overflow", intrinsic).as_str(),
+            loc,
+        );
+        let res = op_fun(a, b);
+        let expr_place = self.codegen_expr_to_place(p, res);
+        Stmt::block(vec![expr_place, check_stmt], loc)
+    }
+
     /// simd_shuffle constructs a new vector from the elements of two input vectors,
     /// choosing values according to an input array of indexes.
     ///

tests/expected/intrinsics/simd-arith-overflows/expected

@@ -0,0 +1,6 @@
+FAILURE\
+attempt to compute simd_add which would overflow
+FAILURE\
+attempt to compute simd_sub which would overflow
+FAILURE\
+attempt to compute simd_mul which would overflow

tests/expected/intrinsics/simd-arith-overflows/main.rs

@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test ensures we detect overflows in SIMD arithmetic operations
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct i8x2(i8, i8);
+
+extern "platform-intrinsic" {
+    fn simd_add<T>(x: T, y: T) -> T;
+    fn simd_sub<T>(x: T, y: T) -> T;
+    fn simd_mul<T>(x: T, y: T) -> T;
+}
+
+#[kani::proof]
+fn main() {
+    let a = kani::any();
+    let b = kani::any();
+    let simd_a = i8x2(a, a);
+    let simd_b = i8x2(b, b);
+
+    unsafe {
+        let _ = simd_add(simd_a, simd_b);
+        let _ = simd_sub(simd_a, simd_b);
+        let _ = simd_mul(simd_a, simd_b);
+    }
+}

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

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test doesn't work because support for SIMD intrinsics isn't available
+//! at the moment in Kani. Support to be added in
+//! <https://github.com/model-checking/kani/issues/1148>
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i8x2(i8, i8);
+
+extern "platform-intrinsic" {
+    fn simd_add<T>(x: T, y: T) -> T;
+    fn simd_sub<T>(x: T, y: T) -> T;
+    fn simd_mul<T>(x: T, y: T) -> T;
+}
+
+macro_rules! verify_no_overflow {
+    ($cf: ident, $uf: ident) => {{
+        let a: i8 = kani::any();
+        let b: i8 = kani::any();
+        let checked = a.$cf(b);
+        kani::assume(checked.is_some());
+        let simd_a = i8x2(a, a);
+        let simd_b = i8x2(b, b);
+        let unchecked: i8x2 = unsafe { $uf(simd_a, simd_b) };
+        assert!(checked.unwrap() == unchecked.0);
+        assert!(checked.unwrap() == unchecked.1);
+    }};
+}
+
+#[kani::proof]
+fn test_simd_ops() {
+    verify_no_overflow!(checked_add, simd_add);
+    verify_no_overflow!(checked_sub, simd_sub);
+    verify_no_overflow!(checked_mul, simd_mul);
+}