Whole-state stack lifecycle for real calls. Unlike the generic StackEffect adapter, local-storage hooks operate on the actual current frame, retaining FrameExtra clock mutations and exact StepError classifications.

structure Miri.Interpreter.CallMachine.Lifecycle (K User C : Type) : Type

• compiler : FrameMetadata.CompilerHooks K User
• storage : MachineHooks.StorageHooks K User
• freshLocalsIdentity : MachineHooks.MachineState K User → MachineHooks.MachineState K User × LocalsIdentity

  Ghost label for the actual new locals buffer; no guessed zero token.

• preambleSpan : LoadedBody → MachineHooks.M K User MIR.SpanRef

  tcx.def_span(body.source.def_id()), not the caller's location.

• requiredConstants : LoadedBody → MachineHooks.M K User Unit

  Instantiate/normalize/evaluate every required_const in source order.

• afterPop : C → Frame Memory.Provenance LocalLayout MachineHooks.FrameExtra → Bool → MachineHooks.M K User ReturnAction

def Miri.Interpreter.CallMachine.pushRaw {K User C : Type} (h : Lifecycle K User C) (debugAssertions : Bool) (fnInstance : CallInstance) (body : LoadedBody) (destination : RuntimeStackPlace Memory.Provenance) (continuation : ReturnContinuation) : MachineHooks.M K User Unit

Source push_stack_frame_raw. Initialization fails before insertion; required-constant failure retains the inserted frame and untouched cache.

Equations

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

def Miri.Interpreter.CallMachine.alwaysLiveVarsAndTemps (body : MIR.Body) : Except StepError (Array MIR.LocalId)

Source mir/syntax.rs StorageLive contract and Body::vars_and_temps_iter: only variables/temporaries with no StorageLive or StorageDead anywhere in the body are implicitly live. Argument and return slots are excluded here.

Equations

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

def Miri.Interpreter.CallMachine.pushDone {K User C : Type} (h : Lifecycle K User C) : MachineHooks.M K User Unit

Source push_stack_frame_done with actual local clocks retained after each storage-live event, including failure prefixes.

Equations

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

def Miri.Interpreter.CallMachine.cleanup {K User C : Type} (h : Lifecycle K User C) (choice : C) (unwinding : Bool) (frame : Frame Memory.Provenance LocalLayout MachineHooks.FrameExtra) : MachineHooks.M K User ReturnAction

Source cleanup_stack_frame; detached locals/varargs retain allocation identity and deallocate in source order. NoCleanup skips the machine hook.

Equations

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

def Miri.Interpreter.CallMachine.withUnwind {K User C Other : Type} (h : Lifecycle K User C) (unwind : Unwind.Hooks K User C Other) : Lifecycle K User C

Bind the machine after_stack_pop implementation, including real caught unwind payload/call transitions, instead of an external success hook.

Equations

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

def Miri.Interpreter.CallMachine.hooks {K User C Other Extern FnABI ArgABI : Type} [DecidableEq K] (base : CallHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI) (lifecycle : Lifecycle K User C) (access : PlaceMachine.AccessConfig K User) (allocation : PlaceMachine.AllocationConfig K User) (compiler : PlaceMachine.CompilerHooks K User C) (queries : TypedRetag.Hooks K User) (retagBudget : Nat) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C) (evaluatePlace : C → MIR.Place → Bool → MachineHooks.M K User (RuntimePlace Memory.Provenance)) : CallHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI

Compiler/ABI/foreign dispatch stays in base; all frame, place, storage and retag actions below are actual canonical machine actions. Miri does not override rustc Machine::after_stack_frame_init, whose pinned implementation returns ().

Equations

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

def Miri.Interpreter.CallMachine.controlHooks {K User C : Type} [DecidableEq K] (base : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User) C (OpTy Memory.Provenance)) (lifecycle : Lifecycle K User C) (access : PlaceMachine.AccessConfig K User) (allocation : PlaceMachine.AllocationConfig K User) (compiler : PlaceMachine.CompilerHooks K User C) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K User) C) (queries : TypedRetag.Hooks K User) : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K User) C (OpTy Memory.Provenance)

Return and unwind terminators use the same raw-pop and detached cleanup pipeline as calls/tail calls, with actual typed return copying.

Equations

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

def Miri.Interpreter.CallMachine.threadedHooks {K User C Other Extern FnABI ArgABI : Type} [DecidableEq K] (base : CallHooks Memory.Provenance (ThreadStacks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI) (lifecycle : Lifecycle K (ThreadStacks.Storage User) C) (access : PlaceMachine.AccessConfig K (ThreadStacks.Storage User)) (allocation : PlaceMachine.AllocationConfig K (ThreadStacks.Storage User)) (compiler : PlaceMachine.CompilerHooks K (ThreadStacks.Storage User) C) (queries : TypedRetag.Hooks K (ThreadStacks.Storage User)) (retagBudget : Nat) (copy : PlaceCopyHooks Memory.Provenance (ThreadStacks.State K User) C) (evaluatePlace : C → MIR.Place → Bool → ThreadStacks.M K User (RuntimePlace Memory.Provenance)) : CallHooks Memory.Provenance (ThreadStacks.State K User) C MachineHooks.FrameExtra Other Extern FnABI ArgABI

Threaded factory uses the actual process-wide locals-buffer identity supply and synchronizes every success/error prefix with saved per-thread real stacks.

Equations

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

def Miri.Interpreter.CallMachine.threadedControlHooks {K User C : Type} [DecidableEq K] (base : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (ThreadStacks.Storage User)) C (OpTy Memory.Provenance)) (lifecycle : Lifecycle K (ThreadStacks.Storage User) C) (access : PlaceMachine.AccessConfig K (ThreadStacks.Storage User)) (allocation : PlaceMachine.AllocationConfig K (ThreadStacks.Storage User)) (compiler : PlaceMachine.CompilerHooks K (ThreadStacks.Storage User) C) (copy : PlaceCopyHooks Memory.Provenance (ThreadStacks.State K User) C) (queries : TypedRetag.Hooks K (ThreadStacks.Storage User)) : ControlHooks Memory.Provenance LocalLayout MachineHooks.FrameExtra (MachineHooks.MachineState K (ThreadStacks.Storage User)) C (OpTy Memory.Provenance)

Threaded return/unwind factory keeps the registry coherent on every protector-release, deallocation and catch-unwind failure prefix.

Equations

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