Matching pinned Unix environment/system-information foreign-item arms.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixEnvironmentDispatch.Operation : Type

• getenv : Operation
• setenv : Operation
• unsetenv : Operation
• cwd : Operation
• hostname : Operation
• chdir : Operation
• pid : Operation
• uname : Operation
• xuname : Operation
• sysconf : Operation
• strerror : Operation
• uid : Operation
• passwd : Operation
• environ : Operation

@[instance_reducible]

instance Miri.Interpreter.UnixEnvironmentDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixEnvironmentDispatch.instReprOperation : Repr Operation

Equations

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

inductive Miri.Interpreter.UnixEnvironmentDispatch.ArgType : Type

• i32 : ArgType
• pointer : ArgType
• sizeT : ArgType
• isize : ArgType
• pidT : ArgType
• uidT : ArgType

@[instance_reducible]

instance Miri.Interpreter.UnixEnvironmentDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixEnvironmentDispatch.instReprArgType : Repr ArgType

Equations

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

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

Equations

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

structure Miri.Interpreter.UnixEnvironmentDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

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

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.UnixEnvironmentDispatch.signature Miri.Interpreter.UnixEnvironmentDispatch.Operation.pid = { args := #[], ret := Miri.Interpreter.UnixEnvironmentDispatch.ArgType.pidT }
• Miri.Interpreter.UnixEnvironmentDispatch.signature Miri.Interpreter.UnixEnvironmentDispatch.Operation.uid = { args := #[], ret := Miri.Interpreter.UnixEnvironmentDispatch.ArgType.uidT }
• Miri.Interpreter.UnixEnvironmentDispatch.signature Miri.Interpreter.UnixEnvironmentDispatch.Operation.environ = { args := #[], ret := Miri.Interpreter.UnixEnvironmentDispatch.ArgType.pointer }

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

• env : UnixEnvironment.Hooks S O E K
• frameInStd : M S Bool
• expectedAbi : String → M S (ABI.FnAbi MIR.TyId)

  Exact compiler query keyed by the invoked foreign symbol.

• 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.UnixEnvironmentDispatch.parse (os name : String) : Option (Operation × Bool)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "getenv" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.getenv, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "setenv" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.setenv, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "unsetenv" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.unsetenv, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "getcwd" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.cwd, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "gethostname" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.hostname, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "chdir" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.chdir, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "getpid" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.pid, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "sysconf" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.sysconf, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "strerror_r" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.strerror, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "getuid" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.uid, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "geteuid" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.uid, false)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "getpwuid_r" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.passwd, true)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "__posix_getpwuid_r" = some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.passwd, true)
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "__xuname" = if (os == "freebsd") = true then some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.xuname, false) else none
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "__xpg_strerror_r" = if (os == "linux") = true then some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.strerror, true) else none
• Miri.Interpreter.UnixEnvironmentDispatch.parse os "_NSGetEnviron" = if (os == "macos") = true then some (Miri.Interpreter.UnixEnvironmentDispatch.Operation.environ, true) else none
• Miri.Interpreter.UnixEnvironmentDispatch.parse os name = none

def Miri.Interpreter.UnixEnvironmentDispatch.dispatch {S O E K : Type} (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.UnixEnvironmentDispatch.bindUnix {S O E K Place Ptr B Inst : Type} (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.