Alive memory model - #1455
Draft
tobiasgrosser wants to merge 14 commits into
Draft
Alive memory model#1455tobiasgrosser wants to merge 14 commits into
tobiasgrosser wants to merge 14 commits into
Conversation
Every other runtime value could be poison; a pointer could not, so the places that should have produced one returned an address of 0 instead. The pointer load even said so in a FIXME. An address of 0 is a value rather than a bottom element, so the substitute was observable. `Data.LLVM.Ptr` now wraps the address the way `Data.LLVM.Int` wraps its bit vector, and `RuntimeValue.addr` carries it. The memory interface stays indexed by a concrete address, because using a poison pointer for an access is undefined behaviour and that is decided by the operation before memory is reached. A pointer is poison when it is loaded from bytes with any poison in them, when it is bitcast from poisoned bits, or when it is offset from a poison pointer or by a poison index. Storing one writes eight poison bytes, which read back as poison both as a pointer and as an integer. Loading or storing through one, or casting one into a RISC-V register, is undefined behaviour: a register is a plain bit pattern with no poison to carry, which is the same reason Alive2's assembly mode drops poison entirely. `freeze` turns one into null. Refinement follows `Int`: poison is refined by every pointer, and a pointer only by itself.
Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>
Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>
Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>
The interpreter's memory model is about to change substantially. This adds the tool that checks it against a reference which already encodes LLVM's rules for provenance, liveness, alignment and poison: random memory-using programs are run under both `veir-interpret` and Alive2's `alive-exec`, and the cases where they disagree are reported. `Tools/memfuzz_generate.py` builds each program once and prints it twice, as generic LLVM-dialect MLIR and as LLVM IR, so a difference in the two answers is a difference in semantics rather than in a translator. Its defaults track what the interpreter models, which today is `alloca`, `getelementptr` and in-bounds integer loads and stores; everything past that is behind an option, and each later change to the model turns on the one it makes correct. Work is split by seed rather than by distributing programs: case `n` of a run is generated from the run identifier and `n` alone, so shard `i` of a hundred covers a block no other shard touches and any case is reproducible anywhere from its index. `farm` starts the shards over ssh, through a SLURM array, or across local cores, and `collect` merges the reports and ranks what turned up. Verdicts separate real findings from the reference being imprecise: a defined VeIR result that agrees bit for bit with an Alive2 poison is a refinement, not a bug. `Test/Tools/memfuzz_smoke.mlir` exercises the half that does not need alive-exec, so a generator that drifts from the interpreter is caught by the ordinary test suite.
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.
Loads and stores now honour their `alignment` attribute: the physical address of the access must be a multiple of it, else the access is undefined behaviour. Without the attribute the natural alignment of the accessed type, its size, applies, as LLVM does for accesses that carry no explicit alignment. RISC-V accesses stay unaligned, as the hardware allows. The condition lives in `MemoryState.checkAccess` beside the bounds check, and like it does not apply to an access of no bytes. With both conditions an access can break in place, the harness turns on deliberately undefined accesses, out-of-bounds offsets and misaligned accesses together, aiming them at any object whose provenance it knows.
A byte of memory is now either a value byte with its poison bits or one of the eight fragments of a stored pointer. Storing a pointer writes its fragments, and loading a pointer type yields the stored pointer when all eight fragments are present in order, the pointer at the stored address when the bytes are defined values, and a poison pointer otherwise, which includes a run of fragments that was partly overwritten. Integer loads over fragments read the pointer's physical address, so pointers leak into integers through memory as in LLVM. RISC-V stores write value bytes and RISC-V loads read addresses through fragments. The `ptrtoint` and `inttoptr` ops convert through the address space, with poison mapping to poison in both directions, and `llvm.intr.memcpy`, `memmove` and `memset` are interpreted. Copies move bytes verbatim, so provenance survives, and `memcpy` requires its two ranges to be equal or disjoint, which is the only thing separating it from `memmove`. `memset` writes value bytes. Memory refinement is defined per byte: value bytes refine as before, a fully poison value byte is refined by anything, and a fragment only by the same fragment. Objects must agree in address and size. The harness gains the pointer-value and memory-intrinsic knobs this makes correct, and takes address differences only from pointers whose provenance it knows: from a poison pointer the difference is poison in VeIR and zero in Alive2, which is a question about poison rather than about memory.
An object now records how it was allocated, the alignment it was given, whether it is still alive and whether it may be written. Two conditions join the access check that every load and store already goes through: an access of at least one byte must reach an object that is alive, and a write must not target a constant object. An access of no bytes stays allowed anywhere, even through a dangling pointer, as in Alive2. Stack objects die at `llvm.intr.lifetime.end` and when the function that allocated them returns; `llvm.intr.lifetime.start` revives one with poison contents. Both marks name a whole object, so applying one to anything but the start of a stack object is undefined behaviour. The remaining kinds, heap and global, have no allocations yet; they arrive with the operations that create them.
`llvm.call` now models the C and C++ allocation functions by name: `malloc`, `calloc`, which zeroes, `realloc`, which copies and then frees, `free`, and `operator new` and `delete` by their mangled names. Each allocation is a fresh object, so pointers from different calls never alias, and a freed object dies but keeps its address, which is never reused, so a use after free is caught rather than landing in whatever was allocated next. Freeing anything but a live heap object at its start is undefined behaviour, which covers double frees and freeing an `alloca`. Whether an allocation fails is the model's first nondeterministic choice, so it is drawn from an oracle carried in the memory state, indexed by how many allocations came before. The default oracle never fails, and two programs being compared are run against the same one. A copy of no bytes now reaches no memory before its pointers are inspected, matching the rule the access check already applies, so a zero-length `memcpy` or `memset` is allowed through any pointer.
`veir-interpret` now materializes the module's globals as objects before `main` runs. A global with a `value` attribute starts with its bytes, integers little-endian and strings verbatim; one with an initializer region starts with the value that region returns; anything else starts as poison. A `constant` global becomes read-only once its initializer has been stored, so writing to it is undefined behaviour. Functions get empty objects of their own, so their addresses are distinct from each other and from every allocation. `llvm.mlir.addressof` looks a symbol up in the map from names to objects that this builds, and yields a pointer to the start of one.
…utes An object records whether its address escaped: stored to memory, converted to an integer or to register bits, passed to a call, or returned from a function. Globals are escaped from the start. Only escaped objects can be reached by code the interpreter does not see. A call to any function that is not one of the modelled allocation functions is an unknown call, which the interpreter cannot enter. It escapes its pointer arguments, then havocs every live, writable, escaped object, replacing its bytes with what the oracle chooses, and returns the oracle's value for each result, poison by default. Objects that never escaped keep their contents across the call. Argument attributes become undefined-behaviour conditions: `llvm.nonnull` forbids null, `llvm.dereferenceable = n` demands `n` readable bytes at the pointer, and `llvm.align = n` demands an address that is a multiple of `n`. They are checked at every `llvm.call` and on entry to an `llvm.func`, and a poison pointer satisfies none of them.
`FunctionResult.isRefinedBy` no longer demands equal final memories. It is now relative to the memory the function started with and follows Alive2: a renaming sends the target's objects to the source's, is the identity on the objects that existed before the call, and sends objects the target allocated to objects the source allocated. Every source object the caller can observe, meaning it existed before the call or its address escaped, must be refined by the target object the renaming sends to it, with the same size and liveness, an escape matched by an escape, and bytes refined pointwise where pointer fragments are related through the renaming. Returned values refine under the renaming too, with a poison pointer refined by any pointer. Objects the source allocated but never leaked are unconstrained, so a transformation may drop an allocation. Reflexivity and transitivity are proved, the latter by composing the two renamings, and `isRefinedByAsFunction` uses the new relation. A bridge lemma shows that equal final memories with refining results still refine, which is what proofs built on the state-level relation provide. That relation and the monotonicity axiom keep memory equality, since a single-operation rewrite does not change the memory.
tobiasgrosser
force-pushed
the
alive_memory_model
branch
from
September 14, 2026 20:17
bf2cea4 to
892706f
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.
No description provided.