Full pinned shims/backtrace.rs driver. Encoded frame pointers preserve actual function provenance and source BytePos offsets. Host/compiler symbol, source-map and hygiene queries are explicit typed leaves; all writes are real machine operations supplied by the connected memory binding.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.Backtrace.Operations (P S D MD B I E Loc : Type) : Type

• target : ABI.TargetDataLayout
• arithmetic : Memory.PointerArithmetic
• hostUsizeMax : Nat
• stack : M S (Stack P LocalLayout E)
• readU64 : OpTy P → M S UInt64
• unitPointerLayout : M S LocalLayout
• misaligned : Memory.Pointer (Option P) → ABI.Align → M S (Option Memory.Misalignment)
• memoryOffset : MemPlace P → ABI.Size → OffsetMode → MemPlaceMeta P → M S (MemPlace P)
• memoryPlace : MPlaceTy P → MD
• layout : MD → LocalLayout
• projectField : MD → Nat → M S MD
• writeScalar : Memory.Scalar P → MD → M S Unit
• writeBytes : Memory.Pointer (Option P) → ByteArray → M S Unit
• functionPointer : CallInstance → M S (Memory.Pointer (Option P))

  Actual fn_ptr(FnVal::Instance(...)), including canonical global identity reservation and machine root-address adjustment, never a DefId-as-address.

• collapsedSpanLo : BodyIdentity → MIR.SpanRef → M S UInt32

  hygiene::walk_chain_collapsed(current_span, body.span).lo(). Actual body metadata is selected by bodyIdentity, not by equal instructions or names.

• allocation : Memory.Pointer (Option P) → M S (Memory.AllocId × ABI.Size)
• globalFunction : Memory.AllocId → M S (Option CallInstance)
• lookupCharPos : UInt32 → M S Loc
• line : Loc → Nat
• column : Loc → Nat
• renderInstance : CallInstance → M S String
• remappedFilename : Loc → M S String

structure Miri.Interpreter.Backtrace.CoreHooks (P S D MD B I E Loc : Type) extends Miri.Interpreter.Backtrace.Operations P S D MD B I E Loc : Type

• target : ABI.TargetDataLayout
• arithmetic : Memory.PointerArithmetic
• hostUsizeMax : Nat
• stack : M S (Stack P LocalLayout E)
• readU64 : OpTy P → M S UInt64
• unitPointerLayout : M S LocalLayout
• misaligned : Memory.Pointer (Option P) → ABI.Align → M S (Option Memory.Misalignment)
• memoryOffset : MemPlace P → ABI.Size → OffsetMode → MemPlaceMeta P → M S (MemPlace P)
• memoryPlace : MPlaceTy P → MD
• layout : MD → LocalLayout
• projectField : MD → Nat → M S MD
• writeScalar : Memory.Scalar P → MD → M S Unit
• writeBytes : Memory.Pointer (Option P) → ByteArray → M S Unit
• functionPointer : CallInstance → M S (Memory.Pointer (Option P))
• collapsedSpanLo : BodyIdentity → MIR.SpanRef → M S UInt32
• allocation : Memory.Pointer (Option P) → M S (Memory.AllocId × ABI.Size)
• globalFunction : Memory.AllocId → M S (Option CallInstance)
• lookupCharPos : UInt32 → M S Loc
• line : Loc → Nat
• column : Loc → Nat
• renderInstance : CallInstance → M S String
• remappedFilename : Loc → M S String
• foreign : ForeignItems.Core P S D MD (Memory.Pointer (Option P)) B I

structure Miri.Interpreter.Backtrace.Hooks (P S D MD B I E Loc : Type) extends Miri.Interpreter.Backtrace.Operations P S D MD B I E Loc : Type

• target : ABI.TargetDataLayout
• arithmetic : Memory.PointerArithmetic
• hostUsizeMax : Nat
• stack : M S (Stack P LocalLayout E)
• readU64 : OpTy P → M S UInt64
• unitPointerLayout : M S LocalLayout
• misaligned : Memory.Pointer (Option P) → ABI.Align → M S (Option Memory.Misalignment)
• memoryOffset : MemPlace P → ABI.Size → OffsetMode → MemPlaceMeta P → M S (MemPlace P)
• memoryPlace : MPlaceTy P → MD
• layout : MD → LocalLayout
• projectField : MD → Nat → M S MD
• writeScalar : Memory.Scalar P → MD → M S Unit
• writeBytes : Memory.Pointer (Option P) → ByteArray → M S Unit
• functionPointer : CallInstance → M S (Memory.Pointer (Option P))
• collapsedSpanLo : BodyIdentity → MIR.SpanRef → M S UInt32
• allocation : Memory.Pointer (Option P) → M S (Memory.AllocId × ABI.Size)
• globalFunction : Memory.AllocId → M S (Option CallInstance)
• lookupCharPos : UInt32 → M S Loc
• line : Loc → Nat
• column : Loc → Nat
• renderInstance : CallInstance → M S String
• remappedFilename : Loc → M S String
• foreign : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I

