Pinned shims/tls.rs::TlsDtorsState::on_stack_empty (247-345), schedule_thread_atexit (392-417), schedule_next_pthread_tls_dtor (423-460), schedule_next_windows_fls_dtor (465-531), schedule_windows_tls_dtor (365-389). Each call schedules an actual canonical instance call; Pending is not success of the destructor body. Re-entry occurs only after its stack becomes empty.

inductive Miri.Interpreter.TlsTargetOs : Type

• linux : TlsTargetOs
• macos : TlsTargetOs
• windows : TlsTargetOs
• other (name : String) : TlsTargetOs

structure Miri.Interpreter.TlsPlatform : Type

• unix : Bool
• os : TlsTargetOs

inductive Miri.Interpreter.TlsCallAbi : Type

• cNoUnwind : TlsCallAbi
• systemNoUnwind : TlsCallAbi

structure Miri.Interpreter.TlsImmediate (P : Type) : Type

• value : Immediate P
• layout : ABI.TyAndLayout MIR.TyId

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

• init {P : Type} : TlsDtorsStage P
• initForExit {P : Type} : TlsDtorsStage P
• pthread {P : Type} (lastKey : Option TlsKey) : TlsDtorsStage P
• afterPthread {P : Type} : TlsDtorsStage P
• threadAtexit {P : Type} : TlsDtorsStage P
• windows {P : Type} (lastKey : Option TlsKey) (remainingKeys : List TlsKey) (callbacks : Array (TlsImmediate P × MIR.SpanRef)) : TlsDtorsStage P
• done {P : Type} : TlsDtorsStage P

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

• tls {Error : Type} (error : ThreadTlsError) : TlsExecutionError Error
• immediate {Error : Type} (error : ImmediateError) : TlsExecutionError Error
• scalar {Error : Type} (error : Memory.ScalarError) : TlsExecutionError Error
• exit {Error : Type} (error : ThreadExitError Error) : TlsExecutionError Error
• leaf {Error : Type} (error : Error) : TlsExecutionError Error

@[instance_reducible]

instance Miri.Interpreter.instReprTlsExecutionError {Error✝ : Type} [Repr Error✝] : Repr (TlsExecutionError Error✝)

Equations

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

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

Equations

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

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

• exit : ThreadExitState P E H
• data : ThreadTlsData P
• stage : TlsDtorsStage P

@[reducible, inline]

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

Equations

• Miri.Interpreter.TlsM P E H Error A = EStateM (Miri.Interpreter.TlsExecutionError Error) (Miri.Interpreter.TlsExecutionState P E H) A

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

• unitPtrMut : ABI.TyAndLayout MIR.TyId

  Actual target/machine layout cache, never inferred from a target triple.

• unitPtrConst : ABI.TyAndLayout MIR.TyId
• u32Layout : ABI.TyAndLayout MIR.TyId
• lookupLinkSection : String → TlsM P E H Error (Array (TlsImmediate P × MIR.SpanRef))
• getPointerFnInstance : Memory.Pointer (Option P) → TlsM P E H Error CallInstance
• evalWindows : String → String → TlsM P E H Error (Memory.Scalar P)
• callThreadRootFunction : CallInstance → TlsCallAbi → Array (OpTy P) → MIR.SpanRef → TlsM P E H Error Unit

  Source call_thread_root_function: ABI checks, real frames, arguments, no return destination, ReturnContinuation::Stop { cleanup: true }, empty-stack/origin-span checks, source span, and call errors are mandatory.

def Miri.Interpreter.tlsOnStackEmpty {P E H Error : Type} [Memory.PointerProvenance P] (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (queries : TlsDestructorQueries P E H Error) : TlsM P E H Error Concurrency.StackEmptyCallbackResult

One source on_stack_empty callback invocation. Stage changes which precede calls and mutations remain on errors; transitions after a failed lookup/call are not performed. There is no fuel cutoff for pthread destructor rounds.

Equations

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

def Miri.Interpreter.finishThreadOnStackEmpty {P E H Error ProvExtra : Type} [Memory.PointerProvenance P] (platform : TlsPlatform) (target : ABI.RuntimeTargetDataLayout) (destructors : TlsDestructorQueries P E H Error) (exit : ThreadExitQueries P E H ProvExtra Error) : TlsM P E H Error Concurrency.StackEmptyCallbackResult

Equations

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