Exact compiler support for machine.rs::extern_static_pointer. Declaration metadata is keyed by shared DefId identity. Exported-static resolution retains the source-selected symbol winner and its allocation ID; the winner is materialized only through the canonical imported global table.

structure Miri.Input.CompilerExternStatic.Declaration : Type

• definition : MIR.DefId
• symbol : String
• size : ABI.Size
• align : ABI.Align
• linkage : Interpreter.ExternStatic.ImportLinkage
• mutable : Bool
• result : Except String Unit

@[instance_reducible]

instance Miri.Input.CompilerExternStatic.instDecidableEqDeclaration : DecidableEq Declaration

Equations

• Miri.Input.CompilerExternStatic.instDecidableEqDeclaration = Miri.Input.CompilerExternStatic.instDecidableEqDeclaration.decEq

def Miri.Input.CompilerExternStatic.instDecidableEqDeclaration.decEq (x✝ x✝¹ : Declaration) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerExternStatic.instReprDeclaration : Repr Declaration

Equations

• Miri.Input.CompilerExternStatic.instReprDeclaration = { reprPrec := Miri.Input.CompilerExternStatic.instReprDeclaration.repr }

def Miri.Input.CompilerExternStatic.instReprDeclaration.repr : Declaration → Nat → Std.Format

Equations

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

structure Miri.Input.CompilerExternStatic.Winner : Type

• definition : Option MIR.DefId
• kind : String
• allocation : Option AllocationId
• status : String
• reason : String

structure Miri.Input.CompilerExternStatic.Selected : Type

• symbol : String
• winner : Winner

structure Miri.Input.CompilerExternStatic.TargetFacts : Type

Target attributes returned by rustc's parsed Session target. families is the exact cfg family set; neither family nor environment is inferred from the target triple.

• os : String
• env : String
• binaryFormat : String
• families : Array String

def Miri.Input.CompilerExternStatic.instDecidableEqTargetFacts.decEq (x✝ x✝¹ : TargetFacts) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerExternStatic.instDecidableEqTargetFacts : DecidableEq TargetFacts

Equations

• Miri.Input.CompilerExternStatic.instDecidableEqTargetFacts = Miri.Input.CompilerExternStatic.instDecidableEqTargetFacts.decEq

def Miri.Input.CompilerExternStatic.instReprTargetFacts.repr : TargetFacts → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerExternStatic.instReprTargetFacts : Repr TargetFacts

Equations

• Miri.Input.CompilerExternStatic.instReprTargetFacts = { reprPrec := Miri.Input.CompilerExternStatic.instReprTargetFacts.repr }

structure Miri.Input.CompilerExternStatic.Prepared : Type

• program : LoweredProgram
• runtime : RuntimeMetadata
• sourceStatus : Except String Unit
• targetFacts : Except String TargetFacts
• declarations : Array Declaration
• selected : Array Selected

def Miri.Input.CompilerExternStatic.prepare (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) : Except String Prepared

Equations

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

Build the source resolver on any persistent machine state. The caller supplies its canonical memory/runtime views and root-pointer operation; this lets constants and allocation-image relocations share one resolver even though the latter intentionally run without a MIR frame.

def Miri.Input.CompilerExternStatic.hooksOn {K S : Type} [DecidableEq K] (p : Prepared) (image : AllocationImage.Imported) (memory : S → Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K) (externStaticState : S → Interpreter.ExternStatic.State) (checkSymbolClash : String → Interpreter.ExternStatic.M S Unit) (rootPointer : Memory.AllocId → Interpreter.ExternStatic.M S Memory.StrictPointer) : Interpreter.ExternStatic.ResolveHooks S Winner

Equations

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

def Miri.Input.CompilerExternStatic.resolveOn {K S : Type} [DecidableEq K] (p : Prepared) (image : AllocationImage.Imported) (memory : S → Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K) (externStaticState : S → Interpreter.ExternStatic.State) (checkSymbolClash : String → Interpreter.ExternStatic.M S Unit) (rootPointer : Memory.AllocId → Interpreter.ExternStatic.M S Memory.StrictPointer) (definitionId : MIR.DefId) : Interpreter.ExternStatic.M S Memory.StrictPointer

Equations

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

Actual full-interpreter adapter, including the source function-pointer root operation and the same runtime ExternStatic storage used by GC.

def Miri.Input.CompilerExternStatic.hooks {K U Other : Type} [DecidableEq K] (p : Prepared) (image : AllocationImage.Imported) (checkSymbolClash : String → Interpreter.MachineHooks.M K U Unit) (functions : Interpreter.FunctionPointers.Hooks K U Other) (externStaticState : U → Interpreter.ExternStatic.State) : Interpreter.ExternStatic.ResolveHooks (Interpreter.MachineHooks.State K U) Winner

Equations

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

def Miri.Input.CompilerExternStatic.resolve {K U Other : Type} [DecidableEq K] (p : Prepared) (image : AllocationImage.Imported) (checkSymbolClash : String → Interpreter.MachineHooks.M K U Unit) (functions : Interpreter.FunctionPointers.Hooks K U Other) (externStaticState : U → Interpreter.ExternStatic.State) (definitionId : MIR.DefId) : Interpreter.MachineHooks.M K U Memory.StrictPointer

Equations

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