Fix the computation of the number of bytes of a pointer offset (#3584)

This PR fixes the logic that computes the number of bytes of a pointer
offset. The logic was incorrectly using the size of the pointer as
opposed to the size of the pointee.

This fixes the soundness issue in #3582 (but not the spurious failures).

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/rvalue.rs

@@ -410,7 +410,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Check that computing `offset` in bytes would not overflow
                 let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
                     ce2.clone().cast_to(Type::ssize_t()),
-                    ty,
+                    pointee_type_stable(ty).unwrap(),
                     Type::ssize_t(),
                     "offset",
                     loc,

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

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

tests/expected/offset-overflow/expected

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

tests/expected/offset-overflow/main.rs

@@ -8,10 +8,13 @@ use std::intrinsics::offset;
 
 #[kani::proof]
 fn test_offset_overflow() {
-    let s: &str = "123";
-    let ptr: *const u8 = s.as_ptr();
+    let a: [i32; 3] = [1, 2, 3];
+    let ptr: *const i32 = a.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, isize::MAX / 8);
+        let _d = offset(ptr, count);
     }
 }

tests/expected/ptr-offset-overflow/expected

@@ -0,0 +1,5 @@
+std::ptr::const_ptr::<impl *const Foo>::offset.arithmetic_overflow\
+Status: FAILURE\
+Description: "offset: attempt to compute number in bytes which would overflow"
+
+VERIFICATION:- FAILED

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

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that Kani detects the overflow in pointer offset
+
+use std::convert::TryFrom;
+
+struct Foo {
+    arr: [i32; 4096],
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn main() {
+    let f = Foo { arr: [0; 4096] };
+    assert_eq!(std::mem::size_of::<Foo>(), 16384);
+    // a large enough count that causes `count * size_of::<Foo>()` to overflow
+    // `isize` without overflowing `usize`
+    let count: usize = 562949953421320;
+    // the `unwrap` ensures that it indeed doesn't overflow `usize`
+    let bytes = count.checked_mul(std::mem::size_of::<Foo>()).unwrap();
+    // ensure that it overflows `isize`:
+    assert!(isize::try_from(bytes).is_err());
+
+    let ptr: *const Foo = &f as *const Foo;
+    // this should fail because `count * size_of::<Foo>` overflows `isize`
+    let _p = unsafe { ptr.offset(count as isize) };
+}