[klee-dev] klee crash question

[Stefan Bucur]

Hi,

In my experience, the crash happens because of a stack overflow in the STP
solver, when converting a very large symbolic array into its bitvector
representation (i.e., "bitblasting"). My workaround was to allow for an
unlimited stack size -- you can run "ulimit -s unlimited" before executing
Klee.

However, even if Klee no longer crashes, such huge constraints are likely
quite expensive, and the solver may get stuck in one of them (unless it
times out...). A quick way to diagnose the problem is to find in the
assembly.ll file generated by Klee the line of code where the large object
was allocated, and see if you can manually tweak the source code to reduce
its size. Klee provides this line in the warning message that you
copy-pasted here.

Stefan


On Tue, Dec 18, 2012 at 11:22 PM, Paul Marinescu <
paul.marinescu at imperial.ac.uk> wrote:

> Hi John,
> This issue seems to be similar to the one mentioned here
> http://keeda.stanford.edu/pipermail/klee-dev/2012-June/000873.html. A
> workaround is to give up some symbolic state by using --max-sym-array-size.
>
> Some more information on the underlying problem is at
> http://keeda.stanford.edu/pipermail/klee-dev/2011-July/000698.html.
>
> Paul
>
> On 18 Dec 2012, at 21:55, John Regehr <regehr at cs.utah.edu> wrote:
>
> Hi,
>
> I'm running Klee (checked out and compiled today) using LLVM 2.9 on 64-bit
> Linux.  I believe that I followed the build/install instructions exactly.
>
> My job here is to call the zlib function inflate() on a small (6-byte)
> symbolic buffer.
>
> Klee runs for a while and generates 81 test cases but then dies like this:
>
> KLEE: WARNING ONCE: flushing 7152 bytes on read, may be slow and/or crash:
> MO641[7152] allocated at zcalloc():  %2 = tail call noalias i8* @malloc(i64
> %1) nounwind, !dbg !5048
>
> Does this mean anything that I can or should want to know?  Can I do
> anything about it?
>
> Thanks,
>
> John Regehr
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed