Exact source read/write finish captures from unix/fd.rs and windows/fs.rs. The data is the source FnOnce environment; it is not an instruction language. Callbacks retain no arbitrary interpreter function in persistent machine state.

@[reducible, inline]

abbrev Miri.Interpreter.IoCompletion.Dest : Type

Equations

• Miri.Interpreter.IoCompletion.Dest = Miri.Interpreter.IoCompletionData.Dest

@[reducible, inline]

abbrev Miri.Interpreter.IoCompletion.Buffer : Type

Equations

• Miri.Interpreter.IoCompletion.Buffer = Miri.Interpreter.IoCompletionData.Buffer

@[reducible, inline]

abbrev Miri.Interpreter.IoCompletion.Capture : Type

Equations

• Miri.Interpreter.IoCompletion.Capture = Miri.Interpreter.IoCompletionData.Capture

structure Miri.Interpreter.IoCompletion.Hooks (S E : Type) : Type

• writeInt : Int → Dest → EStateM StepError S Unit
• writeTargetIsize : Nat → Dest → EStateM StepError S Unit
• errnoNegOne : IoError.Error E → Dest → EStateM StepError S Unit
• deallocateStack : Memory.Pointer (Option Memory.Provenance) → EStateM StepError S Unit
• offsetInbounds : Memory.Pointer (Option Memory.Provenance) → Int64 → EStateM StepError S (Memory.Pointer (Option Memory.Provenance))
• copyNonoverlapping : Memory.Pointer (Option Memory.Provenance) → Memory.Pointer (Option Memory.Provenance) → ABI.Size → EStateM StepError S Unit

def Miri.Interpreter.IoCompletion.invoke {S E : Type} (h : Hooks S E) (capture : Capture) (result : Files.Result E Nat) : EStateM StepError S Unit

Readv writes the result before copying/freeing. Writev frees before writing its result. Failure retains every completed store/copy/free, as in source.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.IoCompletion.invoke h (Miri.Interpreter.IoCompletionData.Capture.unixScalar count dest) (Except.error error) = h.errnoNegOne error dest