@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.WindowsEnvironmentDispatch.Operation : Type

• getVariable : Operation
• setVariable : Operation
• getStrings : Operation
• freeStrings : Operation
• cwd : Operation
• chdir : Operation
• profile : Operation
• pid : Operation
• temp : Operation

@[instance_reducible]

instance Miri.Interpreter.WindowsEnvironmentDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsEnvironmentDispatch.instReprOperation : Repr Operation

Equations

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

inductive Miri.Interpreter.WindowsEnvironmentDispatch.ArgType : Type

• pointer : ArgType
• handle : ArgType
• u32 : ArgType
• bool : ArgType

@[instance_reducible]

instance Miri.Interpreter.WindowsEnvironmentDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.WindowsEnvironmentDispatch.instReprArgType : Repr ArgType

Equations

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

structure Miri.Interpreter.WindowsEnvironmentDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

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

Equations

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

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

Equations

• Miri.Interpreter.WindowsEnvironmentDispatch.parse "GetEnvironmentVariableW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.getVariable
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "SetEnvironmentVariableW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.setVariable
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "GetEnvironmentStringsW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.getStrings
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "FreeEnvironmentStringsW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.freeStrings
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "GetCurrentDirectoryW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.cwd
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "SetCurrentDirectoryW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.chdir
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "GetUserProfileDirectoryW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.profile
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "GetCurrentProcessId" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.pid
• Miri.Interpreter.WindowsEnvironmentDispatch.parse "GetTempPathW" = some Miri.Interpreter.WindowsEnvironmentDispatch.Operation.temp
• Miri.Interpreter.WindowsEnvironmentDispatch.parse x✝ = none

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

• env : WindowsEnvironment.Hooks S O 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)
• 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

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