Exact time entrypoints of Unix/macOS/Windows foreign-item dispatch. Mach entrypoints deliberately keep pinned deprecated lenient ABI checking.

@[reducible, inline]

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

Equations

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

inductive Miri.Interpreter.TimeShimDispatch.Operation : Type

• gettimeofday : Operation
• localtimeR : Operation
• clockGettime : Operation
• nanosleep : Operation
• clockNanosleep : Operation
• filetime : Operation
• preciseFiletime : Operation
• performanceCounter : Operation
• performanceFrequency : Operation
• sleep : Operation
• machAbsolute : Operation
• machTimebase : Operation
• machWait : Operation

@[instance_reducible]

instance Miri.Interpreter.TimeShimDispatch.instDecidableEqOperation : DecidableEq Operation

Equations

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

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

Equations

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

@[instance_reducible]

instance Miri.Interpreter.TimeShimDispatch.instReprOperation : Repr Operation

Equations

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

inductive Miri.Interpreter.TimeShimDispatch.ShimType : Type

• pointer : ShimType
• timevalPointer : ShimType
• timezonePointer : ShimType
• timeTPointer : ShimType
• tmPointer : ShimType
• timespecPointer : ShimType
• clockId : ShimType
• i32 : ShimType
• u32 : ShimType
• u64 : ShimType
• bool : ShimType
• unit : ShimType

@[instance_reducible]

instance Miri.Interpreter.TimeShimDispatch.instDecidableEqShimType : DecidableEq ShimType

Equations

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

def Miri.Interpreter.TimeShimDispatch.instReprShimType.repr : ShimType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.TimeShimDispatch.instReprShimType : Repr ShimType

Equations

• Miri.Interpreter.TimeShimDispatch.instReprShimType = { reprPrec := Miri.Interpreter.TimeShimDispatch.instReprShimType.repr }

structure Miri.Interpreter.TimeShimDispatch.Signature : Type

• systemAbi : Bool
• args : Array ShimType
• ret : ShimType

def Miri.Interpreter.TimeShimDispatch.instDecidableEqSignature.decEq (x✝ x✝¹ : Signature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.TimeShimDispatch.instDecidableEqSignature : DecidableEq Signature

Equations

• Miri.Interpreter.TimeShimDispatch.instDecidableEqSignature = Miri.Interpreter.TimeShimDispatch.instDecidableEqSignature.decEq

def Miri.Interpreter.TimeShimDispatch.instReprSignature.repr : Signature → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.TimeShimDispatch.instReprSignature : Repr Signature

Equations

• Miri.Interpreter.TimeShimDispatch.instReprSignature = { reprPrec := Miri.Interpreter.TimeShimDispatch.instReprSignature.repr }

def Miri.Interpreter.TimeShimDispatch.parse : String → Option Operation

Equations

• Miri.Interpreter.TimeShimDispatch.parse "gettimeofday" = some Miri.Interpreter.TimeShimDispatch.Operation.gettimeofday
• Miri.Interpreter.TimeShimDispatch.parse "localtime_r" = some Miri.Interpreter.TimeShimDispatch.Operation.localtimeR
• Miri.Interpreter.TimeShimDispatch.parse "clock_gettime" = some Miri.Interpreter.TimeShimDispatch.Operation.clockGettime
• Miri.Interpreter.TimeShimDispatch.parse "nanosleep" = some Miri.Interpreter.TimeShimDispatch.Operation.nanosleep
• Miri.Interpreter.TimeShimDispatch.parse "clock_nanosleep" = some Miri.Interpreter.TimeShimDispatch.Operation.clockNanosleep
• Miri.Interpreter.TimeShimDispatch.parse "GetSystemTimeAsFileTime" = some Miri.Interpreter.TimeShimDispatch.Operation.filetime
• Miri.Interpreter.TimeShimDispatch.parse "GetSystemTimePreciseAsFileTime" = some Miri.Interpreter.TimeShimDispatch.Operation.preciseFiletime
• Miri.Interpreter.TimeShimDispatch.parse "QueryPerformanceCounter" = some Miri.Interpreter.TimeShimDispatch.Operation.performanceCounter
• Miri.Interpreter.TimeShimDispatch.parse "QueryPerformanceFrequency" = some Miri.Interpreter.TimeShimDispatch.Operation.performanceFrequency
• Miri.Interpreter.TimeShimDispatch.parse "Sleep" = some Miri.Interpreter.TimeShimDispatch.Operation.sleep
• Miri.Interpreter.TimeShimDispatch.parse "mach_absolute_time" = some Miri.Interpreter.TimeShimDispatch.Operation.machAbsolute
• Miri.Interpreter.TimeShimDispatch.parse "mach_timebase_info" = some Miri.Interpreter.TimeShimDispatch.Operation.machTimebase
• Miri.Interpreter.TimeShimDispatch.parse "mach_wait_until" = some Miri.Interpreter.TimeShimDispatch.Operation.machWait
• Miri.Interpreter.TimeShimDispatch.parse x✝ = none

def Miri.Interpreter.TimeShimDispatch.signature : Operation → Signature

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.TimeShimDispatch.signature Miri.Interpreter.TimeShimDispatch.Operation.machAbsolute = { systemAbi := false, args := #[], ret := Miri.Interpreter.TimeShimDispatch.ShimType.u64 }

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

• time : TimeShims.Hooks S Host System TZ Timestamp
• expectedAbi : String → Signature → M S (ABI.FnAbi MIR.TyId)
• systemConvention : M S ABI.CanonAbi
• 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)

def Miri.Interpreter.TimeShimDispatch.dispatch {S H Y Z T : Type} (h : Hooks S H Y Z T) (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.TimeShimDispatch.bindForeign {S H Y Z T D Ptr B I : Type} (h : Hooks S H Y Z T) (base : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) Ptr B I) : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) Ptr B I

Equations

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