Fix the computation of the number of bytes of a pointer offset

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/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) };
+}