@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsPlatformDispatch.Operation : Type

• heapAlloc : Operation
• heapFree : Operation
• heapRealloc : Operation
• localFree : Operation
• setError : Operation
• getError : Operation
• ntStatus : Operation
• systemInfo : Operation
• commandLine : Operation
• timer : Operation
• symbol : Operation
• exitProcess : Operation
• console : Operation
• moduleName : Operation
• formatMessage : Operation
• unwind : Operation

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatformDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatformDispatch.instReprOperation : Repr Operation

Equations

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

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

Equations

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

inductive Miri.Interpreter.WindowsPlatformDispatch.ArgType : Type

• pointer : ArgType
• handle : ArgType
• usize : ArgType
• u32 : ArgType
• bool : ArgType
• i32 : ArgType
• unit : ArgType
• module : ArgType
• farproc : ArgType
• localHandle : ArgType
• unwindReason : ArgType

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatformDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsPlatformDispatch.instReprArgType : Repr ArgType

Equations

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

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

Equations

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

structure Miri.Interpreter.WindowsPlatformDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

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

Equations

• Miri.Interpreter.WindowsPlatformDispatch.parse "HeapAlloc" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.heapAlloc
• Miri.Interpreter.WindowsPlatformDispatch.parse "HeapFree" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.heapFree
• Miri.Interpreter.WindowsPlatformDispatch.parse "HeapReAlloc" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.heapRealloc
• Miri.Interpreter.WindowsPlatformDispatch.parse "LocalFree" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.localFree
• Miri.Interpreter.WindowsPlatformDispatch.parse "SetLastError" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.setError
• Miri.Interpreter.WindowsPlatformDispatch.parse "GetLastError" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.getError
• Miri.Interpreter.WindowsPlatformDispatch.parse "RtlNtStatusToDosError" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.ntStatus
• Miri.Interpreter.WindowsPlatformDispatch.parse "GetSystemInfo" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.systemInfo
• Miri.Interpreter.WindowsPlatformDispatch.parse "GetCommandLineW" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.commandLine
• Miri.Interpreter.WindowsPlatformDispatch.parse "CreateWaitableTimerExW" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.timer
• Miri.Interpreter.WindowsPlatformDispatch.parse "GetProcAddress" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.symbol
• Miri.Interpreter.WindowsPlatformDispatch.parse "ExitProcess" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.exitProcess
• Miri.Interpreter.WindowsPlatformDispatch.parse "GetConsoleScreenBufferInfo" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.console
• Miri.Interpreter.WindowsPlatformDispatch.parse "GetModuleFileNameW" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.moduleName
• Miri.Interpreter.WindowsPlatformDispatch.parse "FormatMessageW" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.formatMessage
• Miri.Interpreter.WindowsPlatformDispatch.parse "_Unwind_RaiseException" = some Miri.Interpreter.WindowsPlatformDispatch.Operation.unwind
• Miri.Interpreter.WindowsPlatformDispatch.parse x✝ = none

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

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsPlatformDispatch.signature Miri.Interpreter.WindowsPlatformDispatch.Operation.getError = { args := #[], ret := Miri.Interpreter.WindowsPlatformDispatch.ArgType.u32 }
• Miri.Interpreter.WindowsPlatformDispatch.signature Miri.Interpreter.WindowsPlatformDispatch.Operation.commandLine = { args := #[], ret := Miri.Interpreter.WindowsPlatformDispatch.ArgType.pointer }

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

• platform : WindowsPlatform.Hooks S O E K 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
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• startExit : Int32 → M S Unit

  Replace active stack with ProgramExitHandler(ExitCalled), not normal return.

• targetEnv : String
• handleStartUnwind : OpTy Memory.Provenance → M S Unit

def Miri.Interpreter.WindowsPlatformDispatch.dispatch {S O E K F : Type} (h : Hooks S O E K 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.WindowsPlatformDispatch.bindWindows {S O E K F Place Ptr B Inst : Type} (h : Hooks S O E K 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.

def Miri.Interpreter.WindowsPlatformDispatch.bindUnwind {K U C Other O E Kind F : Type} (unwind : Unwind.Hooks K U C Other) (choice : C) (base : Hooks (MachineHooks.State K U) O E Kind F) : Hooks (MachineHooks.State K U) O E Kind F

Bind the actual unwind payload stack; this stores payloads and leaves control transfer to the returned NeedsUnwind, exactly as the source.

Equations

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