[klee-dev] cryptominisat assertion failure (was: Fwd: Delivery Status Notification (Failure))

[Jonathan Neuschäfer]

On Fri, Aug 02, 2013 at 11:30:55AM +0800, shuitao gan wrote:
> Hi, kLEE group.
>  when I test corutils-8.20 using " klee --simplify-sym-indices --write-cvcs
> --write-cov --output-module --max-memory=10000 --disable-inlining
>  --use-forked-stp --use-cex-cache --libc=uclibc --posix-runtime
> --allow-external-sym-calls --only-output-states-covering-new
> --run-in=/tmp/sandbox --max-sym-array-size=4096 --ignore-solver-failures
> --max-instruction-time=30. --max-time=1000000 --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  -check-div-zero
> --batch-instructions=10000  ./fmt.bc (or many other command) --sym-args 0 1
> 2 --sym-args 0 1 300 --sym-files 1 8  --sym-stdout", it sometimes comes
> across the problem  below after it run only 1 hour or less to generate some
> paths, and I think it is not the problem "ulimit -s unlimited"that because
> I try it.  How to solve the problem?
> 
> ......
> klee: ClauseAllocator.cpp:124: void*
> MINISAT::ClauseAllocator::allocEnough(uint32_t): Assertion `dataStart !=
> __null' failed.

This will happen if malloc fails; here's the relevant piece of code:

        uint32_t nextSize; //number of BYTES to allocate
        if (maxSizes.size() != 0)
            nextSize = maxSizes[maxSizes.size()-1]*3*sizeof(uint32_t);
        else
            nextSize = MIN_LIST_SIZE;
        assert(needed <  nextSize);

        uint32_t *dataStart = (uint32_t*)malloc(nextSize);
        assert(dataStart != NULL);
(sat/cryptominisat2/ClauseAllocator.cpp, line 116, in the STP r940 source)

Setting "ulimit -s unlimited" will not help in this case, because it
makes the stack size unlimited, but malloc uses the heap for
allocations.

On modern Linux systems, malloc doesn't fail anymore simply because
you're out of physical memory, due to a feature called "overcommit".
Instead malloc will allocate the whole virtual address space of a
process until it fails, which will usually happens around 3GiB on a
32-bit machine.

I suggest you try to limit KLEE's memory usage with the -max-memory
option.


--
Jonathan Neuschäfer