unix/foreign_items.rs poll and Linux/Android foreign_items.rs epoll arms. No select/pselect/ppoll or epoll_pwait aliases occur in the pinned dispatch.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.PollDispatch.Operation : Type

• poll : Operation
• create : Operation
• control : Operation
• wait : Operation

@[instance_reducible]

instance Miri.Interpreter.PollDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

• Miri.Interpreter.PollDispatch.instDecidableEqOperation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.PollDispatch.instReprOperation.repr : Operation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.PollDispatch.instReprOperation : Repr Operation

Equations

• Miri.Interpreter.PollDispatch.instReprOperation = { reprPrec := Miri.Interpreter.PollDispatch.instReprOperation.repr }

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

• epoll : EpollShims.Hooks S F Iter
• os : String
• communicate : Bool
• pollAndUnblockZero : M S Unit
• pollAbi : M S (ABI.FnAbi MIR.TyId)

  Compiler construction of extern C fn(pointer,nfds_t,i32)->i32.

• argumentCompat : ABI.ArgAbi MIR.TyId → ABI.ArgAbi MIR.TyId → M S Bool
• checkSymbolClash : String → M S Unit
• transmute : OpTy Memory.Provenance → ABI.TyAndLayout MIR.TyId → M S (OpTy Memory.Provenance)

def Miri.Interpreter.PollDispatch.parse (os name : String) : Option Operation

Equations

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

def Miri.Interpreter.PollDispatch.dispatch {S F I : Type} (budget : Nat) (h : Hooks S F I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S ForeignItems.EmulateItemResult

Does not perform the Unix entry poll. Use bindUnix as the outer entry once, or compose dispatch behind another existing outer entry-poll wrapper.

Equations

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

def Miri.Interpreter.PollDispatch.bindUnix {S F I P Ptr B Inst : Type} (budget : Nat) (h : Hooks S F I) (base : ForeignItems.Hooks Memory.Provenance S P (MPlaceTy Memory.Provenance) Ptr B Inst) : ForeignItems.Hooks Memory.Provenance S P (MPlaceTy Memory.Provenance) Ptr B Inst

Equations

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