[klee-dev] rationale behind the parameters used in the KLEE OSDI paper

[Cristian Cadar]

Hi Lei,

> Thank you for your detailed instruction. Now we do like that. And,
> another question, I think there are actually only 88 stand-alone
> utilities in coreutils, unless considering "false" or "test/[" as
> stand-alone. I skipped "dir", "vdir", "ginstall", "groups", "sha*sum",
> "false", and only test one of the "test" and "[" pair. Should I consider
> "false" or "test/[" as stand-alone?
You need to consider ginstall.  But you need to skip arch, which as we 
mention in the paper is just a wrapper for uname -m.  I updated the 
Coreutils experiments webpage with the list of the 89 utilities that we 
considered.

> Besides, how did you modify the buffer used by "sort"? Thank you very much!
I've just looked, and we changed
#define INPUT_FILE_SIZE_GUESS (1024 * 1024)
to
#define INPUT_FILE_SIZE_GUESS 1024

Looking over our archives, I noticed two more changes that we had to do 
during our experiments:
(1) We had to change some _exit calls during replay, since otherwise 
gcov will not record any coverage on those paths.  Of course, note that 
this is a problem when you run the manual test suite too (and gcov in 
general)
(2) We had to disable buffered I/O, as otherwise the sequence of system 
calls issued by some programs is nondeterministic, which is a problem in 
failure mode.

I will try to document these issues -- and any other I encounter while 
looking at our archives -- on the KLEE website as soon as I get a chance.

BTW, I remember you mentioned a patch that addresses the issues you 
encountered while running KLEE with more recent versions of LLVM (incl. 
2.9)?  It would be great if you could contribute it to the mainline.

Best,
Cristian