Compiler hygiene/source-map/rendering evidence, with exact body/span keys. An unseen forged BytePos remains unresolved; no nearby-position approximation.

structure Miri.Input.CompilerBacktraceSource.Position : Type

• bytePosition : UInt32
• line : Nat
• column : Nat
• filename : String

@[instance_reducible]

instance Miri.Input.CompilerBacktraceSource.instDecidableEqPosition : DecidableEq Position

Equations

• Miri.Input.CompilerBacktraceSource.instDecidableEqPosition = Miri.Input.CompilerBacktraceSource.instDecidableEqPosition.decEq

def Miri.Input.CompilerBacktraceSource.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

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

structure Miri.Input.CompilerBacktraceSource.SpanEntry : Type

• span : MIR.SpanRef
• position : Position

structure Miri.Input.CompilerBacktraceSource.Prepared : Type

• program : LoweredProgram
• bodySpans : Array (Except String (Array SpanEntry))
• positions : Array Position
• names : Array (Interpreter.CallInstance × String)

def Miri.Input.CompilerBacktraceSource.prepare (program : LoweredProgram) : Except String Prepared

Equations

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

def Miri.Input.CompilerBacktraceSource.source {S : Type} (p : Prepared) (hostUsizeMax : Nat) (unitPointerLayout : EStateM Interpreter.StepError S Interpreter.LocalLayout) (misaligned : Memory.Pointer (Option Memory.Provenance) → ABI.Align → EStateM Interpreter.StepError S (Option Memory.Misalignment)) (functionPointer : Interpreter.CallInstance → EStateM Interpreter.StepError S (Memory.Pointer (Option Memory.Provenance))) (allocation : Memory.Pointer (Option Memory.Provenance) → EStateM Interpreter.StepError S (Memory.AllocId × ABI.Size)) (globalFunction : Memory.AllocId → EStateM Interpreter.StepError S (Option Interpreter.CallInstance)) : Interpreter.BacktraceMachine.Sources S Position

Compiler-source construction with only runtime global/pointer queries. Every hygiene/source-map/name result is selected by its exact exported key.

Equations

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

def Miri.Input.CompilerBacktraceSource.hooks {P S D MD B I E : Type} (p : Prepared) (base : Interpreter.Backtrace.Hooks P S D MD B I E Position) : Interpreter.Backtrace.Hooks P S D MD B I E Position

Equations

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