Common Unix foreign_items.rs pthread TLS and pthread_atfork arms. Only source-matched symbols evaluate signatures or operands.

@[reducible, inline]

abbrev Miri.Interpreter.UnixTlsDispatch.M (σ α : Type) : Type

Equations

• Miri.Interpreter.UnixTlsDispatch.M = EStateM Miri.Interpreter.StepError

structure Miri.Interpreter.UnixTlsDispatch.Hooks (S D B I : Type) : Type

• signatures : ShimSignatures.PrimitiveHooks Memory.Provenance S
• signature : String → M S (ABI.FnAbi MIR.TyId)
• keyLayout : M S LocalLayout
• dereference : OpTy Memory.Provenance → LocalLayout → M S (MPlaceTy Memory.Provenance)
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• getPointerFnInstance : Memory.Pointer (Option Memory.Provenance) → M S CallInstance
• currentUserRelevantSpan : M S MIR.SpanRef
• activeThread : M S Concurrency.ThreadId
• createKey : Option TlsDestructor → ABI.Size → M S TlsKey
• deleteKey : TlsKey → M S Unit
• load : TlsKey → Concurrency.ThreadId → M S (Memory.Pointer (Option Memory.Provenance))
• store : TlsKey → Concurrency.ThreadId → Memory.Pointer (Option Memory.Provenance) → M S Unit
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• writeNull : MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.UnixTlsDispatch.emulate {S D B I : Type} (h : Hooks S D B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S (Option ForeignItems.EmulateItemResult)

Equations

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

def Miri.Interpreter.UnixTlsDispatch.bind {S D B I : Type} (h : Hooks S D B I) (base : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

Equations

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