Pinned unix/virtual_socket.rs owned virtual socketpair/pipe protocol. No host network substitutes these source-local buffers.

@[reducible, inline]

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

Equations

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

def Miri.Interpreter.VirtualSocket.capacity : Nat

Equations

• Miri.Interpreter.VirtualSocket.capacity = 212992

inductive Miri.Interpreter.VirtualSocket.SocketType : Type

• socketpair : SocketType
• pipeRead : SocketType
• pipeWrite : SocketType

@[instance_reducible]

instance Miri.Interpreter.VirtualSocket.instDecidableEqSocketType : DecidableEq SocketType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.VirtualSocket.instReprSocketType : Repr SocketType

Equations

• Miri.Interpreter.VirtualSocket.instReprSocketType = { reprPrec := Miri.Interpreter.VirtualSocket.instReprSocketType.repr }

def Miri.Interpreter.VirtualSocket.instReprSocketType.repr : SocketType → Nat → Std.Format

Equations

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

structure Miri.Interpreter.VirtualSocket.Buffer : Type

• bytes : ByteArray
• clock : Concurrency.VClock

structure Miri.Interpreter.VirtualSocket.State : Type

• readbuf : Option Buffer
• peer : Option Files.WeakRef
• peerLostData : Bool
• blockedRead : Array Concurrency.ThreadId
• blockedWrite : Array Concurrency.ThreadId
• nonblock : Bool
• kind : SocketType

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

• readiness : Readiness.Hooks S F
• get : F → M S State
• put : F → State → M S Unit
• newSocket : State → M S F
• insert : F → M S Int32
• readBytes : Memory.Pointer (Option Memory.Provenance) → Nat → M S ByteArray
• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit
• libc : String → M S (Memory.Scalar Memory.Provenance)
• libcI32 : String → M S Int32
• errors : IoError.Hooks S E
• os : String
• readI32 : OpTy Memory.Provenance → M S Int32
• derefI32 : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• nextI32 : MPlaceTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• readFieldI32 : MPlaceTy Memory.Provenance → M S Int32
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• readIoctlArgument : M S (OpTy Memory.Provenance)
• wakeBudget : Nat

def Miri.Interpreter.VirtualSocket.name (value : State) : String

Equations

• Miri.Interpreter.VirtualSocket.name value = if (value.kind == Miri.Interpreter.VirtualSocket.SocketType.socketpair) = true then "socketpair" else "pipe"

def Miri.Interpreter.VirtualSocket.metadata (value : State) : String

Equations

• Miri.Interpreter.VirtualSocket.metadata value = if (value.kind == Miri.Interpreter.VirtualSocket.SocketType.socketpair) = true then "S_IFSOCK" else "S_IFIFO"

def Miri.Interpreter.VirtualSocket.asSocket (value : State) : Bool

Equations

• Miri.Interpreter.VirtualSocket.asSocket value = (value.kind == Miri.Interpreter.VirtualSocket.SocketType.socketpair)

def Miri.Interpreter.VirtualSocket.readiness {S F E : Type} (h : Hooks S F E) (socket : F) : M S Files.Readiness

Equations

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

def Miri.Interpreter.VirtualSocket.dropSocket {S F E : Type} (h : Hooks S F E) (value : State) : M S Unit

Called by actual last-FD drop before dropping its ReadinessWatched field.

Equations

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

def Miri.Interpreter.VirtualSocket.getFlags {S F E : Type} (h : Hooks S F E) (socket : F) : M S Int32

Equations

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

def Miri.Interpreter.VirtualSocket.setFlags {S F E : Type} (h : Hooks S F E) (socket : F) (flags : Int32) : M S Int32

Equations

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

def Miri.Interpreter.VirtualSocket.ioctl {S F E : Type} (h : Hooks S F E) (socket : F) (operation : Memory.Scalar Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.VirtualSocket.write {S F E : Type} (budget : Nat) (h : Hooks S F E) (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (nonblock : Bool) (finish : Files.Finish S E) : M S Unit

Consumes the actual owned socket ref. Blocking transfers it into the closure; success transfers both descriptions to readiness in source order.

Equations

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

def Miri.Interpreter.VirtualSocket.read {S F E : Type} (budget : Nat) (h : Hooks S F E) (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (nonblock : Bool) (finish : Files.Finish S E) : M S Unit

Equations

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

def Miri.Interpreter.VirtualSocket.recv {S F E : Type} (budget : Nat) (h : Hooks S F E) (socket : F) (pointer : Memory.Pointer (Option Memory.Provenance)) (length : Nat) (peek nonblock : Bool) (finish : Files.Finish S E) : M S Unit

recv rejects PEEK before delegating, unlike actual TCP sockets.

Equations

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

def Miri.Interpreter.VirtualSocket.socketpair {S F E : Type} (h : Hooks S F E) (domain kind protocol output : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.VirtualSocket.pipe2 {S F E : Type} (h : Hooks S F E) (output : OpTy Memory.Provenance) (flags : Option (OpTy Memory.Provenance)) : M S Int32

Equations

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