Add integer overflow checking for simd_div and simd_rem

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

@@ -509,9 +509,12 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
             ),
             "simd_and" => codegen_intrinsic_binop!(bitand),
-            // TODO: `simd_div` and `simd_rem` don't check for overflow cases.
+            // TODO: `simd_rem` doesn't check for overflow cases for floating point operands.
             // <https://github.com/model-checking/kani/issues/1970>
-            "simd_div" => codegen_intrinsic_binop!(div),
+            // <https://github.com/model-checking/kani/pull/2645>
+            "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 +538,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),
             "simd_shl" | "simd_shr" => {
                 self.codegen_simd_shift_with_distance_check(fargs, intrinsic, p, loc)
             }
@@ -1514,6 +1514,39 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_expr_to_place(p, e)
     }
 
+    /// Codegen for `simd_div` and `simd_rem` intrinsics.
+    /// This checks for overflow in signed integer division (i.e. when dividing the minimum integer
+    /// for the type by -1). Overflow checks on floating point division are handled by CBMC, as is
+    /// division by zero for both integers and floats.
+    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_integer() && 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.
@@ -1549,7 +1582,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)
     }
 
     /// Intrinsics which encode a SIMD bitshift.

tests/expected/intrinsics/simd-div-rem-overflow/expected

@@ -0,0 +1,4 @@
+FAILURE\
+attempt to compute simd_div which would overflow
+FAILURE\
+attempt to compute simd_rem which would overflow

tests/expected/intrinsics/simd-div-rem-overflow/main.rs

@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that the `simd_div` and `simd_rem` intrinsics check for integer overflows.
+
+#![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) };
+}

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

@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that the `simd_div` intrinsic returns the expected results for floating point numbers.
+//! Checks that the `simd_rem` intrinsic exists.
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq)]
+pub struct f32x2(f32, f32);
+
+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() {
+    let dividend: f32 = kani::any::<i8>().into();
+    let divisor: f32 = kani::any::<i8>().into();
+    // Narrow down the divisor interval so the operation finishes in a short time
+    kani::assume(divisor != 0.0 && divisor.abs() < 5.0);
+    let normal_result = dividend / divisor;
+    let dividends = f32x2(dividend, dividend);
+    let divisors = f32x2(divisor, divisor);
+    let simd_result = unsafe { simd_div(dividends, divisors) };
+    assert_eq!(normal_result, simd_result.0);
+}
+
+#[kani::proof]
+fn test_simd_rem() {
+    let dividend: f32 = kani::any::<i8>().into();
+    let divisor: f32 = kani::any::<i8>().into();
+    // Narrow down the divisor interval so the operation finishes in a short time
+    kani::assume(divisor != 0.0 && divisor.abs() < 5.0);
+    let dividends = f32x2(dividend, dividend);
+    let divisors = f32x2(divisor, divisor);
+    let _simd_result = unsafe { simd_rem(dividends, divisors) };
+}