Pinned shims/unix/env.rs and the system-information helpers in unix/foreign_items.rs. Host operations are mandatory stateful effects.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixEnvironment.Hooks (S Os E Kind : Type) : Type

• os : String
• targetEnv : String
• strings : OsStrings.Hooks Memory.Provenance S Os Kind
• env : EnvVars.Hooks (Option Memory.Provenance) Os S
• process : EnvVars.ProcessHooks S
• errors : IoError.Hooks S E
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readUsize : OpTy Memory.Provenance → M S UInt64
• readI32 : OpTy Memory.Provenance → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• isolationReject : String → M S Bool
• checkNoIsolation : String → M S Unit
• currentDirectory : M S (Except (IoError.HostError E) Os)
• setCurrentDirectory : Os → M S (Except (IoError.HostError E) Unit)
• checkAccess : Memory.Pointer (Option Memory.Provenance) → UInt64 → M S Unit

  Exact check_ptr_access over the entire requested range, without a read/write.

• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit
• libcI32 : String → M S Int32
• libcScalar : String → M S (Memory.Scalar Memory.Provenance)
• pageSize : UInt64
• numCpus : UInt32
• architecture : String

  Compiler target.arch.desc_symbol and pinned CARGO_PKG_VERSION.

• miriVersion : String
• derefNamed : OpTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• derefPointerCell : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• projectNamed : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• writeUninit : MPlaceTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• homeDirectory : M S (Option Os)
• hostErrorDisplay : IoError.HostError E → M S Os
• unknownErrorDisplay : Memory.Scalar Memory.Provenance → M S Os

  Exact Scalar Display inside the source's unknown-errnum message.

def Miri.Interpreter.UnixEnvironment.getcwd {S O E K : Type} (h : Hooks S O E K) (buf 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.UnixEnvironment.chdir {S O E K : Type} (h : Hooks S O E K) (path : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixEnvironment.gethostname {S O E K : Type} (h : Hooks S O E K) (name len : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixEnvironment.uname {S O E K : Type} (h : Hooks S O E K) (op : OpTy Memory.Provenance) (fieldSize : Option (OpTy Memory.Provenance)) : M S Int32

Equations

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

def Miri.Interpreter.UnixEnvironment.sysconf {S O E K : Type} (h : Hooks S O E K) (op : OpTy Memory.Provenance) : M S Int64

Equations

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

def Miri.Interpreter.UnixEnvironment.strerror {S O E K : Type} (h : Hooks S O E K) (errnum buf len : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixEnvironment.getpwuid {S O E K : Type} (h : Hooks S O E K) (uid pwd buf len result : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Source std-only adapter: all passwd fields except pw_dir stay uninitialized.

Equations

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