question about -max-time flag

[Shiyu Dong]

Hello,

I have a question about how the -max-time flag should be used. I ran the
coreutil test using the following command and set the max time to 600
seconds. However, when I tried to print out the result using klee-stats the
time cost is 717.57 seconds. I'm wondering where does the extra time come
from? Is that costed by generating the test cases, or simply by halting the
program?

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-cache=false \
--use-cex-cache=false \
--libc=uclibc \
--posix-runtime \
--allow-external-sym-calls \
--only-output-states-covering-new \
--environ=../test.env \
--run-in=/tmp/sandbox \
--max-sym-array-size=4096 \
--max-instruction-time=30. \
--watchdog \
--max-time=600. \
--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" \
base64.bc \
--sym-args 0 1 10 \
--sym-args 0 2 2 \
--sym-files 1 8 \
--sym-stdout"

Thanks,
Shiyu

[Tomasz Kuchta]

Hi Shiyu,

I'm not sure, whether that would be helpful, but I've noticed that
dumping states takes some time.
I personally use --dump-states-on-halt=false option. Maybe that would
make your execution time closer to --max-time?

Hope that helps,

Best regards,
Tomek

Post by Shiyu Dong
Hello,
I have a question about how the -max-time flag should be used. I ran the
coreutil test using the following command and set the max time to 600
seconds. However, when I tried to print out the result using klee-stats
the time cost is 717.57 seconds. I'm wondering where does the extra time
come from? Is that costed by generating the test cases, or simply by
halting the program?
klee \
--simplify-sym-indices \
--write-cvcs \
--write-cov \
--output-module \
--max-memory=1000 \
--disable-inlining \
--use-forked-solver \
--use-cache=false \
--use-cex-cache=false \
--libc=uclibc \
--posix-runtime \
--allow-external-sym-calls \
--only-output-states-covering-new \
--environ=../test.env \
--run-in=/tmp/sandbox \
--max-sym-array-size=4096 \
--max-instruction-time=30. \
--watchdog \
--max-time=600. \
--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" \
base64.bc \
--sym-args 0 1 10 \
--sym-args 0 2 2 \
--sym-files 1 8 \
--sym-stdout"
Thanks,
Shiyu
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev