symbolic execution

UTBot runs KLEE by fork() + exec() method and controls symbolic execution via waitpid(). UTBot uses Z3 version 4.8.7 as SMT-solver for KLEE. Symbolic execution of each function under test issues a separate KLEE run, which symbolically executes the function wrapper generated by UTBot. UTBot gives KLEE a configurable amount of time to symbolically execute given bitcode, and, when it ends, sends KLEE a SIGINT signal, which is correctly handled by KLEE in many cases — the engine saves explored paths and finishes the execution. However, there are scenarios where KLEE does not handle SIGINTs correctly due to missing handlers in some parts of its code; so UTBot waits a specified amount of time and then sends stronger signals: SIGSTOP, and, eventually, SIGKILL. UTBot KLEE configuration. UTBot runs KLEE with the following parameters:

klee --entry-point=klee_entry__max
--libc=klee --posix-runtime --fp-runtime
--only-output-states-covering-new 
--allocate-determ --external-calls=all 
--timer-interval=1s --bcov-check-interval=5s
--disable-verify --output-dir=klee-out-dir
bitcode.bc --sym-stdin 64

Let us explain every KLEE command line option passed by UTBot in detail:

• KLEE is given a bitcode representation of a project target, which may contain many functions, so KLEE understands where to begin symbolic execution by an entry-point option. To improve symbolic execution possibilities, KLEE needs to be supplied with standard C library, i.e. libc, compiled into LLVM IR. There is a choice one can make between using KLEE libc — a small set of libc functions shipped with KLEE itself, or klee-uclibc, a more complete package, which can be linked with KLEE and used during symbolic execution. Again (as with POSIX runtime), this KLEE libc or klee-uclibc library can be treated as stubs that used by KLEE instead of real libc. UTBot uses KLEE libc. Despite that a wider set of functions is implemented in klee-uclibc, using it forces KLEE to analyse additional several thousands of LLVM instructions prior to analysing actual code of UTBot wrapper, consequently, slowing down UTBot test generation. It is understood that coverage may be lost using –libc=klee instead of –libc=uclibc, so it is planned to make the libc selection configurable;
• UTBot uses KLEE POSIX runtime and self-developed floatingpoint runtime library to allow symbolic execution of programs operating with file descriptors and floating-point values;
• –only-output-states-covering-new option is used to not generate tests executing the same path in user functions;
• UTBot allows all external calls to discard minimal number of branches. External call is a possibility of KLEE to execute a function not implemented in LLVM IR. For that, function arguments are concretized, which potentially leads to a coverage loss, but other options of handling external function calls, like killing an execution branch, are even worse in terms of achieving maximal coverage;
• timer-interval and self-invented bcov-check-interval are used to stop symbolic execution of branches not promising to increase coverage;
• UTBot allows using 64 bytes of symbolic stdin;
• UTBot uses –disable-verify as its linking procedure (Section 3.3) passes only correct bitcode to KLEE.