Discussion:
Delivery Status Notification (Failure)
shuitao gan
2013-08-02 03:30:55 UTC
Permalink
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.
0 klee 0x089ff898
1 klee 0x089ffe04
2 0x40022400 __kernel_sigreturn + 0
3 0x40022424 __kernel_vsyscall + 16
4 libc.so.6 0x401b71df gsignal + 79
5 libc.so.6 0x401ba825 abort + 373
6 libc.so.6 0x401b0085
7 libc.so.6 0x401b0137
8 klee 0x08ae922d MINISAT::ClauseAllocator::allocEnough(unsigned int)
+ 925
9 klee 0x08aea69f MINISAT::Clause*
MINISAT::ClauseAllocator::Clause_new<MINISAT::vec<MINISAT::Lit>
(MINISAT::vec<MINISAT::Lit> const&, unsigned int, bool) + 47
10 klee 0x08a66efb MINISAT::Clause*
MINISAT::Solver::addClauseInt<MINISAT::vec<MINISAT::Lit>
(MINISAT::vec<MINISAT::Lit>&, unsigned int) + 507
11 klee 0x08a67189 bool
MINISAT::Solver::addClause<MINISAT::vec<MINISAT::Lit>
(MINISAT::vec<MINISAT::Lit>&, unsigned int, char*) + 457
12 klee 0x08a52f59 BEEV::ToSAT::toSATandSolve(MINISAT::Solver&,
BEEV::ClauseList&, bool, BEEV::CNFMgr*&, bool, bool) + 921
13 klee 0x08a53fea
BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int,
BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const,
BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 122
14 klee 0x08a54b8a BEEV::ToSAT::CallSAT(MINISAT::Solver&,
BEEV::ASTNode const&) + 2954
15 klee 0x08a51017
BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&,
BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 39
16 klee 0x08a3f0eb BEEV::STP::TopLevelSTPAux(MINISAT::Solver&,
BEEV::ASTNode const&, BEEV::ASTNode const&) + 8187
17 klee 0x08a403cc BEEV::STP::TopLevelSTP(BEEV::ASTNode const&,
BEEV::ASTNode const&) + 252
18 klee 0x08a18e06 vc_query + 166
19 klee 0x08218f2e STPSolverImpl::computeInitialValues(klee::Query
const&, std::vector<klee::Array const*, std::allocator<klee::Array const*>
const&, std::vector<std::vector<unsigned char, std::allocator<unsigned
char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned
char> > > >&, bool&) + 2942
20 klee 0x08203166 CexCachingSolver::getAssignment(klee::Query const&,
klee::Assignment*&) + 294
21 klee 0x08203b2b CexCachingSolver::computeValue(klee::Query const&,
klee::ref<klee::Expr>&) + 283
22 klee 0x08201e9f CachingSolver::computeValue(klee::Query const&,
klee::ref<klee::Expr>&) + 79
23 klee 0x08211473 IndependentSolver::computeValue(klee::Query const&,
klee::ref<klee::Expr>&) + 291
24 klee 0x08216abb klee::Solver::getValue(klee::Query const&,
klee::ref<klee::ConstantExpr>&) + 187
25 klee 0x081e34ed klee::TimingSolver::getValue(klee::ExecutionState
const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 637
26 klee 0x081e5470
klee::AddressSpace::resolveOne(klee::ExecutionState&, klee::TimingSolver*,
klee::ref<klee::Expr>, std::pair<klee::MemoryObject const*,
klee::ObjectState const*>&, bool&) + 288
27 klee 0x081ba1b5
klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool,
klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 229
28 klee 0x081c10c0
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10736
29 klee 0x081c46fb klee::Executor::run(klee::ExecutionState&) + 1803
30 klee 0x081c5337 klee::Executor::runFunctionAsMain(llvm::Function*,
int, char**, char**) + 2151
31 klee 0x0819a6ce main + 11358
32 libc.so.6 0x401a24d3 __libc_start_main + 243
33 klee 0x081a7fc1
ERROR: STP did not return successfully. Most likely you forgot to run
'ulimit -s unlimited'
klee: ClauseAllocator.cpp:124: void*
MINISAT::ClauseAllocator::allocEnough(uint32_t): Assertion `dataStart !=
__null' failed.
0 klee 0x089ff898
1 klee 0x089ffe04
2 0x40022400 __kernel_sigreturn + 0
3 0x40022424 __kernel_vsyscall + 16
4 libc.so.6 0x401b71df gsignal + 79
5 libc.so.6 0x401ba825 abort + 373
6 libc.so.6 0x401b0085
7 libc.so.6 0x401b0137
8 klee 0x08ae922d MINISAT::ClauseAllocator::allocEnough(unsigned int)
+ 925
9 klee 0x08aea69f MINISAT::Clause*
MINISAT::ClauseAllocator::Clause_new<MINISAT::vec<MINISAT::Lit>
(MINISAT::vec<MINISAT::Lit> const&, unsigned int, bool) + 47
10 klee 0x08a66efb MINISAT::Clause*
MINISAT::Solver::addClauseInt<MINISAT::vec<MINISAT::Lit>
(MINISAT::vec<MINISAT::Lit>&, unsigned int) + 507
11 klee 0x08a67189 bool
MINISAT::Solver::addClause<MINISAT::vec<MINISAT::Lit>
(MINISAT::vec<MINISAT::Lit>&, unsigned int, char*) + 457
12 klee 0x08a52f59 BEEV::ToSAT::toSATandSolve(MINISAT::Solver&,
BEEV::ClauseList&, bool, BEEV::CNFMgr*&, bool, bool) + 921
13 klee 0x08a53fea
BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int,
BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const,
BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 122
14 klee 0x08a54b8a BEEV::ToSAT::CallSAT(MINISAT::Solver&,
BEEV::ASTNode const&) + 2954
15 klee 0x08a51017
BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&,
BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 39
16 klee 0x08a3f0eb BEEV::STP::TopLevelSTPAux(MINISAT::Solver&,
BEEV::ASTNode const&, BEEV::ASTNode const&) + 8187
17 klee 0x08a403cc BEEV::STP::TopLevelSTP(BEEV::ASTNode const&,
BEEV::ASTNode const&) + 252
18 klee 0x08a18e06 vc_query + 166
19 klee 0x08218f2e STPSolverImpl::computeInitialValues(klee::Query
const&, std::vector<klee::Array const*, std::allocator<klee::Array const*>
const&, std::vector<std::vector<unsigned char, std::allocator<unsigned
char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned
char> > > >&, bool&) + 2942
20 klee 0x08203166 CexCachingSolver::getAssignment(klee::Query const&,
klee::Assignment*&) + 294
21 klee 0x08203b2b CexCachingSolver::computeValue(klee::Query const&,
klee::ref<klee::Expr>&) + 283
22 klee 0x08201e9f CachingSolver::computeValue(klee::Query const&,
klee::ref<klee::Expr>&) + 79
23 klee 0x08211473 IndependentSolver::computeValue(klee::Query const&,
klee::ref<klee::Expr>&) + 291
24 klee 0x08216abb klee::Solver::getValue(klee::Query const&,
klee::ref<klee::ConstantExpr>&) + 187
25 klee 0x081e34ed klee::TimingSolver::getValue(klee::ExecutionState
const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 637
26 klee 0x081b3124 klee::Executor::toConstant(klee::ExecutionState&,
klee::ref<klee::Expr>, char const*) + 292
27 klee 0x081ba219
klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool,
klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 329
28 klee 0x081c10c0
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10736
29 klee 0x081c46fb klee::Executor::run(klee::ExecutionState&) + 1803
30 klee 0x081c5337 klee::Executor::runFunctionAsMain(llvm::Function*,
int, char**, char**) + 2151
31 klee 0x0819a6ce main + 11358
32 libc.so.6 0x401a24d3 __libc_start_main + 243
33 klee 0x081a7fc1
ERROR: STP did not return successfully. Most likely you forgot to run
'ulimit -s unlimited'
klee: Executor.cpp:1009: klee::ref<klee::ConstantExpr>
klee::Executor::toConstant(klee::ExecutionState&, klee::ref<klee::Expr>,
const char*): Assertion `success && "FIXME: Unhandled solver failure"'
failed.
0 klee 0x089ff898
1 klee 0x089ffe04
2 0x40022400 __kernel_sigreturn + 0
3 0x40022424 __kernel_vsyscall + 16
4 libc.so.6 0x401b71df gsignal + 79
5 libc.so.6 0x401ba825 abort + 373
6 libc.so.6 0x401b0085
7 libc.so.6 0x401b0137
8 klee 0x081b3764 klee::Executor::toConstant(klee::ExecutionState&,
klee::ref<klee::Expr>, char const*) + 1892
9 klee 0x081ba219
klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool,
klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 329
10 klee 0x081c10c0
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 10736
11 klee 0x081c46fb klee::Executor::run(klee::ExecutionState&) + 1803
12 klee 0x081c5337 klee::Executor::runFunctionAsMain(llvm::Function*,
int, char**, char**) + 2151
13 klee 0x0819a6ce main + 11358
14 libc.so.6 0x401a24d3 __libc_start_main + 243
15 klee 0x081a7fc1
Aborted (core dumped)
Jonathan Neuschäfer
2013-08-02 09:53:44 UTC
Permalink
Post by shuitao gan
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

Loading...