Coreutils: STP division by zero errors and computeValue assertion failures

Discussion:

Emil Rakadjiev

2014-09-26 01:51:10 UTC

Hello,

I repeated the Coreutils experiment using the information from the
website (very useful, thank you!), and I noticed that for some
applications, the KLEE execution fails and exits prematurely with one of
the following two errors (some more details can be found in the attached
files):

(...)
klee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:311: virtual
bool CexCachingSolver::computeValue(const klee::Query&,
klee::ref<klee::Expr>&): Assertion `a && "computeValue() must have
assignment"' failed.
(...)
KLEE: watchdog exiting (no child)

or

(...)
Fatal Error: BVConstEvaluator:division by zero error
error: STP Error: BVConstEvaluator:division by zero error
(...)
ERROR: STP did not return successfully. Most likely you forgot to run
'ulimit -s unlimited'

My configuration: Ubuntu 14.04, LLVM 2.9, KLEE upstream, STP upstream,
klee-uclibc klee_0_9_29.
Coreutils 6.10, set up exactly as described on the website, KLEE
arguments also from the website with one change: --max-time=1800.
(instead of 3600).
My stack size limit was set to unlimited (and I also had to raise the
open file limit, because I got KLEE errors with the default system limits).

I ran all the 89 applications, on two separate, identically configured
machines simultaneously. Results:
STP Error:
PC1: cp, ginstall; PC2: ginstall
computeValue() Error:
PC1: ls, pr, stat, tsort; PC2: stat, tsort

Then, I reran only the failed symbolic executions, and some of them
completed successfully. Results:
STP Error:
PC1: cp; PC2: ginstall
computeValue() Error:
PC1: pr, stat, tsort; PC2: tsort

And, for the third time, I ran again the few failing applications from
run 2 with KLEE:
STP Error:
PC1: (none); PC2: ginstall
computeValue() Error:
PC1: stat, tsort; PC2: tsort

Do you know what the reason for those sporadic failures could be?

As mentioned above, I attached two files containing the detailed error
messages (incl. some preceding output) from the first run. If you need
further details, please let me know.

Thank you!

Best regards,
Emil

Cristian Cadar

2014-10-08 10:02:24 UTC

Permalink

Hi Emil,

What version of STP did you use for these experiments?
If r940, I would try a more recent version of STP. In fact, we would
like to start recommending a more recent version, but we'd like to have
more experience with this first.

The usual cause of this problem is the stack size, but you say you've
already double-checked that. To debug this further, I would suggest to
log the STP queries, reproduce the problem outside KLEE and then report
it to the STP developers.

Best,
Cristian

Post by Emil Rakadjiev
Hello,
I repeated the Coreutils experiment using the information from the
website (very useful, thank you!), and I noticed that for some
applications, the KLEE execution fails and exits prematurely with one of
the following two errors (some more details can be found in the attached
(...)
klee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:311: virtual
bool CexCachingSolver::computeValue(const klee::Query&,
klee::ref<klee::Expr>&): Assertion `a && "computeValue() must have
assignment"' failed.
(...)
KLEE: watchdog exiting (no child)
or
(...)
Fatal Error: BVConstEvaluator:division by zero error
error: STP Error: BVConstEvaluator:division by zero error
(...)
ERROR: STP did not return successfully. Most likely you forgot to run
'ulimit -s unlimited'
My configuration: Ubuntu 14.04, LLVM 2.9, KLEE upstream, STP upstream,
klee-uclibc klee_0_9_29.
Coreutils 6.10, set up exactly as described on the website, KLEE
arguments also from the website with one change: --max-time=1800.
(instead of 3600).
My stack size limit was set to unlimited (and I also had to raise the
open file limit, because I got KLEE errors with the default system limits).
I ran all the 89 applications, on two separate, identically configured
PC1: cp, ginstall; PC2: ginstall
PC1: ls, pr, stat, tsort; PC2: stat, tsort
Then, I reran only the failed symbolic executions, and some of them
PC1: cp; PC2: ginstall
PC1: pr, stat, tsort; PC2: tsort
And, for the third time, I ran again the few failing applications from
PC1: (none); PC2: ginstall
PC1: stat, tsort; PC2: tsort
Do you know what the reason for those sporadic failures could be?
As mentioned above, I attached two files containing the detailed error
messages (incl. some preceding output) from the first run. If you need
further details, please let me know.
Thank you!
Best regards,
Emil
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Daniel Liew

2014-10-08 10:05:24 UTC

Permalink

