Pinned unix/fs.rs::open and files.rs::open_file_or_dir. Actual host path, metadata, varargs and filesystem effects are required; flags are target queries.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixOpen.Flag : Type

• readonly : Flag
• writeonly : Flag
• readwrite : Flag
• accessMode : Flag
• largefile : Flag
• tmpfile : Flag
• directory : Flag
• append : Flag
• trunc : Flag
• create : Flag
• exclusive : Flag
• cloexec : Flag
• nofollow : Flag
• atCwd : Flag

@[instance_reducible]

instance Miri.Interpreter.UnixOpen.instDecidableEqFlag : DecidableEq Flag

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixOpen.instReprFlag : Repr Flag

Equations

• Miri.Interpreter.UnixOpen.instReprFlag = { reprPrec := Miri.Interpreter.UnixOpen.instReprFlag.repr }

def Miri.Interpreter.UnixOpen.instReprFlag.repr : Flag → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.UnixOpen.ModeUse : Type

• tmpfile : ModeUse
• create : ModeUse

@[instance_reducible]

instance Miri.Interpreter.UnixOpen.instDecidableEqModeUse : DecidableEq ModeUse

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixOpen.instReprModeUse : Repr ModeUse

Equations

• Miri.Interpreter.UnixOpen.instReprModeUse = { reprPrec := Miri.Interpreter.UnixOpen.instReprModeUse.repr }

def Miri.Interpreter.UnixOpen.instReprModeUse.repr : ModeUse → Nat → Std.Format

Equations

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

structure Miri.Interpreter.UnixOpen.Options : Type

• read : Bool
• write : Bool
• append : Bool
• truncate : Bool
• create : Bool
• createNew : Bool
• mode : Option UInt32
• customFlags : UInt32

structure Miri.Interpreter.UnixOpen.Metadata : Type

• isDirectory : Bool
• isSymlink : Bool

inductive Miri.Interpreter.UnixOpen.Opened (H D : Type) : Type

• file {H D : Type} (handle : H) : Opened H D
• directory {H D : Type} (handle : D) : Opened H D

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

• fd : UnixFd.Hooks S H D O E Meta
• hostWindows : Bool
• flag : Flag → M S UInt32
• hostCustomFlag : Flag → M S UInt32
• readMode : ModeUse → M S UInt32
• isolationReject : String → M S Bool
• procAbsolute : Path → M S Bool
• diagnoseProc : M S Unit
• isAbsolute : Path → Bool
• isEmpty : Path → Bool
• isDot : Path → Bool
• emptyPath : Path
• openFile : Option D → Path → Options → M S (Except (IoError.HostError E) H)
• openDirectoryAsFile : Option D → Path → Options → M S (Except (IoError.HostError E) H)
• metadata : H → M S (Except (IoError.HostError E) Metadata)
• asDirectory : H → M S D
• dropFile : H → M S Unit
• dropDirectory : D → M S Unit
• permissionDenied : M S (IoError.HostError E)
• hostUsizeBits : Nat

def Miri.Interpreter.UnixOpen.openFileOrDir {S H D O E Meta P : Type} (h : Hooks S H D O E Meta P) (root : Option D) (path : P) (options : Options) : M S (Except (IoError.HostError E) (Opened H D))

Equations

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

def Miri.Interpreter.UnixOpen.openPath {S H D O E Meta P : Type} (h : Hooks S H D O E Meta P) (dirfd : Option Int32) (path : P) (inputFlags : UInt32) : M S Int32

Equations

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