futimens/utimensat parsing and update policy from pinned unix/fs.rs. Host SystemTime checked arithmetic and real set_times operations are explicit.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.UnixFsTimes.Update (Time : Type) : Type

• omit {Time : Type} : Update Time
• set {Time : Type} (time : Time) : Update Time

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

• fd : UnixFsFd.Hooks S F D Path HM Time E Kind H
• systemNow : M S Time
• sinceEpoch : Clock.Duration → M S (Option Time)

  UNIX_EPOCH.checked_add(duration), preserving possible host overflow.

• indexedField : MPlaceTy Memory.Provenance → Nat → M S (MPlaceTy Memory.Provenance)
• readTargetIsize : MPlaceTy Memory.Provenance → M S Int
• libcTargetIsize : String → M S Int
• timespecLayout : M S LocalLayout
• ptrToPlace : Memory.Pointer (Option Memory.Provenance) → LocalLayout → MPlaceTy Memory.Provenance
• offsetPlace : MPlaceTy Memory.Provenance → ABI.Size → LocalLayout → M S (MPlaceTy Memory.Provenance)
• readTimespec : MPlaceTy Memory.Provenance → M S (Option Clock.Duration)

  Bind TimeShims.readTimespec, retaining its tv_sec/tv_nsec read/check order.

• setFileTimes : H → Update Time → Update Time → M S (Except (IoError.HostError E) Unit)
• setPathTimes : Path → Bool → Update Time → Update Time → M S (Except (IoError.HostError E) Unit)

def Miri.Interpreter.UnixFsTimes.parseSpec {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (place : MPlaceTy Memory.Provenance) : M S (Option (Update T))

Equations

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

def Miri.Interpreter.UnixFsTimes.parseTimes {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (pointer : Memory.Pointer (Option Memory.Provenance)) : M S (Option (Update T × Update T))

Equations

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

def Miri.Interpreter.UnixFsTimes.futimens {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number times : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.UnixFsTimes.utimensat {S F D P HM T E K H : Type} (h : Hooks S F D P HM T E K H) (number path times flags : OpTy Memory.Provenance) : M S Int32

Equations

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