Entire socket/address/pipe arm group in pinned unix/foreign_items.rs. Caller ABI construction uses compiler socklen_t, size_t, ssize_t records.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.SocketDispatch.Operation : Type

• socketpair : Operation
• pipe : Operation
• pipe2 : Operation
• create : Operation
• bind : Operation
• listen : Operation
• accept : Operation
• accept4 : Operation
• connect : Operation
• send : Operation
• recv : Operation
• setOption : Operation
• getOption : Operation
• localName : Operation
• peerName : Operation
• shutdown : Operation
• getaddrinfo : Operation
• freeaddrinfo : Operation

@[instance_reducible]

instance Miri.Interpreter.SocketDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.SocketDispatch.instReprOperation : Repr Operation

Equations

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

inductive Miri.Interpreter.SocketDispatch.ArgType : Type

• i32 : ArgType
• pointer : ArgType
• socklenT : ArgType
• sizeT : ArgType
• ssizeT : ArgType
• unit : ArgType

@[instance_reducible]

instance Miri.Interpreter.SocketDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.SocketDispatch.instReprArgType : Repr ArgType

Equations

• Miri.Interpreter.SocketDispatch.instReprArgType = { reprPrec := Miri.Interpreter.SocketDispatch.instReprArgType.repr }

def Miri.Interpreter.SocketDispatch.instReprArgType.repr : ArgType → Nat → Std.Format

Equations

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

structure Miri.Interpreter.SocketDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

def Miri.Interpreter.SocketDispatch.parse : String → Option Operation

Equations

• Miri.Interpreter.SocketDispatch.parse "socketpair" = some Miri.Interpreter.SocketDispatch.Operation.socketpair
• Miri.Interpreter.SocketDispatch.parse "pipe" = some Miri.Interpreter.SocketDispatch.Operation.pipe
• Miri.Interpreter.SocketDispatch.parse "pipe2" = some Miri.Interpreter.SocketDispatch.Operation.pipe2
• Miri.Interpreter.SocketDispatch.parse "socket" = some Miri.Interpreter.SocketDispatch.Operation.create
• Miri.Interpreter.SocketDispatch.parse "bind" = some Miri.Interpreter.SocketDispatch.Operation.bind
• Miri.Interpreter.SocketDispatch.parse "listen" = some Miri.Interpreter.SocketDispatch.Operation.listen
• Miri.Interpreter.SocketDispatch.parse "accept" = some Miri.Interpreter.SocketDispatch.Operation.accept
• Miri.Interpreter.SocketDispatch.parse "accept4" = some Miri.Interpreter.SocketDispatch.Operation.accept4
• Miri.Interpreter.SocketDispatch.parse "connect" = some Miri.Interpreter.SocketDispatch.Operation.connect
• Miri.Interpreter.SocketDispatch.parse "send" = some Miri.Interpreter.SocketDispatch.Operation.send
• Miri.Interpreter.SocketDispatch.parse "recv" = some Miri.Interpreter.SocketDispatch.Operation.recv
• Miri.Interpreter.SocketDispatch.parse "setsockopt" = some Miri.Interpreter.SocketDispatch.Operation.setOption
• Miri.Interpreter.SocketDispatch.parse "getsockopt" = some Miri.Interpreter.SocketDispatch.Operation.getOption
• Miri.Interpreter.SocketDispatch.parse "getsockname" = some Miri.Interpreter.SocketDispatch.Operation.localName
• Miri.Interpreter.SocketDispatch.parse "getpeername" = some Miri.Interpreter.SocketDispatch.Operation.peerName
• Miri.Interpreter.SocketDispatch.parse "shutdown" = some Miri.Interpreter.SocketDispatch.Operation.shutdown
• Miri.Interpreter.SocketDispatch.parse "getaddrinfo" = some Miri.Interpreter.SocketDispatch.Operation.getaddrinfo
• Miri.Interpreter.SocketDispatch.parse "freeaddrinfo" = some Miri.Interpreter.SocketDispatch.Operation.freeaddrinfo
• Miri.Interpreter.SocketDispatch.parse x✝ = none

def Miri.Interpreter.SocketDispatch.parseTarget (os name : String) : Option (Operation × Bool)

Equations

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

def Miri.Interpreter.SocketDispatch.signature : Operation → Signature

Equations

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

structure Miri.Interpreter.SocketDispatch.Hooks (S F E I : Type) : Type

• socket : Socket.Hooks S F E I
• virtual : VirtualSocket.Hooks S F E
• expectedAbi : String → M S (ABI.FnAbi MIR.TyId)

  Exact rustc signature query for this source symbol. Names are retained because target libc typedefs such as socklen_t cannot be reconstructed from their width or from the operation's coarse argument category.

• 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)
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• pollAndUnblockZero : M S Unit

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

Equations

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

def Miri.Interpreter.SocketDispatch.syscallAccept4 {S F E I : Type} (h : Hooks S F E I) (socket address length flags : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Called by the existing Linux syscall dispatcher only after its sequential check_varargs for [i32,*sockaddr,*socklen_t,i32]; extra varargs stay ignored.

Equations

• Miri.Interpreter.SocketDispatch.syscallAccept4 h socket address length flags dest = Miri.Interpreter.Socket.accept4 h.socket socket address length (some flags) dest

def Miri.Interpreter.SocketDispatch.bindUnix {S F E I Place Ptr B Inst : Type} (h : Hooks S F E I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B Inst) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B Inst

Equations

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