Pinned windows/foreign_items.rs:782–824 exact synchronization entrypoints.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsSyncDispatch.Operation : Type

• beginInitialize : Operation
• complete : Operation
• waitOnAddress : Operation
• wakeSingle : Operation
• wakeAll : Operation

@[instance_reducible]

instance Miri.Interpreter.WindowsSyncDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsSyncDispatch.instReprOperation : Repr Operation

Equations

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

inductive Miri.Interpreter.WindowsSyncDispatch.ArgType : Type

• pointer : ArgType
• u32 : ArgType
• usize : ArgType

@[instance_reducible]

instance Miri.Interpreter.WindowsSyncDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsSyncDispatch.instReprArgType : Repr ArgType

Equations

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

structure Miri.Interpreter.WindowsSyncDispatch.Signature : Type

• args : Array ArgType
• returnsBool : Bool

def Miri.Interpreter.WindowsSyncDispatch.instDecidableEqSignature.decEq (x✝ x✝¹ : Signature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsSyncDispatch.instDecidableEqSignature : DecidableEq Signature

Equations

• Miri.Interpreter.WindowsSyncDispatch.instDecidableEqSignature = Miri.Interpreter.WindowsSyncDispatch.instDecidableEqSignature.decEq

def Miri.Interpreter.WindowsSyncDispatch.instReprSignature.repr : Signature → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsSyncDispatch.instReprSignature : Repr Signature

Equations

• Miri.Interpreter.WindowsSyncDispatch.instReprSignature = { reprPrec := Miri.Interpreter.WindowsSyncDispatch.instReprSignature.repr }

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

Equations

• Miri.Interpreter.WindowsSyncDispatch.parse "InitOnceBeginInitialize" = some Miri.Interpreter.WindowsSyncDispatch.Operation.beginInitialize
• Miri.Interpreter.WindowsSyncDispatch.parse "InitOnceComplete" = some Miri.Interpreter.WindowsSyncDispatch.Operation.complete
• Miri.Interpreter.WindowsSyncDispatch.parse "WaitOnAddress" = some Miri.Interpreter.WindowsSyncDispatch.Operation.waitOnAddress
• Miri.Interpreter.WindowsSyncDispatch.parse "WakeByAddressSingle" = some Miri.Interpreter.WindowsSyncDispatch.Operation.wakeSingle
• Miri.Interpreter.WindowsSyncDispatch.parse "WakeByAddressAll" = some Miri.Interpreter.WindowsSyncDispatch.Operation.wakeAll
• Miri.Interpreter.WindowsSyncDispatch.parse x✝ = none

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

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsSyncDispatch.signature Miri.Interpreter.WindowsSyncDispatch.Operation.wakeSingle = { args := #[Miri.Interpreter.WindowsSyncDispatch.ArgType.pointer], returnsBool := false }
• Miri.Interpreter.WindowsSyncDispatch.signature Miri.Interpreter.WindowsSyncDispatch.Operation.wakeAll = { args := #[Miri.Interpreter.WindowsSyncDispatch.ArgType.pointer], returnsBool := false }

structure Miri.Interpreter.WindowsSyncDispatch.Hooks (S R : Type) : Type

• windows : WindowsSync.Hooks S R
• systemConvention : M S ABI.CanonAbi

  Exact target canonicalization of extern system (not a hardcoded Win64 assumption); compiler construction must use winapi::BOOL or () as requested.

• 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)

def Miri.Interpreter.WindowsSyncDispatch.dispatch {S R : Type} (h : Hooks S R) (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.WindowsSyncDispatch.bindWindows {S R D Ptr B I : Type} (h : Hooks S R) (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

Equations

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