Pinned windows/foreign_items.rs file and handle arms. All use modern check_shim_sig with compiler system ABI and exact imported WinAPI types.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsFileDispatch.Operation : Type

• readFile : Operation
• writeFile : Operation
• create : Operation
• getInformation : Operation
• setInformation : Operation
• flush : Operation
• deleteFile : Operation
• setPointer : Operation
• moveFile : Operation
• stdHandle : Operation
• duplicate : Operation
• close : Operation
• currentProcess : Operation
• currentThread : Operation
• fullPath : Operation

@[instance_reducible]

instance Miri.Interpreter.WindowsFileDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsFileDispatch.instReprOperation : Repr Operation

Equations

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

inductive Miri.Interpreter.WindowsFileDispatch.ArgType : Type

• pointer : ArgType
• handle : ArgType
• u32 : ArgType
• i64 : ArgType
• bool : ArgType
• i32 : ArgType
• fileInfoClass : ArgType

@[instance_reducible]

instance Miri.Interpreter.WindowsFileDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsFileDispatch.instReprArgType : Repr ArgType

Equations

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

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

Equations

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

structure Miri.Interpreter.WindowsFileDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

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

Equations

• Miri.Interpreter.WindowsFileDispatch.parse "NtReadFile" = some Miri.Interpreter.WindowsFileDispatch.Operation.readFile
• Miri.Interpreter.WindowsFileDispatch.parse "NtWriteFile" = some Miri.Interpreter.WindowsFileDispatch.Operation.writeFile
• Miri.Interpreter.WindowsFileDispatch.parse "CreateFileW" = some Miri.Interpreter.WindowsFileDispatch.Operation.create
• Miri.Interpreter.WindowsFileDispatch.parse "GetFileInformationByHandle" = some Miri.Interpreter.WindowsFileDispatch.Operation.getInformation
• Miri.Interpreter.WindowsFileDispatch.parse "SetFileInformationByHandle" = some Miri.Interpreter.WindowsFileDispatch.Operation.setInformation
• Miri.Interpreter.WindowsFileDispatch.parse "FlushFileBuffers" = some Miri.Interpreter.WindowsFileDispatch.Operation.flush
• Miri.Interpreter.WindowsFileDispatch.parse "DeleteFileW" = some Miri.Interpreter.WindowsFileDispatch.Operation.deleteFile
• Miri.Interpreter.WindowsFileDispatch.parse "SetFilePointerEx" = some Miri.Interpreter.WindowsFileDispatch.Operation.setPointer
• Miri.Interpreter.WindowsFileDispatch.parse "MoveFileExW" = some Miri.Interpreter.WindowsFileDispatch.Operation.moveFile
• Miri.Interpreter.WindowsFileDispatch.parse "GetStdHandle" = some Miri.Interpreter.WindowsFileDispatch.Operation.stdHandle
• Miri.Interpreter.WindowsFileDispatch.parse "DuplicateHandle" = some Miri.Interpreter.WindowsFileDispatch.Operation.duplicate
• Miri.Interpreter.WindowsFileDispatch.parse "CloseHandle" = some Miri.Interpreter.WindowsFileDispatch.Operation.close
• Miri.Interpreter.WindowsFileDispatch.parse "GetCurrentProcess" = some Miri.Interpreter.WindowsFileDispatch.Operation.currentProcess
• Miri.Interpreter.WindowsFileDispatch.parse "GetCurrentThread" = some Miri.Interpreter.WindowsFileDispatch.Operation.currentThread
• Miri.Interpreter.WindowsFileDispatch.parse "GetFullPathNameW" = some Miri.Interpreter.WindowsFileDispatch.Operation.fullPath
• Miri.Interpreter.WindowsFileDispatch.parse x✝ = none

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

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.WindowsFileDispatch.signature Miri.Interpreter.WindowsFileDispatch.Operation.currentProcess = { args := #[], ret := Miri.Interpreter.WindowsFileDispatch.ArgType.handle }
• Miri.Interpreter.WindowsFileDispatch.signature Miri.Interpreter.WindowsFileDispatch.Operation.currentThread = { args := #[], ret := Miri.Interpreter.WindowsFileDispatch.ArgType.handle }

structure Miri.Interpreter.WindowsFileDispatch.Hooks (S F H D P HM T E K : Type) : Type

• paths : WindowsPaths.Hooks S F H D P HM T E K
• 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)

def Miri.Interpreter.WindowsFileDispatch.dispatch {S F H D P HM T E K : Type} (h : Hooks S F H D P HM T E K) (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.WindowsFileDispatch.bindWindows {S F H D P HM T E K Place Ptr B I : Type} (h : Hooks S F H D P HM T E K) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B I) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B I

Equations

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