Stateful virtual receiver/vtable dispatch, dynamic drop and caller-location selection from pinned interpret/call.rs and eval_context.rs. Complete compiler instances, argument rebasing, type constructors and inline-scope span queries remain required compiler leaves; no ABI or function identity is guessed.

inductive Miri.Interpreter.VirtualCalls.ReceiverKind : Type

• reference : ReceiverKind
• rawPointer : ReceiverKind
• dynamic : ReceiverKind
• other : ReceiverKind

@[instance_reducible]

instance Miri.Interpreter.VirtualCalls.instDecidableEqReceiverKind : DecidableEq ReceiverKind

Equations

• Miri.Interpreter.VirtualCalls.instDecidableEqReceiverKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.VirtualCalls.instReprReceiverKind.repr : ReceiverKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.VirtualCalls.instReprReceiverKind : Repr ReceiverKind

Equations

• Miri.Interpreter.VirtualCalls.instReprReceiverKind = { reprPrec := Miri.Interpreter.VirtualCalls.instReprReceiverKind.repr }

structure Miri.Interpreter.VirtualCalls.DynamicData : Type

• predicates : Nat
• principal : Option Nat

structure Miri.Interpreter.VirtualCalls.CallerScope : Type

SourceScopeData fields consumed by Body::caller_location_span.

• inlined : Option (CallInstance × MIR.SpanRef)
• inlinedParentScope : Option Nat

structure Miri.Interpreter.VirtualCalls.CompilerHooks (S C : Type) : Type

• classifyReceiver : MIR.TyId → CallM S ReceiverKind
• fieldLayout : LocalLayout → Nat → CallM S LocalLayout
• structTailForCodegen : MIR.TyId → CallM S MIR.TyId
• dynamicData : MIR.TyId → CallM S (Option DynamicData)
• mutPointerType : MIR.TyId → CallM S MIR.TyId
• mutReferenceType : MIR.TyId → CallM S MIR.TyId
• builtinDeref : MIR.TyId → CallM S (Option MIR.TyId)
• layoutOf : MIR.TyId → CallM S LocalLayout
• parentTrait : MIR.DefId → CallM S MIR.DefId
• rebaseVirtualArgs : Array MIR.GenericArg → MIR.DefId → MIR.TyId → CallM S (Array MIR.GenericArg)

  from_assoc→erase_self_ty→with_self_ty→args.rebase_onto, all using compiler generic arguments, not an assumed first-argument replacement.

• expectResolveForVTable : C → MIR.DefId → Array MIR.GenericArg → CallM S CallInstance
• resolveDropGlue : MIR.TyId → CallM S CallInstance
• requiresCallerLocation : CallInstance → CallM S Bool
• sourceScope : BodyIdentity → CallInstance → MIR.Body → Nat → CallM S CallerScope
• unitLayout : CallM S LocalLayout

structure Miri.Interpreter.VirtualCalls.Hooks (P S C E : Type) : Type

• debugAssertions : Bool
• compiler : CompilerHooks S C
• target : ABI.TargetDataLayout
• vtable : VTableHooks P S C CallInstance (ABI.FnAbi MIR.TyId)
• getFrame : CallM S (Frame P LocalLayout E)
• readImmediate : C → OpTy P → CallM S (RvalueImmTy P)
• immPtrToMPlace : C → RvalueImmTy P → CallM S (MPlaceTy P)
• projectField : C → OpTy P → Nat → CallM S (OpTy P)

def Miri.Interpreter.VirtualCalls.pointerPlace {P S C : Type} [Memory.PointerProvenance P] (compiler : CompilerHooks S C) (target : ABI.TargetDataLayout) (misaligned : Memory.Pointer (Option P) → ABI.Align → CallM S (Option Memory.Misalignment)) (value : RvalueImmTy P) : CallM S (MPlaceTy P)

place.rs imm_ptr_to_mplace: type/deref/layout queries precede scalar extraction; this caches misalignment without checking pointer dereferenceability or dynamic size. An unaligned raw receiver can still resolve a virtual method.

Equations

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

def Miri.Interpreter.VirtualCalls.machineHooks {K User C : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K User) (projection : PlaceMachine.CompilerHooks K User C) (compiler : CompilerHooks (MachineHooks.State K User) C) (vtable : VTableHooks Memory.Provenance (MachineHooks.State K User) C CallInstance (ABI.FnAbi MIR.TyId)) (misaligned : Memory.Pointer (Option Memory.Provenance) → ABI.Align → MachineHooks.M K User (Option Memory.Misalignment)) : Hooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra

