\myheading{KLEE}

I've always wanted to generate possible strings for given regular expression.
This is not so hard if to dive into regular expression matcher theory and details,
but can we force RE matcher to do this?

I took a lightest RE engine I've found: \url{https://github.com/cesanta/slre}, and added this:

\begin{lstlisting}
#include "klee.h"

int main(void)
{
#define BUF_SIZE 8
        char s[BUF_SIZE];
        klee_make_symbolic(s, sizeof s, "s");
        s[BUF_SIZE-1]=0;
        if (slre_match("(s|S)t(even|ephen|eve|evie)", s, BUF_SIZE-1, NULL, 0, 0)==BUF_SIZE-1)
                klee_assert(0);
}
\end{lstlisting}

So I wanted a string that matches the Steven name, in both Steven and Stephen form, also couple
diminutive forms (Steve, Stevie).
The whole string must have size of 7 characters plus zero byte.

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

% klee --libc=uclibc --optimize --use-query-log=solver:smt2 slre.bc

...
KLEE: ERROR: slre.c:463: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
...

% ls klee-last | grep err
test000004.assert.err

% ktest-tool klee-last/test000004.ktest | grep data
object 0: data: b'\x00steven\x00'
\end{lstlisting}

This is indeed the correct string, although, not aligned with start and end of buffer.

Now this RE can match only binary strings that are divisible by 3 (\ref{DFA_prime}):

\lstinputlisting[style=customc]{regexp/KLEE/1.c.part}

Got one:

\begin{lstlisting}
% ktest-tool klee-last/test000047.ktest | grep data
object 0: data: b'111110101\xff'
\end{lstlisting}

It's indeed so, 0b111110101=501, is divisible by 3.
Last byte is supposed to be zero-terminating byte, but here is just a noise.
OK.

Now, out of whim, let's force to find such a number that two consecutive bits before last one will be both 0:

\lstinputlisting[style=customc]{regexp/KLEE/2.c.part}

\begin{lstlisting}
% ktest-tool klee-last/test000100.ktest | grep data
object 0: data: b'111010001\xff'
\end{lstlisting}

Indeed, 0b111010001=465, which is divisible by 3.

I tried to force last bit be 0, but KLEE can't find anything -- this is understandable.
If a last bit is zero, the whole number is even, and can't be divided by 3.