Source Miri-specific portable extern arms, foreign_items.rs324-610. Diagnostics are omitted only after all argument reads/checks; operations that can affect memory, provenance or control flow remain explicit. Backtrace APIs and host-path conversion require their actual source implementation.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.MiriShims.Operations (P S D MD B I HostPath : Type) : Type

• readU64 : OpTy P → M S UInt64
• readU8 : OpTy P → M S UInt8
• readBool : OpTy P → M S Bool
• readImmediate : OpTy P → M S (RvalueImmTy P)
• readByteSlice : RvalueImmTy P → M S ByteArray
• writeU64 : UInt64 → MD → M S Unit
• writeUsize : UInt64 → MD → M S Unit
• writeBool : Bool → MD → M S Unit
• allocation : Memory.Pointer (Option P) → M S (Except StepError (Memory.AllocId × ABI.Size))

  Source ptr_get_alloc_id(ptr,0); errors remain values so selected Miri APIs can apply their source Abort conversion while preserving prior effects.

• sourceAllocIdNumber : Memory.AllocId → M S UInt64

  Authoritative numeric rustc AllocId.0.get() for this resolved source allocation. This must come from the same source identity domain; the interpreter's internal/import allocation number is not a substitute.

• allocationInfo : Memory.AllocId → M S (ABI.Size × ABI.Align × Memory.AllocationKind)
• localCAllocation : Memory.AllocId → M S Bool
• trackAllocation : Memory.AllocId → M S Bool
• staticRoot : Memory.AllocId → M S Unit
• startUnwind : OpTy P → M S Unit
• provenanceGc : M S Unit
• namePointer : Memory.Pointer (Option P) → UInt8 → ByteArray → M S Unit

  TB debug naming can reject the requested ancestry; preserve that check.

• printBorrowState : UInt64 → Bool → M S Unit

  The source ABI supplies rustc's raw AllocId number. It must remain raw until the source-image witness resolves its identity domain.

• checkNoIsolation : String → M S Unit
• readHostPath : Memory.Pointer (Option P) → M S HostPath
• writeTargetPath : HostPath → Memory.Pointer (Option P) → UInt64 → M S (Bool × UInt64)
• spawnThread : MD → Memory.Pointer (Option P) → RvalueImmTy P → M S Unit
• threadFromUsize : UInt64 → M S (Option Concurrency.ThreadId)

  Invalid IDs are None; terminated but existing threads are Some.

• joinExclusive : Concurrency.ThreadId → Bool → MD → M S Unit
• yieldThread : M S Unit
• writeHost : Bool → ByteArray → M S Unit

  Host stdout/stderr write errors are ignored by Miri, but missing host semantics is not an I/O error that may be silently ignored.

• symbolicPromise : Memory.Pointer (Option P) → ABI.Align → M S Unit

structure Miri.Interpreter.MiriShims.CoreHooks (P S D MD B I HostPath : Type) extends Miri.Interpreter.MiriShims.Operations P S D MD B I HostPath : Type

• readU64 : OpTy P → M S UInt64
• readU8 : OpTy P → M S UInt8
• readBool : OpTy P → M S Bool
• readImmediate : OpTy P → M S (RvalueImmTy P)
• readByteSlice : RvalueImmTy P → M S ByteArray
• writeU64 : UInt64 → MD → M S Unit
• writeUsize : UInt64 → MD → M S Unit
• writeBool : Bool → MD → M S Unit
• allocation : Memory.Pointer (Option P) → M S (Except StepError (Memory.AllocId × ABI.Size))
• sourceAllocIdNumber : Memory.AllocId → M S UInt64
• allocationInfo : Memory.AllocId → M S (ABI.Size × ABI.Align × Memory.AllocationKind)
• localCAllocation : Memory.AllocId → M S Bool
• trackAllocation : Memory.AllocId → M S Bool
• staticRoot : Memory.AllocId → M S Unit
• startUnwind : OpTy P → M S Unit
• provenanceGc : M S Unit
• namePointer : Memory.Pointer (Option P) → UInt8 → ByteArray → M S Unit
• printBorrowState : UInt64 → Bool → M S Unit
• checkNoIsolation : String → M S Unit
• readHostPath : Memory.Pointer (Option P) → M S HostPath
• writeTargetPath : HostPath → Memory.Pointer (Option P) → UInt64 → M S (Bool × UInt64)
• spawnThread : MD → Memory.Pointer (Option P) → RvalueImmTy P → M S Unit
• threadFromUsize : UInt64 → M S (Option Concurrency.ThreadId)
• joinExclusive : Concurrency.ThreadId → Bool → MD → M S Unit
• yieldThread : M S Unit
• writeHost : Bool → ByteArray → M S Unit
• symbolicPromise : Memory.Pointer (Option P) → ABI.Align → M S Unit
• foreign : ForeignItems.Core P S D MD (Memory.Pointer (Option P)) B I

