Connected call pipeline from pinned interpret/call.rs and step.rs. Compiler queries, ABI compatibility, and machine leaves are mandatory effects.

inductive Miri.Interpreter.FnArg (P : Type) : Type

• Copy {P : Type} (op : OpTy P) : FnArg P
• InPlace {P : Type} (place : MPlaceTy P) : FnArg P

@[instance_reducible]

instance Miri.Interpreter.instReprFnArg {P✝ : Type} [Repr P✝] : Repr (FnArg P✝)

Equations

• Miri.Interpreter.instReprFnArg = { reprPrec := Miri.Interpreter.instReprFnArg.repr }

def Miri.Interpreter.instReprFnArg.repr {P✝ : Type} [Repr P✝] : FnArg P✝ → Nat → Std.Format

Equations

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

def Miri.Interpreter.FnArg.layout {P : Type} : FnArg P → LocalLayout

Equations

• (Miri.Interpreter.FnArg.Copy a).layout = a.layout
• (Miri.Interpreter.FnArg.InPlace a).layout = a.layout

def Miri.Interpreter.FnArg.copyFnArg {P : Type} : FnArg P → OpTy P

Equations

• (Miri.Interpreter.FnArg.Copy a).copyFnArg = a
• (Miri.Interpreter.FnArg.InPlace a).copyFnArg = { op := Miri.Interpreter.Operand.indirect a.mplace, layout := a.layout }

inductive Miri.Interpreter.FnVal (Other : Type) : Type

• Instance {Other : Type} (fnInstance : CallInstance) : FnVal Other
• Other {Other : Type} (value : Other) : FnVal Other

def Miri.Interpreter.instReprFnVal.repr {Other✝ : Type} [Repr Other✝] : FnVal Other✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprFnVal {Other✝ : Type} [Repr Other✝] : Repr (FnVal Other✝)

Equations

• Miri.Interpreter.instReprFnVal = { reprPrec := Miri.Interpreter.instReprFnVal.repr }

inductive Miri.Interpreter.CallFunctionKind : Type

Function-kind query after signature normalization, before callee resolution.

• FnPtr : CallFunctionKind
• FnDef (definition : MIR.DefId) (args : Array MIR.GenericArg) : CallFunctionKind
• invalid : CallFunctionKind

@[instance_reducible]

instance Miri.Interpreter.instReprCallFunctionKind : Repr CallFunctionKind

Equations

• Miri.Interpreter.instReprCallFunctionKind = { reprPrec := Miri.Interpreter.instReprCallFunctionKind.repr }

def Miri.Interpreter.instReprCallFunctionKind.repr : CallFunctionKind → Nat → Std.Format

Equations

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

structure Miri.Interpreter.CallRequest (P Other Extern FnABI : Type) : Type

• callee : FnVal Other
• callerAbi : Extern
• callerFnAbi : Option FnABI
• args : Array (FnArg P)
• withCallerLocation : Bool
• destination : RuntimeStackPlace P
• target : Option MIR.BasicBlockId
• unwind : MIR.UnwindAction

structure Miri.Interpreter.EvaluatedCall (P Other Extern FnABI : Type) : Type

• callee : FnVal Other
• args : Array (FnArg P)
• callerAbi : Extern
• fnAbi : Option FnABI
• withCallerLocation : Bool

@[reducible, inline]

abbrev Miri.Interpreter.CallM (S A : Type) : Type

Equations

• Miri.Interpreter.CallM S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Interpreter.CallHooks (P S C E Other Extern FnABI ArgABI : Type) : Type 1

FnABI, ArgABI, Extern preserve complete compiler ABI records supplied by the caller. No reduced pass-mode or calling-convention enum is invented. checkArgumentCompat implements source layout_compat AND its eq_abi assertion. All memory operations must invoke the canonical memory/provenance hooks.

