Add integer overflow checking for simd_div and simd_rem (model-checki…

…ng#2645)

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

docs/src/rust-feature-support/intrinsics.md

@@ -258,7 +258,7 @@ Name | Support | Notes |
 --- | --- | --- |
 `simd_add` | Yes | |
 `simd_and`  | Yes | |
-`simd_div`  | Yes | Doesn't check for overflow cases [#1970](https://github.com/model-checking/kani/issues/1970) |
+`simd_div`  | Yes | |
 `simd_eq`  | Yes | |
 `simd_extract`  | Yes | |
 `simd_ge`  | Yes | |
@@ -269,9 +269,9 @@ Name | Support | Notes |
 `simd_mul`  | Yes | |
 `simd_ne`  | Yes | |
 `simd_or`  | Yes | |
-`simd_rem`  | Yes | Doesn't check for overflow cases [#1970](https://github.com/model-checking/kani/issues/1970) |
-`simd_shl`  | Yes | Doesn't check for overflow cases [#1963](https://github.com/model-checking/kani/issues/1963) |
-`simd_shr`  | Yes | Doesn't check for overflow cases [#1963](https://github.com/model-checking/kani/issues/1963) |
+`simd_rem`  | Yes | Doesn't check for floating point overflow [#2669](https://github.com/model-checking/kani/issues/2669) |
+`simd_shl`  | Yes | |
+`simd_shr`  | Yes | |
 `simd_shuffle*`  | Yes | |
 `simd_sub`  | Yes | |
 `simd_xor`  | Yes | |

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

@@ -511,9 +511,11 @@ 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),
+            // TODO: `simd_rem` doesn't check for overflow cases for floating point operands.
+            // <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)
@@ -537,9 +539,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)
             }
@@ -1552,6 +1551,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.
@@ -1587,7 +1619,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,8 @@
+FAILURE\
+attempt to compute simd_div which would overflow
+UNREACHABLE\
+assertion failed: quotients.0 == quotients.1
+FAILURE\
+attempt to compute simd_rem which would overflow
+UNREACHABLE\
+assertion failed: remainders.0 == remainders.1

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

@@ -0,0 +1,44 @@
+// 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;
+}
+
+unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
+    simd_div(dividends, divisors)
+}
+
+unsafe fn do_simd_rem(dividends: i32x2, divisors: i32x2) -> i32x2 {
+    simd_rem(dividends, divisors)
+}
+
+#[kani::proof]
+fn test_simd_div_overflow() {
+    let dividend = i32::MIN;
+    let dividends = i32x2(dividend, dividend);
+    let divisor = -1;
+    let divisors = i32x2(divisor, divisor);
+    let quotients = unsafe { do_simd_div(dividends, divisors) };
+    assert_eq!(quotients.0, quotients.1);
+}
+
+#[kani::proof]
+fn test_simd_rem_overflow() {
+    let dividend = i32::MIN;
+    let dividends = i32x2(dividend, dividend);
+    let divisor = -1;
+    let divisors = i32x2(divisor, divisor);
+    let remainders = unsafe { do_simd_rem(dividends, divisors) };
+    assert_eq!(remainders.0, remainders.1);
+}

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

@@ -0,0 +1,39 @@
+// 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.
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, kani::Arbitrary)]
+pub struct f32x2(f32, f32);
+
+impl f32x2 {
+    fn new_with(f: impl Fn() -> f32) -> Self {
+        f32x2(f(), f())
+    }
+
+    fn non_simd_div(self, divisors: Self) -> Self {
+        f32x2(self.0 / divisors.0, self.1 / divisors.1)
+    }
+}
+
+extern "platform-intrinsic" {
+    fn simd_div<T>(x: T, y: T) -> T;
+}
+
+#[kani::proof]
+fn test_simd_div() {
+    let dividends = f32x2::new_with(|| {
+        let multiplier = kani::any_where(|&n: &i8| n >= -5 && n <= 5);
+        0.5 * f32::from(multiplier)
+    });
+    let divisors = f32x2::new_with(|| {
+        let multiplier = kani::any_where(|&n: &i8| n != 0 && n >= -5 && n <= 5);
+        0.5 * f32::from(multiplier)
+    });
+    let normal_results = dividends.non_simd_div(divisors);
+    let simd_results = unsafe { simd_div(dividends, divisors) };
+    assert_eq!(normal_results, simd_results);
+}

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

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that the `simd_rem` intrinsic returns the expected results for floating point numbers.
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, kani::Arbitrary)]
+pub struct f32x2(f32, f32);
+
+impl f32x2 {
+    fn new_with(f: impl Fn() -> f32) -> Self {
+        f32x2(f(), f())
+    }
+
+    fn non_simd_rem(self, divisors: Self) -> Self {
+        f32x2(self.0 % divisors.0, self.1 % divisors.1)
+    }
+}
+
+extern "platform-intrinsic" {
+    fn simd_rem<T>(x: T, y: T) -> T;
+}
+
+#[kani::proof]
+fn test_simd_rem() {
+    let dividends = f32x2::new_with(|| {
+        let multiplier = kani::any_where(|&n: &i8| n >= -5 && n <= 5);
+        0.5 * f32::from(multiplier)
+    });
+    let divisors = f32x2::new_with(|| {
+        let multiplier = kani::any_where(|&n: &i8| n != 0 && n >= -5 && n <= 5);
+        0.5 * f32::from(multiplier)
+    });
+    let normal_results = dividends.non_simd_rem(divisors);
+    let simd_results = unsafe { simd_rem(dividends, divisors) };
+    assert_eq!(normal_results, simd_results);
+}