Audit for unchecked intrinsics

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

@@ -189,6 +189,24 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
+        // Intrinsics which encode a division operation with overflow check
+        macro_rules! codegen_op_with_div_overflow_check {
+            ($f:ident) => {{
+                let a = fargs.remove(0);
+                let b = fargs.remove(0);
+                let div_does_not_overflow = self.div_does_not_overflow(a.clone(), b.clone());
+                let div_overflow_check = self.codegen_assert(
+                    div_does_not_overflow,
+                    PropertyClass::ArithmeticOverflow,
+                    format!("attempt to compute {} which would overflow", intrinsic).as_str(),
+                    loc,
+                );
+                let res = a.$f(b);
+                let expr_place = self.codegen_expr_to_place(p, res);
+                Stmt::block(vec![div_overflow_check, expr_place], loc)
+            }};
+        }
+
         // 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.
@@ -564,9 +582,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_expr_to_place(p, fargs.remove(0).dereference())
             }
             "unchecked_add" => codegen_op_with_overflow_check!(add_overflow),
-            "unchecked_div" => codegen_intrinsic_binop!(div),
+            "unchecked_div" => codegen_op_with_div_overflow_check!(div),
             "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow),
-            "unchecked_rem" => codegen_intrinsic_binop!(rem),
+            "unchecked_rem" => codegen_op_with_div_overflow_check!(rem),
             "unchecked_shl" => codegen_intrinsic_binop!(shl),
             "unchecked_shr" => {
                 if fargs[0].typ().is_signed(self.symbol_table.machine_model()) {
@@ -643,24 +661,30 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::block(vec![finite_check1, finite_check2, stmt], loc)
     }
 
-    fn codegen_exact_div(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>, loc: Location) -> Stmt {
-        // Check for undefined behavior conditions defined in
-        // https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+    fn div_does_not_overflow(&self, a: Expr, b: Expr) -> Expr {
         let mm = self.symbol_table.machine_model();
-        let a = fargs.remove(0);
-        let b = fargs.remove(0);
         let atyp = a.typ();
         let btyp = b.typ();
-        let division_is_exact = a.clone().rem(b.clone()).eq(atyp.zero());
-        let divisor_is_nonzero = b.clone().neq(btyp.zero());
         let dividend_is_int_min = if atyp.is_signed(&mm) {
             a.clone().eq(atyp.min_int_expr(mm))
         } else {
             Expr::bool_false()
         };
         let divisor_is_minus_one =
             if btyp.is_signed(mm) { b.clone().eq(btyp.one().neg()) } else { Expr::bool_false() };
-        let division_does_not_overflow = dividend_is_int_min.and(divisor_is_minus_one).not();
+        dividend_is_int_min.and(divisor_is_minus_one).not()
+    }
+
+    fn codegen_exact_div(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>, loc: Location) -> Stmt {
+        // Check for undefined behavior conditions defined in
+        // https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+        let a = fargs.remove(0);
+        let b = fargs.remove(0);
+        let atyp = a.typ();
+        let btyp = b.typ();
+        let division_is_exact = a.clone().rem(b.clone()).eq(atyp.zero());
+        let divisor_is_nonzero = b.clone().neq(btyp.zero());
+        let division_does_not_overflow = self.div_does_not_overflow(a.clone(), b.clone());
         Stmt::block(
             vec![
                 self.codegen_assert(

tests/kani/ArithOperators/div_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that division triggers overflow checks.
+// Covers the case where `a == T::MIN && b == -1`.
+
+#[kani::proof]
+fn main() {
+    let a: i8 = i8::MIN;
+    let b: i8 = kani::any();
+    kani::assume(b == -1);
+    let _ = a / b;
+}

tests/kani/ArithOperators/div_zero_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that division triggers overflow checks.
+// Covers the case where `b == 0`.
+
+#[kani::proof]
+fn main() {
+    let a: i8 = kani::any();
+    let b: i8 = kani::any();
+    kani::assume(b == 0);
+    let _ = a / b;
+}

tests/kani/ArithOperators/rem_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that remainder triggers overflow checks.
+// Covers the case where `a == T::MIN && b == -1`.
+
+#[kani::proof]
+fn main() {
+    let a: i8 = i8::MIN;
+    let b: i8 = kani::any();
+    kani::assume(b == -1);
+    let _ = a % b;
+}

tests/kani/ArithOperators/rem_zero_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that remainder triggers overflow checks.
+// Covers the case where `b == 0`.
+
+#[kani::proof]
+fn main() {
+    let a: i8 = kani::any();
+    let b: i8 = kani::any();
+    kani::assume(b == 0);
+    let _ = a % b;
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_add` triggers overflow checks.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = kani::any();
+    let b: i32 = kani::any();
+    unsafe { std::intrinsics::unchecked_add(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_div` triggers overflow checks.
+// Covers the case where `a == T::MIN && b == -1`.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = i32::MIN;
+    let b: i32 = -1;
+    unsafe { std::intrinsics::unchecked_div(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_div` triggers overflow checks.
+// Covers the case where `b == 0`.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = kani::any();
+    let b: i32 = 0;
+    unsafe { std::intrinsics::unchecked_div(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_mul` triggers overflow checks.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = kani::any();
+    let b: i32 = kani::any();
+    unsafe { std::intrinsics::unchecked_mul(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/no_overflows.rs

@@ -0,0 +1,57 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that none of these operations trigger spurious overflow checks.
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    unchecked_add, unchecked_div, unchecked_mul, unchecked_rem, unchecked_shl, unchecked_shr,
+    unchecked_sub,
+};
+
+// `checked_shr` and `checked_shl` require `u32` for their argument. We use
+// `u32` in those cases and `u8` for the rest because they perform better.
+macro_rules! verify_no_overflow {
+    ($ty:ty, $cf: ident, $uf: ident) => {{
+        let a: $ty = kani::any();
+        let b: $ty = kani::any();
+        let checked = a.$cf(b);
+        kani::assume(checked.is_some());
+        let unchecked = unsafe { $uf(a, b) };
+        assert!(checked.unwrap() == unchecked);
+    }};
+}
+
+#[kani::proof]
+fn test_unchecked_add() {
+    verify_no_overflow!(u8, checked_add, unchecked_add);
+}
+
+#[kani::proof]
+fn test_unchecked_sub() {
+    verify_no_overflow!(u8, checked_sub, unchecked_sub);
+}
+
+#[kani::proof]
+fn test_unchecked_mul() {
+    verify_no_overflow!(u8, checked_mul, unchecked_mul);
+}
+
+#[kani::proof]
+fn test_unchecked_div() {
+    verify_no_overflow!(u8, checked_div, unchecked_div);
+}
+
+#[kani::proof]
+fn test_unchecked_rem() {
+    verify_no_overflow!(u8, checked_rem, unchecked_rem);
+}
+
+#[kani::proof]
+fn test_unchecked_shl() {
+    verify_no_overflow!(u32, checked_shl, unchecked_shl);
+}
+
+#[kani::proof]
+fn test_unchecked_shr() {
+    verify_no_overflow!(u32, checked_shr, unchecked_shr);
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_rem` triggers overflow checks.
+// Covers the case where `a == T::MIN && b == -1`.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = i32::MIN;
+    let b: i32 = -1;
+    unsafe { std::intrinsics::unchecked_rem(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs

@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_rem` triggers overflow checks.
+// Covers the case where `b == 0`.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = kani::any();
+    let b: i32 = 0;
+    unsafe { std::intrinsics::unchecked_rem(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_shl` triggers overflow checks.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: u32 = kani::any();
+    let b: u32 = kani::any();
+    unsafe { std::intrinsics::unchecked_shl(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_shr` triggers overflow checks.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: u32 = kani::any();
+    let b: u32 = kani::any();
+    unsafe { std::intrinsics::unchecked_shr(a, b) };
+}

tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `unchecked_sub` triggers overflow checks.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: i32 = kani::any();
+    let b: i32 = kani::any();
+    unsafe { std::intrinsics::unchecked_sub(a, b) };
+}