thread.rs replace_active_thread_stack and eval.rs ProgramExitHandler, ExitCalled variant, connected to the same actual main/TLS scheduler callbacks.

@[reducible, inline]

abbrev Miri.Interpreter.WindowsExitMachine.State (U : Type) : Type

Equations

• Miri.Interpreter.WindowsExitMachine.State = Miri.Interpreter.MainMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.WindowsExitMachine.M (U A : Type) : Type

Equations

• Miri.Interpreter.WindowsExitMachine.M = Miri.Interpreter.MainMachine.M

structure Miri.Interpreter.WindowsExitMachine.Handler : Type

• token : Nat
• stage : ProgramExitStage
• tls : TlsDtorsStage Memory.Provenance
• code : Int32

structure Miri.Interpreter.WindowsExitMachine.Registry : Type

• handlers : Array Handler

structure Miri.Interpreter.WindowsExitMachine.Hooks (U C O X F A Aff P : Type) : Type 1

• main : MainMachine.Hooks U C O X F A Aff P
• get : U → Registry
• put : U → Registry → U

def Miri.Interpreter.WindowsExitMachine.start {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (code : Int32) : M U Unit

Source clears frame owners, leaking allocations without running pops, retags, destructors, or deallocation hooks. Diagnostic origin is captured first.

Equations

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

def Miri.Interpreter.WindowsExitMachine.invoke {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (choice : C) (handler : Handler) : M U StackEmptyPoll

Invoked only after take moved the actual owned handler out of the registry.

Equations

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

inductive Miri.Interpreter.WindowsExitMachine.Callback : Type

• exitHandler (handler : Handler) : Callback
• mainOrTls (callback : MainMachine.Callback) : Callback

def Miri.Interpreter.WindowsExitMachine.take {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) : M U Callback

Equations

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

def Miri.Interpreter.WindowsExitMachine.restore {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) : Callback → M U Unit

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsExitMachine.restore h (Miri.Interpreter.WindowsExitMachine.Callback.mainOrTls callback) = Miri.Interpreter.MainMachine.restore h.main callback

def Miri.Interpreter.WindowsExitMachine.bindLoop {U C O X F A Aff P : Type} (h : Hooks U C O X F A Aff P) (base : RunLoopHooks (State U) C Callback) (scheduler : C → ThreadStacks.LocalSchedulerHooks Memory.MiriMemoryKind U) : RunLoopHooks (State U) C Callback

Equations

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

def Miri.Interpreter.WindowsExitMachine.bindPlatform {U C O X F A Aff P Os E Kind FD : Type} (h : Hooks U C O X F A Aff P) (base : WindowsPlatformDispatch.Hooks (State U) Os E Kind FD) : WindowsPlatformDispatch.Hooks (State U) Os E Kind FD

Equations

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