Draft
Conversation
Stevengre
force-pushed
the
jh/pointer2int
branch
2 times, most recently
from
70da3cb to
fcab480
Compare
jberthold
reviewed
Nov 11, 2025
|
|
||
| ```k | ||
| // `prove-rs/interior-mut3.rs` needs this | ||
| // TODO: check its correctness, I assume the pointer offset is the address here and we can use it to recover the PtrLocal |
Member
There was a problem hiding this comment.
Unfortunately this is not correct. The PTR_OFFSET here is an index into an array of elements of a certain type T. To get what would be an address in a byte-addressed memory you have to multiply it with the size of one element in bytes. sizeof<T>.
This becomes interesting for the alignment check when pointers are cast from one element type to another.
Contributor
Author
There was a problem hiding this comment.
The PTR_OFFSET is a local OFFSET for the structure?
Stevengre
force-pushed
the
jh/pointer2int
branch
3 times, most recently
from
1642b91 to
9a0cbd1
Compare
Stevengre
force-pushed
the
jh/pointer2int
branch
from
9a0cbd1 to
27434bd
Compare
Add a `#cast` rule for `castKindTransmute` that handles `PtrLocal` to integer type conversion. The rule extracts the pointer offset from metadata and converts it to the target integer type via `#intAsType`. A helper function `#ptrOffsetBytes` computes byte offsets from pointer offsets, accounting for array element sizes when the pointee is an unsized array type. This fixes the `interior-mut3` test which uses `UnsafeCell::get()` (internally transmutes a pointer to `usize` for alignment checks). The proof now passes cleanly in 333 steps instead of getting stuck on unresolved alignment assertions. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Stevengre
force-pushed
the
jh/pointer2int
branch
from
236c269 to
bbee7f9
Compare
9 tasks
Stevengre
added a commit
that referenced
this pull request
Mar 26, 2026
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>
4 tasks
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
2 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.
No description provided.