Entire pinned unix/mem.rs plus posix_memalign/aligned_alloc/reallocarray source policy. Miri's deliberately restricted mmap is preserved: unsupported mapping modes are not replaced with successful anonymous allocations.

@[reducible, inline]

abbrev Miri.Interpreter.UnixMemory.M (σ α : Type) : Type

Equations

• Miri.Interpreter.UnixMemory.M = EStateM Miri.Interpreter.StepError

structure Miri.Interpreter.UnixMemory.Hooks (P S D MD B I : Type) : Type

• foreign : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I
• pointerSize : UInt64
• pageSize : UInt64
• targetIsizeMax : UInt64
• frameInStd : M S Bool
• libcI32 : String → M S Int32
• setErrno : String → M S Unit
• mapFailed : M S (Memory.Scalar P)
• writeScalar : Memory.Scalar P → MD → M S Unit
• writeI32 : Int32 → MD → M S Unit
• derefPointerOutput : OpTy P → M S MD

  Actual deref_pointer_as(memptr, machine.layouts.unit_ptr_mut).

• expectedAbi : String → M S (ABI.FnAbi MIR.TyId)

  Compiler-generated exact libc off_t signature/query; no host type alias.

• readOffset : OpTy P → M S Int
• checkAccess : Memory.Pointer (Option P) → UInt64 → M S (Except Unit Unit)

  A returned error is an actual source pointer-access failure. Missing metadata/environment must throw an explicit unresolved operation instead.

def Miri.Interpreter.UnixMemory.mmap {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (offset : Int) (dest : MD) : M S Unit

Offset is read by the foreign dispatcher BEFORE any other mmap argument.

Equations

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

def Miri.Interpreter.UnixMemory.munmap {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.UnixMemory.mprotect {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.UnixMemory.madvise {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.UnixMemory.posixMemalign {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (dest : MD) : M S Unit

POSIX invalid alignment returns EINVAL without setting errno. Dereference of the pointer-output operand precedes scalar alignment/size reads.

Equations

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

def Miri.Interpreter.UnixMemory.alignedAlloc {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.UnixMemory.reallocarray {P S D MD B I : Type} (h : Hooks P S D MD B I) (args : Array (OpTy P)) (dest : MD) : M S Unit

Equations

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

def Miri.Interpreter.UnixMemory.emulate {P S D MD B I : Type} (h : Hooks P S D MD B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S (Option ForeignItems.EmulateItemResult)

The Unix foreign-item wrapper controls arity/type checks and off_t reading. Availability checks occur before the signature query where source does so.

Equations

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

def Miri.Interpreter.UnixMemory.bindUnix {P S D MD B I : Type} (h : Hooks P S D MD B I) : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I

Equations

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