Complete pinned windows/thread.rs and the TLS/FLS/thread-description arm family of windows/foreign_items.rs. Handles and TLS are canonical source data.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.WindowsThread.Hooks (S F : Type) : Type

• handles : WindowsHandles.Hooks S F
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readImmediate : OpTy Memory.Provenance → M S (RvalueImmTy Memory.Provenance)
• readUsize : OpTy Memory.Provenance → M S UInt64
• readU32 : OpTy Memory.Provenance → M S UInt32
• u32Layout : M S LocalLayout
• dereference : OpTy Memory.Provenance → LocalLayout → M S (MPlaceTy Memory.Provenance)
• pointerLayout : M S LocalLayout
• windowsU32 : String → M S UInt32
• start : Option (MPlaceTy Memory.Provenance) → Memory.Pointer (Option Memory.Provenance) → RvalueImmTy Memory.Provenance → LocalLayout → M S Concurrency.ThreadId
• join : Concurrency.ThreadId → Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit

  Non-exclusive join_thread, not pthread join_thread_exclusive.

• getTls : M S (ThreadTlsData Memory.Provenance)
• putTls : ThreadTlsData Memory.Provenance → M S Unit
• tlsError : ThreadTlsError → StepError
• resolveDestructor : Memory.Pointer (Option Memory.Provenance) → M S TlsDestructor
• readWide : Memory.Pointer (Option Memory.Provenance) → M S (Array UInt16)
• putThreads : Concurrency.ThreadManager → M S Unit
• allocateName : ByteArray → M S (Memory.Pointer (Option Memory.Provenance))

  bytes_to_os_str followed by alloc_os_str_as_wide_str, WinLocal kind.

• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.WindowsThread.utf16Lossy (units : Array UInt16) : ByteArray

String::from_utf16_lossy: unmatched surrogates each emit U+FFFD.

Equations

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

def Miri.Interpreter.WindowsThread.create {S F : Type} (h : Hooks S F) (security stacksize start argument flags output : OpTy Memory.Provenance) : M S Concurrency.ThreadId

Equations

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

def Miri.Interpreter.WindowsThread.wait {S F : Type} (h : Hooks S F) (handle timeout : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsThread.tlsAlloc {S F : Type} (h : Hooks S F) (destructor : Option (OpTy Memory.Provenance)) (size : ABI.Size) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsThread.tlsGet {S F : Type} (h : Hooks S F) (key : OpTy Memory.Provenance) : M S (Memory.Pointer (Option Memory.Provenance))

Equations

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

def Miri.Interpreter.WindowsThread.tlsSet {S F : Type} (h : Hooks S F) (key value : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsThread.tlsFree {S F : Type} (h : Hooks S F) (fiber : Bool) (key : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsThread.setDescription {S F : Type} (h : Hooks S F) (handle name : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsThread.getDescription {S F : Type} (h : Hooks S F) (handle output : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsThread.getId {S F : Type} (h : Hooks S F) (handle : Option (OpTy Memory.Provenance)) : M S Concurrency.ThreadId

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsThread.getId h none = do let __do_lift ← h.handles.threads pure __do_lift.activeThread