\myheading{KLEE}

(All timings are when KLEE 3.0 running on AMD Ryzen 5 3600.)

I've also rewritten Sudoku example (\ref{sudoku_SMT}) for KLEE:

\lstinputlisting[numbers=left]{puzzles/sudoku/KLEE/klee_sudoku_or1.c}

Let's run it:

\begin{lstlisting}
% clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ klee_sudoku_or1.c

...

% time klee --libc=uclibc --optimize klee_sudoku_or1.bc
...
KLEE: ERROR: klee_sudoku_or1.c:96: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 23675
KLEE: done: completed paths = 102
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 103

real    6m4.584s
user    6m3.999s
\end{lstlisting}

Now this is really slower (on AMD Ryzen 5 3600) in comparison to Z3Py solution (\ref{sudoku_SMT}).

But the answer is correct:

\begin{lstlisting}
% ls klee-last/*err
klee-last/test000103.external.err

% ktest-tool klee-last/test000103.ktest
ktest file : 'klee-last/test000103.ktest'
args       : ['klee_sudoku_or1.bc']
num objects: 1
object 0: name: 'cells'
object 0: size: 81
object 0: data: b'\x01\x04\x05\x03\x02\x07\x06\t\x08\x08\x03\t\x06\x05\x04\x01\x02\x07\x06\x07\x02\t\x01\x08\x05\x04\x03\x04\t\x06\x01\x08\x05\x03\x07\x02\x02\x01\x08\x04\x07\x03\t\x05\x06\x07\x05\x03\x02\t\x06\x04\x08\x01\x03\x06\x07\x05\x04\x02\x08\x01\t\t\x08\x04\x07\x06\x01\x02\x03\x05\x05\x02\x01\x08\x03\t\x07\x06\x04'
object 0: hex : 0x010405030207060908080309060504010207060702090108050403040906010805030702020108040703090506070503020906040801030607050402080109090804070601020305050201080309070604
object 0: text: .................................................................................
\end{lstlisting}

Character \TT{\textbackslash{}t} has code of 9 in C/C++,
and KLEE prints byte array as a C/C++ string, so it shows some values in such way.
We can just keep in mind that there is 9 at the each place where we see \TT{\textbackslash{}t}.
The solution, while not properly formatted, correct indeed.

By the way, at lines 45 and 46 you may see how we tell to KLEE that all array elements must be within some limits.
If we comment these lines out, we've got this:

\begin{lstlisting}
...
KLEE: ERROR: klee_sudoku_or1.c:54: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:55: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:58: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:59: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:60: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:61: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:62: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:56: overshift error
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_sudoku_or1.c:57: overshift error
KLEE: NOTE: now ignoring this error at this location
...
\end{lstlisting}

KLEE warns us that shift value at lines 54...62 is too big.
Indeed, KLEE may try all byte values up to 255 (0xFF), which are pointless to use there,
and may be a symptom of error or bug, so KLEE warns about it. % FIXME chk spelling

Now let's use \verb|klee_assume()| again:

\lstinputlisting{puzzles/sudoku/KLEE/klee_sudoku_or2.c}

\begin{lstlisting}
...
KLEE: ERROR: klee_sudoku_or2.c:96: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 16739
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1

real    0m18.663s
user    0m18.409s
...
\end{lstlisting}

That works much faster: because only one path to explore.
And, as we see, the only one path has been found (one we actually interesting in it) instead of 161.

It's still much slower than Z3Py solution, though.