structure Miri.Interpreter.MiriShims.Hooks (P S D MD B I HostPath : Type) extends Miri.Interpreter.MiriShims.Operations P S D MD B I HostPath : Type

• readU64 : OpTy P → M S UInt64
• readU8 : OpTy P → M S UInt8
• readBool : OpTy P → M S Bool
• readImmediate : OpTy P → M S (RvalueImmTy P)
• readByteSlice : RvalueImmTy P → M S ByteArray
• writeU64 : UInt64 → MD → M S Unit
• writeUsize : UInt64 → MD → M S Unit
• writeBool : Bool → MD → M S Unit
• allocation : Memory.Pointer (Option P) → M S (Except StepError (Memory.AllocId × ABI.Size))
• sourceAllocIdNumber : Memory.AllocId → M S UInt64
• allocationInfo : Memory.AllocId → M S (ABI.Size × ABI.Align × Memory.AllocationKind)
• localCAllocation : Memory.AllocId → M S Bool
• trackAllocation : Memory.AllocId → M S Bool
• staticRoot : Memory.AllocId → M S Unit
• startUnwind : OpTy P → M S Unit
• provenanceGc : M S Unit
• namePointer : Memory.Pointer (Option P) → UInt8 → ByteArray → M S Unit
• printBorrowState : UInt64 → Bool → M S Unit
• checkNoIsolation : String → M S Unit
• readHostPath : Memory.Pointer (Option P) → M S HostPath
• writeTargetPath : HostPath → Memory.Pointer (Option P) → UInt64 → M S (Bool × UInt64)
• spawnThread : MD → Memory.Pointer (Option P) → RvalueImmTy P → M S Unit
• threadFromUsize : UInt64 → M S (Option Concurrency.ThreadId)
• joinExclusive : Concurrency.ThreadId → Bool → MD → M S Unit
• yieldThread : M S Unit
• writeHost : Bool → ByteArray → M S Unit
• symbolicPromise : Memory.Pointer (Option P) → ABI.Align → M S Unit
• foreign : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I

def Miri.Interpreter.MiriShims.Hooks.core {P S D MD B I HostPath : Type} (h : Hooks P S D MD B I HostPath) : CoreHooks P S D MD B I HostPath

Equations

• h.core = { toOperations := h.toOperations, foreign := h.foreign.toCore }

@[instance_reducible]

instance Miri.Interpreter.MiriShims.instCoeOutHooksCoreHooks {P S D MD B I HostPath : Type} : CoeOut (Hooks P S D MD B I HostPath) (CoreHooks P S D MD B I HostPath)

Equations

• Miri.Interpreter.MiriShims.instCoeOutHooksCoreHooks = { coe := Miri.Interpreter.MiriShims.Hooks.core }

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

Equations

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

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

Equations

• Miri.Interpreter.MiriShims.emulate h name abi args dest = Miri.Interpreter.MiriShims.Source.emulate h.core name abi args dest

def Miri.Interpreter.MiriShims.bind {P S D MD B I HostPath : Type} (h : Hooks P S D MD B I HostPath) : 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.