feat(interpreter): give memory blocks with a physical address space - #1454
Closed
tobiasgrosser wants to merge 1 commit into
Closed
tobiasgrosser wants to merge 1 commit into
tobiasgrosser wants to merge 1 commit into
Conversation
tobiasgrosser
force-pushed
the
tobias/memory_model_blocks
branch
2 times, most recently
from
September 17, 2026 05:23
1d1a673 to
58218c3
Compare
tobiasgrosser
marked this pull request as draft
September 17, 2026 05:23
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. Loads and stores are checked against their own object by `MemoryState.checkAccess`, which is 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 a 64 KiB arena that machine code may address directly. A pointer converts to an integer as base plus offset, and an integer converts back by binary search over the bases, so bitcasts, unrealized casts to registers and pointers stored in memory keep their meaning. RISC-V accesses decode the register value the same way and grow the object they land in up to the next object's base, which keeps machine code that addresses memory freely working. Memory refinement lifts from the flat array to the objects: the same number of objects, each at the same address and refined bytewise. The fuzzing harness gains the null-dereference knob this makes correct. Deliberately undefined accesses stay off until the next change adds alignment, since before it the two tools would disagree on misaligned accesses for a reason unrelated to bounds.
tobiasgrosser
force-pushed
the
tobias/memory_model_blocks
branch
from
September 17, 2026 05:46
58218c3 to
9d71151
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.
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. Loads and stores are checked against their own object by
MemoryState.checkAccess, the one place where every later condition on an access is added, so leaving the object is UB.Every object has a base address assigned by a bump allocator that honours the allocation's declared alignment, leaves a guard byte between objects, and starts past a 64 KiB arena that machine code may address directly. A pointer converts to an integer as base plus offset, and an integer converts back by binary search over the bases, so bitcasts, unrealized casts to registers and pointers stored in memory keep their meaning. RISC-V accesses decode the register value the same way and grow the object they land in up to the next object's base, which keeps machine code that addresses memory freely working.
Memory refinement lifts from the flat array to the objects: the same number of objects, each at the same address and refined bytewise.