Fix OffsetModel missing UB for offsets wrapping CBMC's pointer encoding

CBMC encodes pointers as an (object, offset) pair where the offset
field has pointer_width - object_bits bits. Pointer arithmetic
therefore wraps offsets at 2^(64 - object_bits) rather than 2^64
(#1150). For the
OffsetModel this meant that a symbolic byte offset that is a non-zero
multiple of 2^(64 - object_bits) (2^48 with Kani's default of 16
object bits) made `wrapping_byte_offset` alias the original pointer,
so the subsequent same-allocation safety check passed spuriously and
genuine out-of-bounds `offset` calls verified successfully - including
"proving" the false fact that the result equals the base pointer.

Detect the wrap by additionally requiring that the address of the
result is consistent with full-width integer arithmetic on the address
of the original pointer; any truncation in the pointer addition
falsifies this equation. Two alternative formulations do not work:

* Computing the new pointer via integer arithmetic
  (addr().wrapping_add_signed(off) followed by a cast back, as
  previously suggested in a FIXME here) is sound, but makes the solver
  case-split the integer address over every object; harnesses using
  e.g. `sort()` then run out of memory. These are the "unexpected
  failures" mentioned in the removed comment (reproduced on:
  expected/cover/cover-pass, expected/string-repeat,
  expected/loop-backedge, expected/shadow/unsupported_num_objects).

* Comparing POINTER_OFFSET(new) against full-width
  POINTER_OFFSET(orig) + offset is defeated by CBMC's simplifier,
  which rewrites POINTER_OFFSET(p + k) to POINTER_OFFSET(p) + k in
  full-width arithmetic, making the equation trivially true.

The `addr()` transmute is opaque to that simplification, keeps all
operations in the pointer domain, and adds negligible solver cost:
the full expected (459) and kani (593) suites pass unchanged.

The underlying encoding wrap is fixed on the CBMC side in
diffblue/cbmc#9134 (out-of-range results are
directed to the invalid object). The equation here also states Rust's
address-arithmetic contract for `offset` and produces the same verdicts
with and without that CBMC fix, so it is kept as a semantic guard
rather than a version-specific workaround.

Partially addresses #1150: this fixes the missed-UB soundness hole in
the checked `offset`/`arith_offset` intrinsic model. Not addressed is
the `wrapping_offset` family, which Kani codegens to plain CBMC pointer
addition: under CBMC versions without the encoding fix its result
aliases the base pointer for wrap-multiple offsets
(tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs), and even with
the CBMC fix the result address is indeterminate rather than the
exactly-wrapped address that Rust defines. Exact modeling would require
integer arithmetic plus an integer-to-pointer cast, which makes the
solver case-split over all objects (see above).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

library/kani_core/src/models.rs

@@ -124,16 +124,39 @@ macro_rules! generate_models {
                 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
+                // The equation below asserts Rust's semantic contract for `offset`:
+                // the address of the result must equal the address of the original
+                // pointer plus the byte offset, in full-width (2^64) integer
+                // arithmetic.
                 //
-                // 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;
+                // Besides documenting that contract, it guards against CBMC's
+                // pointer encoding wrapping offsets at
+                // 2^(pointer_width - object_bits) rather than 2^pointer_width: for
+                // symbolic offsets that are multiples of 2^(64 - object_bits) the
+                // pointer addition below aliases back into the allocation, so the
+                // same-allocation check alone would pass spuriously and hide
+                // genuine UB (https://github.com/model-checking/kani/issues/1150).
+                // CBMC fixed this in https://github.com/diffblue/cbmc/pull/9134 by
+                // directing out-of-range results to the invalid object at a
+                // nondeterministic address (which makes the equation below
+                // refutable, so this safety check still fails; the two mechanisms
+                // agree); the guard remains necessary for CBMC versions without
+                // that fix, and remains correct with it.
+                //
+                // Implementation notes:
+                // * `addr()` (a pointer-to-integer transmute) is deliberately used
+                //   here rather than `kani::mem::pointer_offset`: CBMC's simplifier
+                //   rewrites `POINTER_OFFSET(p + k)` to `POINTER_OFFSET(p) + k` in
+                //   full-width arithmetic, which would make a pointer_offset-based
+                //   equation trivially true and hide the wrap again.
+                // * This formulation keeps all operations in the pointer domain (no
+                //   integer-to-pointer casts, which make the solver case-split the
+                //   address over every object and blow up, e.g., on harnesses using
+                //   `sort()`).
                 let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset);
+                let no_wrap = new_ptr.addr() == orig_ptr.addr().wrapping_add(byte_offset as usize);
                 kani::safety_check(
-                    kani::mem::same_allocation_internal(orig_ptr, new_ptr),
+                    no_wrap && 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)

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

@@ -0,0 +1,16 @@
+Checking harness check_valid_negative_offset...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_ub_sym_wrap_min...
+Failed Checks: Offset result and original pointer must point to the same allocation
+VERIFICATION:- FAILED
+
+Checking harness check_ub_sym_wrap_negative...
+Failed Checks: Offset result and original pointer must point to the same allocation
+VERIFICATION:- FAILED
+
+Checking harness check_ub_sym_wrap_positive...
+Failed Checks: Offset result and original pointer must point to the same allocation
+VERIFICATION:- FAILED
+
+Complete - 1 successfully verified harnesses, 3 failures, 4 total.

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

@@ -0,0 +1,54 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the offset UB check is not defeated by CBMC's pointer-offset
+//! encoding, which wraps offsets at 2^(pointer_width - object_bits) rather
+//! than 2^pointer_width: a symbolic byte offset that is a non-zero multiple
+//! of 2^(64 - object_bits) (e.g. 2^48 with Kani's default of 16 object bits)
+//! used to alias the original pointer, making the same-allocation check pass
+//! spuriously and hiding genuine UB.
+//! See <https://github.com/model-checking/kani/issues/1150>.
+//!
+//! CBMC fixed the underlying encoding wrap in
+//! <https://github.com/diffblue/cbmc/pull/9134> (out-of-range results are
+//! directed to the invalid object); these harnesses must produce the same
+//! verdicts with and without that fix, via the address-arithmetic guard in
+//! Kani's OffsetModel.
+
+#[kani::proof]
+fn check_ub_sym_wrap_positive() {
+    let v = [0u8; 8];
+    let p: *const u8 = &v[0];
+    let off: isize = kani::any();
+    kani::assume(off == 1isize << 48);
+    let _q = unsafe { p.offset(off) }; // UB: far out of bounds
+}
+
+#[kani::proof]
+fn check_ub_sym_wrap_negative() {
+    let v = [0u8; 8];
+    let p: *const u8 = &v[0];
+    let off: isize = kani::any();
+    kani::assume(off == -(1isize << 48));
+    let _q = unsafe { p.offset(off) }; // UB: far out of bounds
+}
+
+#[kani::proof]
+fn check_ub_sym_wrap_min() {
+    let v = [0u8; 8];
+    let p: *const u8 = &v[0];
+    let off: isize = kani::any();
+    kani::assume(off == isize::MIN);
+    let _q = unsafe { p.byte_offset(off) }; // UB: far out of bounds
+}
+
+/// In-bounds negative offsets must still verify, including the extremes.
+#[kani::proof]
+fn check_valid_negative_offset() {
+    let v = [0u8; 8];
+    let p: *const u8 = &v[4];
+    let off: isize = kani::any();
+    kani::assume(off >= -4 && off <= 3);
+    let q = unsafe { p.offset(off) };
+    assert_eq!(unsafe { q.offset_from(v.as_ptr()) }, 4 + off);
+}