[klee-dev] Beginnier to KLEE

[Dan Liew]

Hi,

> I want to explore symbolic execution and KLEE seems like a good choice for
> beginning. But I would like you guidance in getting to know the best way to
> understand the code of KLEE.

One thing you certainly do is read the OSDI'08 paper on KLEE to get a
high level understanding of what it tries to do.

One approach you could take to trying to understand the code is by
trying to run a simple closed world (i.e. makes no external calls)
program that contains no symbolic variables and does not link in any
libraries (i.e. do not use --posix-runtime or --libc=...). Once you
understand what KLEE has done by looking at the output files (e.g.
assembly.ll) you could try following what KLEE is doing by running
through gdb and break at points of interest and then following through
what KLEE does.

If you succeed in doing that try introducing a symbolic variable in
your simple closed world program and running through gdb and see how
KLEE behaves.

This requires that you learn how to use gdb or use it indirectly via
an IDE like Eclipse (with the CDT plug-in). It will certainly take
time to learn this but IMHO it's worth the effort.