Remove the overflow checks for wrapping_offset (#3589)

This PR removes the overflow checks done for the `arith_offset`
intrinsic, which is used in implementation of `ptr::wrapping_offset`.
According to the documentation, this operation is always safe:


https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_offset
https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html

See
#3582 (comment)
for the context.

Resolves #3582 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

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

@@ -296,9 +296,7 @@ impl<'tcx> GotocCtx<'tcx> {
             Intrinsic::AddWithOverflow => {
                 self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, place, loc)
             }
-            Intrinsic::ArithOffset => {
-                self.codegen_offset(intrinsic_str, instance, fargs, place, loc)
-            }
+            Intrinsic::ArithOffset => self.codegen_arith_offset(fargs, place, loc),
             Intrinsic::AssertInhabited => {
                 self.codegen_assert_intrinsic(instance, intrinsic_str, span)
             }
@@ -1017,51 +1015,16 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Computes the offset from a pointer.
     ///
-    /// Note that this function handles code generation for:
-    ///  1. The `offset` intrinsic.
-    ///     <https://doc.rust-lang.org/std/intrinsics/fn.offset.html>
-    ///  2. The `arith_offset` intrinsic.
+    /// This function handles code generation for the `arith_offset` intrinsic.
     ///     <https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html>
-    ///
-    /// Note(std): We don't check that the starting or resulting pointer stay
-    /// within bounds of the object they point to. Doing so causes spurious
-    /// failures due to the usage of these intrinsics in the standard library.
-    /// See <https://github.com/model-checking/kani/issues/1233> for more details.
-    /// Also, note that this isn't a requirement for `arith_offset`, but it's
-    /// one of the safety conditions specified for `offset`:
-    /// <https://doc.rust-lang.org/std/primitive.pointer.html#safety-2>
-    fn codegen_offset(
-        &mut self,
-        intrinsic: &str,
-        instance: Instance,
-        mut fargs: Vec<Expr>,
-        p: &Place,
-        loc: Location,
-    ) -> Stmt {
+    /// According to the documenation, the operation is always safe.
+    fn codegen_arith_offset(&mut self, mut fargs: Vec<Expr>, p: &Place, loc: Location) -> Stmt {
         let src_ptr = fargs.remove(0);
         let offset = fargs.remove(0);
 
-        // Check that computing `offset` in bytes would not overflow
-        let args = instance_args(&instance);
-        let ty = args.0[0].expect_ty();
-        let (offset_bytes, bytes_overflow_check) =
-            self.count_in_bytes(offset.clone(), *ty, Type::ssize_t(), intrinsic, loc);
-
-        // Check that the computation would not overflow an `isize`
-        // 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_assume(
-            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
+        // Compute `dst_ptr` with standard addition to avoid conversion
         let dst_ptr = src_ptr.plus(offset);
-        let expr_place = self.codegen_expr_to_place_stable(p, dst_ptr, loc);
-        Stmt::block(vec![bytes_overflow_check, overflow_check, expr_place], loc)
+        self.codegen_expr_to_place_stable(p, dst_ptr, loc)
     }
 
     /// ptr_offset_from returns the offset between two pointers

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

@@ -420,6 +420,13 @@ impl<'tcx> GotocCtx<'tcx> {
                 // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
                 // These checks may allow a wrapping-around behavior in CBMC:
                 // https://github.com/model-checking/kani/issues/1150
+                // Note(std): We don't check that the starting or resulting pointer stay
+                // within bounds of the object they point to. Doing so causes spurious
+                // failures due to the usage of these intrinsics in the standard library.
+                // See <https://github.com/model-checking/kani/issues/1233> for more details.
+                // Note that this is one of the safety conditions for `offset`:
+                // <https://doc.rust-lang.org/std/primitive.pointer.html#safety-2>
+
                 let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes);
                 let overflow_check = self.codegen_assert_assume(
                     overflow_res.overflowed.not(),

tests/expected/arith-offset-overflow/expected

@@ -1,2 +1 @@
-FAILURE\
-attempt to compute offset which would overflow
+VERIFICATION:- SUCCESSFUL

tests/expected/arith-offset-overflow/main.rs

@@ -1,8 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that `arith_offset` fails if the offset computation would
-// result in an arithmetic overflow
+// Checks that `arith_offset` succeeds even if the offset computation would
+// result in an arithmetic overflow as it uses wrapping:
+// https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html
 #![feature(core_intrinsics)]
 use std::intrinsics::arith_offset;
 

tests/expected/offset-overflow/expected

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

tests/expected/offset-overflow/main.rs

@@ -8,13 +8,12 @@ use std::intrinsics::offset;
 
 #[kani::proof]
 fn test_offset_overflow() {
-    let a: [i32; 3] = [1, 2, 3];
-    let ptr: *const i32 = a.as_ptr();
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
 
-    // a value that when multiplied by the size of i32 (i.e. 4 bytes)
-    // would overflow `isize`
-    let count: isize = isize::MAX / 4 + 1;
     unsafe {
-        let _d = offset(ptr, count);
+        // This should fail because adding `isize::MAX` to `ptr` would overflow
+        // `isize`
+        let _d = offset(ptr, isize::MAX);
     }
 }

tests/expected/wrapping-offset-bytes-overflow/expected

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

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

@@ -2,7 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Check that an offset (computed with `wrapping_offset`) that overflows an
-// `isize::MAX` triggers a verification failure.
+// `isize::MAX` does NOT trigger a verification failure as the operation is
+// always safe:
+// https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_offset
 use std::convert::TryInto;
 
 #[kani::proof]