Actual canonical memory reads and existing operand field projection. Compiler/global-vtable/host-alignment leaves remain explicit dictionaries.

Equations

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

def Miri.Interpreter.VirtualCalls.nonOneZstField {S C : Type} (compiler : CompilerHooks S C) (layout : LocalLayout) : CallM S (Option Nat)

Source TyAndLayout::non_1zst_field exits immediately on a second non-1-ZST field; no later field query is executed. It does not project/read field values.

Equations

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

def Miri.Interpreter.VirtualCalls.receiverPlace {P S C E : Type} (h : Hooks P S C E) (choice : C) : Nat → OpTy P → CallM S (MPlaceTy P)

Receiver unwrapping performs ordinary typed immediate reads but never a reference dereference/validity check: raw dyn receivers need not be accessible. The budget is a concrete runner recursion limit, not source semantics.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.VirtualCalls.receiverPlace h choice 0 x✝ = throw (Miri.Interpreter.StepError.resourceExhaustion "virtual receiver newtype traversal")

def Miri.Interpreter.VirtualCalls.assertConcrete {S C : Type} (compiler : CompilerHooks S C) (choice : C) (dynTy : MIR.TyId) (definition : MIR.DefId) (virtualInstance concreteInstance : CallInstance) : CallM S Unit

Exact full-instance consistency assertion after symbolic Method selection. Compiler rebasing preserves all method-level generic arguments and shim kind.

Equations

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

def Miri.Interpreter.VirtualCalls.resolveVirtual {P S C E : Type} [Memory.PointerProvenance P] (h : Hooks P S C E) (choice : C) (budget : Nat) (virtualInstance : CallInstance) (definition : MIR.DefId) (slot : Nat) (callerAbi : ABI.FnAbi MIR.TyId) (args : Array (FnArg P)) : CallM S (CallInstance × ABI.FnAbi MIR.TyId × Array (FnArg P))

Source Virtual arm: unwrap receiver, inspect dyn tail, check symbolic vtable, select Method, assert full instance, build thin raw receiver, then patch only the first caller-ABI argument's type. The real callee ABI check occurs in the normal recursive Call pipeline, not eagerly at vtable selection.

Equations

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

def Miri.Interpreter.VirtualCalls.callerLocationSpan {S C : Type} (compiler : CompilerHooks S C) (bodyIdentity : BodyIdentity) (fnInstance : CallInstance) (body : MIR.Body) (trackedCaller : Option MIR.SpanRef) : Nat → MIR.SourceInfo → CallM S MIR.SpanRef

rustc_middle Body::caller_location_span walks only inlined-parent scopes, stopping inside the first non-track_caller callee; the incoming argument is a fallback only after the whole inlined chain has been considered.

Equations

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

def Miri.Interpreter.VirtualCalls.callerLocation {P S C E : Type} (h : Hooks P S C E) (budget : Nat) : CallM S MIR.SpanRef

eval_context.rs caller_location: Call's fn_span replaces only SourceInfo's span; inline-scope-aware compiler handling still receives trackCallerArg.

Equations

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

def Miri.Interpreter.VirtualCalls.unpackDynForDrop {P S C E : Type} [Memory.PointerProvenance P] (h : Hooks P S C E) (choice : C) (place : MPlaceTy P) : CallM S (MPlaceTy P)

Concrete dyn drop unpacks the symbolic vtable's type/layout with a wrapping zero offset and clears metadata, retaining the canonical pointer/misalignment.

Equations

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

def Miri.Interpreter.VirtualCalls.mplaceToMutRef {P S C E : Type} [Memory.PointerProvenance P] (h : Hooks P S C E) (place : MPlaceTy P) : CallM S (OpTy P)

call.rs constructs an erased-region mutable reference, then mplace_to_imm_ptr converts the place before builtin-deref/layout assertions.

Equations

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

def Miri.Interpreter.VirtualCalls.bind {P S C E Other Extern : Type} [Memory.PointerProvenance P] (h : Hooks P S C E) (budget : Nat) (base : CallHooks P S C E Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) : CallHooks P S C E Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)

Install actual runtime dispatch and location selection while preserving mandatory normal-call/ABI/body/machine leaves in the base Call dictionary.

Equations

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