Concrete unix/mem.rs allocation/access bindings. Global addresses, allocation extras, provenance and errno use canonical machine state. Exact libc ABI/constants, imported type layouts, host errors and page configuration remain required facts, never host-platform guesses.

@[reducible, inline]

abbrev Miri.Interpreter.UnixMemoryMachine.State (U : Type) : Type

Equations

• Miri.Interpreter.UnixMemoryMachine.State U = Miri.Interpreter.PointerMachine.State Miri.Memory.MiriMemoryKind U

@[reducible, inline]

abbrev Miri.Interpreter.UnixMemoryMachine.M (U A : Type) : Type

Equations

• Miri.Interpreter.UnixMemoryMachine.M U A = Miri.Interpreter.PointerMachine.M Miri.Memory.MiriMemoryKind U A

structure Miri.Interpreter.UnixMemoryMachine.Hooks (U C Host Payload : Type) : Type

• allocation : ReallocationDriver.Hooks Memory.MiriMemoryKind U Payload
• compiler : PlaceMachine.CompilerHooks Memory.MiriMemoryKind (PointerMachine.User U) C
• frame : FrameMetadata.CompilerHooks Memory.MiriMemoryKind (PointerMachine.User U)
• errors : IoError.Hooks (State U) Host
• errnoPlaces : U → Array (Memory.AllocId × MPlaceTy Memory.Provenance)

  Typed backing for ThreadRecord.lastErrorLocation's canonical AllocId token.

• putErrnoPlaces : U → Array (Memory.AllocId × MPlaceTy Memory.Provenance) → U
• u32Layout : LocalLayout
• unitPtrMut : LocalLayout
• pageSize : UInt64
• symbolicAlignment : Bool
• enforceAlignment : Bool

structure Miri.Interpreter.UnixMemoryMachine.Choices : Type

• allocation : Memory.AllocAddresses.AddressRandomChoices
• reuse : Bool

def Miri.Interpreter.UnixMemoryMachine.driver {U C Host Payload : Type} (h : Hooks U C Host Payload) : AllocationDriver.Hooks Memory.MiriMemoryKind U Payload

Reuse-pool source distinguishes Stack from every other MemoryKind.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.access {U C Host Payload : Type} (h : Hooks U C Host Payload) : PlaceMachine.AccessConfig Memory.MiriMemoryKind (PointerMachine.User U)

Physical accesses share the same actual extras installed by allocation.

Equations

• Miri.Interpreter.UnixMemoryMachine.access h = Miri.Interpreter.MemoryExtras.bindAccess h.allocation.driver.allocation.extras h.allocation.access

def Miri.Interpreter.UnixMemoryMachine.allocationForKind {U C Host Payload : Type} (h : Hooks U C Host Payload) (allocationKind : Memory.MiriMemoryKind) : M U (ReallocationDriver.Hooks Memory.MiriMemoryKind U Payload)

Source init_allocation records spans after tree/race/weak initialization only for kinds which request them. The original stack remains valid throughout these machine-only initialization hooks; post-hook machine state is preserved.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.writeScalar {U C Host Payload : Type} (h : Hooks U C Host Payload) (choice : C) (value : Memory.Scalar Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M U Unit

Equations

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

def Miri.Interpreter.UnixMemoryMachine.readScalar {U C Host Payload : Type} (h : Hooks U C Host Payload) (place : MPlaceTy Memory.Provenance) : M U (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.UnixMemoryMachine.misalignment {U C Host Payload : Type} (h : Hooks U C Host Payload) (pointer : Memory.Pointer (Option Memory.Provenance)) (required : ABI.Align) : M U (Option Memory.Misalignment)

Canonical shared symbolic-alignment promises, with a cached error instead of immediate UB, exactly as ptr_to_mplace. No output memory is read here.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.derefPointerOutput {U C Host Payload : Type} (h : Hooks U C Host Payload) (operand : OpTy Memory.Provenance) : M U (MPlaceTy Memory.Provenance)

Equations

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

def Miri.Interpreter.UnixMemoryMachine.checkAccess {U C Host Payload : Type} (h : Hooks U C Host Payload) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : UInt64) : M U (Except Unit Unit)

mprotect/madvise only check bounds, not memory-read/TB/race access. Real access failures are returned for source remapping; unavailable metadata throws.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.errnoRootPlaces {U C Host Payload : Type} (h : Hooks U C Host Payload) (state : State U) : Except StepError (Array (MPlaceTy Memory.Provenance))

Source Thread::visit_provenance visits last_error, including retained terminated threads. Only actual thread tokens are roots; stale table entries are not promoted to roots. The caller can feed these places to its GC visitor.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.errorHooks {U C Host Payload : Type} (h : Hooks U C Host Payload) (choice : C) (choices : Choices) : IoError.Hooks (State U) Host

Actual per-thread errno storage, allocated lazily with Machine ownership. The side table retains the original full u32 layout and pointer provenance.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.foreign {U C Host Payload D B I : Type} (h : Hooks U C Host Payload) (choice : C) (choices : Choices) (base : ForeignItems.Hooks Memory.Provenance (State U) D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : ForeignItems.Hooks Memory.Provenance (State U) D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

Concrete foreign allocation operations, preserving the source memory kind and actual align/old-layout values. All random choices remain explicit inputs.

Equations

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

def Miri.Interpreter.UnixMemoryMachine.bind {U C Host Payload D B I : Type} (h : Hooks U C Host Payload) (choice : C) (choices : Choices) (base : UnixMemory.Hooks Memory.Provenance (State U) D (MPlaceTy Memory.Provenance) B I) : M U (UnixMemory.Hooks Memory.Provenance (State U) D (MPlaceTy Memory.Provenance) B I)

Exact ABI/off_t and libc constants stay compiler queries. Pointer-output places and offset values are obtained from actual operand reads.

Equations

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