Linux and Android foreign_items.rs legacy eventfd wrapper.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.EventFdDispatch.Hooks (S F D MD B I : Type) : Type

• event : EventFd.Hooks S F
• foreign : ForeignItems.Hooks Memory.Provenance S D MD (Memory.Pointer (Option Memory.Provenance)) B I
• writeI32 : Int32 → MD → M S Unit

structure Miri.Interpreter.EventFdDispatch.SourceHooks (S F : Type) : Type

Nonrecursive eventfd operations used while assembling a source callback dispatcher. The caller supplies the exact source OS and symbol-clash operation, without needing a second, partially assembled Unix dispatcher.

• event : EventFd.Hooks S F
• os : String
• checkSymbolClash : String → M S Unit
• writeI32 : Int32 → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.EventFdDispatch.emulateSource {S F : Type} (h : SourceHooks S F) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S (Option ForeignItems.EmulateItemResult)

Equations

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

def Miri.Interpreter.EventFdDispatch.emulate {S F D MD B I : Type} (h : Hooks S F D MD B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MD) : M S (Option ForeignItems.EmulateItemResult)

Equations

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

def Miri.Interpreter.EventFdDispatch.bind {S F D MD B I : Type} (h : Hooks S F D MD B I) : ForeignItems.Hooks Memory.Provenance S D MD (Memory.Pointer (Option Memory.Provenance)) B I

Equations

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

def Miri.Interpreter.EventFdDispatch.bindWrite {K U C F D B I : Type} (place : PlaceHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (choice : C) (base : Hooks (MachineHooks.State K U) F D (MPlaceTy Memory.Provenance) B I) : Hooks (MachineHooks.State K U) F D (MPlaceTy Memory.Provenance) B I

Equations

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