Remove isize overflow check for zst offsets

library/kani_core/src/models.rs

@@ -99,29 +99,35 @@ macro_rules! generate_models {
             /// An offset model that checks UB.
             #[kanitool::fn_marker = "OffsetModel"]
             pub fn offset<T, P: Ptr<T>, O: ToISize>(ptr: P, offset: O) -> P {
-                let offset = offset.to_isize();
                 let t_size = core::mem::size_of::<T>() as isize;
-                if offset == 0 || t_size == 0 {
+                if t_size == 0 {
+                    // It's always safe to perform an offset on a ZST.
+                    return ptr;
+                }
+
+                // Note that this check must come after the t_size check, c.f. https://github.com/model-checking/kani/issues/3896
+                let offset = offset.to_isize();
+                if offset == 0 {
                     // It's always safe to perform an offset of length 0.
-                    ptr
-                } else {
-                    let (byte_offset, overflow) = offset.overflowing_mul(t_size);
-                    kani::safety_check(!overflow, "Offset in bytes overflows isize");
-                    let orig_ptr = ptr.to_const_ptr();
-                    // NOTE: For CBMC, using the pointer addition can have unexpected behavior
-                    // when the offset is higher than the object bits since it will wrap around.
-                    // See for more details: https://github.com/model-checking/kani/issues/1150
-                    //
-                    // However, when I tried implementing this using usize operation, we got some
-                    // unexpected failures that still require further debugging.
-                    // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T;
-                    let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset);
-                    kani::safety_check(
-                        kani::mem::same_allocation_internal(orig_ptr, new_ptr),
-                        "Offset result and original pointer must point to the same allocation",
-                    );
-                    P::from_const_ptr(new_ptr)
+                    return ptr;
                 }
+
+                let (byte_offset, overflow) = offset.overflowing_mul(t_size);
+                kani::safety_check(!overflow, "Offset in bytes overflows isize");
+                let orig_ptr = ptr.to_const_ptr();
+                // NOTE: For CBMC, using the pointer addition can have unexpected behavior
+                // when the offset is higher than the object bits since it will wrap around.
+                // See for more details: https://github.com/model-checking/kani/issues/1150
+                //
+                // However, when I tried implementing this using usize operation, we got some
+                // unexpected failures that still require further debugging.
+                // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T;
+                let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset);
+                kani::safety_check(
+                    kani::mem::same_allocation_internal(orig_ptr, new_ptr),
+                    "Offset result and original pointer must point to the same allocation",
+                );
+                P::from_const_ptr(new_ptr)
             }
 
             pub trait Ptr<T> {

tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected

@@ -1,4 +1,6 @@
 Failed Checks: Offset result and original pointer must point to the same allocation
-Verification failed for - check_ptr_oob
+Failed Checks: Offset result and original pointer must point to the same allocation
 
-Complete - 1 successfully verified harnesses, 1 failures, 2 total.
+Verification failed for - test_offset_overflow
+Verification failed for - check_ptr_oob
+Complete - 1 successfully verified harnesses, 2 failures, 3 total.

tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs

@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Check that Kani offset operations correctly detect out-of-bound access.
 
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+
 /// Verification should fail because safety violation is not a regular panic.
 #[kani::proof]
 #[kani::should_panic]
@@ -24,3 +27,15 @@ fn check_ptr_end() {
     // Safety: Pointers point to the same allocation
     assert_eq!(unsafe { end_ptr.offset_from(base_ptr) }, 1);
 }
+
+#[kani::proof]
+fn test_offset_overflow() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        // This should fail because adding `isize::MAX` to `ptr` would overflow
+        // `isize`
+        let _d = offset(ptr, isize::MAX);
+    }
+}

tests/expected/offset-overflows-isize/expected

@@ -0,0 +1,8 @@
+<usize as kani::rustc_intrinsics::ToISize>::to_isize.safety_check\
+	 - Status: FAILURE\
+	 - Description: "Offset value overflows isize"
+
+Failed Checks: Offset value overflows isize
+
+Verification failed for - test_non_zst
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/offset-overflows-isize/main.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `offset` does not accept a `count` greater than isize::MAX,
+// except for ZSTs, c.f. https://github.com/model-checking/kani/issues/3896
+
+#[kani::proof]
+fn test_zst() {
+    let mut x = ();
+    let ptr: *mut () = &mut x as *mut ();
+    let count: usize = (isize::MAX as usize) + 1;
+    let _ = unsafe { ptr.add(count) };
+}
+
+#[kani::proof]
+fn test_non_zst() {
+    let mut x = 7;
+    let ptr: *mut i32 = &mut x as *mut i32;
+    let count: usize = (isize::MAX as usize) + 1;
+    let _ = unsafe { ptr.add(count) };
+}