Source Unix and selected OS filesystem dispatch. Expected ABI records come from compiler types including mode_t/off_t/stat/stat64, never type-by-size guesses.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixFsDispatch.Operation : Type

• unlink : Operation
• symlink : Operation
• linkat : Operation
• stat : Operation
• lstat : Operation
• fstat : Operation
• fstatat : Operation
• statx : Operation
• chmod : Operation
• fchmod : Operation
• rename : Operation
• mkdir : Operation
• rmdir : Operation
• opendir : Operation
• readdir : Operation
• dirfd : Operation
• closedir : Operation
• seek : Operation
• truncate : Operation
• fsync : Operation
• fdatasync : Operation
• futimens : Operation
• utimensat : Operation
• readlink : Operation
• advise : Operation
• posixAllocate : Operation
• allocate : Operation
• syncRange : Operation
• realpath : Operation
• mkstemp : Operation
• isatty : Operation
• flock : Operation

@[instance_reducible]

instance Miri.Interpreter.UnixFsDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixFsDispatch.instReprOperation : Repr Operation

Equations

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

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

Equations

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

inductive Miri.Interpreter.UnixFsDispatch.ArgType : Type

• pointer : ArgType
• i32 : ArgType
• usize : ArgType
• isize : ArgType
• modeT : ArgType
• offT : ArgType
• off64T : ArgType
• statPointer : ArgType
• stat64Pointer : ArgType

@[instance_reducible]

instance Miri.Interpreter.UnixFsDispatch.instDecidableEqArgType : DecidableEq ArgType

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixFsDispatch.instReprArgType : Repr ArgType

Equations

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

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

Equations

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

structure Miri.Interpreter.UnixFsDispatch.Signature : Type

• args : Array ArgType
• ret : ArgType

structure Miri.Interpreter.UnixFsDispatch.Request : Type

• operation : Operation
• signature : Signature
• legacy : Bool
• dirent : String
• directI64 : Bool

  Whether offset operands use literal to_i64 rather than layout-sized to_int.

def Miri.Interpreter.UnixFsDispatch.parse (os name : String) : Option Request

Equations

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

structure Miri.Interpreter.UnixFsDispatch.Hooks (S F D Path HM Time E Kind H ReadDir Entry : Type) : Type

• directories : UnixDirectories.Hooks S F D Path HM Time E Kind ReadDir Entry
• times : UnixFsTimes.Hooks S F D Path HM Time E Kind H
• temporary : UnixTempFile.Hooks S F D Path HM Time E Kind H
• expectedAbi : String → Signature → M S (ABI.FnAbi MIR.TyId)

  Query the compiler ABI by the exact source symbol. The locally parsed Signature only supplies the source argument-shape checks; it is never used to guess a rustc ABI.

• 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)
• readSignedAtLayout : OpTy Memory.Provenance → M S Int
• readI64 : OpTy Memory.Provenance → M S Int64
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• writeUsize : UInt64 → MPlaceTy Memory.Provenance → M S Unit
• flock : F → Bool → UnixFileOperations.LockOp → M S (Except (IoError.HostError E) Unit)
• communicate : Bool
• pollAndUnblockZero : M S Unit

def Miri.Interpreter.UnixFsDispatch.dispatch {S F D P HM T E K H R Ent : Type} (h : Hooks S F D P HM T E K H R Ent) (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.UnixFsDispatch.bindUnix {S F D P HM T E K H R Ent Place Ptr B I : Type} (h : Hooks S F D P HM T E K H R Ent) (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

Exactly one outer Unix wrapper performs entry poll; dispatch itself does not.

Equations

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