Pinned unix/foreign_items.rs pthread synchronization dispatch. ABI records are compiler-produced, compared via source LayoutCompat and argument transmute.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.PthreadDispatch.ArgType : Type

• pointer : ArgType
• i32 : ArgType
• u32 : ArgType

@[instance_reducible]

instance Miri.Interpreter.PthreadDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadDispatch.instReprArgType : Repr ArgType

Equations

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

inductive Miri.Interpreter.PthreadDispatch.Operation : Type

• mutexattrInit : Operation
• mutexattrSettype : Operation
• mutexattrDestroy : Operation
• mutexInit : Operation
• mutexLock : Operation
• mutexTrylock : Operation
• mutexUnlock : Operation
• mutexDestroy : Operation
• rwlockRead : Operation
• rwlockTryread : Operation
• rwlockWrite : Operation
• rwlockTrywrite : Operation
• rwlockUnlock : Operation
• rwlockDestroy : Operation
• condattrInit : Operation
• condattrSetclock : Operation
• condattrGetclock : Operation
• condattrDestroy : Operation
• condInit : Operation
• condSignal : Operation
• condBroadcast : Operation
• condWait : Operation
• condTimedwait : Operation
• condDestroy : Operation
• semInit : Operation
• semWait : Operation
• semTimedwait : Operation
• semPost : Operation
• semDestroy : Operation

@[instance_reducible]

instance Miri.Interpreter.PthreadDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PthreadDispatch.instReprOperation : Repr Operation

Equations

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

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

Equations

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

def Miri.Interpreter.PthreadDispatch.parse (name : String) : Option Operation

Equations

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

def Miri.Interpreter.PthreadDispatch.argumentTypes : Operation → Array ArgType

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.PthreadDispatch.argumentTypes x✝ = #[Miri.Interpreter.PthreadDispatch.ArgType.pointer]

structure Miri.Interpreter.PthreadDispatch.Hooks (S R Duration : Type) : Type

• pthread : PthreadSync.Hooks S R Duration
• expectedAbi : Array ArgType → M S (ABI.FnAbi MIR.TyId)

  Exact nonvariadic extern C signature, returning i32; pointer entries are shim_sig wildcard-pointee raw pointers, not arbitrary pointer-sized integers.

• 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)
• readI32 : OpTy Memory.Provenance → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32

def Miri.Interpreter.PthreadDispatch.dispatch {S R T : Type} (budget : Nat) (h : Hooks S R T) (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.PthreadDispatch.bindUnix {S R T D Ptr B I : Type} (budget : Nat) (h : Hooks S R T) (base : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) Ptr B I) : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) Ptr B I

Install this family ahead of the remaining required Unix handlers, keeping ForeignItems native/math/allocator/return/MIR-fallback ordering unchanged.

Equations

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