Canonical actual-memory binding for backtrace.rs. Raw string copying owns bounds/init/provenance/race/TB transitions through RawMemoryMachine; typed pointer and field writes use PlaceMachine's source place writer.

def Miri.Interpreter.BacktraceMachine.hooks {K User C D B I Loc : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra) (choice : C) (base : Backtrace.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) B I MachineHooks.FrameExtra Loc) : Backtrace.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) B I MachineHooks.FrameExtra Loc

Machine source/span rendering and compiler signature leaves stay required. This binding supplies actual active frames (including body IDs), actual typed scalar reads, local projections and all raw/typed destination writes.

Equations

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

structure Miri.Interpreter.BacktraceMachine.Sources (S Loc : Type) : Type

Exact compiler/global source capabilities. Physical frame reads, pointer and field writes are built below and cannot be replaced by this record.

• hostUsizeMax : Nat
• unitPointerLayout : EStateM StepError S LocalLayout
• misaligned : Memory.Pointer (Option Memory.Provenance) → ABI.Align → EStateM StepError S (Option Memory.Misalignment)
• functionPointer : CallInstance → EStateM StepError S (Memory.Pointer (Option Memory.Provenance))
• collapsedSpanLo : BodyIdentity → MIR.SpanRef → EStateM StepError S UInt32
• allocation : Memory.Pointer (Option Memory.Provenance) → EStateM StepError S (Memory.AllocId × ABI.Size)
• globalFunction : Memory.AllocId → EStateM StepError S (Option CallInstance)
• lookupCharPos : UInt32 → EStateM StepError S Loc
• line : Loc → Nat
• column : Loc → Nat
• renderInstance : CallInstance → EStateM StepError S String
• remappedFilename : Loc → EStateM StepError S String

def Miri.Interpreter.BacktraceMachine.core {K User C Loc D B I : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra) (choice : C) (source : Sources (MachineHooks.State K User) Loc) (foreign : ForeignItems.Core Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : Backtrace.CoreHooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) B I MachineHooks.FrameExtra Loc

Nonrecursive source construction: no baseline portable/foreign dispatcher.

Equations

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

def Miri.Interpreter.BacktraceMachine.bind {K User C D B I Loc : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra) (choice : C) (base : Backtrace.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) B I MachineHooks.FrameExtra Loc) (adtReprC : MIR.TyId → MachineHooks.M K User (Option Bool)) : ForeignItems.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

Equations

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

def Miri.Interpreter.BacktraceMachine.bindMiriShims {K User C D B I Loc HostPath : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K User) (arithmetic : Memory.PointerArithmetic) (projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K User) C MachineHooks.FrameExtra) (choice : C) (backtrace : Backtrace.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) B I MachineHooks.FrameExtra Loc) (miri : MiriShims.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) B I HostPath) (adtReprC : MIR.TyId → MachineHooks.M K User (Option Bool)) : ForeignItems.Hooks Memory.Provenance (MachineHooks.State K User) D (RuntimePlace Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

Connect the four source APIs to the Miri-only portable dispatch chain. Other portable/foreign operations retain the already bound source dictionary.

Equations

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