Source unwind/panic operational dictionaries over the canonical World. Only compiler string allocation/lang-item queries and the internal recursive call edge remain arguments. Reads, writes, allocation materialization, function-pointer resolution and payload storage are actual source operations. Sources: shims/{unwind,panic}.rs; interpret/place.rs::mplace_to_imm_ptr.

@[reducible, inline]

abbrev Miri.Input.EvalCallRuntime.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalCallRuntime.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

abbrev Miri.Input.EvalCallRuntime.State (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalCallRuntime.State = Miri.Input.EvalCoreMachine.State

def Miri.Input.EvalCallRuntime.unwind {Os R P H D O Aff B Host C : Type} (access : Interpreter.ValidityMachine.Access Memory.MiriMemoryKind (EvalCoreMachine.Stored Os R P H D O Aff B Host)) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) O) (panicUnwinds : Bool) (callFunction : C → Interpreter.CallInstance → Array (Interpreter.RvalueImmTy Memory.Provenance) → Interpreter.ReturnContinuation → Interpreter.MachineHooks.M Memory.MiriMemoryKind (User Os R P H D O Aff B Host) Unit) : Interpreter.Unwind.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) C O

The recursive call edge is installed internally by the top-level runner. It is not an after-pop result oracle; Unwind.afterStackPop still owns source write/pop/resolve/call order and every failure prefix.

Equations

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

def Miri.Input.EvalCallRuntime.toImmediatePointer {K U : Type} (p : CompilerProviders.Prepared) (target : ABI.TargetDataLayout) (place : Interpreter.MPlaceTy Memory.Provenance) : Interpreter.MachineHooks.M K U (Interpreter.RvalueImmTy Memory.Provenance)

Canonical mplace_to_imm_ptr(None): reference reconstruction precedes Ty::new_mut_ptr, and its exact compiler layout is queried afterward.

Equations

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

structure Miri.Input.EvalCallRuntime.PanicQueries (K U C : Type) : Type

• allocateStringDedup : C → String → Interpreter.MachineHooks.M K U (Interpreter.MPlaceTy Memory.Provenance)

  Source tcx.allocate_bytes_dedup + str layout/metadata pipeline. This compiler-global allocation operation must retain real pointer provenance.

• langItem : C → Interpreter.Panic.LangItem → Interpreter.MachineHooks.M K U (Option MIR.DefId)
• genericParameters : C → MIR.DefId → Interpreter.MachineHooks.M K U (Array Interpreter.MainGenericParameter)

def Miri.Input.EvalCallRuntime.panic {K U C O : Type} (p : CompilerProviders.Prepared) (queries : PanicQueries K U C) (target : ABI.TargetDataLayout) (driver : Interpreter.Unwind.Hooks K U C O) (operands : Interpreter.OperandMachine.Hooks K U C) : Interpreter.Panic.Hooks K U C O

Equations

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