Surviving compiler/platform capabilities of the source call constructor. Frame/local operations, ABI projections, argument projection, retagging, varargs storage and MIR/foreign/backend dispatch algorithms are not callbacks.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.ExecutionCallLeaves.TargetFeature : Type

• name : String
• implied : Bool

structure Miri.Interpreter.ExecutionCallLeaves.TargetFeatures (S : Type) : Type

• required : CallInstance → M S (Array TargetFeature)
• available : String → M S Bool
• isLikeWasm : M S Bool

def Miri.Interpreter.ExecutionCallLeaves.checkTargetFeatures {S : Type} (h : TargetFeatures S) (callee : CallInstance) : M S Unit

machine.rs check_fn_target_features: the first guard includes implied features, while the reported list excludes them. WASM aborts instead of UB.

Equations

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

structure Miri.Interpreter.ExecutionCallLeaves.Compiler (S C Extern : Type) : Type

• functionSignature : C → LocalLayout → M S (Nat × Extern)
• functionKind : MIR.TyId → M S CallFunctionKind
• resolve : C → MIR.DefId → Array MIR.GenericArg → M S CallInstance
• fnAbiOfFnPtr : C → LocalLayout → Array MIR.TyId → M S (ABI.FnAbi MIR.TyId)
• fnAbiOfInstance : C → CallInstance → Array MIR.TyId → M S (ABI.FnAbi MIR.TyId)
• isRustCall : Extern → Bool
• rustAbi : Extern
• checkArgumentCompat : C → ABI.ArgAbi MIR.TyId → ABI.ArgAbi MIR.TyId → M S Bool
• targetFeatures : TargetFeatures S
• tupleFields : MIR.TyId → M S (Array MIR.TyId)
• isClosureLike : CallInstance → M S Bool
• closureUpvarCount : MIR.TyId → M S (Option Nat)
• llvmLinkName : CallInstance → M S String

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

• compiler : Compiler S C Extern
• dispatch : CallDispatchMachine.Hooks S C Other
• llvm : CallInstance → EStateM StepError S (IntrinsicArchitecture.DispatchHooks Memory.Provenance S C (RuntimePlace Memory.Provenance))

def Miri.Interpreter.ExecutionCallLeaves.nonCapturingClosure {S C X : Type} (h : Compiler S C X) (callee : CallInstance) (abi : ABI.FnAbi MIR.TyId) : M S Bool

Source call.rs non-capturing-closure test, including its short circuit. ClosureOnce avoids the def-kind query; the first ABI argument is touched only for closure-like instances, and upvars only for a Closure type.

Equations

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

structure Miri.Interpreter.ExecutionCallLeaves.Virtual (K U C : Type) : Type

Virtual compiler/vtable data and actual alignment-state access only.

• compiler : VirtualCalls.CompilerHooks (MachineHooks.State K U) C
• vtable : VTableHooks Memory.Provenance (MachineHooks.State K U) C CallInstance (ABI.FnAbi MIR.TyId)
• alignment : PointerPlaceMachine.AlignmentContext U

structure Miri.Interpreter.ExecutionCallLeaves.IdentityAccess (U : Type) : Type

The actual shared locals-buffer ghost-identity supply. Callers provide a representation lens, not a callback that chooses a frame identity.

• get : U → LocalsIdentitySupply
• put : U → LocalsIdentitySupply → U

structure Miri.Interpreter.ExecutionCallLeaves.Helpers (S C Extern : Type) : Type

Source helper signature queries/data only; actual call/stack/origin actions are constructed from the canonical machine state.

• loadMir : C → CallInstance → M S LoadedBody
• unitLayout : LocalLayout
• fnAbiOfSignature : C → FunctionCalls.SignatureRequest Extern → M S (ABI.FnAbi MIR.TyId)
• callerLocationType : M S MIR.TyId
• dummySpan : MIR.SpanRef