Pinned shims/tls.rs::TlsData (44-220). Keys retain actual typed runtime pointers, full destructor instances and source spans. NULL normalization uses source pointer addresses; no pointer is reconstructed from an opaque token.

@[reducible, inline]

abbrev Miri.Interpreter.TlsKey : Type

Equations

• Miri.Interpreter.TlsKey = Miri.ABI.U128

structure Miri.Interpreter.TlsDestructor : Type

• fnInstance : CallInstance
• span : MIR.SpanRef

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

• key : TlsKey
• data : Array (Concurrency.ThreadId × Memory.Pointer (Option P))
• destructor : Option TlsDestructor

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

• fnInstance : CallInstance
• data : Memory.Scalar P
• span : MIR.SpanRef

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

• nextKey : TlsKey
• keys : Array (TlsKeyEntry P)
• threadAtexit : Array (Concurrency.ThreadId × Array (ThreadAtexitEntry P))

inductive Miri.Interpreter.ThreadTlsError : Type

• keyCounterOverflow : ThreadTlsError
• keySpaceExhausted : ThreadTlsError
• duplicateKey : ThreadTlsError
• nonexistentKey (key : TlsKey) : ThreadTlsError
• destructorsRemain : ThreadTlsError
• size (error : ABI.SizeError) : ThreadTlsError
• nullDestructorData : ThreadTlsError

@[instance_reducible]

instance Miri.Interpreter.instReprThreadTlsError : Repr ThreadTlsError

Equations

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

def Miri.Interpreter.instReprThreadTlsError.repr : ThreadTlsError → Nat → Std.Format

Equations

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

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

All source GC-relevant values, including atexit arguments. Function instances and callback stages contain only compiler identities.

• pointer {P : Type} (value : Memory.Pointer (Option P)) : TlsProvenanceRoot P
• scalar {P : Type} (value : Memory.Scalar P) : TlsProvenanceRoot P

def Miri.Interpreter.ThreadTlsData.initial {P : Type} : ThreadTlsData P

Exact source TlsData::default. Windows forbids allocating key zero.

Equations

• Miri.Interpreter.ThreadTlsData.initial = { nextKey := 1#128, keys := #[], threadAtexit := #[] }

def Miri.Interpreter.ThreadTlsData.createKey {P : Type} (data : ThreadTlsData P) (destructor : Option TlsDestructor) (keySize : ABI.Size) : EStateM.Result ThreadTlsError (ThreadTlsData P) TlsKey

Equations

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

def Miri.Interpreter.ThreadTlsData.deleteKey {P : Type} (data : ThreadTlsData P) (key : TlsKey) : EStateM.Result ThreadTlsError (ThreadTlsData P) (TlsKeyEntry P)

Equations

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

def Miri.Interpreter.ThreadTlsData.load {P : Type} (data : ThreadTlsData P) (key : TlsKey) (thread : Concurrency.ThreadId) : Except ThreadTlsError (Memory.Pointer (Option P))

Equations

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

def Miri.Interpreter.ThreadTlsData.store {P : Type} (data : ThreadTlsData P) (key : TlsKey) (thread : Concurrency.ThreadId) (pointer : Memory.Pointer (Option P)) : Except ThreadTlsError (ThreadTlsData P)

Equations

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

def Miri.Interpreter.ThreadTlsData.addThreadAtexit {P : Type} (data : ThreadTlsData P) (thread : Concurrency.ThreadId) (entry : ThreadAtexitEntry P) : ThreadTlsData P

Equations

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

def Miri.Interpreter.ThreadTlsData.fetchDestructor {P : Type} (data : ThreadTlsData P) (lastKey : Option TlsKey) (thread : Concurrency.ThreadId) : Option (TlsDestructor × Memory.Pointer (Option P) × TlsKey) × ThreadTlsData P

Pthread keys are visited in BTreeMap numeric order and cleared before call. The caller restarts from None after reaching the end of the current round.

Equations

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

def Miri.Interpreter.ThreadTlsData.popThreadAtexit {P : Type} (data : ThreadTlsData P) (thread : Concurrency.ThreadId) : Option (ThreadAtexitEntry P) × ThreadTlsData P

Equations

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

def Miri.Interpreter.ThreadTlsData.deleteAllThreadTls {P : Type} (data : ThreadTlsData P) (thread : Concurrency.ThreadId) : EStateM.Result ThreadTlsError (ThreadTlsData P) Unit

Equations

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

def Miri.Interpreter.ThreadTlsData.leakAllThreadTls {P : Type} [Memory.PointerProvenance P] (data : ThreadTlsData P) (thread : Concurrency.ThreadId) (roots : Array Memory.AllocId) : Array Memory.AllocId

Equations

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

def Miri.Interpreter.ThreadTlsData.provenanceRoots {P : Type} (data : ThreadTlsData P) : Array (TlsProvenanceRoot P)

Exact fields visited by source VisitProvenance for TlsData. No integer address is mistaken for an allocation ID; consumers visit the typed values.

Equations

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