• debugAssertions : Bool
• getFrame : CallM S (Frame P LocalLayout E)
• setFrame : Frame P LocalLayout E → CallM S Unit
• frameIndex : CallM S Nat
• evalOperand : C → MIR.Operand → CallM S (OpTy P)
• evalOperandAt : C → OperandPath → MIR.Operand → CallM S (OpTy P)
• evalPlace : C → MIR.Place → Bool → CallM S (RuntimeStackPlace P)
• placeToOp : C → RuntimeStackPlace P → CallM S (OpTy P)
• forceAllocation : C → RuntimeStackPlace P → CallM S (MPlaceTy P)
• functionSignature : C → LocalLayout → CallM S (Nat × Extern)
• functionKind : MIR.TyId → CallM S CallFunctionKind
• readPointer : C → OpTy P → CallM S (Memory.Pointer (Option P))
• getPtrFn : C → Memory.Pointer (Option P) → CallM S (FnVal Other)
• resolve : C → MIR.DefId → Array MIR.GenericArg → CallM S CallInstance
• fnAbiOfFnPtr : C → LocalLayout → Array MIR.TyId → CallM S FnABI
• fnAbiOfInstance : C → CallInstance → Array MIR.TyId → CallM S FnABI
• requiresCallerLocation : CallInstance → CallM S Bool
• callerLocation : CallM S MIR.SpanRef
• abiCanUnwind : FnABI → Bool
• abiVariadic : FnABI → Bool
• abiFixedCount : FnABI → Nat
• abiArgs : FnABI → Array ArgABI
• abiReturn : FnABI → ArgABI
• sameConvention : FnABI → FnABI → Bool
• isRustCall : Extern → Bool
• rustAbi : Extern
• argLayout : ArgABI → LocalLayout
• argIsIgnore : ArgABI → Bool
• isOneZst : LocalLayout → Bool
• checkArgumentCompat : C → ArgABI → ArgABI → CallM S Bool
• checkTargetFeatures : C → CallInstance → CallM S Unit
• tupleFields : MIR.TyId → CallM S (Array MIR.TyId)
• projectFnArg : C → FnArg P → Nat → CallM S (FnArg P)
• localLayout : C → MIR.LocalId → CallM S LocalLayout
• localSpan : MIR.Body → MIR.LocalId → CallM S MIR.SpanRef
• storageLiveDyn : C → MIR.LocalId → MemPlaceMeta P → CallM S Unit
• copyAllowTransmute : C → OpTy P → RuntimeStackPlace P → CallM S Unit
• protectArgument : C → MPlaceTy P → CallM S Unit
• withRetagMode {A : Type} : C → TreeBorrows.RetagPolicy.RetagMode → CallM S A → CallM S A
• nonCapturingClosure : C → CallInstance → FnABI → CallM S Bool
• allocateStack : C → LocalLayout → CallM S (MPlaceTy P)
• copyToMemory : C → OpTy P → MPlaceTy P → CallM S Unit
• vaListPtr : C → Array (MPlaceTy P) → CallM S (Memory.Pointer (Option P))
• writeZeroBytes : C → Memory.Pointer (Option P) → ABI.Size → CallM S Unit
• vaListKeyField : C → MPlaceTy P → CallM S (MPlaceTy P)
• writePointerToMemory : C → Memory.Pointer (Option P) → MPlaceTy P → CallM S Unit
• pushRaw : C → CallInstance → LoadedBody → RuntimeStackPlace P → ReturnContinuation → CallM S Unit
• pushDone : C → CallM S Unit
• popRaw : C → CallM S (Frame P LocalLayout E)
• cleanup : C → Bool → Frame P LocalLayout E → CallM S ReturnAction
• afterFrameInit : C → CallM S Unit
• callExtra : C → Other → FnABI → Array (FnArg P) → RuntimeStackPlace P → Option MIR.BasicBlockId → MIR.UnwindAction → CallM S Unit
• callIntrinsic : C → CallInstance → Array (OpTy P) → RuntimeStackPlace P → Option MIR.BasicBlockId → MIR.UnwindAction → CallM S (Option CallInstance)

  Check intrinsic metadata; fallback must be Item and not must_be_overridden.

