Immutable compiler symbol and allocator-shim tables. This module contains only source metadata decoding and exact lookup policy, so preparation can be cached by the compiler provider without depending on runtime foreign hooks.

structure Miri.Input.CompilerForeignSymbolTables.Candidate : Type

• symbol : String
• explicitSymbol : Bool
• fnInstance : Option Interpreter.CallInstance

  Only callable exports need a MIR instance. Statics/non-callables must still participate in symbol clashes and in the exported-function UB guard.

• crateIndex : Nat
• crateName : String
• weak : Bool
• spanLo : Nat
• spanHi : Nat
• kind : Interpreter.ForeignItems.ExportKind
• compilerBuiltins : Bool

def Miri.Input.CompilerForeignSymbolTables.instReprCandidate.repr : Candidate → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instReprCandidate : Repr Candidate

Equations

• Miri.Input.CompilerForeignSymbolTables.instReprCandidate = { reprPrec := Miri.Input.CompilerForeignSymbolTables.instReprCandidate.repr }

def Miri.Input.CompilerForeignSymbolTables.instDecidableEqCandidate.decEq (x✝ x✝¹ : Candidate) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instDecidableEqCandidate : DecidableEq Candidate

Equations

• Miri.Input.CompilerForeignSymbolTables.instDecidableEqCandidate = Miri.Input.CompilerForeignSymbolTables.instDecidableEqCandidate.decEq

inductive Miri.Input.CompilerForeignSymbolTables.AllocatorTarget : Type

• redirect (symbol : String) : AllocatorTarget
• special (method : Interpreter.ForeignItems.SpecialAllocatorMethod) : AllocatorTarget

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instReprAllocatorTarget : Repr AllocatorTarget

Equations

• Miri.Input.CompilerForeignSymbolTables.instReprAllocatorTarget = { reprPrec := Miri.Input.CompilerForeignSymbolTables.instReprAllocatorTarget.repr }

def Miri.Input.CompilerForeignSymbolTables.instReprAllocatorTarget.repr : AllocatorTarget → Nat → Std.Format

Equations

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

def Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorTarget.decEq (x✝ x✝¹ : AllocatorTarget) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorTarget : DecidableEq AllocatorTarget

Equations

• Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorTarget = Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorTarget.decEq

structure Miri.Input.CompilerForeignSymbolTables.AllocatorEntry : Type

• symbol : String
• target : AllocatorTarget

def Miri.Input.CompilerForeignSymbolTables.instReprAllocatorEntry.repr : AllocatorEntry → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instReprAllocatorEntry : Repr AllocatorEntry

Equations

• Miri.Input.CompilerForeignSymbolTables.instReprAllocatorEntry = { reprPrec := Miri.Input.CompilerForeignSymbolTables.instReprAllocatorEntry.repr }

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorEntry : DecidableEq AllocatorEntry

Equations

• Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorEntry = Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorEntry.decEq

def Miri.Input.CompilerForeignSymbolTables.instDecidableEqAllocatorEntry.decEq (x✝ x✝¹ : AllocatorEntry) : Decidable (x✝ = x✝¹)

Equations

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

structure Miri.Input.CompilerForeignSymbolTables.Prepared : Type

• noAllocShimSymbol : String
• candidates : Array Candidate

  Exact iter_exported_symbols iteration order; do not sort this array.

• allocatorEntries : Array AllocatorEntry

def Miri.Input.CompilerForeignSymbolTables.instReprPrepared.repr : Prepared → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instReprPrepared : Repr Prepared

Equations

• Miri.Input.CompilerForeignSymbolTables.instReprPrepared = { reprPrec := Miri.Input.CompilerForeignSymbolTables.instReprPrepared.repr }

def Miri.Input.CompilerForeignSymbolTables.instDecidableEqPrepared.decEq (x✝ x✝¹ : Prepared) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerForeignSymbolTables.instDecidableEqPrepared : DecidableEq Prepared

Equations

• Miri.Input.CompilerForeignSymbolTables.instDecidableEqPrepared = Miri.Input.CompilerForeignSymbolTables.instDecidableEqPrepared.decEq

def Miri.Input.CompilerForeignSymbolTables.prepare (instances : CompilerVTableRuntime.Prepared) : Except String Prepared

Decode the exact compiler symbol tables. CompilerVTableRuntime.Prepared already owns the final shared instance table, so every emitted candidate ID is resolved through that table and never reconstructed from a path/display.

Equations

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

def Miri.Input.CompilerForeignSymbolTables.lookup (prepared : Prepared) (symbol : String) : Except Interpreter.StepError (Option Candidate)

Miri's lookup_exported_symbol weak/strong precedence and duplicate error. The array order is the pinned iterator order, including local-crate-first and linked dependency order. Equal-strength duplicate definitions terminate.

Equations

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

def Miri.Input.CompilerForeignSymbolTables.lookupFunction {S : Type} (prepared : Prepared) (loadMir : Interpreter.CallInstance → EStateM Interpreter.StepError S Interpreter.LoadedBody) (symbol : String) : EStateM Interpreter.StepError S (Option (Interpreter.LoadedBody × Interpreter.CallInstance))

Exact lookup_exported_fn type guard. Loading MIR is a separate canonical CompilerCallPipeline operation, and its missing-body error is preserved.

Equations

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

def Miri.Input.CompilerForeignSymbolTables.allocatorSymbol (prepared : Prepared) (symbol : String) : Option (Interpreter.ForeignItems.AllocatorSymbol Interpreter.CallInstance)

Equations

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

def Miri.Input.CompilerForeignSymbolTables.checkSymbolClash (prepared : Prepared) (symbol : String) : Except Interpreter.StepError Unit

Source sig.rs exemption: compiler-builtins definitions do not clash with Miri's built-in implementation. Every other exact exported candidate does.

Equations

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