FileHandle::{flock,get_flags} and DirHandle::get_flags, unix/fs.rs:143–190. The blocking lock is deliberately unavailable, exactly as in pinned Miri.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixFileOperations.LockOp : Type

• shared (nonblocking : Bool) : LockOp
• exclusive (nonblocking : Bool) : LockOp
• unlock : LockOp

inductive Miri.Interpreter.UnixFileOperations.TryLockError (E : Type) : Type

• host {E : Type} (error : IoError.HostError E) : TryLockError E
• wouldBlock {E : Type} : TryLockError E

structure Miri.Interpreter.UnixFileOperations.Hooks (S H E : Type) : Type

• tryLock : H → Bool → M S (Except (TryLockError E) Unit)
• unlock : H → M S (Except (IoError.HostError E) Unit)
• fromKind : IoError.ErrorKind → M S (IoError.HostError E)
• libc : String → M S (Memory.Scalar Memory.Provenance)

def Miri.Interpreter.UnixFileOperations.flock {S H E : Type} (h : Hooks S H E) (file : H) (communicate : Bool) (operation : LockOp) : M S (Except (IoError.HostError E) Unit)

Equations

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

def Miri.Interpreter.UnixFileOperations.fileFlags {S H E : Type} (h : Hooks S H E) (readable writable : Bool) : M S (Memory.Scalar Memory.Provenance)

Equations

• Miri.Interpreter.UnixFileOperations.fileFlags h true true = h.libc "O_RDWR"
• Miri.Interpreter.UnixFileOperations.fileFlags h true false = h.libc "O_RDONLY"
• Miri.Interpreter.UnixFileOperations.fileFlags h false true = h.libc "O_WRONLY"
• Miri.Interpreter.UnixFileOperations.fileFlags h false false = throw (Miri.Interpreter.StepError.invalidProgram "FileHandle flags unreachable path-only access")

def Miri.Interpreter.UnixFileOperations.directoryFlags {S H E : Type} (h : Hooks S H E) : M S (Memory.Scalar Memory.Provenance)

Equations

• Miri.Interpreter.UnixFileOperations.directoryFlags h = h.libc "O_RDONLY"

def Miri.Interpreter.UnixFileOperations.flockFd {S F D P HM T E : Type} (metadata : UnixFsMetadata.Hooks S F D P HM T E) (communicate : Bool) (operation : F → Bool → LockOp → M S (Except (IoError.HostError E) Unit)) (number flags : Int32) : M S Int32

unix/fd.rs::flock wrapper, including target constants after descriptor lookup.

Equations

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