• callLlvmIntrinsic : C → CallInstance → Array (OpTy P) → RuntimeStackPlace P → Option MIR.BasicBlockId → CallM S Unit
• findMirOrEvalFn : C → CallInstance → FnABI → Array (FnArg P) → RuntimeStackPlace P → Option MIR.BasicBlockId → MIR.UnwindAction → CallM S (Option (LoadedBody × CallInstance))
• resolveVirtual : C → CallInstance → MIR.DefId → Nat → FnABI → Array (FnArg P) → CallM S (CallInstance × FnABI × Array (FnArg P))

  Unwrap DispatchFromDyn newtypes, read pointer without dereferencing, validate dyn tail/vtable, select Method, cross-check fnInstance, thin receiver and ABI type. Kept required until vtable compiler queries and typed pointer construction port.

• isDynamic : MIR.TyId → CallM S Bool
• unpackDynForDrop : C → MPlaceTy P → CallM S (MPlaceTy P)
• resolveDropGlue : C → MIR.TyId → CallM S CallInstance
• mplaceToMutRef : C → MPlaceTy P → CallM S (OpTy P)
• fakeUnitReturn : C → CallM S (RuntimeStackPlace P)

def Miri.Interpreter.Call.moveDefinitelyDisjoint (args : Array MIR.SpannedOperand) (dest : MIR.Place) : Bool

Equations

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

def Miri.Interpreter.Call.evalFnCallArgumentAt {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (operand : MIR.Operand) (disjoint : Bool) (path : OperandPath) : CallM S (FnArg P)

Equations

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

def Miri.Interpreter.Call.evalFnCallArgument {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (operand : MIR.Operand) (disjoint : Bool) : CallM S (FnArg P)

Equations

• Miri.Interpreter.Call.evalFnCallArgument h choice operand disjoint = Miri.Interpreter.Call.evalFnCallArgumentAt h choice operand disjoint #[]

def Miri.Interpreter.Call.evalCalleeAndArgs {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (func : MIR.Operand) (args : Array MIR.SpannedOperand) (dest : MIR.Place) : CallM S (EvaluatedCall P Other Extern FnABI)

Equations

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

def Miri.Interpreter.Call.passArgument {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (caller : FnArg P) (callerAbi calleeAbi : ArgABI) (calleeIndex : Nat) (dest : MIR.Place) (calleeTy : MIR.TyId) (alreadyLive : Bool) : CallM S Unit

Argument copy precedes protection; StorageLive precedes evaluating callee place.

Equations

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

def Miri.Interpreter.Call.allocateVarargs {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (args : Array (FnArg P × ArgABI)) (calleeAbis : Array ArgABI) : CallM S (Array (MPlaceTy P))

Source stack.rs allocate_varargs: static callee ABI checks precede allocation and copy; no in-place protection is performed for varargs.

Equations

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

def Miri.Interpreter.Call.initStackFrame {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (fnInstance : CallInstance) (loadedBody : LoadedBody) (callerFnAbi : FnABI) (args : Array (FnArg P)) (withCallerLocation : Bool) (destination : RuntimeStackPlace P) (cont : ReturnContinuation) : CallM S Unit

Source init_stack_frame, including all four argument initialization arms.

Equations

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

def Miri.Interpreter.Call.initFnCallStep {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (request : CallRequest P Other Extern FnABI) : CallM S (Option (CallRequest P Other Extern FnABI))

One source dispatch, returning a recursive request for intrinsic fallback or virtual dispatch. This avoids hiding recursion in opaque machine callbacks.

Equations

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

inductive Miri.Interpreter.Call.DispatchPrefix {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) : CallRequest P Other Extern FnABI → S → CallRequest P Other Extern FnABI → S → Prop

Unbounded finite dispatch prefixes. This relation has no runner budget; resource exhaustion of initFnCall says nothing about later UB freedom.

• refl {P S C E Other Extern FnABI ArgABI : Type} {h : CallHooks P S C E Other Extern FnABI ArgABI} {choice : C} (request : CallRequest P Other Extern FnABI) (state : S) : DispatchPrefix h choice request state request state
• next {P S C E Other Extern FnABI ArgABI : Type} {h : CallHooks P S C E Other Extern FnABI ArgABI} {choice : C} {request : CallRequest P Other Extern FnABI} {state : S} {nextRequest : CallRequest P Other Extern FnABI} {nextState : S} {finalRequest : CallRequest P Other Extern FnABI} {finalState : S} (step : initFnCallStep h choice request state = EStateM.Result.ok (some nextRequest) nextState) (rest : DispatchPrefix h choice nextRequest nextState finalRequest finalState) : DispatchPrefix h choice request state finalRequest finalState

def Miri.Interpreter.Call.initFnCall {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (budget : Nat) (request : CallRequest P Other Extern FnABI) : CallM S Unit

Source recursive dispatch is executable with an explicit resource budget. Exhaustion is reported, never successful execution or an omitted arm.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Call.initFnCall h choice 0 request = throw (Miri.Interpreter.StepError.resourceExhaustion "call dispatch budget exhausted")

def Miri.Interpreter.Call.initFnTailCall {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (budget : Nat) (evaluated : EvaluatedCall P Other Extern FnABI) : CallM S Unit

Equations

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

def Miri.Interpreter.Call.evalCallTerminator {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (budget : Nat) (terminator : MIR.Terminator) : CallM S Unit

Equations

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

def Miri.Interpreter.Call.evalTailCallTerminator {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (budget : Nat) (terminator : MIR.Terminator) : CallM S Unit

Equations

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

def Miri.Interpreter.Call.initDropInPlaceCall {P S C E Other Extern FnABI ArgABI : Type} (h : CallHooks P S C E Other Extern FnABI ArgABI) (choice : C) (budget : Nat) (place : RuntimeStackPlace P) (originalInstance : CallInstance) (target : MIR.BasicBlockId) (unwind : MIR.UnwindAction) : CallM S Unit

Equations

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

def Miri.Interpreter.Call.liftStackResult {P E Machine A : Type} (operation : Stack P LocalLayout E → Machine → StackRunResult P LocalLayout E Machine A) : CallM (StepState P LocalLayout E Machine) A

Canonical Stack adapters: callbacks receive the full machine state, and all stack/machine mutations are installed before returning an error.

Equations

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

def Miri.Interpreter.Call.pushRawFromStack {P E Machine : Type} (hooks : StackLifecycleHooks P LocalLayout E Machine) (bodySpan : MIR.Body → Except StepError MIR.SpanRef) (fnInstance : CallInstance) (body : LoadedBody) (destination : RuntimeStackPlace P) (cont : ReturnContinuation) : CallM (StepState P LocalLayout E Machine) Unit

Equations

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

def Miri.Interpreter.Call.pushDoneFromStack {P E Machine : Type} (hooks : StackLifecycleHooks P LocalLayout E Machine) : CallM (StepState P LocalLayout E Machine) Unit

Equations

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

def Miri.Interpreter.Call.popRawFromStack {P E Machine : Type} (hooks : StackLifecycleHooks P LocalLayout E Machine) : CallM (StepState P LocalLayout E Machine) (Frame P LocalLayout E)

Equations

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

def Miri.Interpreter.Call.cleanupFromStack {P E Machine : Type} (hooks : StackLifecycleHooks P LocalLayout E Machine) (unwinding : Bool) (frame : Frame P LocalLayout E) : CallM (StepState P LocalLayout E Machine) ReturnAction

Equations

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

def Miri.Interpreter.Call.run {S A : Type} (computation : CallM S A) (state : S) : StepResult S A

Adapt to ControlFlow.TerminatorHooks while retaining EStateM error state.

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.Call.ZeroHooks (P S C E Other Extern : Type) : Type 1

Equations

• Miri.Interpreter.Call.ZeroHooks P S C E Other Extern = Miri.Interpreter.CallHooks P S C E Other Extern (Miri.ABI.FnAbi Miri.MIR.TyId) (Miri.ABI.ArgAbi Miri.MIR.TyId)

def Miri.Interpreter.Call.zeroCore {P S C E Other Extern : Type} (h : ZeroHooks P S C E Other Extern) (choice : C) (fnInstance : CallInstance) (body : LoadedBody) (abi : ABI.FnAbi MIR.TyId) (destination : MPlaceTy P) (cont : ReturnContinuation) : CallM S Unit

Equations

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

theorem Miri.Interpreter.Call.zero_entry_core {P S C E Other Extern : Type} (h : ZeroHooks P S C E Other Extern) (choice : C) (fnInstance : CallInstance) (body : LoadedBody) (abi : ABI.FnAbi MIR.TyId) (destination : MPlaceTy P) (cont : ReturnContinuation) (requires : h.requiresCallerLocation fnInstance = pure false) (instanceAbi : h.fnAbiOfInstance choice fnInstance #[] = pure abi) (features : h.checkTargetFeatures choice fnInstance = pure ()) (memory : h.placeToOp choice (RuntimeStackPlace.memory destination) = pure { op := Operand.indirect destination.mplace, layout := destination.layout }) (closure : h.nonCapturingClosure choice fnInstance abi = pure false) (variadic : h.abiVariadic abi = false) (convention : h.sameConvention abi abi = true) (arguments : h.abiArgs abi = #[]) (ret : h.abiReturn abi = abi.ret) (count : body.body.argumentCount = 0) : initStackFrame h choice fnInstance body abi #[] false (RuntimeStackPlace.memory destination) cont = zeroCore h choice fnInstance body abi destination cont

def Miri.Interpreter.Call.zeroImmediateCore {P S C E Other Extern : Type} (h : ZeroHooks P S C E Other Extern) (choice : C) (fnInstance : CallInstance) (body : LoadedBody) (abi : ABI.FnAbi MIR.TyId) (destination : RuntimeStackPlace P) (cont : ReturnContinuation) : CallM S Unit

Source specialization for a zero-argument call whose actual preflight operand is immediate. The preflight equation is an internal composition edge.

Equations

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

theorem Miri.Interpreter.Call.zero_entry_immediate {P S C E Other Extern : Type} (h : ZeroHooks P S C E Other Extern) (choice : C) (fnInstance : CallInstance) (body : LoadedBody) (abi : ABI.FnAbi MIR.TyId) (destination : RuntimeStackPlace P) (cont : ReturnContinuation) (before cached : S) (value : Immediate P) (layout : LocalLayout) (requires : h.requiresCallerLocation fnInstance = pure false) (instanceAbi : h.fnAbiOfInstance choice fnInstance #[] = pure abi) (features : h.checkTargetFeatures choice fnInstance = pure ()) (immediate : h.placeToOp choice destination before = EStateM.Result.ok { op := Operand.immediate value, layout := layout } cached) (closure : h.nonCapturingClosure choice fnInstance abi = pure false) (variadic : h.abiVariadic abi = false) (convention : h.sameConvention abi abi = true) (arguments : h.abiArgs abi = #[]) (ret : h.abiReturn abi = abi.ret) (count : body.body.argumentCount = 0) : initStackFrame h choice fnInstance body abi #[] false destination cont before = zeroImmediateCore h choice fnInstance body abi destination cont cached

def Miri.Interpreter.Call.zeroIndirectCore {P S C E Other Extern : Type} (h : ZeroHooks P S C E Other Extern) (choice : C) (fnInstance : CallInstance) (body : LoadedBody) (abi : ABI.FnAbi MIR.TyId) (destination : RuntimeStackPlace P) (memory : MPlaceTy P) (cont : ReturnContinuation) : CallM S Unit

Equations

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

theorem Miri.Interpreter.Call.zero_entry_indirect {P S C E Other Extern : Type} (h : ZeroHooks P S C E Other Extern) (choice : C) (fnInstance : CallInstance) (body : LoadedBody) (abi : ABI.FnAbi MIR.TyId) (destination : RuntimeStackPlace P) (cont : ReturnContinuation) (before cached : S) (memory : MPlaceTy P) (requires : h.requiresCallerLocation fnInstance = pure false) (instanceAbi : h.fnAbiOfInstance choice fnInstance #[] = pure abi) (features : h.checkTargetFeatures choice fnInstance = pure ()) (indirect : h.placeToOp choice destination before = EStateM.Result.ok { op := Operand.indirect memory.mplace, layout := memory.layout } cached) (closure : h.nonCapturingClosure choice fnInstance abi = pure false) (variadic : h.abiVariadic abi = false) (convention : h.sameConvention abi abi = true) (arguments : h.abiArgs abi = #[]) (ret : h.abiReturn abi = abi.ret) (count : body.body.argumentCount = 0) : initStackFrame h choice fnInstance body abi #[] false destination cont before = zeroIndirectCore h choice fnInstance body abi destination memory cont cached