[klee-dev] Reproduce the OSDI'08 coreutils result on the latest version of KLEE

[Paul Marinescu]

Hi Shiyu,
For --max-forks=10 the number of completed paths is 42 due to a bug: klee still forks when encountering switch statements. A patch is available at https://github.com/paulmar/klee/commit/90601a60fb6a0f22337c46680f150ec04ad3c6cb . The output should now look similar to

KLEE: done: total instructions = 154095
KLEE: done: completed paths = 11
KLEE: done: generated tests = 9

For --stop-after-n-tests=10, KLEE does stop, but generates tests for the partially explored paths before exiting. These are included in the 'completed paths'  count.

Paul

On 24 Sep 2013, at 23:51, Shiyu Dong <shiyud at utexas.edu> wrote:

> Hi Cristian,
> 
> I am still confused about these two flags. For example, when trying to run the paste.bc as showed in the tutorial, if I use --max-forks=10 I got the following:
> 
> KLEE: done: total instructions = 421007
> KLEE: done: completed paths = 42
> KLEE: done: generated tests = 11
> 
> However, if I use --stop-after-n-tests=10, I got:
> 
> KLEE: done: total instructions = 348114
> KLEE: done: completed paths = 238
> KLEE: done: generated tests = 35
> 
> For testing purpose I only give it 1 minute to run. However, none of those "completed paths" is equal to 10, and for the second case the "generated tests" is grater than 10 also. I'm wondering if there's anything that I did wrong. Thanks.
> 
> Here's the command that I used:
> 
> klee \
> --simplify-sym-indices \
> --write-cvcs \
> --write-cov \
> --output-module \
> --max-memory=1000 \
> --disable-inlining \
> --use-forked-solver \
> --use-cex-cache \
> --libc=uclibc \
> --posix-runtime \
> --allow-external-sym-calls \
> --only-output-states-covering-new \
> --environ=test.env \
> --run-in=/tmp/sandbox \
> # --stop-after-n-tests=10 or --max-forks=10, I put one of them here.
> --max-sym-array-size=4096 \
> --max-instruction-time=30. \
> --max-time=60. \
> --watchdog \
> --max-memory-inhibit=false \
> --max-static-fork-pct=1 \
> --max-static-solve-pct=1 \
> --max-static-cpfork-pct=1 \
> --switch-type=internal \
> --randomize-fork \
> --search=random-path \
> --search=nurs:covnew \
> --use-batching-search \
> --batch-instructions=10000 \
> ./paste.bc \
> --sym-args 0 1 10 \
> --sym-args 0 2 2 \
> --sym-files 1 8 \
> --sym-stdout
> 
> Best,
> Shiyu
> 
> 
> On Tue, Sep 24, 2013 at 4:24 PM, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> Hi Shiyu,
> 
> 
> On 24/09/2013 22:06, Shiyu Dong wrote:
> One more question: does KLEE has any way to limit to the number of paths to
> explore? From the --help command the only possible option I see is
> "-stop-after-n-tests=<uint>" because I assume each test case corresponds to
> one path by observing the test results that I already have. Is that a good
> assumption?
> At some level, yes, but this ignores the partial paths that have not resulted in a test case yet.  Also, to avoid excessive test case generation, it is often a good idea to use the flag -only-output-states-covering-new, which only generates a test case when new code is covered (note that the command line discussed before includes this flag).
> 
> 
> Are there better flags to use?
> If I understand correctly, what you want is actually -max-forks=<uint>.
> 
> Best,
> Cristian
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed