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
On 26/09/14 02:51, Emil Rakadjiev wrote:
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
_______________________________________________
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
