Overview of KLEE’s main command-line options
- KLEE usage
- KLEE Output
- Symbolic Environment
- Search Heuristics
- Constraint Solving Options
- External Call Policy
- Startup Options
- Calls to
- KLEE debug
- Memory Management
- Making KLEE Exit on Events
- Linking External Libraries
The general form of a KLEE command-line is: first the arguments to KLEE itself (
[klee-options]), then the LLVM bitcode file to execute (
program.bc), followed by any arguments to pass to the application (
In particular, the KLEE option
-posix-runtime enables the use of the symbolic environment options as part of the program’s options.
Note that to enable integer overflow detection, you need to have built
clang with the option
-fsanitize=signed-integer-overflow for signed integer overflow, and with the option
-fsanitize=unsigned-integer-overflow for unsigned integer overflow. These
clang options instrument
program.bc with overflow checks that are used by KLEE.
To get a complete list of KLEE’s command-line options run:
klee --help. The remainder of this page illustrate KLEE’s main command-line options.
The files generated by KLEE are discussed here.
By default KLEE outputs warnings both on screen and in the file
klee-last/warnings.txt. To output the warnings only to the file, and not on screen, one can use:
KLEE provides several options as part of its symbolic environment:
-sym-arg <N>- Replace by a symbolic argument with length N.
-sym-args <MIN> <MAX> <N>- Replace by at least MIN arguments and at most MAX arguments, each with maximum length N.
-sym-files <NUM> <N>- Make NUM symbolic files (‘A’, ‘B’, ‘C’, etc.), each with size N (excluding stdin)
-sym-stdin <N>- Make stdin symbolic with size N.
-sym-stdout- Make stdout symbolic.
-save-all-writes- Allow write operations to execute as expected even if they exceed the file size (default=on). When off, all writes exceeding the initial file size are discarded. Note: file offset is always incremented.
-max-fail <N>- Allow up to N injected failures.
-fd-fail- Shortcut for ‘-max-fail 1’.
Usage examples for
-sym-files are provided in this tutorial.
Main search heuristics
KLEE provides four main search heuristics:
- Depth-First Search (DFS): Traverses states in depth-first order.
- Random State Search: Randomly selects a state to explore.
- Random Path Selection: Described in our KLEE OSDI’08 paper.
- Non Uniform Random Search (NURS): Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc.
To select a search heuristic, use the
--search option provided by KLEE. For example:
demo.o using DFS, while
runs it using the random path selection strategy. The full list of options is shown in KLEE’s help message:
$ klee --help -search - Specify the search heuristic (default=random-path interleaved with nurs:covnew) =dfs - use Depth First Search (DFS) =random-state - randomly select a state to explore =random-path - use Random Path Selection (see OSDI'08 paper) =nurs:covnew - use Non Uniform Random Search (NURS) with Coverage-New heuristic =nurs:md2u - use NURS with Min-Dist-to-Uncovered heuristic =nurs:depth - use NURS with 2^depth heuristic =nurs:icnt - use NURS with Instr-Count heuristic =nurs:cpicnt - use NURS with CallPath-Instr-Count heuristic =nurs:qc - use NURS with Query-Cost heuristic
Interleaving search heuristics
Search heuristics in KLEE can be interleaved in a round-robin fashion. To interleave several search heuristics, use the
--search option multiple times. For example:
interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion.
Batching search heuristics
The main interpreter loop in KLEE selects a new state after every executed instruction.
To execute multiple instructions before selecting another state, the
-use-batching-search flag can be enabled.
Further options allow to specify the batch size by number of instructions (e.g.
-batch-instructions=1000) or execution time (e.g.
Default search heuristics
The default heuristics used by KLEE are
random-path interleaved with
Constraint Solving Options
The constraint solving options are documented separately on the Solver Chain page.
External Call Policy
KLEE provides three policies for handling calls to external functions:
None: No external function calls are allowed. Note that KLEE always allows some external calls with concrete arguments to go through (in particular
puts), regardless of this option.
Concrete: Only external function calls with concrete arguments are allowed (default)
All: All external function calls are allowed. This concretizes any symbolic arguments in calls to external functions.
The external call policy can be specified with the option
--external-calls, which can be set to one of
Warnings about external calls can be controlled via
--external-call-warnings, which can be set to one of
These following options affect how execution is started:
--entry-point=<function_name>: Execution will start from this function instead of
--env-file=<file_name>: Execution will start by initializing the environment from the given file (in “env” format)
--optimize: optimizes the code before execution by running various compiler optimization passes (default=false)
--output-dir=<dir_name>: Directory in which to write results (default=klee-out-
--run-in-dir=<dir_name>: Change to the given directory before starting execution (default=location of tested file).
By default, KLEE will report an error if the assumed condition is infeasible. The option
-silent-klee-assume can be used to silently terminate the current path exploration in such cases.
KLEE generates two files containing statistics concerning the code exploration:
- run.stats: This is a text file containing various statistics emitted by KLEE. While this file can be inspected manually, you should use the klee-stats tool for that.
- run.istats: This is a text file in Callgrind format containing global statistics emitted by KLEE for each line of code in the program. This file can be inspected with frontends which are able to read it (e.g. kcachegrind)
There are several options to modify how KLEE outputs statistics:
-stats- Enable statistics output from program (default=on)
-output-stats- Write running stats trace file (default=on)
-output-istats- Write instruction level statistics in callgrind format (default=on)
-stats-write-interval=TIME- Approximate number of seconds between stats writes (default=1.0s)
-istats-write-interval=TIME- Approximate number of seconds between istats writes (default=10.0s)
-stats-write-after-instructions=N- Write statistics after each
Ninstructions, 0 to disable (default=0)
-istats-write-after-instructions=N- Write istats after each
Ninstructions, 0 to disable (default=0)
KLEE provides several debugging options:
-debug-print-instructions=FORMAT- Log the LLVM instructions executed by KLEE (default=off).
The output may include: the source code file and line (
src), the instruction identifier as assigned by KLEE (
inst_id), and the LLVM instruction with debugging informations (
llvm_inst). The output format can be controlled with the following options:
=all:stderr- Log all instructions to stderr in format
[src, inst_id, llvm_inst]
=src:stderr- Log all instructions to stderr in format
=compact:stderr- Log all instructions to stderr in format
=all:file- Log all instructions to file instructions.txt in format
[src, inst_id, llvm_inst]
=src:file- Log all instructions to file instructions.txt in format
=compact:file- Log all instructions to file instructions.txt in format
-debug-compress-instructions- Compress the
KLEE explicitly intercepts calls for memory management (like
free()) and forwards them to a memory allocator.
In its default configuration this is the same allocator that KLEE uses for its internal data structures which has several disadvantages.
Therefore, a new deterministic allocator (KDAlloc) has been developed and integrated that offers features such as cross-run/cross-path determinism, spatially and temporally distanced allocations, and stability.
The following options are available to configure KDAlloc:
--kdalloc- Allocate memory deterministically (default=
--kdalloc-mark-as-unneeded- Mark allocations as unneeded after external function calls (default=
--kdalloc-globals-size- Reserved memory for globals in GiB (default=
--kdalloc-constants-size- Reserved memory for constant globals in GiB (default=
--kdalloc-heap-size- Reserved memory for heap in GiB (default=
--kdalloc-stack-size- Reserved memory for stack in GiB (default=
--kdalloc-globals-start-address- Start address for globals segment (has to be page aligned)
--kdalloc-constants-start-address- Start address for constant globals segment (has to be page aligned)
--kdalloc-heap-start-address- Start address for heap segment (has to be page aligned)
--kdalloc-stack-start-address- Start address for stack segment (has to be page aligned)
--kdalloc-quarantine- Size of quarantine queues in allocator (default=
The default sizes might seem excessive but keep in mind that KDAlloc only reserves the address space and does not actually allocate that amount of memory. The quarantine queue prevents KLEE from re-using memory addresses immediately and increases the probability to detect use-after-free bugs which might have gone unnoticed otherwise. For more information see Schemmel et al.: A Deterministic Memory Allocator for Dynamic Symbolic Execution.
Additionally, KLEE can be configured to return
NULL in case
malloc is called with a size of
--return-null-on-zero-malloc- Returns NULL if malloc(0) is called (default=
Making KLEE Exit on Events
KLEE does not exit if a bug is found in the analyzed application by default. On the other hand, KLEE implicitly exits on some failures. This behaviour can be changed by the following options:
-exit-on-error- Exit on the first arbitrary error.
-exit-on-error-type=TYPE- Exit on the first error of type
TYPE. This parameter can be repeated to exit after more types.
TYPEcan one of the following:
=Abort- The program crashed
=Assert- An assertion was hit
=Exec- Trying to execute an unexpected instruction
=External- External objects referenced
=Free- Freeing invalid memory
=Model- Memory model limit hit
=Overflow- An overflow occurred
=Ptr- Pointer error
=ReadOnly- Write to read-only memory
=Unhandled- Unhandled instruction hit
-ignore-solver-failures- Do not exit upon solver failure.
Linking External Libraries
Definitions of undefined functions are taken from files given using the option
If some functions in the input file are defined in an external LLVM IR file, an
archive (.a) of LLVM IR files, or a shared object with LLVM IR code, these
external files can be linked in using the option
For example, the following command runs KLEE on the program
a helper library:
The option can be provided multiple times. For instance, linking two libraries, helper and helper2, can be done with the following command: