Pinned shims/global_ctor.rs::GlobalCtorState::on_stack_empty (23-98). Binary format is explicit target metadata. Link sections are matched exactly; constructor lists retain source order and are popped from the end.

inductive Miri.Interpreter.ConstructorBinaryFormat : Type

• coff : ConstructorBinaryFormat
• machO : ConstructorBinaryFormat
• elf : ConstructorBinaryFormat
• wasm : ConstructorBinaryFormat
• other (name : String) : ConstructorBinaryFormat

inductive Miri.Interpreter.GlobalCtorStage (P : Type) : Type

• init {P : Type} : GlobalCtorStage P
• constructors {P : Type} (remaining : Array (TlsImmediate P × MIR.SpanRef)) : GlobalCtorStage P
• done {P : Type} : GlobalCtorStage P

structure Miri.Interpreter.GlobalCtorState (P E H : Type) : Type

• execution : TlsExecutionState P E H
• stage : GlobalCtorStage P

@[reducible, inline]

abbrev Miri.Interpreter.GlobalCtorM (P E H Error A : Type) : Type

Equations

• Miri.Interpreter.GlobalCtorM P E H Error A = EStateM (Miri.Interpreter.TlsExecutionError Error) (Miri.Interpreter.GlobalCtorState P E H) A

structure Miri.Interpreter.GlobalCtorQueries (P E H Error : Type) : Type

• lookupLinkSection : (String → Bool) → GlobalCtorM P E H Error (Array (TlsImmediate P × MIR.SpanRef))
• getPointerFnInstance : Memory.Pointer (Option P) → GlobalCtorM P E H Error CallInstance
• callConstructor : CallInstance → MIR.SpanRef → GlobalCtorM P E H Error Unit

  Actual call_thread_root_function with C ABI, unwind=false, no arguments, no return destination, Stop{cleanup:true}, source empty-stack/origin checks.

def Miri.Interpreter.constructorSectionMatches (format : ConstructorBinaryFormat) (sectionName : String) : Bool

Source splitn(3, ',') retains the entire suffix in the third component.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.constructorSectionMatches Miri.Interpreter.ConstructorBinaryFormat.coff sectionName = (sectionName == ".CRT$XCU")
• Miri.Interpreter.constructorSectionMatches Miri.Interpreter.ConstructorBinaryFormat.elf sectionName = (sectionName == ".init_array")
• Miri.Interpreter.constructorSectionMatches Miri.Interpreter.ConstructorBinaryFormat.wasm sectionName = (sectionName == ".init_array")
• Miri.Interpreter.constructorSectionMatches (Miri.Interpreter.ConstructorBinaryFormat.other name) sectionName = false

def Miri.Interpreter.globalConstructorsOnStackEmpty {P E H Error : Type} [Memory.PointerProvenance P] (format : ConstructorBinaryFormat) (target : ABI.RuntimeTargetDataLayout) (queries : GlobalCtorQueries P E H Error) : GlobalCtorM P E H Error Concurrency.StackEmptyCallbackResult

Equations

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