KLEE Tools

1. ktest-tool
2. klee-stats

ktest-tool

klee-stats

klee-stats is a Python script used to extract and present in a tabular form runtime statistics for a KLEE execution. The runtime statistics include:

• The number of executed instructions
• Instruction coverage in the LLVM bitcode (%)
• Branch coverage in the LLVM bitcode (%)
• Total static instructions in the LLVM bitcode
• The number of currently active states
• Megabytes of memory currently used
• The number of queries issued to STP
• The average number of query constructs per query
• Various time statistics:
  • Total user time
  • Total wall time
  • Time spent in the constraint solver
  • Time spent in the counterexample caching code
  • Time spent forking
  • Time spent in object resolution

klee-stats extracts statistics information from the run.stats file present in the klee-out-* directory created during a KLEE execution. The exact usage of klee-stats is as follows:

klee-stats [options] directories

The directories parameter is a list of klee-out-* directories created by KLEE. A common scenario is to simply run klee-stats on klee-last.

In order to limit printed information only to the values of measured times, the following options can be used:

• --print-rel-times—display time values relative to measured execution time
• --print-abs-times—display absolute time values

The --precision option can be used to configure the number of fractional digits displayed in floating point values. By default, 2 fractional digits are displayed, but in some cases that might be not sufficient—if the value is very small, e.g. 0.0001, with 2-digits precision it will be printed as 0.00.

Various other options can be used to specify what values are displayed and how they are displayed. Options for comparison of statistics are also provided. More information about available options can be obtained using the command:

klee-stats --help