KLEE

Version 1.4.0

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.

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 sliently 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