DirTable/DirStream and opendir/readdir/dirfd/closedir from pinned unix/fs.rs. Opaque DIR IDs are target usize scalars, not allocated or dereferenceable pointers.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixDirectories.Stream (ReadDir : Type) : Type

• host : ReadDir
• fd : Int32
• identity : Files.FdId
• specials : Array String
• entry : Option (Memory.Pointer (Option Memory.Provenance) × String)

structure Miri.Interpreter.UnixDirectories.Table (ReadDir : Type) : Type

• nextId : UInt64
• streams : Array (UInt64 × Stream ReadDir)

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

• paths : UnixFsPaths.Hooks S F D Path HM Time E Kind
• get : M S (Table ReadDir)
• put : Table ReadDir → M S Unit
• readDir : Path → M S (Except (IoError.HostError E) ReadDir)
• openDirectory : Path → M S (Except (IoError.HostError E) D)
• dropReadDir : ReadDir → M S Unit
• insertDirectory : D → M S (Int32 × Files.FdId)

  Owns/transfers the actual directory handle into FileOwnership + FD table.

• id : F → Files.FdId
• nextEntry : ReadDir → M S (Option (Except (IoError.HostError E) Entry))
• entryName : Entry → Path
• entryType : Entry → M S (Except (IoError.HostError E) UnixFsMetadata.FileType)
• entryInode : Entry → UInt64
• readUsize : OpTy Memory.Provenance → M S UInt64
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• direntLayout : String → M S LocalLayout

  Compiler dirent layout, last-field offset and ABI alignment; no inferred shape.

• allocateRuntime : ABI.Size → ABI.Align → M S (Memory.Pointer (Option Memory.Provenance))
• asPlace : Memory.Pointer (Option Memory.Provenance) → LocalLayout → MPlaceTy Memory.Provenance
• wrappingOffset : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S (Memory.Pointer (Option Memory.Provenance))
• optionalField : MPlaceTy Memory.Provenance → String → M S (Option (MPlaceTy Memory.Provenance))
• writeNull : MPlaceTy Memory.Provenance → M S Unit
• deallocateRuntime : Memory.Pointer (Option Memory.Provenance) → M S Unit
• closeFd : Int32 → M S Int32
• libcU8 : String → M S UInt8

def Miri.Interpreter.UnixDirectories.openDir {S F D P HM T E K R Ent : Type} (h : Hooks S F D P HM T E K R Ent) (name : OpTy Memory.Provenance) : M S UInt64

Equations

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

def Miri.Interpreter.UnixDirectories.readDir {S F D P HM T E K R Ent : Type} (h : Hooks S F D P HM T E K R Ent) (dir : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) (kind : String) : M S Unit

Equations

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

def Miri.Interpreter.UnixDirectories.dirFd {S F D P HM T E K R Ent : Type} (h : Hooks S F D P HM T E K R Ent) (dir : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.UnixDirectories.closeDir {S F D P HM T E K R Ent : Type} (h : Hooks S F D P HM T E K R Ent) (dir : OpTy Memory.Provenance) : M S Int32

Equations

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