Pinned concurrency/scheduler.rs::run_on_stack_empty (31-41), instantiated for eval.rs::MainThreadState's captured closure. Source take/reset/invoke/restore ordering is preserved. Machine-stop exits and errors do not restore the taken callback; successful Pending (including callback continuation) restores it.

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

• main : MainThreadState P E H
• token : Nat
• installed : Bool

inductive Miri.Interpreter.MainThreadCallbackError (Error : Type) : Type

• thread {Error : Type} (error : Concurrency.ThreadError) : MainThreadCallbackError Error
• unavailableCallback {Error : Type} : MainThreadCallbackError Error
• wrongCallback {Error : Type} (expected : Nat) (actual : Option Nat) : MainThreadCallbackError Error
• body {Error : Type} (error : MainThreadError Error) : MainThreadCallbackError Error

def Miri.Interpreter.instReprMainThreadCallbackError.repr {Error✝ : Type} [Repr Error✝] : MainThreadCallbackError Error✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprMainThreadCallbackError {Error✝ : Type} [Repr Error✝] : Repr (MainThreadCallbackError Error✝)

Equations

• Miri.Interpreter.instReprMainThreadCallbackError = { reprPrec := Miri.Interpreter.instReprMainThreadCallbackError.repr }

@[reducible, inline]

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

Equations

• Miri.Interpreter.MainThreadCallbackM P E H Error A = EStateM (Miri.Interpreter.MainThreadCallbackError Error) (Miri.Interpreter.MainThreadCallbackState P E H) A

def Miri.Interpreter.runMainThreadCallback {P E H Error : Type} (dummySpanToken : Nat) (body : MainThreadM P E H Error ProgramExitPoll) : MainThreadCallbackM P E H Error ProgramExitPoll

The dummy-span token must denote actual source DUMMY_SP in the caller's span representation. It is deliberately supplied rather than inventing span0.

Equations

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

def Miri.Interpreter.runMainThreadOnStackEmpty {P E H Error ProvExtra : Type} [Memory.PointerProvenance P] (dummySpanToken : Nat) (format : ConstructorBinaryFormat) (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (constructors : GlobalCtorQueries P E H Error) (main : MainThreadQueries P E H Error) (destructors : TlsDestructorQueries P E H Error) (termination : ThreadExitQueries P E H ProvExtra Error) : MainThreadCallbackM P E H Error ProgramExitPoll

Complete main/global-ctor/main-return/program-exit callback, for an actual empty stack. Entry selection and machine initialization precede this API.

Equations

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