Pinned unix/windows foreign_items.rs std-only dispatch arms. These are source stubs, enabled by the actual frame predicate, never general FFI defaults.

@[reducible, inline]

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

Equations

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

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

• foreign : ForeignItems.Core P S D MD (Memory.Pointer (Option P)) B I

  Only the nonrecursive source core is needed by std-only arms. Keeping the full foreign dispatcher out of this record prevents a std-only constructor from accepting or capturing an arbitrary platform chain.

• frameInStd : M S Bool
• targetEnv : String
• pageSize : UInt64
• stackAddress : UInt64
• stackSize : UInt64
• layout : String → M S LocalLayout

  Exact source compiler layout: usize, unit_ptr_mut or named libc type.

• dereference : OpTy P → LocalLayout → M S MD
• pointerOf : MD → Memory.Pointer (Option P)
• writeUnsigned : UInt64 → MD → M S Unit
• writeUninit : MD → M S Unit
• projectNamed : MD → String → M S MD
• readU32 : OpTy P → M S UInt32
• checkNoIsolation : String → M S Unit
• homeDirectory : M S String
• writePath : String → Memory.Pointer (Option P) → UInt64 → M S Bool
• libcValue : String → M S (Memory.Scalar P)
• windowsValue : String → M S (Memory.Scalar P)
• writeScalar : Memory.Scalar P → MD → M S Unit
• allocateStringDedup : String → M S (Memory.Pointer (Option P))
• windowsAbi : String → M S (ABI.FnAbi MIR.TyId)

  Exact compiler shim_sig!(extern system ...) ABI for the named source arm.

• yieldActiveThread : M S Unit
• setLastError : String → M S Unit

def Miri.Interpreter.StdOnlyShims.unix {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 ForeignItems.EmulateItemResult

Equations

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

structure Miri.Interpreter.StdOnlyShims.WindowsHooks (P S D MD B I : Type) : Type

Windows uses no Unix path, layout or passwd operations. Keep its source construction independent of those capabilities.

• foreign : ForeignItems.Core P S D MD (Memory.Pointer (Option P)) B I
• frameInStd : M S Bool
• windowsAbi : String → M S (ABI.FnAbi MIR.TyId)
• windowsValue : String → M S (Memory.Scalar P)
• writeScalar : Memory.Scalar P → MD → M S Unit
• writeUnsigned : UInt64 → MD → M S Unit
• yieldActiveThread : M S Unit
• setLastError : String → M S Unit

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

Equations

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

def Miri.Interpreter.StdOnlyShims.windows {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 ForeignItems.EmulateItemResult

Equations

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

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

Recognized but unavailable std arms fall through to the existing platform handler, matching source guards rather than claiming a successful stub.

Equations

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

def Miri.Interpreter.StdOnlyShims.machine {K User D MD B I : Type} (compiler : FrameMetadata.CompilerHooks K User) (base : Hooks Memory.Provenance (MachineHooks.State K User) D MD B I) : Hooks Memory.Provenance (MachineHooks.State K User) D MD B I

Equations

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