Pinned eval.rs::ProgramExitHandler: run TLS cleanup, yield 256 times, then terminate with for_exit=true. Machine stop remains an explicit outcome.

inductive Miri.Interpreter.ProgramExitType : Type

• mainThreadFinish : ProgramExitType
• exitCalled : ProgramExitType

def Miri.Interpreter.instReprProgramExitType.repr : ProgramExitType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprProgramExitType : Repr ProgramExitType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqProgramExitType : DecidableEq ProgramExitType

Equations

• Miri.Interpreter.instDecidableEqProgramExitType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.Interpreter.ProgramExitStage : Type

• tls : ProgramExitStage
• yield (remaining : UInt32) : ProgramExitStage
• done : ProgramExitStage
• unreachable : ProgramExitStage

def Miri.Interpreter.instReprProgramExitStage.repr : ProgramExitStage → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprProgramExitStage : Repr ProgramExitStage

Equations

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

def Miri.Interpreter.instDecidableEqProgramExitStage.decEq (x✝ x✝¹ : ProgramExitStage) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq Miri.Interpreter.ProgramExitStage.tls Miri.Interpreter.ProgramExitStage.tls = isTrue ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq Miri.Interpreter.ProgramExitStage.tls (Miri.Interpreter.ProgramExitStage.yield remaining) = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq (Miri.Interpreter.ProgramExitStage.yield remaining) Miri.Interpreter.ProgramExitStage.tls = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq (Miri.Interpreter.ProgramExitStage.yield a) (Miri.Interpreter.ProgramExitStage.yield b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq (Miri.Interpreter.ProgramExitStage.yield remaining) Miri.Interpreter.ProgramExitStage.done = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq (Miri.Interpreter.ProgramExitStage.yield remaining) Miri.Interpreter.ProgramExitStage.unreachable = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq Miri.Interpreter.ProgramExitStage.done (Miri.Interpreter.ProgramExitStage.yield remaining) = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq Miri.Interpreter.ProgramExitStage.done Miri.Interpreter.ProgramExitStage.done = isTrue ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq Miri.Interpreter.ProgramExitStage.unreachable (Miri.Interpreter.ProgramExitStage.yield remaining) = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitStage.decEq Miri.Interpreter.ProgramExitStage.unreachable Miri.Interpreter.ProgramExitStage.unreachable = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqProgramExitStage : DecidableEq ProgramExitStage

Equations

• Miri.Interpreter.instDecidableEqProgramExitStage = Miri.Interpreter.instDecidableEqProgramExitStage.decEq

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

• execution : TlsExecutionState P E H
• stage : ProgramExitStage
• exitCode : Int32
• exitType : ProgramExitType

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

• tls {Error : Type} (error : TlsExecutionError Error) : ProgramExitError Error
• termination {Error : Type} (error : ThreadExitError Error) : ProgramExitError Error
• leaf {Error : Type} (error : Error) : ProgramExitError Error
• unreachableHandler {Error : Type} : ProgramExitError Error

@[instance_reducible]

instance Miri.Interpreter.instReprProgramExitError {Error✝ : Type} [Repr Error✝] : Repr (ProgramExitError Error✝)

Equations

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

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

Equations

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

inductive Miri.Interpreter.ProgramExitPoll : Type

• pending : ProgramExitPoll
• machineStop (exitCode : Int32) (leakCheck : Bool) : ProgramExitPoll

@[instance_reducible]

instance Miri.Interpreter.instReprProgramExitPoll : Repr ProgramExitPoll

Equations

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

def Miri.Interpreter.instReprProgramExitPoll.repr : ProgramExitPoll → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqProgramExitPoll : DecidableEq ProgramExitPoll

Equations

• Miri.Interpreter.instDecidableEqProgramExitPoll = Miri.Interpreter.instDecidableEqProgramExitPoll.decEq

def Miri.Interpreter.instDecidableEqProgramExitPoll.decEq (x✝ x✝¹ : ProgramExitPoll) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqProgramExitPoll.decEq Miri.Interpreter.ProgramExitPoll.pending Miri.Interpreter.ProgramExitPoll.pending = isTrue ⋯
• Miri.Interpreter.instDecidableEqProgramExitPoll.decEq Miri.Interpreter.ProgramExitPoll.pending (Miri.Interpreter.ProgramExitPoll.machineStop exitCode leakCheck) = isFalse ⋯
• Miri.Interpreter.instDecidableEqProgramExitPoll.decEq (Miri.Interpreter.ProgramExitPoll.machineStop exitCode leakCheck) Miri.Interpreter.ProgramExitPoll.pending = isFalse ⋯

@[reducible, inline]

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

Equations

• Miri.Interpreter.ProgramExitM P E H Error A = EStateM (Miri.Interpreter.ProgramExitError Error) (Miri.Interpreter.ProgramExitState P E H) A

def Miri.Interpreter.ProgramExitState.new {P E H : Type} (state : TlsExecutionState P E H) (exitCode : Int32) (exitType : ProgramExitType) : ProgramExitState P E H

Source constructs a fresh TlsDtorsState::new_for_exit, retaining the actual machine/TLS data. The handler is separate from normal-thread callback state.

Equations

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

def Miri.Interpreter.programExitOnStackEmpty {P E H Error ProvExtra : Type} [Memory.PointerProvenance P] (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (destructors : TlsDestructorQueries P E H Error) (termination : ThreadExitQueries P E H ProvExtra Error) : ProgramExitM P E H Error ProgramExitPoll

Actual ordered stateful exit protocol, including state changes before a failed callback. A source machine-stop outcome must stop the interpreter loop; it is not a normal Poll::Ready return from the callback.

Equations

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