Remaining portable Windows foreign-item policies from the pinned source. Allocation, compiler layouts and host error text are mandatory typed effects.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsPlatform.DynamicSymbol : Type

• setThreadDescription : DynamicSymbol
• getThreadDescription : DynamicSymbol
• waitOnAddress : DynamicSymbol
• wakeByAddressSingle : DynamicSymbol

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatform.instDecidableEqDynamicSymbol : DecidableEq DynamicSymbol

Equations

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

def Miri.Interpreter.WindowsPlatform.instReprDynamicSymbol.repr : DynamicSymbol → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatform.instReprDynamicSymbol : Repr DynamicSymbol

Equations

• Miri.Interpreter.WindowsPlatform.instReprDynamicSymbol = { reprPrec := Miri.Interpreter.WindowsPlatform.instReprDynamicSymbol.repr }

def Miri.Interpreter.WindowsPlatform.DynamicSymbol.name : DynamicSymbol → String

Equations

• Miri.Interpreter.WindowsPlatform.DynamicSymbol.setThreadDescription.name = "SetThreadDescription"
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.getThreadDescription.name = "GetThreadDescription"
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.waitOnAddress.name = "WaitOnAddress"
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.wakeByAddressSingle.name = "WakeByAddressSingle"

def Miri.Interpreter.WindowsPlatform.DynamicSymbol.parse : String → Option DynamicSymbol

Equations

• Miri.Interpreter.WindowsPlatform.DynamicSymbol.parse "SetThreadDescription" = some Miri.Interpreter.WindowsPlatform.DynamicSymbol.setThreadDescription
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.parse "GetThreadDescription" = some Miri.Interpreter.WindowsPlatform.DynamicSymbol.getThreadDescription
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.parse "WaitOnAddress" = some Miri.Interpreter.WindowsPlatform.DynamicSymbol.waitOnAddress
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.parse "WakeByAddressSingle" = some Miri.Interpreter.WindowsPlatform.DynamicSymbol.wakeByAddressSingle
• Miri.Interpreter.WindowsPlatform.DynamicSymbol.parse x✝ = none

inductive Miri.Interpreter.WindowsPlatform.HeapKind : Type

• heap : HeapKind
• local : HeapKind

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatform.instDecidableEqHeapKind : DecidableEq HeapKind

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatform.instReprHeapKind : Repr HeapKind

Equations

• Miri.Interpreter.WindowsPlatform.instReprHeapKind = { reprPrec := Miri.Interpreter.WindowsPlatform.instReprHeapKind.repr }

def Miri.Interpreter.WindowsPlatform.instReprHeapKind.repr : HeapKind → Nat → Std.Format

Equations

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

structure Miri.Interpreter.WindowsPlatform.Hooks (S O E K F : Type) : Type

• environment : WindowsEnvironment.Hooks S O E K
• handles : WindowsHandles.Hooks S F
• pointerSize : ABI.Size
• readUsize : OpTy Memory.Provenance → M S UInt64
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• allocate : ABI.Size → ABI.Align → Memory.AllocInit → HeapKind → M S (Memory.Pointer (Option Memory.Provenance))
• deallocate : Memory.Pointer (Option Memory.Provenance) → HeapKind → M S Unit
• reallocate : Memory.Pointer (Option Memory.Provenance) → ABI.Size → ABI.Align → HeapKind → M S (Memory.Pointer (Option Memory.Provenance))
• nullPointer : Memory.Pointer (Option Memory.Provenance)
• functionPointer : DynamicSymbol → M S (Memory.Pointer (Option Memory.Provenance))

  fn_ptr(FnVal::Other(...)): source always reserves a fresh identity.

• readCString : Memory.Pointer (Option Memory.Provenance) → M S ByteArray
• commandLine : M S (Option (Memory.Pointer (Option Memory.Provenance)))
• currentExe : M S (Option O)
• derefSystemInfo : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• derefPointer : OpTy Memory.Provenance → M S Unit
• projectNamed : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• zeroBytes : Memory.Pointer (Option Memory.Provenance) → UInt64 → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• hostErrorDisplay : IoError.HostError E → M S O
• unknownMessageDisplay : Memory.Scalar Memory.Provenance → M S O
• pageSize : UInt64
• numCpus : UInt32

def Miri.Interpreter.WindowsPlatform.heapAlloc {S O E K F : Type} (h : Hooks S O E K F) (handle flags size : 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.WindowsPlatform.heapFree {S O E K F : Type} (h : Hooks S O E K F) (handle flags pointer : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsPlatform.heapRealloc {S O E K F : Type} (h : Hooks S O E K F) (handle flags pointer size : 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.WindowsPlatform.localFree {S O E K F : Type} (h : Hooks S O E K F) (pointer : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsPlatform.ntStatusToDos : UInt32 → UInt32

Literal table in upstream, including fallback ERROR_MR_MID_NOT_FOUND.

Equations

• Miri.Interpreter.WindowsPlatform.ntStatusToDos 3221225634 = 19
• Miri.Interpreter.WindowsPlatform.ntStatusToDos 3221225624 = 1006
• Miri.Interpreter.WindowsPlatform.ntStatusToDos 3221225599 = 112
• Miri.Interpreter.WindowsPlatform.ntStatusToDos 3221225861 = 1117
• Miri.Interpreter.WindowsPlatform.ntStatusToDos 3221225506 = 5
• Miri.Interpreter.WindowsPlatform.ntStatusToDos x✝ = 317

def Miri.Interpreter.WindowsPlatform.systemInfo {S O E K F : Type} (h : Hooks S O E K F) (output : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.WindowsPlatform.getProcAddress {S O E K F : Type} (h : Hooks S O E K F) (module name : 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.WindowsPlatform.moduleFileName {S O E K F : Type} (h : Hooks S O E K F) (handle output size : 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.WindowsPlatform.formatMessage {S O E K F : Type} (h : Hooks S O E K F) (flags module message language buffer size arguments : OpTy Memory.Provenance) : M S UInt64

Equations

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

def Miri.Interpreter.WindowsPlatform.timer {S O E K F : Type} (h : Hooks S O E K F) (attributes name flags access : OpTy Memory.Provenance) : M S Unit

Equations

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