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

[tautschnig]

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).

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This pull request strengthens Kani’s OffsetModel safety checking to detect and reject undefined behavior that was previously missed due to CBMC’s pointer encoding truncating/wrapping the offset field (issue #1150), and adds a regression test to ensure the soundness hole stays closed across CBMC versions.

Changes:

• Add an address-consistency guard (addr()-based) to detect offset truncation/wrap in CBMC’s pointer encoding before relying on same-allocation checks.
• Add a new expected-suite regression test covering symbolic high-offset wrap cases (positive, negative, and isize::MIN), plus an in-bounds control harness.
• Add corresponding .expected output asserting the new failures are reported.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
tests/expected/offset-bounds-check/offset_wrap_sym.rs	New regression harnesses exercising the high-offset wrap soundness hole and a valid in-bounds negative-offset case.
tests/expected/offset-bounds-check/offset_wrap_sym.expected	Expected output for the new regression tests (3 failures, 1 success).
library/kani_core/src/models.rs	Tightens OffsetModel UB detection by adding an address-arithmetic consistency check alongside same-allocation checking.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[feliperodri]

I'd implement the Copilot comments before merging it.