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

[Shiyu Dong]

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
>
-------------- next part --------------
HTML attachment scrubbed and removed