\myheading{UNIX date/time} UNIX date/time is a number of seconds that have elapsed since 1-Jan-1970 00:00 UTC. C/C++ gmtime() function is used to decode this value into human-readable date/time. Here is a piece of code I've copypasted from some ancient version of Minix OS\footnote{ \url{https://web.archive.org/web/20170413223528/http://www.cise.ufl.edu/~cop4600/cgi-bin/lxr/http/source.cgi/lib/ansi/gmtime.c}} and reworked slightly: \lstinputlisting[numbers=left]{KLEE/klee_time1.c} Let's try it\footnote{All timings are when KLEE 3.0 running on AMD Ryzen 5 3600.}. \begin{lstlisting} % clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ klee_time1.c ... % time klee --libc=uclibc --optimize klee_time1.bc KLEE: ERROR: klee_time1.c:89: external call with symbolic argument: printf KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_time1.c:86: ASSERTION FAIL: 0 KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 68809 KLEE: done: completed paths = 0 KLEE: done: partially completed paths = 1635 KLEE: done: generated tests = 2 real 1m42.781s user 1m32.635s ... \end{lstlisting} Wow, assert() at line 86 has been triggered, why? Let's see a value of UNIX time which triggers it: \begin{lstlisting} % ls klee-last assembly.ll run.istats test000001.exec.err test000002.assert.err warnings.txt info run.stats test000001.kquery test000002.kquery messages.txt solver-queries.smt2 test000001.ktest test000002.ktest % ktest-tool klee-last/test000002.ktest | grep uint object 0: uint: 978243712 \end{lstlisting} Let's decode this value using UNIX date utility: \begin{lstlisting} % date -u --date='@978243712' Sun Dec 31 06:21:52 AM UTC 2000 \end{lstlisting} After my investigation, I've found that \TT{month} variable can hold incorrect value of 12 (while 11 is maximal, for December), because LEAPYEAR() macro must receive year number as 2000, not as 100. Correct fix would be moving year substraction expression down: \begin{lstlisting} % diff -u klee_time1.c klee_time1_fixed.c --- klee_time1.c 2023-12-04 18:25:34.077200826 +0200 +++ klee_time1_fixed.c 2023-12-04 18:48:28.352408590 +0200 @@ -57,8 +57,6 @@ year++; } - year = year - YEAR0; - int month = 0; while (dayno >= _ytab[LEAPYEAR(year)][month]) @@ -66,6 +64,8 @@ dayno -= _ytab[LEAPYEAR(year)][month]; month++; } + + year = year - YEAR0; \end{lstlisting} So I've introduced a bug during rewriting this function, and KLEE found it! Or was it bug in the original code? Just interesting, what would be if I'll replace switch() to array of strings, like it usually happens in concise C/C++ code? \begin{lstlisting} % diff -u klee_time1.c klee_time2.c --- klee_time1.c 2023-12-04 18:25:34.077200826 +0200 +++ klee_time2.c 2023-12-04 18:34:34.388646376 +0200 @@ -67,24 +67,7 @@ month++; } - char *s; - switch (month) - { - case 0: s="January"; break; - case 1: s="February"; break; - case 2: s="March"; break; - case 3: s="April"; break; - case 4: s="May"; break; - case 5: s="June"; break; - case 6: s="July"; break; - case 7: s="August"; break; - case 8: s="September"; break; - case 9: s="October"; break; - case 10: s="November"; break; - case 11: s="December"; break; - default: - assert(0); - }; + const char *s=_months[month]; \end{lstlisting} KLEE detects attempt to read beyond array boundaries: \begin{lstlisting} % time klee --libc=uclibc --optimize klee_time2.bc ... KLEE: ERROR: klee_time2.c:72: external call with symbolic argument: printf KLEE: NOTE: now ignoring this error at this location KLEE: ERROR: klee_time2.c:70: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 69094 KLEE: done: completed paths = 0 KLEE: done: partially completed paths = 1635 KLEE: done: generated tests = 2 real 1m44.795s user 1m33.958s ... \end{lstlisting} This is the same UNIX time value we've already seen: \begin{lstlisting} % ls klee-last | grep err test000001.exec.err test000002.ptr.err % ktest-tool klee-last/test000002.ktest | grep uint object 0: uint: 978243712 \end{lstlisting} So, if this piece of code can be triggered on remote computer, with this input value (\emph{input of death}), it's possible to crash the process (with some luck, though). \myhrule{} OK, now I'm fixing a bug by moving year subtracting expression down, and let's find, what UNIX time value corresponds to some fancy date like 2022-February-2? \lstinputlisting[numbers=left]{KLEE/klee_time3.c_part} \begin{lstlisting} % klee --libc=uclibc --optimize klee_time3.bc ... KLEE: ERROR: klee_time3.c:49: ASSERTION FAIL: 0 KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 175170 KLEE: done: completed paths = 1634 KLEE: done: partially completed paths = 1 KLEE: done: generated tests = 1635 real 0m56.272s user 0m51.168s % ls klee-last | grep err test000569.assert.err % ktest-tool klee-last/test000569.ktest | grep uint object 0: uint: 1645488640 % date -u --date='@1645488640' Tue Feb 22 00:10:40 UTC 2022 \end{lstlisting} Success, but hours/minutes/seconds are seems random---they are random indeed, because KLEE satisfied all constraints we've put, nothing else. We didn't ask it to set hours/minutes/seconds to zeroes. Let's add constraints to hours/minutes/seconds as well: \lstinputlisting[numbers=left]{KLEE/klee_time4.c_part} Let's run it and check \dots \begin{lstlisting} % ls klee-last | grep err test000578.assert.err % ktest-tool klee-last/test000578.ktest | grep uint object 0: uint: 1645568542 % date -u --date='@1645568542' Tue Feb 22 22:22:22 UTC 2022 \end{lstlisting} Now that is precise. Yes, of course, C/C++ libraries has function(s) to encode human-readable date into UNIX time value, but what we've got here is KLEE working \emph{antipode} of decoding function, \emph{inverse function} in a way.