Repository navigation
Conversation
Statics were added to alloc_map, so a constant with the same initial bytes could be codegen'd as a read of the static, and a store to the static changed the constant. Only cache constant allocations. Resolves model-checking#5088
github-actions
Bot
added
Z-EndToEndBenchCI
r-near
marked this pull request as ready for review
October 28, 2026 07:31
Contributor
There was a problem hiding this comment.
🟢 Approval recommended
No active review issues block the change separating constant allocations from static storage.
No open issues 🎉
What changed in this PR
Fixes #5088 by preventing constants from reusing a static’s storage when their initial bytes match, avoiding false verification results in Kani.
Changes:
- Restricts allocation-cache insertion to constant allocations, keeping static storage separate.
- Adds a regression harness checking that writes to equal-bytes statics do not change a constant’s value.
| File | Description |
|---|---|
tests/kani/Static/static_const_same_bytes.rs |
Tests that a constant remains unchanged after atomic static stores. |
kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs |
Moves cache insertion from shared allocation code into constant allocation code. |
Review effort: Balanced
This branch has not been deployed
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.
Statics were inserted into
alloc_map, socodegen_const_allocationcould return a static's address for a constant with the same initial bytes, and a store to the static then changed the constant (false proofs / false failures). This moves the insert so only constant allocations are cached.Adds
tests/kani/Static/static_const_same_bytes.rs, which fails before this change.Resolves #5088
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.