Conversation
The existing region_allocations* tests all expect success, and the older
memory-safety failure tests predate the split, so they only ever exercise
a single allocation class. Nothing yet checks that a violation is still
*detected* once liveness is partitioned -- the failure that matters here
is a use-after-free that silently verifies because the free updated one
class map and the dereference read another.
Add three tests, each with two allocation classes:
- use_after_free_fail: free one class, dereference it
- double_free_fail: free the same pointer twice
- interprocedural_fail: allocate, free, and dereference in three
different procedures
Each was checked to actually catch the regression it targets: with
$free's `A.out[p] := false` removed from the model, all three report
"SMACK found no errors" instead of an error. double_free_fail leaves its
second allocation unfreed on purpose -- freeing it would leave the
allocation counter unbalanced under that mutation, and the resulting
memory-leak error would mask the missing double-free error.
Verified across no-reuse-impls, no-reuse, and reuse with both Corral and
Boogie (18/18). Only no-reuse-impls attributes a double free to
{:valid_free}; the other two models encode $free's check as a `requires`
on a bodyless procedure, so the violation surfaces as a generic
precondition failure. That is pre-existing -- simple_double_free.c
behaves the same way on develop -- so double_free_fail asserts only
@expect error rather than a specific message.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
allocationIdx relies on an invariant that was never written down: no two entries of `allocations` may satisfy mayShareAllocation, because findAllocation returns the first match and would otherwise pick an arbitrary one of several. The old post-merge rescan only walked forward from the class that absorbed the region. That is sufficient, but only because the invariant already caps us at one `incomplete` and one `complicated` class -- any two of either would have merged earlier. Nothing states that, and mayShareAllocation is not transitive, so widening the predicate later would silently break the single pass. Rescan to a fixed point instead, over all classes rather than just the ones after `a`, so correctness no longer rests on that side condition. Document the invariant and why establishing it needs a fixed point. Add Regions::allocationsAreDisjoint, asserted once at the end of runOnModule. The check is quadratic in the number of classes and allocationIdx runs at every tracked access, so checking per merge would tax every translation in the Debug build we ship by default. No behavioral change observed: the six region_allocations* tests keep identical class counts and results, and the assertion did not fire across 250 translations of c/memory-safety, c/ntdrivers-simplified, and c/data under --check=memory-safety, with and without --no-memory-splitting. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
shaobo-he
force-pushed
the
fix-768-region-allocations
branch
from
August 16, 2026 07:27
7ffac63 to
2ea8951
Compare
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
1 participant
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.
Fixes #768.
Summary
free, and memory-safety-check helpers
Design
Allocation classes are tracked separately from SMACK memory regions. A memory
region can represent a disjoint offset range within an object, but all offsets
of that object must observe the same allocation state. Consequently, a strict
one-to-one
$Alloc.xto$M.xmapping would reject valid interior accesses.The no-reuse models use the global monotonic address counter to keep allocation
classes disjoint, so their old shared
$Allocmap can be removed. The reusemodel must still prevent simultaneously live allocations from different
classes from receiving overlapping addresses. It therefore keeps the existing
shared occupancy map for allocator freshness while dereference and free checks
use class-local liveness maps.
The allocator helpers take maps as values and return exact map updates. This
also replaces quantified frame conditions for the class-local state.
Evaluation
On a synthetic program with 32 independent allocation sites, end-to-end Boogie
times were:
The reuse cost is expected from retaining global occupancy while adding local
liveness. The complete existing memory-safety suite remained approximately
neutral overall; the split pays off as the number of independent allocation
sites grows.
Testing
no-reuse-impls,no-reuse, andreuse, using both Boogie and Corral--no-memory-splittingRegressions cover independent allocation classes, classes merged through a
common pointer, and allocation/use/free across procedure boundaries.