KLEE

master branch

Options

Overview of KLEE’s main command-line options

Contents

KLEE usage

$ klee [klee-options] <program.bc> [program-options]

The general form of a KLEE command-line is first the arguments for KLEE itself ([klee-options]), then the LLVM bitcode file to execute (program.bc), and then any arguments to pass to the application ([program-options]). 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 overlow detection, you need to have built program.bc using clang and 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.

KLEE Output

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 --warnings-only-to-file ...

Symbolic Environment

KLEE provides several options as part of its symbolic environment:

  1. -sym-arg <N> - Replace by a symbolic argument with length N.
  2. -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most MAX arguments, each with maximum length N.
  3. -sym-files <NUM> <N> - Make NUM symbolic files (‘A’, ‘B’, ‘C’, etc.), each with size N (excluding stdin)
  4. -sym-stdin <N> - Make stdin symbolic with size N.
  5. -sym-stdout - Make stdout symbolic.
  6. -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.
  7. -max-fail <N> - Allow up to N injected failures.
  8. -fd-fail - Shortcut for ‘-max-fail 1’.

Some usage examples:

$ klee -posix-runtime <program.bc> -sym-arg 16
$ klee -posix-runtime <program.bc> -sym-files 2 30 -sym-stdin

Search Heuristics

Main search heuristics

KLEE provides four main search heuristics:

  1. Depth-First Search (DFS): Traverses states in depth-first order.
  2. Random State Search:Randomly selects a state to explore.
  3. Random Path Selection: Described in our KLEE OSDI’08 paper.
  4. 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:

$ klee --search=dfs demo.o

runs demo.o using DFS, while

$ klee --search=random-path demo.o

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 to be interleaved, use the --search multiple times. For example:

$ klee --search=random-state --search=nurs:md2u demo.o

interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion.

Default search heuristics

The default heuristics used by KLEE are random-path interleaved with nurs:covnew.

Query Logging

To log the queries issued by KLEE during symbolic execution see Solver Chain.

Entry Point

To change the entry point you can use the option -entry-point=FUNCTION_NAME, where FUNCTION_NAME is the name of the function to use as the entry point for execution.

Calls to klee-assume

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.

Statistics

By default, KLEE generates two files containing statistics concerning the code exploration:

There are several options to modify how KLEE outputs statistics:

KLEE debug

KLEE provides several debugging options:

Memory Management

KLEE explicitly intercepts calls for memory management (like malloc() and free()) and forwards to an existing memory allocators. To change this behaviour, following options are provided:

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:

Examples:

klee -exit-on-error input.bc
klee -exit-on-error-type=Assert -exit-on-error-type=Ptr input.bc

Linking External Libraries

Definitions of undefined functions are taken from files given using the option -link-llvm-lib.

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 -link-llvm-lib=LIB_FILENAME.

For example, the following command runs KLEE on the program test.bc, linking a helper library:

$ klee -link-llvm-lib=libhelper.so.bc test.bc

The option can be provided multiple times. For instance, linking two libraries, helper and helper2, can be done with the following command:

$ klee -link-llvm-lib=libhelper.so.bc -link-llvm-lib=libhelper2.so.bc test.bc