Pinned unix/poll.rs. Compiler field/layout queries, actual memory access and monotonic deadline creation are mandatory leaves, never synthetic pollfd data.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.PollShims.DeferredBackend (S : Type) : Type

• legacy {S : Type} : DeferredBackend S
• typed {S : Type} (block : Nat → Array (Int32 × MPlaceTy Memory.Provenance) → MPlaceTy Memory.Provenance → Option Concurrency.ThreadDeadline → M S Unit) : DeferredBackend S

structure Miri.Interpreter.PollShims.Hooks (S F Iter : Type) : Type

• deferred : DeferredBackend S
• readiness : Readiness.Hooks S F
• hasRdHup : Bool

  True exactly for Linux, Android, FreeBSD, Illumos target OS.

• libcU16 : String → M S UInt16
• readI32 : OpTy Memory.Provenance → M S Int32
• readNfds : OpTy Memory.Provenance → M S UInt64

  Query nfds_t layout, read scalar, signed conversion at that size, checked u64.

• derefArray : OpTy Memory.Provenance → String → UInt64 → M S (MPlaceTy Memory.Provenance)
• arrayFields : MPlaceTy Memory.Provenance → M S Iter
• nextField : Iter → M S (Option (MPlaceTy Memory.Provenance × Iter))
• namedField : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• readFieldI32 : MPlaceTy Memory.Provenance → M S Int32
• readFieldU16 : MPlaceTy Memory.Provenance → M S UInt16
• writeU16 : UInt16 → MPlaceTy Memory.Provenance → M S Unit
• writeU32 : UInt32 → MPlaceTy Memory.Provenance → M S Unit
• lookupFd : Int32 → M S (Option F)

  Actual FD-table lookup clones a reference, including temporary is_some lookup.

• newWatcher : M S Nat
• deadlineMillis : UInt32 → M S Concurrency.ThreadDeadline
• iterationBudget : Nat

  Explicit execution resource for source effectful array iteration.

def Miri.Interpreter.PollShims.onError {S A : Type} (action : M S A) (cleanup : M S Unit) : M S A

Equations

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

def Miri.Interpreter.PollShims.block {S F : Type} (h : Readiness.Hooks S F) (deadline : Option Concurrency.ThreadDeadline) (callback : Concurrency.SyncRuntime.Callback S) : M S Unit

Equations

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

def Miri.Interpreter.PollShims.toFlags {S F I : Type} (h : Hooks S F I) (ready : Files.Readiness) : M S UInt16

Equations

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

def Miri.Interpreter.PollShims.fromFlags {S F I : Type} (h : Hooks S F I) (flags : UInt16) : M S Files.Readiness

Equations

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

def Miri.Interpreter.PollShims.checkedIncrement {S : Type} (value : UInt32) : M S UInt32

Equations

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

def Miri.Interpreter.PollShims.writeReady {S F I : Type} (budget : Nat) (h : Hooks S F I) (watcher : Nat) (interests : Array (Int32 × MPlaceTy Memory.Provenance)) : M S UInt32

ready_count is sampled before getReadyInterests processes delayed updates.

Equations

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

def Miri.Interpreter.PollShims.poll {S F I : Type} (budget : Nat) (h : Hooks S F I) (fds nfds timeout : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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