Pinned unix/fd.rs close/dup/dup2/read/write and read_from_fd/write_to_fd; plus FileHandle positional I/O from unix/fs.rs. Async finish is a real closure.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixFd.Hooks (S H D O E Meta : Type) : Type

• files : Files.Hooks S H D O E Meta
• errors : IoError.Hooks S E
• os : String
• communicate : Bool
• shortFdOperations : Bool
• targetIsizeMax : UInt64
• hostIsizeMax : UInt64
• table : M S (Files.Table (Files.Description H D O))
• putTable : Files.Table (Files.Description H D O) → M S Unit
• newReference : Files.Description H D O → M S (Files.Ref (Files.Description H D O))

  Actual Rc clone/drop semantics. Pending IO owns its transferred strong ref; weak-reference liveness must count those owners, not just table entries.

• cloneRef : Files.Ref (Files.Description H D O) → M S (Files.Ref (Files.Description H D O))
• dropRef : Files.Ref (Files.Description H D O) → M S Unit
• asUnix : Files.Ref (Files.Description H D O) → M S Unit
• removeFileNumInterests : Files.Ref (Files.Description H D O) → Int32 → M S Unit
• checkAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit
• randomShort : M S Bool
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• otherPositionalRead : Files.Ref (Files.Description H D O) → UInt64 → Memory.Pointer (Option Memory.Provenance) → Nat → Files.Finish S E → M S Unit
• otherPositionalWrite : Files.Ref (Files.Description H D O) → UInt64 → Memory.Pointer (Option Memory.Provenance) → Nat → Files.Finish S E → M S Unit

def Miri.Interpreter.UnixFd.close {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (number : Int32) : M S Int32

Equations

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

def Miri.Interpreter.UnixFd.dup {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (number : Int32) : M S Int32

Equations

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

def Miri.Interpreter.UnixFd.dup2 {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (old new : Int32) : M S Int32

Equations

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

def Miri.Interpreter.UnixFd.readWrite {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (number : Int32) (pointer : Memory.Pointer (Option Memory.Provenance)) (count : UInt64) (offset : Option Int) (write : Bool) (dest : MPlaceTy Memory.Provenance) : M S Unit

Full requested range is checked before count capping and FD lookup. The finish closure owns all return-value work even if the description blocks.

Equations

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

def Miri.Interpreter.UnixFd.transferDescription {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (ref : Files.Ref (Files.Description H D O)) (pointer : Memory.Pointer (Option Memory.Provenance)) (len : Nat) (offset : Option Int) (write : Bool) (finish : Files.Finish S E) : M S Unit

Source internal read_from_fd/write_to_fd entry: unlike read/write wrappers, no count capping or pre-lookup range check is inserted here. Ownership of ref is transferred to the actual operation, including a delayed finish callback.

Equations

• Miri.Interpreter.UnixFd.transferDescription h ref pointer len offset write finish = Miri.Interpreter.UnixFd.transfer✝ h ref pointer len offset write finish