machine.rs find_mir_or_eval_fn/call_extra_fn. The foreign interpreter owns its effects; body loading is an exact compiler query.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.CallDispatchMachine.Backend (S : Type) : Type

• selection : S → Except StepError IntrinsicBackend.Kind

structure Miri.Interpreter.CallDispatchMachine.Hooks (S C Other : Type) : Type 1

• foreign : Option (M S (ForeignItems.Hooks Memory.Provenance S (RuntimePlace Memory.Provenance) (RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) LoadedBody CallInstance))

  Foreign interpretation is constructed at the actual call state. This keeps live source policy (for example native-library enablement) from being captured when the outer execution configuration was created.

• returnToBlock : Option MIR.BasicBlockId → M S Unit
• isForeignItem : CallInstance → M S Bool
• symbolName : CallInstance → M S String
• loadMir : C → CallInstance → M S LoadedBody
• backend : Backend S
• dynSymName : Other → String
• foreignScope {A : Type} : M S A → M S A

  Source-owned scope around the complete foreign shim action. Deadline tokens are created and consumed inside one shim call, including callbacks run between timeout creation and blocking; keep those temporary tokens live until the call returns. Low-level constructors may retain identity scope.

def Miri.Interpreter.CallDispatchMachine.findMirOrEvalFn {S C Other : Type} (h : Hooks S C Other) (choice : C) (callee : CallInstance) (abi : ABI.FnAbi MIR.TyId) (args : Array (FnArg Memory.Provenance)) (destination : RuntimeStackPlace Memory.Provenance) (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : M S (Option (LoadedBody × CallInstance))

Equations

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

def Miri.Interpreter.CallDispatchMachine.callExtra {S C Other : Type} (h : Hooks S C Other) (_choice : C) (symbol : Other) (abi : ABI.FnAbi MIR.TyId) (args : Array (FnArg Memory.Provenance)) (destination : RuntimeStackPlace Memory.Provenance) (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : M S Unit

Equations

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