KLEE

master branch

Tools

Overview of the auxiliary tools provided by KLEE

Contents

ktest-tool

KLEE can be configured to output .ktest files whenever it finds an error, covers new code or terminates a path. The content of a .ktest file describes the program input that is needed to guide a concrete execution exactly along the corresponding execution path. Typically, it comprises concrete values for symbolic input files, symbolic arguments, and symbolic variables introduced with klee_make_symbolic. The ktest-tool is a Python script that converts the contents of a .ktest file into human-readable form. For instance for the get_sign.c example from the KLEE directory it would print a concrete value for the symbolic 32bit integer a in different representations (Python byte string, hexadecimal, little-endian uint/int, …):

$ ktest-tool klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\\x00\\x00\\x00\\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

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:

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:

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.

Several table styles are supported, e.g. latex_booktabs or html, and can be enabled with --table-format=<format>.

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

Conversion to comma-separated values (csv)

Starting with version 2.0, KLEE switched from csv to SQLite3 to store its statistics. Of course, these files can be opened and queried with any SQLite client, e.g.:

$ sqlite3 <klee-out-dir>/run.stats
> SELECT * FROM stats

The easiest way to convert all statistics to comma-separated values (csv) is to use klee-stats with --to-csv flag. If the output needs to be modified or limited to specific columns and rows an SQLite client such as sqlite3 comes handy:

$ sqlite3 -csv -header run.stats "select Instructions,printf(\"%.2f\",100.0*CoveredInstructions/(CoveredInstructions+UncoveredInstructions)) AS 'Icov(%)',printf(\"%.2f\",1.0*SolverTime/60000000) AS 'SolverTime(min)',NumQueries from stats ORDER BY WallTime DESC LIMIT 1" 
Instructions,Icov(%),SolverTime(min),NumQueries
2376923,3.96,51.77,514

Live-monitoring with Grafana

klee-stats can also be used as a Grafana data-source. This enables you to create Grafana dashboards for live monitoring of your KLEE process. First, klee-stats needs to be started with the -grafana flag to start serving the data:

klee-stats --grafana <klee-out-dir>

Which starts on port 5000 by default. Then you can start the preconfigured Grafana Docker image with:

docker run -d --net=host --name=grafana klee/grafana

This will create a daemon container running Grafana on port 3000. The image may take half a minute or so to start up. Go to http://localhost:3000, then click on ‘Home’ in the top left hand corner and select the dashboard named ‘KLEE’ from the dropdown.

If you would like to see the progress as Grafana starts, you can instead run Grafana in the foreground by omitting the -d flag. Grafana is ready when the output stops and you see a line like this:

t=... lvl=info msg="HTTP Server Listen" logger=http.server address=0.0.0.0:3000 protocol=http subUrl= socket=

If you are using Grafana to view the statistics of a KLEE run that has already finished, make sure to select a time range that includes the time when KLEE was running. The time range can be changed by with the dropdown in the top right corner.

You can then of course customize your dashboard, add more panels change time ranges and enjoy the live monitoring of KLEE.

To stop Grafana:

docker stop grafana

Or if Grafana is running in the foreground then use Ctrl-C.

Logging granularity

The intervals at which KLEE writes its statistics are configurable. All times are lower bounds and a long running solver query might prevent KLEE from writing new entries.