Support pointer arithmetic in quantifier predicates#4583
Merged
feliperodri merged 2 commits intoMay 13, 2026
Conversation
feliperodri
added
[C] Feature / Enhancement
github-actions
Bot
added
Z-EndToEndBenchCI
feliperodri
force-pushed
the
quantifier-pointer-arithmetic
branch
4 times, most recently
from
b3ebaec to
546e834
Compare
adpaco-aws
approved these changes
Apr 30, 2026
feliperodri
force-pushed
the
quantifier-pointer-arithmetic
branch
from
546e834 to
56e0b81
Compare
adpaco-aws
reviewed
May 13, 2026
rajath-mk
approved these changes
May 13, 2026
Lower known pointer arithmetic intrinsics directly to CBMC pointer Plus
expressions in the pure expression inliner. These intrinsics have no
GOTO body to inline, so they need special handling in
inline_call_as_pure_expr.
Supported intrinsics:
- Element-offset variants: wrapping_add, wrapping_sub, wrapping_offset
- Byte-offset variants: wrapping_byte_offset, wrapping_byte_add,
wrapping_byte_sub
Since CBMC pointer Plus scales the offset by the pointee size:
- Element-offset variants apply Plus directly (scaling matches).
- Byte-offset variants first cast the pointer to *u8 so Plus scales
by 1 byte (matching Rust semantics that cast to u8 internally).
- Sub variants negate the offset before adding.
This enables quantifier predicates like:
forall!(|i in (0, len)| unsafe { *ptr.wrapping_byte_offset(i as isize) == 0 })
Changes:
- goto_ctx.rs: Recognize pointer arithmetic intrinsics by name and emit
correctly scaled ptr.plus(offset) expressions.
- rfc/0010-quantifiers.md: Document all supported variants and scaling
rules in the Detailed Design section.
- tests/kani/Quantifiers/pointer_arithmetic.rs: 8 harnesses covering
wrapping_byte_offset on u8 and u32 (scaling correctness),
wrapping_add/sub on u32, wrapping_byte_sub, and exists/forall.
feliperodri
force-pushed
the
quantifier-pointer-arithmetic
branch
from
56e0b81 to
d3192cb
Compare
Merged
via the queue into
model-checking:main
with commit May 13, 2026
71ab36e
32 of 34 checks passed
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
3 participants
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.
Lower wrapping pointer arithmetic intrinsics (
wrapping_add,wrapping_byte_offset) directly to CBMC pointerPlusexpressions in the pure expression inliner. These intrinsics have no GOTO body to inline, so they need special handling.Problem
Quantifier predicates that dereference pointers with offsets — e.g.,
*ptr.wrapping_byte_offset(i as isize)— failed because theinline_as_pure_exprinliner couldn't resolve pointer arithmetic intrinsics. These functions have no body in the symbol table (they're compiler intrinsics), so the inliner returned the original expression unchanged, leaving unresolved function calls that CBMC rejected.Solution
In
inline_call_as_pure_expr(goto_ctx.rs), before attempting to look up the function body, check if the function name matches a known wrapping pointer arithmetic intrinsic (wrapping_add,wrapping_byte_offset). If so, directly emitptr.plus(offset)— the CBMC expression for pointer arithmetic. A type guard (arguments[0].typ().is_pointer()) prevents misapplication to non-pointer functions.Non-wrapping variants (
offset,add,arith_offset) are intentionally excluded because they trigger CBMC bounds checks inside quantifier bodies, which fail in the symbolic evaluation context.Example
Changes
goto_ctx.rs: Recognize wrapping pointer arithmetic intrinsics and lower toptr.plus(offset)rfc/src/rfcs/0010-quantifiers.md: Document pointer arithmetic intrinsic lowering in the Detailed Design sectiontests/kani/Quantifiers/pointer_arithmetic.rs: 4 harnesses coveringwrapping_byte_offset(forall + exists) andwrapping_add(u32 + u8)By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.