Do not silently wrap pointer offsets in the propositional encoding - #9134
Open
tautschnig wants to merge 2 commits into
Open
Do not silently wrap pointer offsets in the propositional encoding#9134tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
The propositional encoding packs pointers into object bits and offset
bits, and performed pointer arithmetic on the offset field only: any
result offset outside [0, 2^offset_bits) silently wrapped around within
the same object. The simplifier and constant propagation, however,
compute pointer arithmetic in full-width arithmetic, so semantically
identical programs produced contradictory verification results
depending on whether the arithmetic was constant-folded, e.g.:
char x, *p = &x;
uint64_t k;
char *r = p + k;
if(k == (1ULL << 48))
assert(r != p); // was: refuted (with 16 object bits)
char *q = p + (1ULL << 48);
assert(q != p); // was: proved
This inconsistency also defeated out-of-bounds checks built on top of
the encoding: Kani's pointer-offset UB check missed genuine
out-of-bounds offsets that are multiples of 2^(64 - object_bits)
because the wrapped pointer aliased the base pointer and thus passed a
same-allocation check
(model-checking/kani#1150).
Perform offset arithmetic at full address width instead and, when the
mathematical result does not fit the offset field, direct the result to
the invalid object, mirroring what integer-to-pointer conversion does
for unknown addresses. Out-of-encoding-range results thereby compare
unequal to every pointer into the original object, consistent with
full-width arithmetic, and is_invalid_pointer now correctly identifies
them - pointer-overflow-check's "pointer invalid" assertion in
regression/cbmc/pointer-overflow3 now fails for `p - 10` on a
5-element allocation, which is reflected in the updated test
expectations.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
July 23, 2026 12:12
There was a problem hiding this comment.
Pull request overview
Note
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Updates CBMC’s propositional pointer encoding to avoid silent offset wrap-around by performing pointer-offset arithmetic at full address width and mapping out-of-encoding-range results to the invalid object, aligning solver behavior with simplification/constant folding and strengthening UB checks.
Changes:
- Compute pointer offset sums at (address width + 1) instead of truncating to
offset_bits, deferring range handling tooffset_arithmetic. - Detect out-of-range offset results and replace the pointer’s object with the invalid object to prevent aliasing due to wrap-around.
- Update/add regression expectations to reflect the new “pointer invalid” behavior on overflow/underflow cases.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| src/solvers/flattening/bv_pointers.cpp | Switches pointer-offset arithmetic to full address width and redirects out-of-range results to the invalid object. |
| regression/cbmc/pointer-overflow3/no-simplify.desc | Updates expected failures to include the new “pointer invalid” report. |
| regression/cbmc/pointer-arithmetic-offset-wrap/test.desc | Adds a regression driver for the previously inconsistent wrap-around behavior. |
| regression/cbmc/pointer-arithmetic-offset-wrap/main.c | New test case exercising non-constant vs constant-folded pointer arithmetic consistency. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+511
to
+517
| if(op.size() < sum.size()) | ||
| op = bv_utils.extension(op, sum.size(), rep); | ||
| else if(op.size() > sum.size()) | ||
| sum = bv_utils.extension( | ||
| sum, op.size(), bv_utilst::representationt::SIGNED); | ||
|
|
||
| sum=bv_utils.add(sum, op); | ||
| sum = bv_utils.add(sum, op); |
Comment on lines
+914
to
+923
| bvt bv_tmp(sum_ext.begin(), sum_ext.begin() + offset_bits); | ||
|
|
||
| bvt bv_tmp = bv_utils.add(offset_bv, bv_index); | ||
| // On overflow, replace the object by the invalid object so that the | ||
| // result compares unequal to any pointer into the original object. | ||
| bvt object_bv = object_literals(bv, type); | ||
| bvt invalid_object_bv = | ||
| object_literals(encode(pointer_logic.get_invalid_object(), type), type); | ||
| bvt new_object_bv = bv_utils.select(overflow, invalid_object_bv, object_bv); | ||
|
|
||
| return object_offset_encoding(object_literals(bv, type), bv_tmp); | ||
| return object_offset_encoding(new_object_bv, bv_tmp); |
Comment on lines
+18
to
+19
| if(k == (1ULL << 48)) | ||
| assert(r != p); |
Comment on lines
+25
to
+26
| char *q = p + (1ULL << 48); | ||
| assert(q != p); |
The previous commit directed pointer-arithmetic results whose offset
does not fit the pointer encoding's offset field to the invalid object,
but kept the truncated offset. Two identically-shifted pointers into
*different* objects thereby received bit-identical encodings, making
their equality provable:
char x, y, *p = &x, *p2 = &y;
uint64_t k;
char *w1 = p + k, *w2 = p2 + k;
if(k == (1ULL << 48))
assert(w1 == w2); // was: proved (16 object bits)
No concrete address assignment can make disjoint objects shifted by the
same amount collide, so proving this equality is unsound.
Use a nondeterministic offset for out-of-range results instead: such a
pointer now has an unknown address, so neither equality nor inequality
between two of them is provable, and all previously established
properties (inequality with any pointer into the original object,
is_invalid_pointer identification) are preserved. This matches the
overall model in which object base addresses are chosen arbitrarily and
the address of an out-of-range pointer is unconstrained.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This was referenced Jul 24, 2026
Merged
feliperodri
added a commit
to tautschnig/kani
that referenced
this pull request
Aug 14, 2026
…ng (model-checking#4671) 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 (model-checking#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 model-checking#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. --------- Signed-off-by: Felipe Monteiro <felisous@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The propositional encoding packs pointers into object bits and offset bits, and performed pointer arithmetic on the offset field only: any result offset outside [0, 2^offset_bits) silently wrapped around within the same object. The simplifier and constant propagation, however, compute pointer arithmetic in full-width arithmetic, so semantically identical programs produced contradictory verification results depending on whether the arithmetic was constant-folded, e.g.:
char x, *p = &x;
uint64_t k;
char *r = p + k;
if(k == (1ULL << 48))
assert(r != p); // was: refuted (with 16 object bits)
char *q = p + (1ULL << 48);
assert(q != p); // was: proved
This inconsistency also defeated out-of-bounds checks built on top of the encoding: Kani's pointer-offset UB check missed genuine out-of-bounds offsets that are multiples of 2^(64 - object_bits) because the wrapped pointer aliased the base pointer and thus passed a same-allocation check
(model-checking/kani#1150).
Perform offset arithmetic at full address width instead and, when the mathematical result does not fit the offset field, direct the result to the invalid object, mirroring what integer-to-pointer conversion does for unknown addresses. Out-of-encoding-range results thereby compare unequal to every pointer into the original object, consistent with full-width arithmetic, and is_invalid_pointer now correctly identifies them - pointer-overflow-check's "pointer invalid" assertion in regression/cbmc/pointer-overflow3 now fails for
p - 10on a 5-element allocation, which is reflected in the updated test expectations.