\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:

\url{\RepoURL/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
info
messages.txt
run.istats
run.stats
solver-queries.smt2
test000001.exec.err
test000001.kquery
test000001.ktest
test000002.assert.err
test000002.kquery
test000002.ktest
warnings.txt

% 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,basicstyle=\ttfamily\small]{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.

