Reproduce the OSDI'08 coreutils result on the latest version of KLEE

[Shiyu Dong]

Hi all,

I want to try to reproduce the result of the coreutils experiment on the
latest version of KLEE, and I found this tutorial.

http://klee.llvm.org/CoreutilsExperiments.html

I used the command specified in question #7. However it takes forever to
run on my machine.

I'm wondering if there's any update on those commands. Also, I'm running
KLEE on ubuntu 12.04 64 bit. Is there anything specific that I need to pay
attention to on 64 bit machine?

Thanks,
Shiyu

[Cristian Cadar]

Hi Shiyu,

Post by Shiyu Dong
http://klee.llvm.org/CoreutilsExperiments.html
I used the command specified in question #7. However it takes forever to
run on my machine.

I'm not sure what you mean: as specified by the --max-time option, that
should take approximately one hour :) (modulo some extra test generation
at the end, and benchmarks that complete in less than one hour). Don't
you see the message "HaltTimer invoked" after 1h?

This being said, it is unlikely that you'll obtain the same results as
in the original paper, for reasons that are discussed on the webpage
above and in prior messages (changes in KLEE, different LLVM and STP
versions, 64 vs 32bit, etc.)

Best,
Cristian

[Shiyu Dong]

Hi Cristian,

Thanks for your information. That's really helpful.

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? Are there better flags to use?

Best,
Shiyu

Post by Cristian Cadar
Hi Shiyu,

http://klee.llvm.org/**CoreutilsExperiments.html<http://klee.llvm.org/CoreutilsExperiments.html>
I used the command specified in question #7. However it takes forever to
run on my machine.

I'm not sure what you mean: as specified by the --max-time option, that
should take approximately one hour :) (modulo some extra test generation at
the end, and benchmarks that complete in less than one hour). Don't you
see the message "HaltTimer invoked" after 1h?
This being said, it is unlikely that you'll obtain the same results as in
the original paper, for reasons that are discussed on the webpage above and
in prior messages (changes in KLEE, different LLVM and STP versions, 64 vs
32bit, etc.)
Best,
Cristian
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>

[Cristian Cadar]

Hi Shiyu,

Post by Shiyu Dong
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).

Post by Shiyu Dong
Are there better flags to use?

If I understand correctly, what you want is actually -max-forks=<uint>.

Best,
Cristian

[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

Post by Cristian Cadar
Hi Shiyu,

Post by Shiyu Dong
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

[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

Post by Shiyu Dong
Hi Cristian,
KLEE: done: total instructions = 421007
KLEE: done: completed paths = 42
KLEE: done: generated tests = 11
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.
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
Hi Shiyu,
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev