Add integer overflow checking for simd_div and simd_rem

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

@@ -509,9 +509,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
             ),
             "simd_and" => codegen_intrinsic_binop!(bitand),
-            // TODO: `simd_div` and `simd_rem` don't check for overflow cases.
-            // <https://github.com/model-checking/kani/issues/1970>
-            "simd_div" => codegen_intrinsic_binop!(div),
+            "simd_div" | "simd_rem" => {
+                self.codegen_simd_div_with_overflow(fargs, intrinsic, p, loc)
+            }
             "simd_eq" => self.codegen_simd_cmp(Expr::vector_eq, fargs, p, span, farg_types, ret_ty),
             "simd_extract" => {
                 self.codegen_intrinsic_simd_extract(fargs, p, farg_types, ret_ty, span)
@@ -535,9 +535,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty)
             }
             "simd_or" => codegen_intrinsic_binop!(bitor),
-            // TODO: `simd_div` and `simd_rem` don't check for overflow cases.
-            // <https://github.com/model-checking/kani/issues/1970>
-            "simd_rem" => codegen_intrinsic_binop!(rem),
             // TODO: `simd_shl` and `simd_shr` don't check overflow cases.
             // <https://github.com/model-checking/kani/issues/1963>
             "simd_shl" => codegen_intrinsic_binop!(shl),
@@ -1522,6 +1519,37 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_expr_to_place(p, e)
     }
 
+    /// Codegen for `simd_div` and `simd_rem` intrinsics including overflow checks.
+    /// The divide-by-zero check appears to already be handled by CBMC.
+    fn codegen_simd_div_with_overflow(
+        &mut self,
+        fargs: Vec<Expr>,
+        intrinsic: &str,
+        p: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let op_fun = match intrinsic {
+            "simd_div" => Expr::div,
+            "simd_rem" => Expr::rem,
+            _ => unreachable!("expected simd_div or simd_rem"),
+        };
+        let base_type = fargs[0].typ().base_type().unwrap().clone();
+        if base_type.is_signed(self.symbol_table.machine_model()) {
+            let min_int_expr = base_type.min_int_expr(self.symbol_table.machine_model());
+            let negative_one = Expr::int_constant(-1, base_type);
+            self.codegen_simd_op_with_overflow(
+                op_fun,
+                |a, b| a.eq(min_int_expr.clone()).and(b.eq(negative_one.clone())),
+                fargs,
+                intrinsic,
+                p,
+                loc,
+            )
+        } else {
+            self.binop(p, fargs, op_fun)
+        }
+    }
+
     /// 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.
@@ -1557,7 +1585,7 @@ impl<'tcx> GotocCtx<'tcx> {
         );
         let res = op_fun(a, b);
         let expr_place = self.codegen_expr_to_place(p, res);
-        Stmt::block(vec![expr_place, check_stmt], loc)
+        Stmt::block(vec![check_stmt, expr_place], loc)
     }
 
     /// `simd_shuffle` constructs a new vector from the elements of two input

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

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that the `simd_div` and `simd_rem` intrinsics check for overflows.
+// kani-verify-fail
+
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i32x2(i32, i32);
+
+extern "platform-intrinsic" {
+    fn simd_div<T>(x: T, y: T) -> T;
+    fn simd_rem<T>(x: T, y: T) -> T;
+}
+
+#[kani::proof]
+fn test_simd_div_overflow() {
+    let dividend = kani::any();
+    kani::assume(dividend == i32::MIN);
+    let dividends = i32x2(dividend, dividend);
+    let divisor = kani::any();
+    kani::assume(divisor == -1);
+    let divisors = i32x2(divisor, divisor);
+    let _quotient = unsafe { simd_div(dividends, divisors) };
+}
+
+#[kani::proof]
+fn test_simd_rem_overflow() {
+    let dividend = kani::any();
+    kani::assume(dividend == i32::MIN);
+    let dividends = i32x2(dividend, dividend);
+    let divisor = kani::any();
+    kani::assume(divisor == -1);
+    let divisors = i32x2(divisor, divisor);
+    let _remainder = unsafe { simd_rem(dividends, divisors) };
+}