Entire unix/fd.rs readv/writev policy. IO executes once against a temporary Stack allocation. Return/copy/free/error order is significant and retained.

@[reducible, inline]

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

Equations

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

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

• fd : UnixFd.Hooks S H D O E Meta
• readI32 : OpTy Memory.Provenance → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readSigned : OpTy Memory.Provenance → M S Int
• arrayPlace : Memory.Pointer (Option Memory.Provenance) → UInt64 → M S (MPlaceTy Memory.Provenance)
• startArray : MPlaceTy Memory.Provenance → M S ArrayProjection.Iterator
• index : ArrayProjection.Iterator → Nat → M S (MPlaceTy Memory.Provenance)
• field : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• readFieldSigned : MPlaceTy Memory.Provenance → M S Int
• readFieldPointer : MPlaceTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• allocateStack : ABI.Size → M S (Memory.Pointer (Option Memory.Provenance))
• deallocateStack : Memory.Pointer (Option Memory.Provenance) → M S Unit
• offsetInbounds : Memory.Pointer (Option Memory.Provenance) → Int64 → M S (Memory.Pointer (Option Memory.Provenance))
• copyNonoverlapping : Memory.Pointer (Option Memory.Provenance) → Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit
• writeTargetIsize : Nat → MPlaceTy Memory.Provenance → M S Unit
• hostUsizeBits : Nat
• checkedSum : Bool

  Source host build's ordinary-add overflow setting, not the MIR flag.

def Miri.Interpreter.UnixVectored.execute {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (fd iov count : OpTy Memory.Provenance) (position : Option (OpTy Memory.Provenance)) (write : Bool) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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