\myheading{Inverse function for base64 decoder}

It's piece of cake for KLEE to reconstruct input base64 string given just base64 decoder code without corresponding encoder code.
I've copypasted this piece of code from
\url{http://www.opensource.apple.com/source/QuickTimeStreamingServer/QuickTimeStreamingServer-452/CommonUtilitiesLib/base64.c}.

We add constraints (lines 86, 87) so that output buffer must have byte values from 0 to 15.
We also tell to KLEE that the Base64decode() function must return 16 (i.e., size of output buffer in bytes, line 84).

\lstinputlisting[numbers=left]{KLEE/klee_base64.c}

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

% klee --libc=uclibc --optimize --use-query-log=solver:smt2 klee_base64.bc
KLEE: ERROR: klee_base64.c:84: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_base64.c:89: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_base64.c:70: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_base64.c:66: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: klee_base64.c:50: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 19251
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 32
KLEE: done: generated tests = 5
...
\end{lstlisting}

We're interesting in the second error, where \TT{klee\_assert()} has been triggered:

\begin{lstlisting}
% ls klee-last | grep err
test000001.user.err
test000002.assert.err
test000003.ptr.err
test000004.ptr.err
test000005.ptr.err

% ktest-tool klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args       : ['klee_base64.bc']
num objects: 1
object 0: name: 'input'
object 0: size: 32
object 0: data: b'AAECAwQFBgcICQoLDA0OD+\x00\xff\xff\xff\xff\xff\xff\xff\xff\x00'
object 0: hex : 0x41414543417751464267634943516f4c4441304f442b00ffffffffffffffff00
object 0: text: AAECAwQFBgcICQoLDA0OD+..........
\end{lstlisting}

This is indeed a real base64 string, terminated with the zero byte, just as it's requested by C/C++ standards.
The final zero byte at 31th byte (starting at zeroth byte) is our deed: so that KLEE would report lesser number of errors. % FIXME spelling

The base64 string is indeed correct:

\begin{lstlisting}
% echo AAECAwQFBgcICQoLDA0OD+ | base64 -d | xxd -g 1
base64: invalid input
00000000: 00 01 02 03 04 05 06 07 08 09 0a 0b 0c 0d 0e 0f  ................
\end{lstlisting}

base64 decoder Linux utility I've just run blaming for ``invalid input''---it means the input string is not properly padded.
Now let's pad it manually, and decoder utility will no complain anymore:

\begin{lstlisting}
% echo AAECAwQFBgcICQoLDA0OD+== | base64 -d | xxd -g 1
00000000: 00 01 02 03 04 05 06 07 08 09 0a 0b 0c 0d 0e 0f  ................
\end{lstlisting}

The reason our generated base64 string is not padded is because base64 decoders are usually discards padding symbols (``='') at the end.
In other words, they are not require them, so is the case of our decoder.
Hence, padding symbols are left unnoticed to KLEE.

So we again made \emph{antipode} or \emph{inverse function} of base64 decoder.