Alive memory model - #1455

Draft

tobiasgrosser wants to merge 14 commits into

mainfrom

alive_memory_model

Commits on Sep 14, 2026

feat(interpreter): poison pointers
tobiasgrosser
committed
44d9650
Update Veir/Data/LLVM/Ptr.lean

tobiasgrosser
and
luigirinaldi
authored
82d067a
Update Veir/Data/LLVM/Ptr.lean

tobiasgrosser
and
luigirinaldi
authored
c5dbac7
Update Veir/Data/LLVM/Ptr.lean

tobiasgrosser
and
luigirinaldi
authored
5be7b81
Add a comment about freeze
tobiasgrosser
committed
25ecfe2
test: differential harness for the memory model against Alive2
tobiasgrosser
committed
6838e32
feat(interpreter): give memory blocks with a physical address space
tobiasgrosser
committed
56cceac
feat(interpreter): check alignment on LLVM accesses
tobiasgrosser
committed
8d45947
feat(interpreter): pointer bytes in memory
tobiasgrosser
committed
fe7c25e
feat(interpreter): object metadata and stack lifetime
tobiasgrosser
committed
c0b23c6
feat(interpreter): the heap allocation family
tobiasgrosser
committed
cb9e6bd
feat(interpreter): globals and llvm.mlir.addressof
tobiasgrosser
committed
3344ec7
feat(interpreter): escaped objects, unknown calls and argument attributes
tobiasgrosser
committed
b844a5e
feat(interpreter): Alive2-style refinement of function results
tobiasgrosser
committed
892706f