High offsets cause wrapping-around behavior in CBMC

[adpaco]

In an example introduced in #1131 , we reproduced an issue where a high offset causes a "wrapping around" behavior in CBMC.
There is more information on the test, but basically we should either enforce stricter checks than Rust (because of CBMC object bits limitations) or add these checks to CBMC itself.

[celinval]

I think we will need to stop using CBMC's pointer offset operation in the case of wrapping_offset. Instead, we need to convert the pointer into a usize, perform a wrapping_add considering the object size, then convert back to a pointer.

[celinval]

BTW, here is a small example that shows the problem:

/// This harness shows the issue with the current implementation of wrapping offset.
///
/// Invoking `wrapping_byte_offset` should return a pointer that is different from the original
/// pointer if the offset value is not 0.
#[kani::proof]
fn fixme_incorrect_wrapping_offset() {
    let ptr: *const u8 = &0u8;
    let offset = kani::any_where(|v: &isize| *v != 0);
    let new_ptr = ptr.wrapping_byte_offset(offset);
    assert_ne!(ptr, new_ptr, "Expected new_ptr to be different than ptr");
}

[tautschnig]

Status update after a detailed investigation of this issue (all findings reproduced against current main + CBMC 6.10.0; details in the linked PRs).

Root cause, characterized: CBMC's propositional encoding packs pointers into object|offset bits, so pointer arithmetic wrapped offsets at 2^(64 − object_bits) instead of 2^64 (with Kani's default --object-bits 16: at 2^48). Constant-folded arithmetic, however, is computed at full width by CBMC's simplifier — so semantically identical harnesses gave different verdicts for constant vs. symbolic offsets. Beyond the spurious counterexample shown above, this was a soundness hole: p.offset(k) on an 8-byte allocation with symbolic k == 1 << 48 verified successfully — the wrapped result aliases p, so the same-allocation UB check passed spuriously.

The fixes and how they compose:

1. Fix OffsetModel missing UB for offsets wrapping CBMC's pointer encoding #4671 (Kani, mergeable now): the OffsetModel additionally requires new_ptr.addr() == orig_ptr.addr().wrapping_add(byte_offset) — Rust's address-arithmetic contract for offset, which any encoding truncation falsifies. This closes the missed-UB hole on all current CBMC releases. It deliberately avoids two alternatives that don't work: POINTER_OFFSET-based formulations (defeated by the simplifier rewriting POINTER_OFFSET(p + k) to POINTER_OFFSET(p) + k at full width) and computing the pointer via integer round-trip (see blow-up data below).

2. Do not silently wrap pointer offsets in the propositional encoding diffblue/cbmc#9134 (CBMC default encoding): pointer arithmetic whose result offset doesn't fit the offset field now yields the invalid object at a nondeterministic address instead of silently wrapping. This makes the default encoding sound for out-of-range pointers: nothing false is provable anymore (the initial invalid-object-only version could still prove equality of two identically-shifted pointers into disjoint objects; the nondet-address amendment fixes that). Residual imprecision: relations between wrapped pointers become refutable rather than exact — false alarms only. Notably, this fix alone makes the fixme_wrap_nonzero_offset example above pass.

3. Add --wide-pointer-encoding: 192-bit pointers with flat addresses diffblue/cbmc#8954 (--wide-pointer-encoding, draft): the full resolution. A flat address component maintained through arithmetic makes wrapping_offset semantics exact: correct verdicts on all address relations, and the wrap-out-and-back-then-dereference pattern (defined in Rust — wrapping_offset preserves provenance) works because the object component survives alongside the exact address.

Why not model exact semantics in Kani directly (the integer round-trip suggested above): measured on tests/expected/cover/cover-pass (a 5-element sort()), it explodes symbolic execution from 10,314 to 287,290 SSA steps and from 69 to 13,762 surviving VCCs, then OOMs at 16 GB (baseline: 6 s / 0.34 GB). The cost isn't the arithmetic — it's provenance loss: every later dereference of an int-derived pointer case-splits over every object, nested through loops. Exactness for wrapped addresses is structurally at odds with the provenance abstraction that makes CBMC's pointer reasoning tractable, which is why the fix belongs at the encoding level (#8954).

Composition checkpoints going forward:

• When rebasing Add --wide-pointer-encoding: 192-bit pointers with flat addresses diffblue/cbmc#8954 onto a develop containing Do not silently wrap pointer offsets in the propositional encoding diffblue/cbmc#9134 (both touch offset_arithmetic): the out-of-range redirect must apply to the object/offset components only, with the flat address staying exact — then OOB-offset() UB detection and exact equality coexist.
• Under --wide-pointer-encoding, the kani#4671 guard becomes trivially true (the address is exact), shifting the UB-detection burden entirely to the same-allocation check — sound iff the previous point holds. The offset_wrap_sym regression test added in kani#4671 pins this and should stay in the suite permanently.
• Kani will eventually need plumbing to opt into the wide encoding (it's a ~3× internal pointer-width tax, so likely per-harness, like --object-bits).

Suggested disposition: keep this issue open until CBMC ships #9134 and Kani's pin reaches it (then drop the fixme_ prefix on fixme_wrap_nonzero_offset.rs); at that point either close with the documented false-alarm-only imprecision for wrapped-address arithmetic, or keep open narrowly tracking exact semantics via #8954.