feat(rt): add address allocation model for pointer-to-integer semantics#1003
Draft
feat(rt): add address allocation model for pointer-to-integer semantics#1003
Conversation
Implements Miri-style lazy address allocation (Issue #1002): Configuration: - `<addressMap>`: maps allocation keys to (base_address, size) pairs - `<nextAddress>`: next available address (starts at 4096 to avoid NULL) - `<exposedSet>`: tracks allocations with exposed provenance Semantics: - `#allocAddressFor`: lazily assigns aligned base addresses on demand - `#alignUp`: aligns addresses to type alignment requirements - `castKindTransmute` PtrLocal→int: computes base + byte_offset - `castKindPointerExposeAddress`: same as transmute but also exposes provenance Verified via LLVM backend execution: - interior-mut3-fail.rs reaches #EndProgram (alignment check passes with addr=4096) - Address uniqueness: different locals get different base addresses Note: Haskell backend (prove) performance regresses due to 3 new configuration cells increasing the matching state space. This needs further optimization (e.g. cell multiplicity annotations or rule priorities). Closes #1002 Supersedes #812, #877 Fixes #638 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.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
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.
Summary
Implements Miri-style lazy address allocation for pointer-to-integer casts (Issue #1002).
<addressMap>,<nextAddress>,<exposedSet>configuration cellscastKindTransmutePtrLocal→int andcastKindPointerExposeAddressVerification
LLVM backend execution confirms correctness:
interior-mut3-fail.rs: reaches#EndProgramwithaddr=4096, alignment check passesallocKey(0, local(1)) |-> addrEntry(4096, 0)Known issue
Haskell backend (symbolic prove) performance regresses — 3 new configuration cells increase matching state space. Needs optimization before the prove tests can run in reasonable time.
Related
Test plan
make buildpassesinterior-mut3-fail.rsexecutes to#EndProgram🤖 Generated with Claude Code