Hello Cristian,
In my first email about this issue I listed all the Coreutils tools that
failed. They produce the respective error in most cases, but not always.
In the case of the "computeValue() must have assignment/no child" error,
tsort always failed for me so far.
In the case of the div zero problem, the most error-prone tool seems to
be ginstall, but in less than 50% of my tries the 30 min symbolic
execution completed successfully. If the error is thrown, it's usually
in the first few minutes.
Today, I've set up a KLEE+Coreutils environment again, this time on
Ubunutu 12.04, and I got the same errors.
Environment: Ubuntu 12.04 or 14.04, LLVM 2.9, STP upstream, KLEE-uclibc
0_9_29, KLEE upstream, Coreutils 6.10.
Hard and soft limits for all users and root: unlimited stack size,
999999 open files.
I build Coreutils according to the instructions on the website:
../configure --disable-nls CFLAGS="-g"
make CC="/home/er/klee/klee/scripts/klee-gcc"
make -C src arch hostname CC="/home/er/klee/klee/scripts/klee-gcc"
Before running each tool, I set up a clean sandbox:
env -i /bin/bash -c '(source testing-env.sh; env >test.env)'
rm -rf /tmp/*
cp sandbox.tgz /tmp
$(cd /tmp; tar -xzf sandbox.tgz)
And here is e.g. the command to start ginstall (same is used for all the
other tools, with the exceptions mentioned on the website):
klee --simplify-sym-indices --write-cvcs --write-cov --output-module
--max-memory=1000 --disable-inlining --optimize --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" --max-sym-array-size=4096
--max-instruction-time=30. --max-time=1800. --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
"/home/er/klee/test/coreutils-6.10/build-llvm/src/ginstall.bc"
--sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout
Best regards,
Emil
On 10/9/2014 11:41 PM, Cristian Cadar wrote:
On 09/10/14 08:31, Emil Rakadjiev wrote:
Besides the div zero issue, I also saw this other error: virtual bool
CexCachingSolver::computeValue(const klee::Query&,
klee::ref<klee::Expr>&): Assertion `a && "computeValue() must have
assignment"' failed.
(...)
KLEE: watchdog exiting (no child)
In what benchmark? Is this reproducible?
Thanks,
Cristian
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
