Pinned unix/fs.rs path mutations, readlink and realpath. Real filesystem operations are typed effects; no virtual or guessed host filesystem is supplied.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixFsPaths.Hooks (S F D Path HM Time E Kind : Type) : Type

• metadata : UnixFsMetadata.Hooks S F D Path HM Time E
• strings : OsStrings.Hooks Memory.Provenance S Path Kind
• cKind : Kind
• readMode : OpTy Memory.Provenance → M S UInt32
• readU16 : OpTy Memory.Provenance → M S UInt16
• readUsize : OpTy Memory.Provenance → M S UInt64
• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit
• procAbsolute : Path → M S Bool

  Host path::absolute(...).is_ok_and(starts_with("/proc")); errors map false.

• pathToString : Path → Option String
• currentExe : M S (Option Path)
• hostUsizeBits : Nat
• removeFile : Path → M S (Except (IoError.HostError E) Unit)
• removeDirectory : Path → M S (Except (IoError.HostError E) Unit)
• symlinkDirectory : Path → M S Bool
• linkTargetDirectory : Path → Path → M S Bool

  Windows link.parent().is_some_and(parent.join(target).is_dir()).

• createSymlink : Path → Path → Bool → M S (Except (IoError.HostError E) Unit)
• hardLink : Path → Path → M S (Except (IoError.HostError E) Unit)
• setPermissions : Path → UInt32 → M S (Except (IoError.HostError E) Unit)
• rename : Path → Path → M S (Except (IoError.HostError E) Unit)
• mkdir : Path → Option UInt32 → M S (Except (IoError.HostError E) Unit)
• readLink : Path → M S (Except (IoError.HostError E) Path)
• canonicalize : Path → M S (Except (IoError.HostError E) Path)

def Miri.Interpreter.UnixFsPaths.unlink {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.rmdir {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.symlink {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (target link : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.linkat {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (oldfd oldpath newfd newpath flags : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.chmod {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (op mode : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.rename {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (oldpath newpath : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.mkdir {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (op mode : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsPaths.readlink {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (op buffer size : OpTy Memory.Provenance) : M S Int64

Equations

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

def Miri.Interpreter.UnixFsPaths.realpath {S F D P HM T E K : Type} (h : Hooks S F D P HM T E K) (op processed : OpTy Memory.Provenance) : M S (Memory.Pointer (Option Memory.Provenance))

Equations

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