One Windows platform foreign-item chain. All handlers execute on the same S; direct dispatch avoids captured older platform fallback chains.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.WindowsForeign.Hooks (S Place F H D Os HM T E Kind R Host System TZ Timestamp B I : Type) : Type

• environment : WindowsEnvironmentDispatch.Hooks S Os E Kind
• files : WindowsFileDispatch.Hooks S F H D Os HM T E Kind
• thread : WindowsThreadDispatch.Hooks S F
• time : TimeShimDispatch.Hooks S Host System TZ Timestamp
• sync : WindowsSyncDispatch.Hooks S R
• random : WindowsRandomDispatch.Hooks S Place B I
• platform : WindowsPlatformDispatch.Hooks S Os E Kind F
• stdOnly : StdOnlyShims.WindowsHooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) B I

def Miri.Interpreter.WindowsForeign.dispatch {Os S Place F H D HM T E Kind R Host System TZ Timestamp B I : Type} [DecidableEq Os] (h : Hooks S Place F H D Os HM T E Kind R Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S ForeignItems.EmulateItemResult

Inventory-specific direct dispatch. Each nonmatching handler returns before operand reads/ABI queries, and each matching handler's actual errors propagate.

Equations

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

def Miri.Interpreter.WindowsForeign.bind {Os S Place F H D HM T E Kind R Host System TZ Timestamp B I : Type} [DecidableEq Os] (h : Hooks S Place F H D Os HM T E Kind R Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

Terminal platform handler: unknown Windows names return NotSupported to the canonical foreign-item dispatcher, which owns unsupported/native/MIR policy.

Equations

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

def Miri.Interpreter.WindowsForeign.dynamic {Os S Place F H D HM T E Kind R Host System TZ Timestamp B I : Type} [DecidableEq Os] (h : Hooks S Place F H D Os HM T E Kind R Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (symbol : WindowsPlatform.DynamicSymbol) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : Place) (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : M S Unit

Source DynSym dispatch uses the same chain, ABI queries and current state. The canonical FunctionPointers Other registry must embed/recover this symbol.

Equations

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