Post by Cristian Cadar
Hi Emil,
What version of STP did you use for these experiments?
If r940, I would try a more recent version of STP. In fact, we would
like to start recommending a more recent version, but we'd like to have
more experience with this first.
The usual cause of this problem is the stack size, but you say you've
already double-checked that. To debug this further, I would suggest to
log the STP queries, reproduce the problem outside KLEE and then report
it to the STP developers.

Just to note there is a known issue with division by zero in STP

https://github.com/stp/stp/issues/106

Hristina Palikareva

2014-10-08 11:39:08 UTC

Permalink

Hi all,

There is functionality in STP to make division by 0 total and I have
used it to avoid crashes. The code is in make_division_total() -- it
defines x / 0 = 1 and x % 0 = x.

Best regards,
Hristina

Post by Daniel Liew

Just to note there is a known issue with division by zero in STP
https://github.com/stp/stp/issues/106
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Emil Rakadjiev

2014-10-09 07:31:50 UTC

Permalink

Hello everyone,

Thank you for the replies!

Cristian, I used upstream STP (I think it was commit ce5f484 at that
time). Stack size and open file limits were definitely set appropriately.

Daniel, the division by zero errors I got could be due to issue #106.
Hristina's suggestion of setting the division_by_zero_returns_one_flag
would be an easy workaround to try. I've currently torn down my
KLEE+Coreutils test environment, but later on I'll set it up again and
test it.

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)

Best regards,
Emil

Post by Hristina Palikareva
Hi all,
There is functionality in STP to make division by 0 total and I have
used it to avoid crashes. The code is in make_division_total() -- it
defines x / 0 = 1 and x % 0 = x.
Best regards,
Hristina

Post by Daniel Liew

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.

Cristian Cadar

2014-10-09 14:41:30 UTC

Permalink

Post by Emil Rakadjiev
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

Emil Rakadjiev

2014-10-10 09:34:56 UTC

Permalink

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

Post by Cristian Cadar

In what benchmark? Is this reproducible?
Thanks,
Cristian
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.

Emil Rakadjiev

2014-10-10 09:48:13 UTC

Permalink

Hristina, I tried your suggestion today and added a
make_division_total(vc); call to the STPSolverImpl constructor in
lib/Solver/Solver.cpp (line 557).

I already did 3 (the 4th is running) 30 min runs on the ginstall tool
and, as expected, I haven't seen the div zero error so far. I want to do
further tests, because they are not deterministic in this regard. I also
want to test if this has any effect on the other error I encountered.

What side-effects does this workaround have on KLEE (if any)?
Thank you!

Best regards,
Emil

Post by Daniel Liew

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.

Emil Rakadjiev

2014-10-18 10:49:09 UTC

Permalink

Hi everyone,

I looked into the other, "computeValue() must have assignment" error a
little. It happens on basically every run of tsort and only with cex
cache turned on. Here is the relevant trace:

CexCachingSolver::computeValue(query, result)
...
CexCachingSolver::getAssignment(query.withFalse(), assignment)
...
STPSolverImp::computeInitialValues(query, objects, values,
hasSolution)
...
runStatusCode=SRSS_UNSOLVABLE, success=true, hasSolution=false
return true
...
hasSolution=false, assignment=null
return true;
assert(assignment) // fails, since assignment is null

In other words, a query with a false expression has no solution, so
getAssignment sets the assignment to 0, saves this in the cache and
returns true. But in computeValidity() and computeValue(), after the
call to getAssignment, there is an assertion that assignment must not be
0. In those two methods, why is getAssignment called with
query.withFalse() and not just with query?

I attached the failing query from the last run in .pc and .smt2 formats.
Kleaver reports VALID and stp says unsat.

Some other things:
- On some runs of tsort, I got "memory error: out of bound pointer"
errors. I replayed the test cases on the regular executable, but there
was no memory error.
- The STP division by zero error with ginstall is solved by adding a
make_division_total(vc) call to the STPSolverImpl constructor, as
suggested by Hristina.

Best regards,
Emil

Post by Emil Rakadjiev
Hristina, I tried your suggestion today and added a
make_division_total(vc); call to the STPSolverImpl constructor in
lib/Solver/Solver.cpp (line 557).
I already did 3 (the 4th is running) 30 min runs on the ginstall tool
and, as expected, I haven't seen the div zero error so far. I want to
do further tests, because they are not deterministic in this regard. I
also want to test if this has any effect on the other error I
encountered.
What side-effects does this workaround have on KLEE (if any)?
Thank you!
Best regards,
Emil

Post by Daniel Liew

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.