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 < [email protected]> 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 <[email protected]> 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 > [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 > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
