Windows thread/TLS foreign arms, with compiler system ABI checking.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsThreadDispatch.Operation : Type

• create : Operation
• wait : Operation
• tlsAlloc : Operation
• flsAlloc : Operation
• tlsGet : Operation
• tlsSet : Operation
• tlsFree : Operation
• flsFree : Operation
• isFiber : Operation
• setDescription : Operation
• getDescription : Operation
• getId : Operation
• currentId : Operation

@[instance_reducible]

instance Miri.Interpreter.WindowsThreadDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

def Miri.Interpreter.WindowsThreadDispatch.instReprOperation.repr : Operation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsThreadDispatch.instReprOperation : Repr Operation

Equations

• Miri.Interpreter.WindowsThreadDispatch.instReprOperation = { reprPrec := Miri.Interpreter.WindowsThreadDispatch.instReprOperation.repr }

inductive Miri.Interpreter.WindowsThreadDispatch.ArgType : Type

• pointer : ArgType
• handle : ArgType
• usize : ArgType
• u32 : ArgType
• bool : ArgType
• i32 : ArgType
• flsCallback : ArgType

@[instance_reducible]

instance Miri.Interpreter.WindowsThreadDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

def Miri.Interpreter.WindowsThreadDispatch.instReprArgType.repr : ArgType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsThreadDispatch.instReprArgType : Repr ArgType

Equations

• Miri.Interpreter.WindowsThreadDispatch.instReprArgType = { reprPrec := Miri.Interpreter.WindowsThreadDispatch.instReprArgType.repr }

structure Miri.Interpreter.WindowsThreadDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

def Miri.Interpreter.WindowsThreadDispatch.parse : String → Option Operation

Equations

• Miri.Interpreter.WindowsThreadDispatch.parse "CreateThread" = some Miri.Interpreter.WindowsThreadDispatch.Operation.create
• Miri.Interpreter.WindowsThreadDispatch.parse "WaitForSingleObject" = some Miri.Interpreter.WindowsThreadDispatch.Operation.wait
• Miri.Interpreter.WindowsThreadDispatch.parse "TlsAlloc" = some Miri.Interpreter.WindowsThreadDispatch.Operation.tlsAlloc
• Miri.Interpreter.WindowsThreadDispatch.parse "FlsAlloc" = some Miri.Interpreter.WindowsThreadDispatch.Operation.flsAlloc
• Miri.Interpreter.WindowsThreadDispatch.parse "TlsGetValue" = some Miri.Interpreter.WindowsThreadDispatch.Operation.tlsGet
• Miri.Interpreter.WindowsThreadDispatch.parse "FlsGetValue" = some Miri.Interpreter.WindowsThreadDispatch.Operation.tlsGet
• Miri.Interpreter.WindowsThreadDispatch.parse "TlsSetValue" = some Miri.Interpreter.WindowsThreadDispatch.Operation.tlsSet
• Miri.Interpreter.WindowsThreadDispatch.parse "FlsSetValue" = some Miri.Interpreter.WindowsThreadDispatch.Operation.tlsSet
• Miri.Interpreter.WindowsThreadDispatch.parse "TlsFree" = some Miri.Interpreter.WindowsThreadDispatch.Operation.tlsFree
• Miri.Interpreter.WindowsThreadDispatch.parse "FlsFree" = some Miri.Interpreter.WindowsThreadDispatch.Operation.flsFree
• Miri.Interpreter.WindowsThreadDispatch.parse "IsThreadAFiber" = some Miri.Interpreter.WindowsThreadDispatch.Operation.isFiber
• Miri.Interpreter.WindowsThreadDispatch.parse "SetThreadDescription" = some Miri.Interpreter.WindowsThreadDispatch.Operation.setDescription
• Miri.Interpreter.WindowsThreadDispatch.parse "GetThreadDescription" = some Miri.Interpreter.WindowsThreadDispatch.Operation.getDescription
• Miri.Interpreter.WindowsThreadDispatch.parse "GetThreadId" = some Miri.Interpreter.WindowsThreadDispatch.Operation.getId
• Miri.Interpreter.WindowsThreadDispatch.parse "GetCurrentThreadId" = some Miri.Interpreter.WindowsThreadDispatch.Operation.currentId
• Miri.Interpreter.WindowsThreadDispatch.parse x✝ = none

def Miri.Interpreter.WindowsThreadDispatch.signature : Operation → Signature

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsThreadDispatch.signature Miri.Interpreter.WindowsThreadDispatch.Operation.tlsAlloc = { args := #[], ret := Miri.Interpreter.WindowsThreadDispatch.ArgType.u32 }
• Miri.Interpreter.WindowsThreadDispatch.signature Miri.Interpreter.WindowsThreadDispatch.Operation.currentId = { args := #[], ret := Miri.Interpreter.WindowsThreadDispatch.ArgType.u32 }
• Miri.Interpreter.WindowsThreadDispatch.signature Miri.Interpreter.WindowsThreadDispatch.Operation.isFiber = { args := #[], ret := Miri.Interpreter.WindowsThreadDispatch.ArgType.bool }

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

• thread : WindowsThread.Hooks S F
• systemConvention : M S ABI.CanonAbi
• expectedAbi : String → Signature → M S (ABI.FnAbi MIR.TyId)

  The exact shim symbol is part of the compiler query identity.

• argumentCompat : ABI.ArgAbi MIR.TyId → ABI.ArgAbi MIR.TyId → M S Bool
• checkSymbolClash : String → M S Unit
• transmute : OpTy Memory.Provenance → ABI.TyAndLayout MIR.TyId → M S (OpTy Memory.Provenance)
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.WindowsThreadDispatch.dispatch {S F : Type} (h : Hooks S F) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S ForeignItems.EmulateItemResult

Equations

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

def Miri.Interpreter.WindowsThreadDispatch.bindWindows {S F Place Ptr B Inst : Type} (h : Hooks S F) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B Inst) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B Inst

Equations

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