From a801db501b217487ffddd70b4da6c5101bdee62c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Jul 2026 18:26:27 +0000 Subject: [PATCH] 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 (https://github.com/model-checking/kani/issues/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 https://github.com/diffblue/cbmc/pull/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 --- library/kani_core/src/models.rs | 37 ++++++++++--- .../offset_wrap_sym.expected | 16 ++++++ .../offset-bounds-check/offset_wrap_sym.rs | 54 +++++++++++++++++++ 3 files changed, 100 insertions(+), 7 deletions(-) create mode 100644 tests/expected/offset-bounds-check/offset_wrap_sym.expected create mode 100644 tests/expected/offset-bounds-check/offset_wrap_sym.rs diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 2c15d9d98743..b7e0030b1f98 100644 --- a/library/kani_core/src/models.rs +++ b/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) diff --git a/tests/expected/offset-bounds-check/offset_wrap_sym.expected b/tests/expected/offset-bounds-check/offset_wrap_sym.expected new file mode 100644 index 000000000000..3d49cfd8de86 --- /dev/null +++ b/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. diff --git a/tests/expected/offset-bounds-check/offset_wrap_sym.rs b/tests/expected/offset-bounds-check/offset_wrap_sym.rs new file mode 100644 index 000000000000..a0e3bfa44068 --- /dev/null +++ b/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 . +//! +//! CBMC fixed the underlying encoding wrap in +//! (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); +}