Remaining regular-file length/permissions/seek/sync policy in unix/fs.rs. Strong FD lookup/drop and actual host effects are mandatory.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixFsFd.File (H : Type) : Type

• handle : H
• readable : Bool
• writable : Bool

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

• paths : UnixFsPaths.Hooks S F D Path HM Time E Kind
• communicate : Bool
• asFile : F → Option (File H)
• seek : F → Bool → Files.SeekFrom → M S (Except (IoError.Error E) UInt64)
• isTty : F → Bool → M S Bool
• setLength : H → UInt64 → M S (Except (IoError.HostError E) Unit)
• fileLength : H → M S (Except (IoError.HostError E) UInt64)
• setPermissions : H → UInt32 → M S (Except (IoError.HostError E) Unit)
• sync : H → Bool → M S (Except (IoError.HostError E) Unit)

  False = File::sync_all, true = File::sync_data, not a success acknowledgement.

def Miri.Interpreter.UnixFsFd.truncate {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number : Int32) (length : Int) : M S Int32

Equations

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

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

Equations

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

def Miri.Interpreter.UnixFsFd.seek {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number : Int32) (offset : Int) (whence : Int32) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.UnixFsFd.allocateImpl {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number : Int32) (offset length : Int64) : M S (Except (IoError.Error E) Unit)

Equations

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

def Miri.Interpreter.UnixFsFd.posixAllocate {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number : Int32) (offset length : Int64) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.UnixFsFd.linuxAllocate {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number mode : Int32) (offset length : Int64) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsFd.syncFile {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number : Int32) (dataOnly : Bool) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsFd.syncRange {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number : Int32) (offset count : Int64) (flags : Int32) : M S Int32

Equations

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

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

Equations

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