Refactor overflow checks in intrinsics code (#1131)

* Modify expected tests

* Final changes

* Change expectation and add comment

* Use `count` instead of `number`

* Add comment above `v_wrap` assignment

* Review overflow check in `ptr_offset_from`

* Update test that triggers failure, add a new one for wrap-around

* Remove instance argument

Co-authored-by: Celina G. Val <celinval@amazon.com>

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

@@ -528,7 +528,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "pref_align_of" => codegen_intrinsic_const!(),
             "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
             "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
-            "ptr_offset_from" => self.codegen_ptr_offset_from(instance, fargs, p, loc),
+            "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
             "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
             "rintf32" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
@@ -637,7 +637,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "wrapping_sub" => codegen_wrapping_op!(sub),
             "write_bytes" => {
                 assert!(self.place_ty(p).is_unit());
-                self.codegen_write_bytes(instance, intrinsic, fargs, loc)
+                self.codegen_write_bytes(instance, fargs, loc)
             }
             // Unimplemented
             _ => codegen_unimplemented_intrinsic!(
@@ -887,26 +887,22 @@ impl<'tcx> GotocCtx<'tcx> {
         let src_ptr = fargs.remove(0);
         let offset = fargs.remove(0);
 
-        // Check that computing `bytes` would not overflow
+        // Check that computing `offset` in bytes would not overflow
         let ty = self.monomorphize(instance.substs.type_at(0));
-        let layout = self.layout_of(ty);
-        let size = Expr::int_constant(layout.size.bytes(), Type::ssize_t());
-        let bytes = offset.clone().mul_overflow(size);
-        let bytes_overflow_check = self.codegen_assert(
-            bytes.overflowed.not(),
-            PropertyClass::ArithmeticOverflow,
-            "attempt to compute offset in bytes which would overflow",
-            loc,
-        );
+        let (offset_bytes, bytes_overflow_check) =
+            self.count_in_bytes(offset.clone(), ty, Type::ssize_t(), "offset", loc);
 
         // Check that the computation would not overflow an `isize`
-        let dst_ptr_of = src_ptr.clone().cast_to(Type::ssize_t()).add_overflow(bytes.result);
+        // These checks may allow a wrapping-around behavior in CBMC:
+        // https://github.com/model-checking/kani/issues/1150
+        let dst_ptr_of = src_ptr.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes);
         let overflow_check = self.codegen_assert(
             dst_ptr_of.overflowed.not(),
             PropertyClass::ArithmeticOverflow,
             "attempt to compute offset which would overflow",
             loc,
         );
+
         // Re-compute `dst_ptr` with standard addition to avoid conversion
         let dst_ptr = src_ptr.plus(offset);
         let expr_place = self.codegen_expr_to_place(p, dst_ptr);
@@ -917,7 +913,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html
     fn codegen_ptr_offset_from(
         &mut self,
-        instance: Instance<'tcx>,
         mut fargs: Vec<Expr>,
         p: &Place<'tcx>,
         loc: Location,
@@ -928,17 +923,15 @@ impl<'tcx> GotocCtx<'tcx> {
         // Compute the offset with standard substraction using `isize`
         let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t());
         let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t());
-        let offset = cast_dst_ptr.sub(cast_src_ptr);
+        let offset = cast_dst_ptr.sub_overflow(cast_src_ptr);
 
-        // Check that computing `offset_bytes` would not overflow an `isize`
-        let ty = self.monomorphize(instance.substs.type_at(0));
-        let layout = self.layout_of(ty);
-        let size = Expr::int_constant(layout.size.bytes(), Type::ssize_t());
-        let offset_bytes = offset.clone().mul_overflow(size);
+        // Check that computing `offset` in bytes would not overflow an `isize`
+        // These checks may allow a wrapping-around behavior in CBMC:
+        // https://github.com/model-checking/kani/issues/1150
         let overflow_check = self.codegen_assert(
-            offset_bytes.overflowed.not(),
+            offset.overflowed.not(),
             PropertyClass::ArithmeticOverflow,
-            "attempt to compute offset in bytes which would overflow",
+            "attempt to compute offset in bytes which would overflow an `isize`",
             loc,
         );
 
@@ -1218,7 +1211,6 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_write_bytes(
         &mut self,
         instance: Instance<'tcx>,
-        intrinsic: &str,
         mut fargs: Vec<Expr>,
         loc: Location,
     ) -> Stmt {
@@ -1236,18 +1228,41 @@ impl<'tcx> GotocCtx<'tcx> {
             loc,
         );
 
-        // Check that computing `bytes` would not overflow
+        // Check that computing `count` in bytes would not overflow
+        let (count_bytes, overflow_check) =
+            self.count_in_bytes(count, ty, Type::size_t(), "write_bytes", loc);
+
+        let memset_call = BuiltinFn::Memset.call(vec![dst, val, count_bytes], loc);
+        Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc)
+    }
+
+    /// Computes (multiplies) the equivalent of a memory-related number (e.g., an offset) in bytes.
+    /// Because this operation may result in an arithmetic overflow, it includes an overflow check.
+    /// Returns a tuple with:
+    ///  * The result expression of the computation.
+    ///  * An assertion statement to ensure the operation has not overflowed.
+    fn count_in_bytes(
+        &self,
+        count: Expr,
+        ty: Ty<'tcx>,
+        res_ty: Type,
+        intrinsic: &str,
+        loc: Location,
+    ) -> (Expr, Stmt) {
+        assert!(res_ty.is_integer());
         let layout = self.layout_of(ty);
-        let size = Expr::int_constant(layout.size.bytes(), Type::size_t());
-        let bytes = count.mul_overflow(size);
-        let overflow_check = self.codegen_assert(
-            bytes.overflowed.not(),
+        let size_of_elem = Expr::int_constant(layout.size.bytes(), res_ty);
+        let size_of_count_elems = count.mul_overflow(size_of_elem);
+        let message = format!(
+            "{}: attempt to compute number in bytes which would overflow",
+            intrinsic.to_string()
+        );
+        let assert_stmt = self.codegen_assert(
+            size_of_count_elems.overflowed.not(),
             PropertyClass::ArithmeticOverflow,
-            format!("{}: attempt to compute `bytes` which would overflow", intrinsic).as_str(),
+            message.as_str(),
             loc,
         );
-
-        let memset_call = BuiltinFn::Memset.call(vec![dst, val, bytes.result], loc);
-        Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc)
+        (size_of_count_elems.result, assert_stmt)
     }
 }