def Miri.Interpreter.Backtrace.Hooks.core {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) : CoreHooks P S D MD B I E Loc

Equations

• h.core = { toOperations := h.toOperations, foreign := h.foreign.toCore }

@[instance_reducible]

instance Miri.Interpreter.Backtrace.instCoeOutHooksCoreHooks {P S D MD B I E Loc : Type} : CoeOut (Hooks P S D MD B I E Loc) (CoreHooks P S D MD B I E Loc)

Equations

• Miri.Interpreter.Backtrace.instCoeOutHooksCoreHooks = { coe := Miri.Interpreter.Backtrace.Hooks.core }

def Miri.Interpreter.Backtrace.Source.currentSpan {P E : Type} (frame : Frame P LocalLayout E) : Except StepError MIR.SpanRef

stack.rs Frame::current_span, including the unwinding-span path.

Equations

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

def Miri.Interpreter.Backtrace.Source.size {P S D MD B I E Loc : Type} (h : CoreHooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S Unit

No symbol or stack query occurs on the invalid-flags path.

Equations

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

def Miri.Interpreter.Backtrace.Source.get {P S D MD B I E Loc : Type} (h : CoreHooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S Unit

Gather all source spans first, then create every encoded function pointer, then check flags and write the caller's array in order. Even obsolete flags perform the source pointer-generation effects before returning Unsupported.

Equations

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

def Miri.Interpreter.Backtrace.Source.resolvePointer {P S D MD B I E Loc : Type} (h : CoreHooks P S D MD B I E Loc) (operand : OpTy P) : M S (CallInstance × Loc × String × String)

The byte offset encodes source position; therefore ordinary get_ptr_fn, which rejects nonzero function offsets, is deliberately not used.

Equations

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

def Miri.Interpreter.Backtrace.Source.resolveFrame {P S D MD B I E Loc : Type} (h : CoreHooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) (adtReprC : MIR.TyId → M S (Option Bool)) : M S Unit

Equations

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

def Miri.Interpreter.Backtrace.Source.resolveNames {P S D MD B I E Loc : Type} (h : CoreHooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S Unit

Equations

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

def Miri.Interpreter.Backtrace.Source.emulate {P S D MD B I E Loc : Type} (h : CoreHooks P S D MD B I E Loc) (adtReprC : MIR.TyId → M S (Option Bool)) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S (Option ForeignItems.EmulateItemResult)

Equations

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

def Miri.Interpreter.Backtrace.currentSpan {P E : Type} (frame : Frame P LocalLayout E) : Except StepError MIR.SpanRef

Equations

• Miri.Interpreter.Backtrace.currentSpan frame = Miri.Interpreter.Backtrace.Source.currentSpan frame

def Miri.Interpreter.Backtrace.size {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S Unit

Equations

• Miri.Interpreter.Backtrace.size h abi args dest = Miri.Interpreter.Backtrace.Source.size h.core abi args dest

def Miri.Interpreter.Backtrace.get {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S Unit

Equations

• Miri.Interpreter.Backtrace.get h abi args = Miri.Interpreter.Backtrace.Source.get h.core abi args

def Miri.Interpreter.Backtrace.resolvePointer {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (operand : OpTy P) : M S (CallInstance × Loc × String × String)

Equations

• Miri.Interpreter.Backtrace.resolvePointer h operand = Miri.Interpreter.Backtrace.Source.resolvePointer h.core operand

def Miri.Interpreter.Backtrace.resolveFrame {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) (adtReprC : MIR.TyId → M S (Option Bool)) : M S Unit

Equations

• Miri.Interpreter.Backtrace.resolveFrame h abi args dest adtReprC = Miri.Interpreter.Backtrace.Source.resolveFrame h.core abi args dest adtReprC

def Miri.Interpreter.Backtrace.resolveNames {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) : M S Unit

Equations

• Miri.Interpreter.Backtrace.resolveNames h abi args = Miri.Interpreter.Backtrace.Source.resolveNames h.core abi args

def Miri.Interpreter.Backtrace.emulate {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (adtReprC : MIR.TyId → M S (Option Bool)) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy P)) (dest : MD) : M S (Option ForeignItems.EmulateItemResult)

Equations

• Miri.Interpreter.Backtrace.emulate h adtReprC name abi args dest = Miri.Interpreter.Backtrace.Source.emulate h.core adtReprC name abi args dest

def Miri.Interpreter.Backtrace.bind {P S D MD B I E Loc : Type} (h : Hooks P S D MD B I E Loc) (adtReprC : MIR.TyId → M S (Option Bool)) : ForeignItems.Hooks P S D MD (Memory.Pointer (Option P)) B I

Equations

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