Time.lean🔗

Clock and Time Syscalls

Trusted model of the Linux AArch64 clock_gettime syscall (kernel/time/posix-timers.c, include/uapi/linux/time.h), defining SYS_CLOCK_GETTIME, the 16-byte struct timespec encoder encodeTimespec, and execClockGettime.

@[expose] public section

namespace Arm64

def SYS_CLOCK_GETTIMEL26–27 ↗#

Linux AArch64 clock_gettime syscall number (__NR_clock_gettime = 113, include/uapi/asm-generic/unistd.h:318, kernel/time/posix-timers.c:1150).

def SYS_CLOCK_GETTIME : BitVec 64 := 113#64

def encodeTimespecL29–32 ↗#

16-byte little-endian Linux AArch64 struct timespec (tv_sec at +0, tv_nsec at +8, matching put_timespec64 in kernel/time/time.c:89).

def encodeTimespec (ts : Timespec) : List (BitVec 8) :=
  leBytes64 ts.sec ++ leBytes64 (BitVec.ofNat 64 ts.nsec.val)

def execClockGettimeL34–59 ↗#

clock_gettime(clk_id, tp) (__NR_clock_gettime = 113, kernel/time/posix-timers.c:1150): models SYSCALL_DEFINE2(clock_gettime, ...) and the AArch64 vDSO __kernel_clock_gettime (lib/vdso/gettimeofday.c) for static POSIX clocks 0..7 (CLOCK_REALTIME = 0, CLOCK_MONOTONIC = 1, CLOCK_PROCESS_CPUTIME_ID = 2, CLOCK_THREAD_CPUTIME_ID = 3, CLOCK_MONOTONIC_RAW = 4, CLOCK_REALTIME_COARSE = 5, CLOCK_MONOTONIC_COARSE = 6, CLOCK_BOOTTIME = 7):

[INTENTIONAL_SCOPE]: if clk.toNat > 7, fails closed with .Exception "unmodeled clock_gettime clockid" without consuming an oracle entry;
if !s.mem.canWrite tp 16, returns EFAULT_RET (-EFAULT, matching put_timespec64 copy_to_user in kernel/time/time.c) without consuming an oracle entry;
[INTENTIONAL_OVERAPPROX]: queries ts := s.oracle.clockGettime s.oracleIdx, writes the 16-byte little-endian struct timespec (encodeTimespec ts), consumes one oracle entry via s.nextOracle, and returns 0. No monotonicity is assumed across successive calls.

def execClockGettime (s : State) : State :=
  let clk := s.readReg32 Reg.x0
  let tp  := s.readReg64 Reg.x1
  if clk.toNat > 7 then
    s.setStatus (.Exception "unmodeled clock_gettime clockid")
  else if !s.mem.canWrite tp 16 then
    (s.writeReg64 Reg.x0 EFAULT_RET).advancePC
  else
    let ts := s.oracle.clockGettime s.oracleIdx
    (((s.setMem (s.mem.writeBytes tp (encodeTimespec ts))).nextOracle).writeReg64 Reg.x0 0#64).advancePC

end Arm64