Real FD dynamic dispatch for source flags and ioctl, using the canonical file/socket descriptions and the actual physical scalar/memory operations.

@[reducible, inline]

abbrev Miri.Interpreter.UnixFdControlMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.UnixFdControlMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.UnixFdControlMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.UnixFdControlMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

@[reducible, inline]

abbrev Miri.Interpreter.UnixFdControlMachine.Ref (H D O : Type) : Type

Equations

• Miri.Interpreter.UnixFdControlMachine.Ref H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

def Miri.Interpreter.UnixFdControlMachine.bind {Place K U O H D E R L T P Host C Meta B I : Type} [DecidableEq K] (access : ValidityMachine.Access K U) (descriptor : SocketMachine.Descriptor O) (virtual : VirtualSocket.Hooks (State K U) (Ref H D O) E) (tcp : TcpSocket.Hooks (State K U) (Ref H D O) R L T E P Host) (file : UnixFileOperations.Hooks (State K U) H E) (i32Layout : M K U LocalLayout) (i32PointerType : M K U MIR.TyId) (place : PlaceHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (choice : C) (base : UnixFdControlDispatch.Hooks (State K U) H D O E Meta Place B I) : UnixFdControlDispatch.Hooks (State K U) H D O E Meta Place B I

Equations

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