tests/expected/intrinsics/write_bytes/overflow/expected

@@ -1,2 +1,2 @@
 FAILURE\
-write_bytes: attempt to compute `bytes` which would overflow
+write_bytes: attempt to compute number in bytes which would overflow

tests/expected/offset-bytes-overflow/expected

@@ -1,2 +1,2 @@
 FAILURE\
-attempt to compute offset in bytes which would overflow
+offset: attempt to compute number in bytes which would overflow

tests/expected/offset-from-bytes-overflow/expected

@@ -1,2 +1,4 @@
 FAILURE\
-attempt to compute offset in bytes which would overflow
+attempt to compute offset which would overflow
+FAILURE\
+attempt to compute offset in bytes which would overflow an `isize`

tests/expected/offset-from-bytes-overflow/main.rs

@@ -7,11 +7,11 @@ use std::convert::TryInto;
 
 #[kani::proof]
 fn main() {
-    let v: &[u128] = &[0; 200];
-    let v_100: *const u128 = &v[100];
-    let max_offset = usize::MAX / std::mem::size_of::<u128>();
+    let v: &[u128] = &[0; 10];
+    let v_0: *const u128 = &v[0];
+    let high_offset = usize::MAX / (std::mem::size_of::<u128>() * 2);
     unsafe {
-        let v_wrap: *const u128 = v_100.add((max_offset + 1).try_into().unwrap());
-        let _ = v_wrap.offset_from(v_100) == 2;
+        let v_wrap: *const u128 = v_0.add(high_offset.try_into().unwrap());
+        let _ = v_wrap.offset_from(v_0);
     }
 }

tests/expected/offset-wraps-around/expected

@@ -0,0 +1,2 @@
+FAILURE\
+assertion failed: high_offset == wrapped_offset.try_into().unwrap()

tests/expected/offset-wraps-around/main.rs

@@ -0,0 +1,35 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that a high offset causes a "wrapping around" behavior in CBMC.
+
+// This example can be really confusing. This program works fine in Rust and
+// it's okay to assert that the value coming from `offset_from` is equal to
+// `high_offset`. But CBMC's memory model is going to cause a "wrapping around"
+// behavior in `v_wrap`, so any values that depend on it are going to show a
+// strange behavior as well.
+use std::convert::TryInto;
+
+#[kani::proof]
+fn main() {
+    let v: &[u128] = &[0; 10];
+    let v_0: *const u128 = &v[0];
+    let high_offset = usize::MAX / (std::mem::size_of::<u128>() * 4);
+    unsafe {
+        // Adding `high offset` to `v_0` is undefined behavior, but Kani's
+        // default behavior does not report it. This kind of operations
+        // are quite common in the standard library, and we disabled such
+        // checks in order to avoid spurious verification failures.
+        //
+        // Note that this instance of undefined behavior will be reported
+        // by `miri` and also by Kani with `--extra-pointer-checks`.
+        // Also, dereferencing the pointer will also be reported by Kani's
+        // default behavior.
+        let v_wrap: *const u128 = v_0.add(high_offset.try_into().unwrap());
+        let wrapped_offset = v_wrap.offset_from(v_0);
+        // Both offsets should be the same, but because of the "wrapping around"
+        // behavior in CBMC, `wrapped_offset` does not equal `high_offset`
+        // https://github.com/model-checking/kani/issues/1150
+        assert!(high_offset == wrapped_offset.try_into().unwrap());
+    }
+}