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