Alive memory model - #1455
Closed
tobiasgrosser wants to merge 6 commits into
Closed
Alive memory model#1455tobiasgrosser wants to merge 6 commits into
tobiasgrosser wants to merge 6 commits into
Conversation
tobiasgrosser
force-pushed
the
alive_memory_model
branch
9 times, most recently
from
September 19, 2026 04:18
64845fe to
359c943
Compare
A pointer into interpreter memory was a bare `UInt64`. It is now a `Pointer` in `Veir/Data/Pointer`, the object it may access and a byte offset into it, with `Pointer.null` and `Pointer.isNull`. The flat memory model has a single object, 0, whose offsets are the addresses themselves, so every access uses the offset, and pointer arithmetic keeps the object. Pointers print as object and offset. The round trips from a pointer through an integer or bytes and back no longer hold as lemmas, since they forget the object; a memory model with several objects gives them their meaning. Along the way the flat model's accessors take `mem` and `p` instead of `state` and `addr`, on one line where the signature fits, with the docstrings following the renames.
tobiasgrosser
force-pushed
the
alive_memory_model
branch
3 times, most recently
from
September 19, 2026 10:28
1c52a57 to
4b8e12d
Compare
An `alloca` computed its size as a `Nat` and truncated it to 64 bits, so a request for more than the address space silently allocated less. Its size now converts through `memorySize`, which makes a size that does not fit undefined behaviour: an `alloca` has no way to report failure, and this is what Alive2 does. `MemoryState.alloc` returns in `Interp` and fails the run when memory would pass the end of the address space, which is not the program's fault.
`store`, `load` and `loadPoison` each compared offset plus size against the size of memory. `MemoryState.checkAccess` now decides it once, on 64-bit values and without an addition, so the comparison cannot wrap, which is how Alive2 states it. An access of no bytes is allowed anywhere. `empoison` keeps its own comparison, which its proof needs. Later conditions on an access are added in this one place.
Memory is now an array of objects, each its bytes and a poison mask, and a pointer names an object and an offset into it. The flat model has a single object, 0, whose offsets are the addresses themselves, so nothing observable changes. Every access looks its object up with `getObject?`, `checkAccess` returns the object it checked, and refinement is stated per object.
A physical address converts to a pointer with `MemoryState.decode` and a pointer to its address with `MemoryState.address`. With one object both are trivial: the address is the offset. RISC-V accesses decode the register value instead of building the pointer by hand, and the pointer conversions go through the state as `ptrFromInt`, `intFromPtr`, `ptrOfByte` and `byteOfPtr`, so `Ptr.toInt`, `ofInt`, `ofByte` and `toByte` and their lemmas retire.
Memory was one flat byte array, so a pointer could walk from one allocation into its neighbour and nothing distinguished allocations. Memory is now an array of objects, one per allocation, and a pointer is an object index with a 64-bit offset. LLVM accesses are checked against their own object by `MemoryState.checkAccess`, the one place every later condition on an access is added. Every object has a base address, assigned by a bump allocator that honours the alignment its allocation declares, leaves a guard byte between objects, and starts past the low 64 KiB so that a small integer never denotes an object. A pointer converts to an integer as base plus offset, and an integer converts back by binary search over the bases, so casts and pointers stored in memory keep their meaning. RISC-V accesses decode the register value the same way and are then checked against that object like LLVM accesses, so machine code that runs past an allocation or dereferences null is undefined behaviour, as it is in Alive2's assembly mode. Memory refinement lifts from the flat array to the objects: the same number of objects, each at the same address and refined bytewise.
tobiasgrosser
force-pushed
the
alive_memory_model
branch
from
September 19, 2026 12:07
4b8e12d to
984f389
Compare
Collaborator
Author
|
This will be upstreamed step-by-step. Close this for now. |
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.
No description provided.