How to run Klee

To all my undergrads struggling with Klee and their poor documentation

Given a simple file

int main()
{
int x[10], i=0;
int y;
/* declare the memory region occupied by
* variable "x" to be symbolic */
/* This means the program will be executed
* with uninstantiated, i.e., symbolic
* values of x */
klee_make_symbolic(x, 10*sizeof(x[0]), "x");
while (i < 10) {
if (x[i] < 5)
y++;
else
y--;
i++;
}
}

How do you run this? Do it the easiest way!

Go and install docker(I assume you are on linux/OS X) -> this is pretty straight forward, just go and read get docker.

Then go to klee’s website and find the get started guide for docker. Follow all the instructions on it.

Example commands I typed into the terminal, sequentially

Note: the >> is meant to simulate the command line. Dont type it literally into the terminal.

>> docker pull klee/klee
>> docker pull klee/klee:master
>> docker run --rm -ti --ulimit='stack=-1:-1' klee/klee:master

Now, create the file you want to run.

>> vim sym.c

And paste in the c code you want, eg, the file at the top of this tutorial. Then run

>> clang -emit-llvm -c sym.c

If you would like the smt2s file to run SAT on, say in a rise4fun z3, you can do one more command

>> klee --write-smt2s sym2.bc

You can “ls” and see that there will be a klee-last folder in the root docker container space.

Copy that folder out onto your local machine if you want to use it. To do that, we need some standard docker commands

Open another terminal not running the active container.

>> docker ps

Get the container ID from there. Here, I’ve used 12345678 as an example. Now, copy the desired folder out.

Note: the trailing “/” at “…klee-last/” is very important!

>> docker cp 12345678:/home/klee/klee-last/ ~/somefolder/

You are set!