Pinned unix/socket_address.rs. Network bytes are independent of target endianness; native flowinfo/scope fields use typed scalar operations.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.SocketAddress.Address : Type

• v4 (bits : UInt32) (port : UInt16) : Address
• v6 (bits : BitVec 128) (port : UInt16) (flow scope : UInt32) : Address

def Miri.Interpreter.SocketAddress.instDecidableEqAddress.decEq (x✝ x✝¹ : Address) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.SocketAddress.instDecidableEqAddress : DecidableEq Address

Equations

• Miri.Interpreter.SocketAddress.instDecidableEqAddress = Miri.Interpreter.SocketAddress.instDecidableEqAddress.decEq

@[instance_reducible]

instance Miri.Interpreter.SocketAddress.instReprAddress : Repr Address

Equations

• Miri.Interpreter.SocketAddress.instReprAddress = { reprPrec := Miri.Interpreter.SocketAddress.instReprAddress.repr }

def Miri.Interpreter.SocketAddress.instReprAddress.repr : Address → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.SocketAddress.Kind : Type

• stack : Kind
• socketAddress : Kind
• machine : Kind

@[instance_reducible]

instance Miri.Interpreter.SocketAddress.instDecidableEqKind : DecidableEq Kind

Equations

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

def Miri.Interpreter.SocketAddress.instReprKind.repr : Kind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.SocketAddress.instReprKind : Repr Kind

Equations

• Miri.Interpreter.SocketAddress.instReprKind = { reprPrec := Miri.Interpreter.SocketAddress.instReprKind.repr }

structure Miri.Interpreter.SocketAddress.Hooks (S E Iterator : Type) : Type

• errors : IoError.Hooks S E
• gnu : Bool
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isLiteralNull : Memory.Pointer (Option Memory.Provenance) → Bool
• readCString : Memory.Pointer (Option Memory.Provenance) → M S ByteArray
• readScalar : MPlaceTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• readSigned : MPlaceTy Memory.Provenance → ABI.Size → M S Int
• readU32 : MPlaceTy Memory.Provenance → M S UInt32
• readSocklen : OpTy Memory.Provenance → M S UInt64
• layout : String → M S LocalLayout
• u128Layout : M S LocalLayout
• pointerLayout : M S LocalLayout
• derefAs : OpTy Memory.Provenance → LocalLayout → M S (MPlaceTy Memory.Provenance)
• ptrToPlace : Memory.Pointer (Option Memory.Provenance) → LocalLayout → MPlaceTy Memory.Provenance
• transmute : MPlaceTy Memory.Provenance → LocalLayout → M S (MPlaceTy Memory.Provenance)
• offsetZero : MPlaceTy Memory.Provenance → LocalLayout → M S (MPlaceTy Memory.Provenance)
• field : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• readBytes : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S ByteArray
• writeBytes : Memory.Pointer (Option Memory.Provenance) → ByteArray → M S Unit
• writeZeros : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit
• pointer : MPlaceTy Memory.Provenance → Memory.Pointer (Option Memory.Provenance)
• allocate : LocalLayout → Kind → M S (MPlaceTy Memory.Provenance)
• deallocate : Memory.Pointer (Option Memory.Provenance) → Kind → M S Unit
• memCopy : Memory.Pointer (Option Memory.Provenance) → Memory.Pointer (Option Memory.Provenance) → ABI.Size → Bool → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• readPlacePointer : MPlaceTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• libc : String → M S (Memory.Scalar Memory.Provenance)
• libcI32 : String → M S Int32
• scalarSigned : Memory.Scalar Memory.Provenance → ABI.Size → M S Int
• resolve : String → UInt16 → M S (Except (IoError.HostError E) Iterator)

  Actual host ToSocketAddrs iterator, including each next operation.

• nextAddress : Iterator → M S (Option (Address × Iterator))
• dropIterator : Iterator → M S Unit
• resolutionDiagnostic : IoError.HostError E → M S Unit
• listBudget : Nat

def Miri.Interpreter.SocketAddress.read {S E I : Type} (h : Hooks S E I) (address length : OpTy Memory.Provenance) (name : String) : M S (Except (IoError.Error E) Address)

Equations

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

def Miri.Interpreter.SocketAddress.write {S E I : Type} (h : Hooks S E I) (address : Address) (output length : Memory.Pointer (Option Memory.Provenance)) (name : String) : M S Unit

Equations

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

def Miri.Interpreter.SocketAddress.getaddrinfo {S E I : Type} (h : Hooks S E I) (node service hints result : OpTy Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.SocketAddress.freeaddrinfo {S E I : Type} (h : Hooks S E I) (operand : OpTy Memory.Provenance) : M S Unit

Equations

• Miri.Interpreter.SocketAddress.freeaddrinfo h operand = do let __do_lift ← h.readPointer operand Miri.Interpreter.SocketAddress.freeInfos✝ h __do_lift h.listBudget