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

[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.

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