Entire pinned windows/handle.rs runtime policy. Packing constants are Miri's private enum encoding, not guessed Windows ABI constants.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsHandles.Pseudo : Type

• currentThread : Pseudo
• currentProcess : Pseudo

@[instance_reducible]

instance Miri.Interpreter.WindowsHandles.instDecidableEqPseudo : DecidableEq Pseudo

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsHandles.instReprPseudo : Repr Pseudo

Equations

• Miri.Interpreter.WindowsHandles.instReprPseudo = { reprPrec := Miri.Interpreter.WindowsHandles.instReprPseudo.repr }

def Miri.Interpreter.WindowsHandles.instReprPseudo.repr : Pseudo → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.WindowsHandles.Handle : Type

• null : Handle
• pseudo (value : Pseudo) : Handle
• thread (id : Concurrency.ThreadId) : Handle
• file (fd : Int32) : Handle
• invalid : Handle

def Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (x✝ x✝¹ : Handle) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.null Miri.Interpreter.WindowsHandles.Handle.null = isTrue ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.null (Miri.Interpreter.WindowsHandles.Handle.pseudo value) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.null (Miri.Interpreter.WindowsHandles.Handle.thread id) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.null (Miri.Interpreter.WindowsHandles.Handle.file fd) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.pseudo value) Miri.Interpreter.WindowsHandles.Handle.null = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.pseudo value) (Miri.Interpreter.WindowsHandles.Handle.thread id) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.pseudo value) (Miri.Interpreter.WindowsHandles.Handle.file fd) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.pseudo value) Miri.Interpreter.WindowsHandles.Handle.invalid = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.thread id) Miri.Interpreter.WindowsHandles.Handle.null = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.thread id) (Miri.Interpreter.WindowsHandles.Handle.pseudo value) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.thread id) (Miri.Interpreter.WindowsHandles.Handle.file fd) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.thread id) Miri.Interpreter.WindowsHandles.Handle.invalid = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.file fd) Miri.Interpreter.WindowsHandles.Handle.null = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.file fd) (Miri.Interpreter.WindowsHandles.Handle.pseudo value) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.file fd) (Miri.Interpreter.WindowsHandles.Handle.thread id) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq (Miri.Interpreter.WindowsHandles.Handle.file fd) Miri.Interpreter.WindowsHandles.Handle.invalid = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.invalid (Miri.Interpreter.WindowsHandles.Handle.pseudo value) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.invalid (Miri.Interpreter.WindowsHandles.Handle.thread id) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.invalid (Miri.Interpreter.WindowsHandles.Handle.file fd) = isFalse ⋯
• Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq Miri.Interpreter.WindowsHandles.Handle.invalid Miri.Interpreter.WindowsHandles.Handle.invalid = isTrue ⋯

@[instance_reducible]

instance Miri.Interpreter.WindowsHandles.instDecidableEqHandle : DecidableEq Handle

Equations

• Miri.Interpreter.WindowsHandles.instDecidableEqHandle = Miri.Interpreter.WindowsHandles.instDecidableEqHandle.decEq

@[instance_reducible]

instance Miri.Interpreter.WindowsHandles.instReprHandle : Repr Handle

Equations

• Miri.Interpreter.WindowsHandles.instReprHandle = { reprPrec := Miri.Interpreter.WindowsHandles.instReprHandle.repr }

def Miri.Interpreter.WindowsHandles.instReprHandle.repr : Handle → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.WindowsHandles.HandleError : Type

• threadNotFound : HandleError
• invalidHandle : HandleError

@[instance_reducible]

instance Miri.Interpreter.WindowsHandles.instDecidableEqHandleError : DecidableEq HandleError

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsHandles.instReprHandleError : Repr HandleError

Equations

• Miri.Interpreter.WindowsHandles.instReprHandleError = { reprPrec := Miri.Interpreter.WindowsHandles.instReprHandleError.repr }

def Miri.Interpreter.WindowsHandles.instReprHandleError.repr : HandleError → Nat → Std.Format

Equations

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

def Miri.Interpreter.WindowsHandles.packed (handle : Handle) : Except StepError UInt32

Equations

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

def Miri.Interpreter.WindowsHandles.fromPacked (value : UInt32) : Option Handle

Equations

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

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

• pointerSize : ABI.Size
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• targetIsize : Memory.Scalar Memory.Provenance → M S Int

  Scalar.to_target_isize includes pointer-to-int/size errors.

• readI32 : OpTy Memory.Provenance → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• windows : String → M S (Memory.Scalar Memory.Provenance)
• scalarI32 : Memory.Scalar Memory.Provenance → M S Int32
• threads : M S Concurrency.ThreadManager
• detachThread : Concurrency.ThreadId → Bool → M S Unit
• lookupFd : Int32 → M S (Option F)
• insertFd : F → M S Int32

  Transfers one existing owned reference into actual FD table.

• removeFd : Int32 → M S (Option F)
• dropFd : F → M S Unit
• derefUsize : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.WindowsHandles.toScalar {S F : Type} (h : Hooks S F) (handle : Handle) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsHandles.tryFromScalar {S F : Type} (h : Hooks S F) (value : Memory.Scalar Memory.Provenance) : M S (Except HandleError Handle)

Equations

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

def Miri.Interpreter.WindowsHandles.invalid {S A : Type} (functionName : String) : M S A

Equations

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

def Miri.Interpreter.WindowsHandles.read {S F : Type} (h : Hooks S F) (value : OpTy Memory.Provenance) (functionName : String) : M S Handle

Equations

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

def Miri.Interpreter.WindowsHandles.stdHandle {S F : Type} (h : Hooks S F) (which : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsHandles.duplicate {S F : Type} (h : Hooks S F) (sourceProcess source targetProcess target access inherit options : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.WindowsHandles.close {S F : Type} (h : Hooks S F) (operand : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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