[klee-dev] Coreutils: STP division by zero errors and computeValue assertion failures

[Emil Rakadjiev]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> .
>