Hi Petar, On Thu, Oct 29, 2009 at 9:46 AM, Petar Tsankov <peshko at gatech.edu> wrote: > Hello, > > I wanted to use KLEE to generate a Test suite for one of my research subjects > - Sed. I installed KLEE and the uclibc library and ran KLEE in the following > way: > > $klee --libc=uclibc --posix-runtime --init-env sed.bc --sym-args > 0 3 5 --sym-files 0 2 10 > > My intend is to run KLEE with up to 3 symbolic program arguments and 2 > symbolic files with max length of 10. I let KLEE run for about 10 hours and it > generated 2-3 thousands of test cases. I was surprised that the coverage of > the test suite was very low, and I am not sure why this is the case. The > source code of Sed is ~ 15K lines. > > Am I using klee incorrectly?
Not really, but let's just say klee doesn't make itself easy to use. One likely problem is that you are just using the default search strategy, which is depth-first-search which performs badly in practice (but is easy to understand). This is a historical artifact, we really should change the default to be something more sensible. Try running klee with these options: $ klee --only-output-states-covering-new --max-instruction-time=10. --switch-type=internal --randomize-fork --use-random-path --use-interleaved-covnew-NURS --use-batching-search --batch-instructions 10000 which will run with a more reasonable set of options (albeit relatively ad hoc) for exploring real programs. If you want to dive in a little more, http://klee.llvm.org/TestingCoreutils.html explains the basics of how to use kcachegrind to look at what code is actually getting covered. - Daniel
