Pinned shims/time.rs. Host time, Chrono timezone data and target layouts are required effects; all source clock/error/control/arithmetic policy is here.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.TimeShims.Constant : Type

• realtime : Constant
• monotonic : Constant
• realtimeCoarse : Constant
• monotonicCoarse : Constant
• uptimeRaw : Constant
• timerAbstime : Constant

@[instance_reducible]

instance Miri.Interpreter.TimeShims.instDecidableEqConstant : DecidableEq Constant

Equations

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

@[instance_reducible]

instance Miri.Interpreter.TimeShims.instReprConstant : Repr Constant

Equations

• Miri.Interpreter.TimeShims.instReprConstant = { reprPrec := Miri.Interpreter.TimeShims.instReprConstant.repr }

def Miri.Interpreter.TimeShims.instReprConstant.repr : Constant → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.TimeShims.Layout : Type

• inferred : Layout
• timespec : Layout
• filetime : Layout
• i64 : Layout
• u64 : Layout
• machTimebase : Layout

@[instance_reducible]

instance Miri.Interpreter.TimeShims.instDecidableEqLayout : DecidableEq Layout

Equations

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

@[instance_reducible]

instance Miri.Interpreter.TimeShims.instReprLayout : Repr Layout

Equations

• Miri.Interpreter.TimeShims.instReprLayout = { reprPrec := Miri.Interpreter.TimeShims.instReprLayout.repr }

def Miri.Interpreter.TimeShims.instReprLayout.repr : Layout → Nat → Std.Format

Equations

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

structure Miri.Interpreter.TimeShims.BrokenDown : Type

• second : Nat
• minute : Nat
• hour : Nat
• day : Nat
• month0 : Nat
• weekdaySunday : Nat
• ordinal0 : Nat
• year : Int32
• offsetSeconds : Int32

structure Miri.Interpreter.TimeShims.Hooks (S Host System TZ Timestamp : Type) : Type

• family : ForeignItems.Family
• os : String
• communicate : Bool
• host : Clock.HostHooks Host System S
• monotonic : M S (Clock.Monotonic Host)
• encodeDeadline : Clock.Deadline Host System → M S Concurrency.ThreadDeadline
• runtime : Concurrency.SyncRuntime.Hooks S Nat Int32 (MPlaceTy Memory.Provenance)
• noIsolation : String → M S Unit
• systemDurationSinceUnix : System → M S (Option Clock.Duration)
• constant : Constant → M S (Memory.Scalar Memory.Provenance)
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• scalarSigned : Memory.Scalar Memory.Provenance → ABI.Size → M S Int
• clockIdSize : M S ABI.Size
• readI32 : OpTy Memory.Provenance → M S Int32
• readU32 : OpTy Memory.Provenance → M S UInt32
• readU64 : OpTy Memory.Provenance → M S UInt64
• deref : OpTy Memory.Provenance → Layout → M S (MPlaceTy Memory.Provenance)
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• projectNamed : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• readSignedPlace : MPlaceTy Memory.Provenance → M S Int
• writeFields : Array Int → MPlaceTy Memory.Provenance → M S Unit
• writeNamed : Array (String × Int) → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writePointer : Memory.Pointer (Option Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit
• dedupBytes : ByteArray → M S (Memory.Pointer (Option Memory.Provenance))
• setEinvalAndReturnNeg1 : M S Int32
• utcTimestamp : Int64 → M S (Option Timestamp)

  Source DateTime::from_timestamp(...). None is its source assertion failure.

• getTimezoneEnv : M S (Option (Except Unit String))
• utc : TZ
• parseTimezone : String → M S (Option TZ)
• withTimezone : Timestamp → TZ → M S BrokenDown

def Miri.Interpreter.TimeShims.systemTimeToDuration {S H Y Z T : Type} (h : Hooks S H Y Z T) (time : Y) : M S Clock.Duration

Equations

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

def Miri.Interpreter.TimeShims.parseClockId {S H Y Z T : Type} (h : Hooks S H Y Z T) (id : Memory.Scalar Memory.Provenance) : M S (Option Clock.TimeoutClock)

Equations

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

def Miri.Interpreter.TimeShims.clockGettime {S H Y Z T : Type} (h : Hooks S H Y Z T) (id tp : OpTy Memory.Provenance) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.TimeShims.gettimeofday {S H Y Z T : Type} (h : Hooks S H Y Z T) (tv tz : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.readTimespec {S H Y Z T : Type} (h : Hooks S H Y Z T) (place : MPlaceTy Memory.Provenance) : M S (Option Clock.Duration)

Equations

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

def Miri.Interpreter.TimeShims.readTimeval {S H Y Z T : Type} (h : Hooks S H Y Z T) (place : MPlaceTy Memory.Provenance) : M S (Option Clock.Duration)

Equations

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

def Miri.Interpreter.TimeShims.nanosleep {S H Y Z T : Type} (h : Hooks S H Y Z T) (duration rem : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.clockNanosleep {S H Y Z T : Type} (h : Hooks S H Y Z T) (clock flags spec rem : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.sleep {S H Y Z T : Type} (h : Hooks S H Y Z T) (timeout : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.TimeShims.systemTimeSinceWindowsEpoch {S H Y Z T : Type} (h : Hooks S H Y Z T) (time : Y) : M S Clock.Duration

Equations

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

def Miri.Interpreter.TimeShims.windowsTicksFor (duration : Clock.Duration) : Except StepError UInt64

Equations

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

def Miri.Interpreter.TimeShims.getSystemTimeAsFileTime {S H Y Z T : Type} (h : Hooks S H Y Z T) (name : String) (op : OpTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.TimeShims.queryPerformanceCounter {S H Y Z T : Type} (h : Hooks S H Y Z T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.queryPerformanceFrequency {S H Y Z T : Type} (h : Hooks S H Y Z T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.machAbsoluteTime {S H Y Z T : Type} (h : Hooks S H Y Z T) : M S UInt64

Equations

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

def Miri.Interpreter.TimeShims.machTimebaseInfo {S H Y Z T : Type} (h : Hooks S H Y Z T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.machWaitUntil {S H Y Z T : Type} (h : Hooks S H Y Z T) (op : OpTy Memory.Provenance) : M S Int32

Equations

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

def Miri.Interpreter.TimeShims.localtimeR {S H Y Z T : Type} (h : Hooks S H Y Z T) (timep result : OpTy Memory.Provenance) : M S (Memory.Pointer (Option Memory.Provenance))

Equations

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