Revert the changes to use intermediate usize

Author: celinval

library/kani_core/src/models.rs

@@ -59,9 +59,12 @@ macro_rules! generate_models {
                     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.
-                    // TODO: Use `wrapping_byte_offset` once we fix:
-                    //       https://github.com/model-checking/kani/issues/1150
-                    let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T;
+                    // 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",

…ffset-bounds-check/offset_usize.expected …bounds-check/fixme_offset_usize.expectedtests/expected/offset-bounds-check/offset_usize.expected renamed to tests/expected/offset-bounds-check/fixme_offset_usize.expected tests/expected/offset-bounds-check/offset_usize.expected renamed to tests/expected/offset-bounds-check/fixme_offset_usize.expected

@@ -1,5 +1,6 @@
 SUMMARY:\
- ** 5 of
+ ** 6 of
+Failed Checks: "Expected 0 and 1 to be the only safe values for offset"
 Failed Checks: Offset in bytes overflows isize
 Failed Checks: Offset result and original pointer must point to the same allocation
 Failed Checks: Offset value overflows isize

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

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check different violations that can be triggered when providing an usize offset
+//! with a type that has size > 1.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::offset;
+use std::ptr::addr_of;
+
+/// This harness exercises different scenarios when providing unconstrained offset counter.
+///
+/// We expect the following UB to be detected:
+/// 1. The offset value, `delta`, itself is greater than `isize::MAX`.
+/// 2. The offset in bytes, `delta * size_of::<u32>()`,  is greater than `isize::MAX`.
+/// 3. Offset result does not point to the same allocation as the original pointer.
+///
+/// The offset operation should only succeed for delta values:
+/// - `0`: The new pointer is the same as the base of the array.
+/// - `1`: The new pointer points to the end of the allocation.
+///
+/// FIXME: Because of CBMC wrapping behavior with pointer arithmetic, the assertion that checks
+/// that `delta <= 1` currently fails. See <https://github.com/model-checking/kani/issues/1150>.
+#[kani::proof]
+fn check_intrinsic_args() {
+    let array = [0u32];
+    let delta: usize = kani::any();
+    let new = unsafe { offset(addr_of!(array), delta) };
+    assert!(delta <= 1, "Expected 0 and 1 to be the only safe values for offset");
+    assert_eq!(new, &array, "This should fail for delta `1`");
+    assert_ne!(new, &array, "This should fail for delta `0`");
+}