Concrete portable C memory/string shim dictionary. All raw reads/writes, initialization/provenance checks, race/weak/TB/sync hooks and alignment use the canonical interpreter machine. Only actual compiler type layouts and foreign ABI/dispatch policies remain inputs.

@[reducible, inline]

abbrev Miri.Interpreter.MemoryShimMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.MemoryShimMachine.State = Miri.Interpreter.PointerMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.MemoryShimMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.MemoryShimMachine.M = Miri.Interpreter.PointerMachine.M

structure Miri.Interpreter.MemoryShimMachine.Hooks (K U C E : Type) : Type

• access : PlaceMachine.AccessConfig K (PointerMachine.User U)
• pointer : PointerMachine.Hooks K U
• place : PlaceHooks Memory.Provenance (State K U) C E
• i32Layout : C → M K U LocalLayout
• usizeLayout : C → M K U LocalLayout
• wcharLayout : C → M K U LocalLayout
• symbolicAlignment : Bool
• enforceAlignment : Bool

def Miri.Interpreter.MemoryShimMachine.writeI32 {K U C E : Type} (h : Hooks K U C E) (choice : C) (value : Int32) (dest : RuntimePlace Memory.Provenance) : M K U Unit

Equations

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

def Miri.Interpreter.MemoryShimMachine.writeUsize {K U C E : Type} (h : Hooks K U C E) (choice : C) (value : UInt64) (dest : RuntimePlace Memory.Provenance) : M K U Unit

Equations

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

def Miri.Interpreter.MemoryShimMachine.bind {K U C E D B I : Type} [DecidableEq K] (h : Hooks K U C E) (choice : C) (base : MemoryShims.Hooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I) : MemoryShims.Hooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I

Source read_c_str in MemoryShims scans with readByte and then performs a second readBytes. Both passes reach real allocation accesses through this binding; no cached string length suppresses the second read or its hooks.

Equations

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

def Miri.Interpreter.MemoryShimMachine.core {K U C E D B I : Type} [DecidableEq K] (h : Hooks K U C E) (choice : C) (foreign : ForeignItems.Core Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : MemoryShims.CoreHooks Memory.Provenance (State K U) D (RuntimePlace Memory.Provenance) B I

Production construction from source primitives. No whole foreign baseline or fallback interpreter is requested or captured.

Equations

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