FileMetadata and stat/statx core from pinned unix/fs.rs. Optional host-only fields represent source absence, not unknown compiler metadata.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixFsMetadata.FileType : Type

• regular : FileType
• directory : FileType
• symlink : FileType
• socket : FileType
• fifo : FileType
• character : FileType
• block : FileType
• other : FileType

@[instance_reducible]

instance Miri.Interpreter.UnixFsMetadata.instDecidableEqFileType : DecidableEq FileType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixFsMetadata.instReprFileType : Repr FileType

Equations

• Miri.Interpreter.UnixFsMetadata.instReprFileType = { reprPrec := Miri.Interpreter.UnixFsMetadata.instReprFileType.repr }

def Miri.Interpreter.UnixFsMetadata.instReprFileType.repr : FileType → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.UnixFsMetadata.TimeField : Type

• created : TimeField
• accessed : TimeField
• modified : TimeField

@[instance_reducible]

instance Miri.Interpreter.UnixFsMetadata.instDecidableEqTimeField : DecidableEq TimeField

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixFsMetadata.instReprTimeField : Repr TimeField

Equations

• Miri.Interpreter.UnixFsMetadata.instReprTimeField = { reprPrec := Miri.Interpreter.UnixFsMetadata.instReprTimeField.repr }

def Miri.Interpreter.UnixFsMetadata.instReprTimeField.repr : TimeField → Nat → Std.Format

Equations

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

structure Miri.Interpreter.UnixFsMetadata.UnixFields : Type

• dev : UInt64
• ino : UInt64
• nlink : UInt64
• uid : UInt32
• gid : UInt32
• blksize : UInt64
• blocks : UInt64
• permissions : UInt32

structure Miri.Interpreter.UnixFsMetadata.Metadata : Type

• mode : UInt32
• size : UInt64
• created : Option (UInt64 × UInt32)
• accessed : Option (UInt64 × UInt32)
• modified : Option (UInt64 × UInt32)
• dev : Option UInt64
• ino : Option UInt64
• nlink : Option UInt64
• uid : Option UInt32
• gid : Option UInt32
• blksize : Option UInt64
• blocks : Option UInt64

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

• os : String
• hostUnix : Bool
• hostWindows : Bool
• errors : IoError.Hooks S E
• libcI32 : String → M S Int32
• libcU32 : String → M S UInt32
• libcMode : String → M S UInt32

  eval_libc followed by mode_t-sized unsigned conversion and checked u32.

• readI32 : OpTy Memory.Provenance → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• readPath : Memory.Pointer (Option Memory.Provenance) → M S Path
• isolationReject : String → M S Bool
• lookupFd : Int32 → M S (Option F)
• dropFd : F → M S Unit
• asDirectory : F → Option D
• fdMetadata : F → M S (Except (IoError.HostError E) HM ⊕ String)
• isEmpty : Path → Bool
• isAbsolute : Path → Bool
• isDot : Path → Bool
• emptyPath : Path
• metadata : Option D → Path → Bool → M S (Except (IoError.HostError E) HM)
• fileType : HM → FileType
• length : HM → UInt64
• time : HM → TimeField → M S (Except (IoError.HostError E) Time)
• sinceEpoch : Time → M S Clock.Duration

  Actual system_time_to_duration: before epoch remains interpreter error.

• unixFields : HM → UnixFields
• readonly : HM → Bool
• deref : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• derefAs : OpTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• writeFields : Array (String × Int) → MPlaceTy Memory.Provenance → M S Unit
• field : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• index : MPlaceTy Memory.Provenance → UInt64 → M S (MPlaceTy Memory.Provenance)
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.UnixFsMetadata.modeName (hostUnix : Bool) : FileType → String

Equations

• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.regular = "S_IFREG"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.directory = "S_IFDIR"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.symlink = "S_IFLNK"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.socket = if hostUnix = true then "S_IFSOCK" else "S_IFREG"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.fifo = if hostUnix = true then "S_IFIFO" else "S_IFREG"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.character = if hostUnix = true then "S_IFCHR" else "S_IFREG"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.block = if hostUnix = true then "S_IFBLK" else "S_IFREG"
• Miri.Interpreter.UnixFsMetadata.modeName hostUnix Miri.Interpreter.UnixFsMetadata.FileType.other = "S_IFREG"

def Miri.Interpreter.UnixFsMetadata.synthetic {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (mode : String) : M S Metadata

Equations

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

def Miri.Interpreter.UnixFsMetadata.fromHost {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (metadata : Except (IoError.HostError E) HM) : M S (Except (IoError.Error E) Metadata)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.UnixFsMetadata.fromHost h (Except.error a) = pure (Except.error (Miri.Interpreter.IoError.Error.host a))

def Miri.Interpreter.UnixFsMetadata.fromFd {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (number : Int32) : M S (Except (IoError.Error E) Metadata)

Equations

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

def Miri.Interpreter.UnixFsMetadata.atPath {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (number : Int32) (path : P) (nofollow empty : Bool) : M S (Except (IoError.Error E) Metadata)

Equations

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

def Miri.Interpreter.UnixFsMetadata.writeStat {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (metadata : Metadata) (buf : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsMetadata.stat {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (path buf : OpTy Memory.Provenance) (nofollow : Bool) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsMetadata.fstat {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (fd buf : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsMetadata.fstatat {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (fd path buf flags : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsMetadata.statx {S F D P HM T E : Type} (h : Hooks S F D P HM T E) (fd pathname flags mask buf : OpTy Memory.Provenance) : M S Int32

Equations

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