Pinned unix/fd.rs fcntl and ioctl policies, preserving lazy target-constant queries, descriptor ownership, varargs checks and platform-specific guards.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

• fd : UnixFd.Hooks S H D O E Meta
• libc : String → M S (Memory.Scalar Memory.Provenance)
• libcI32 : String → M S Int32
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• readI32 : OpTy Memory.Provenance → M S Int32
• takeI32 : String → ShimSignatures.Varargs Memory.Provenance → M S (OpTy Memory.Provenance)
• getFlags : Ref H D O → M S (Memory.Scalar Memory.Provenance)
• setFlags : Ref H D O → Int32 → M S (Memory.Scalar Memory.Provenance)
• ioctl : Ref H D O → Memory.Scalar Memory.Provenance → ShimSignatures.Varargs Memory.Provenance → M S Int32
• frameInStd : M S Bool
• rejectIsolation : String → M S Bool

  Source reject_in_isolation effect, true iff configured Reject branch.

• fullSync : Int32 → M S (Memory.Scalar Memory.Provenance)

def Miri.Interpreter.UnixFdControl.ioctl {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (fd op : OpTy Memory.Provenance) (rest : ShimSignatures.Varargs Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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

def Miri.Interpreter.UnixFdControl.fcntl {S H D O E Meta : Type} (h : Hooks S H D O E Meta) (fd cmd : OpTy Memory.Provenance) (rest : ShimSignatures.Varargs Memory.Provenance) : M S (Memory.Scalar Memory.Provenance)

Equations

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