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); +}