Control transitions from pinned eval_context.rs:513–558, call.rs:1134–1210, and step.rs:537–707. Required callbacks carry the remaining interpreter operations; this is not a closed Rust semantics.

structure Miri.Interpreter.ControlHooks (P L E M C Op : Type) : Type

• bodySpan : Frame P L E → Except StepError MIR.SpanRef
• returnOperand : C → StepState P L E M → StepResult (StepState P L E M) Op
• popFrame : C → StepState P L E M → StepResult (StepState P L E M) (Frame P L E)
• copyReturn : C → Op → RuntimeStackPlace P → StepState P L E M → StepResult (StepState P L E M) Unit
• cleanupFrame : C → Bool → Frame P L E → StepState P L E M → StepResult (StepState P L E M) ReturnAction
• unwindTerminate : C → MIR.UnwindTerminateReason → StepState P L E M → StepResult (StepState P L E M) Unit

def Miri.Interpreter.ControlFlow.setLocation {P L E M : Type} (state : StepState P L E M) (location : FrameLocation) : StepResult (StepState P L E M) Unit

Source jumps assign the location directly; target validation belongs to body loading/next step, not an extra check before this assignment.

Equations

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

def Miri.Interpreter.ControlFlow.goToBlock {P L E M : Type} (target : MIR.BasicBlockId) (state : StepState P L E M) : StepResult (StepState P L E M) Unit

Equations

• Miri.Interpreter.ControlFlow.goToBlock target state = Miri.Interpreter.ControlFlow.setLocation state (Miri.Interpreter.FrameLocation.mir { block := target, statementIndex := 0 })

def Miri.Interpreter.ControlFlow.returnToBlock {P L E M : Type} (target : Option MIR.BasicBlockId) (state : StepState P L E M) : StepResult (StepState P L E M) Unit

Equations

• Miri.Interpreter.ControlFlow.returnToBlock (some block) state = Miri.Interpreter.ControlFlow.goToBlock block state
• Miri.Interpreter.ControlFlow.returnToBlock none state = (state, Except.error (Miri.Interpreter.StepError.undefinedBehavior "Unreachable"))

def Miri.Interpreter.ControlFlow.unwindToBlock {P L E M C Op : Type} (hooks : ControlHooks P L E M C Op) (choice : C) (target : MIR.UnwindAction) (state : StepState P L E M) : StepResult (StepState P L E M) Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ControlFlow.unwindToBlock hooks choice (Miri.MIR.UnwindAction.Cleanup block) state = (pure (Miri.Interpreter.ControlFlow.goToBlock block state)).run

def Miri.Interpreter.ControlFlow.returnFromCurrentFrame {P L E M C Op : Type} (hooks : ControlHooks P L E M C Op) (choice : C) (unwinding : Bool) (state : StepState P L E M) : StepResult (StepState P L E M) Unit

Return reads local 0 even on unwind, pops before copying, then performs cleanup before following the continuation. Every error preserves prior effects.

Equations

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

structure Miri.Interpreter.TerminatorHooks (P L E M C Op Imm : Type) extends Miri.Interpreter.ControlHooks P L E M C Op : Type

• bodySpan : Frame P L E → Except StepError MIR.SpanRef
• returnOperand : C → StepState P L E M → StepResult (StepState P L E M) Op
• popFrame : C → StepState P L E M → StepResult (StepState P L E M) (Frame P L E)
• copyReturn : C → Op → RuntimeStackPlace P → StepState P L E M → StepResult (StepState P L E M) Unit
• cleanupFrame : C → Bool → Frame P L E → StepState P L E M → StepResult (StepState P L E M) ReturnAction
• unwindTerminate : C → MIR.UnwindTerminateReason → StepState P L E M → StepResult (StepState P L E M) Unit
• evalDiscriminant : C → MIR.Operand → StepState P L E M → StepResult (StepState P L E M) Imm
• compareSwitchCase : C → Imm → Nat → StepState P L E M → StepResult (StepState P L E M) Bool

  Must run MIR Eq against a same-layout ImmTy::from_uint, then to_bool; raw pointer discriminants must not be converted to integer addresses here.

• call : C → MIR.Terminator → StepState P L E M → StepResult (StepState P L E M) Unit
• tailCall : C → MIR.Terminator → StepState P L E M → StepResult (StepState P L E M) Unit
• drop : C → MIR.Place → MIR.BasicBlockId → MIR.UnwindAction → StepState P L E M → StepResult (StepState P L E M) Unit
• ignoreOptionalOverflowChecks : StepState P L E M → Bool
• readAssertCondition : C → MIR.Operand → StepState P L E M → StepResult (StepState P L E M) Bool
• assertPanic : C → MIR.AssertKind → MIR.UnwindAction → StepState P L E M → StepResult (StepState P L E M) Unit

def Miri.Interpreter.ControlFlow.isOptionalOverflowCheck : MIR.AssertKind → Bool

rustc's optional overflow checks are arithmetic overflow and negation.

Equations

• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck (Miri.MIR.AssertKind.Overflow Miri.MIR.BinOp.Add left right) = true
• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck (Miri.MIR.AssertKind.Overflow Miri.MIR.BinOp.Sub left right) = true
• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck (Miri.MIR.AssertKind.Overflow Miri.MIR.BinOp.Mul left right) = true
• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck (Miri.MIR.AssertKind.Overflow Miri.MIR.BinOp.Shl left right) = true
• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck (Miri.MIR.AssertKind.Overflow Miri.MIR.BinOp.Shr left right) = true
• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck (Miri.MIR.AssertKind.OverflowNeg operand) = true
• Miri.Interpreter.ControlFlow.isOptionalOverflowCheck x✝ = false

def Miri.Interpreter.ControlFlow.evalTerminator {P L E M C Op Imm : Type} (hooks : TerminatorHooks P L E M C Op Imm) (choice : C) (terminator : MIR.Terminator) (state : StepState P L E M) : StepResult (StepState P L E M) Unit

Equations

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