Dynamic memory layout on the actual machine state. Canonical type identity survives the memory view; symbolic vtable reads need no invented stack or placeholder full vtable dictionary. Every failing dynamic query retains its StepError through AccessState.pendingError, including UB classifications.

@[reducible, inline]

abbrev Miri.Input.EvalDynamicMemory.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalDynamicMemory.User = Miri.Input.EvalProjectionMachine.User

@[reducible, inline]

abbrev Miri.Input.EvalDynamicMemory.Machine (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalDynamicMemory.Machine Os R P H D O Aff B Host = Miri.Interpreter.PlaceMachine.Machine Miri.Memory.MiriMemoryKind (Miri.Input.EvalDynamicMemory.User Os R P H D O Aff B Host)

def Miri.Input.EvalDynamicMemory.arrays {Os R P H D O Aff B Host : Type} : RuntimeArrayQueries.Access (Machine Os R P H D O Aff B Host)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalDynamicMemory.vtables {Os R P H D O Aff B Host : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) : Interpreter.VTableReadHooks Memory.Provenance (Machine Os R P H D O Aff B Host) Unit

Only source symbolic read operations: resolve identity, look up the actual registry/imported vtable, compare normalized predicates and query its layout.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalDynamicMemory.dynamic {Os R P H D O Aff B Host : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (maximum : ABI.Size) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) : Interpreter.DynamicLayoutHooks Memory.Provenance (Machine Os R P H D O Aff B Host) Unit

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.EvalDynamicMemory.resolver {Os R P H D O Aff B Host : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (maximum : ABI.Size) (fuel : Nat) (pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Interpreter.ValidityMachine.Control (Interpreter.ThreadStacks.Storage (EvalWorld.World Os R P H D O Aff B Host)))) : Interpreter.DynamicLayoutResolver Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind (Interpreter.PlaceMachine.AccessState Memory.MiriMemoryKind (User Os R P H D O Aff B Host))

The source operation runs on the real machine carried by the memory context. No layout-equality search or synthetic interpreter frame is used.

Equations

• One or more equations did not get rendered due to their size.