Selected connected unix/foreign_items.rs FD/open dispatch. Varargs remain real imported operands and are consumed only by the flag-selected mode query.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixFdDispatch.Operation : Type

• read : Operation
• write : Operation
• pread : Operation
• pwrite : Operation
• close : Operation
• dup : Operation
• dup2 : Operation
• openPath : Operation
• openat : Operation

@[instance_reducible]

instance Miri.Interpreter.UnixFdDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixFdDispatch.instReprOperation : Repr Operation

Equations

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

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

Equations

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

inductive Miri.Interpreter.UnixFdDispatch.ArgType : Type

• i32 : ArgType
• pointer : ArgType
• usize : ArgType
• offT : ArgType
• isize : ArgType

@[instance_reducible]

instance Miri.Interpreter.UnixFdDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixFdDispatch.instReprArgType : Repr ArgType

Equations

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

structure Miri.Interpreter.UnixFdDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType
• variadic : Bool

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

Equations

• Miri.Interpreter.UnixFdDispatch.parse "read" = some Miri.Interpreter.UnixFdDispatch.Operation.read
• Miri.Interpreter.UnixFdDispatch.parse "write" = some Miri.Interpreter.UnixFdDispatch.Operation.write
• Miri.Interpreter.UnixFdDispatch.parse "pread" = some Miri.Interpreter.UnixFdDispatch.Operation.pread
• Miri.Interpreter.UnixFdDispatch.parse "pwrite" = some Miri.Interpreter.UnixFdDispatch.Operation.pwrite
• Miri.Interpreter.UnixFdDispatch.parse "close" = some Miri.Interpreter.UnixFdDispatch.Operation.close
• Miri.Interpreter.UnixFdDispatch.parse "dup" = some Miri.Interpreter.UnixFdDispatch.Operation.dup
• Miri.Interpreter.UnixFdDispatch.parse "dup2" = some Miri.Interpreter.UnixFdDispatch.Operation.dup2
• Miri.Interpreter.UnixFdDispatch.parse "open" = some Miri.Interpreter.UnixFdDispatch.Operation.openPath
• Miri.Interpreter.UnixFdDispatch.parse "openat" = some Miri.Interpreter.UnixFdDispatch.Operation.openat
• Miri.Interpreter.UnixFdDispatch.parse x✝ = none

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

Equations

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

structure Miri.Interpreter.UnixFdDispatch.Hooks (S H D O E Meta Path : Type) : Type

• file : UnixOpen.Hooks S H D O E Meta Path
• expectedAbi : String → Signature → M S (ABI.FnAbi MIR.TyId)

  Query the exact invoked symbol; aliases may have distinct compiler ABI rows.

• 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)
• readI32 : OpTy Memory.Provenance → M S Int32
• readUsize : OpTy Memory.Provenance → M S UInt64
• readOffset : OpTy Memory.Provenance → M S Int
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readPath : Memory.Pointer (Option Memory.Provenance) → M S Path
• readMode : String → ShimSignatures.Varargs Memory.Provenance → UnixOpen.ModeUse → M S UInt32

  Implements source check_varargs for mode_t (promoted to i32 if <4 bytes), including signed/unsigned C variadic value compatibility. No default mode.

• pollAndUnblockZero : M S Unit

def Miri.Interpreter.UnixFdDispatch.dispatch {S H D O E Meta P : Type} (h : Hooks S H D O E Meta P) (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.UnixFdDispatch.bindUnix {S H D O E Meta P Place Ptr B I : Type} (h : Hooks S H D O E Meta P) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B I) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) Ptr B I

This must be the outer Unix entry wrapper: its poll is the source's one entry poll. Remaining handlers supplied as base.unix must not poll again.

Equations

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