helpers.rs::lookup_link_section, eval_context.rs::eval_global and place.rs::raw_const_to_mplace. Source symbol order and used filtering are exported; actual static pointers, initializer reads and projection execute here.

structure Miri.Input.CompilerLinkSections.Memory (K U Other : Type) : Type

• functions : Interpreter.FunctionPointers.Hooks K U Other
• externStatic : MIR.DefId → Interpreter.MachineHooks.M K U (Memory.Pointer Memory.Provenance)
• projection : Interpreter.MachineHooks.M K U (Interpreter.ProjectionCx Memory.Provenance)
• readImmediate : Interpreter.OpTy Memory.Provenance → Interpreter.MachineHooks.M K U (Interpreter.RvalueImmTy Memory.Provenance)

structure Miri.Input.CompilerLinkSections.GlobalRef : Type

• definition : MIR.DefId
• ty : MIR.TyId
• allocation : AllocationId
• expectStatic : Bool

def Miri.Input.CompilerLinkSections.globalRef {K U Other : Type} (runtime : RuntimeMetadata) (h : Memory K U Other) (entryData : GlobalRef) : Interpreter.MachineHooks.M K U (Interpreter.OpTy Memory.Provenance)

Equations

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

def Miri.Input.CompilerLinkSections.global {K U Other : Type} (p : CompilerMain.Prepared) (h : Memory K U Other) (entryData : CompilerMain.Section) : Interpreter.MachineHooks.M K U (Interpreter.OpTy Memory.Provenance)

Equations

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

def Miri.Input.CompilerLinkSections.lookup {K U Other : Type} (p : CompilerMain.Prepared) (h : Memory K U Other) (includeName : String → Bool) : Interpreter.MachineHooks.M K U (Array (Interpreter.TlsImmediate Memory.Provenance × MIR.SpanRef))

Reads occur in source order; earlier initialization/provenance/race effects remain in the machine if a later static or element read fails.

Equations

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

def Miri.Input.CompilerLinkSections.hooks {U O C F A Aff P : Type} (p : CompilerMain.Prepared) (memory : Memory Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage U) O) (base : Interpreter.MainMachine.Hooks U C O ABI.ExternAbi F A Aff P) : Interpreter.MainMachine.Hooks U C O ABI.ExternAbi F A Aff P

Main's linker-section compiler query executes actual imported global reads; all MainMachine scheduler/callback/termination effects remain unchanged.

Equations

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