[klee-dev] Coreutils: STP division by zero errors and computeValue assertion failures
Emil Rakadjiev
emil.rakadjiev.bf at hitachi.com
Fri Sep 26 02:51:10 BST 2014
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
-------------- next part --------------
cp:
...
Try `(null) --help' for more information.
missing file operand
Try `(null) --help' for more information.
missing file operand
Try `(null) --help' for more information.
cannot stat `\001'
: No such file or directorytarget `' is not a directory
missing destination file operand after `\00'
Try `(null) --help' for more information.
KLEE: WARNING ONCE: calling external: getpagesize()
KLEE: ERROR: /home/er/klee/test/coreutils-6.10/build-llvm/lib/../../lib/xmalloc.c:49: concretized symbolic size
KLEE: NOTE: now ignoring this error at this location
Fatal Error: BVConstEvaluator:division by zero error
error: STP Error: BVConstEvaluator:division by zero error
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b1856f92340
3 libc.so.6 0x00002b1857bfabb9 gsignal + 57
4 libc.so.6 0x00002b1857bfdfc8 abort + 328
5 klee 0x00000000005f0439
6 klee 0x0000000000e30967
7 klee 0x0000000000e32290 BEEV::NonMemberBVConstEvaluator(BEEV::STPMgr*, BEEV::Kind, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&, unsigned int) + 6336
8 klee 0x0000000000e32680 BEEV::NonMemberBVConstEvaluator(BEEV::ASTNode const&) + 96
9 klee 0x0000000000d9931d SimplifyingNodeFactory::CreateTerm(BEEV::Kind, unsigned int, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) + 269
10 klee 0x0000000000d952d7 NodeFactory::CreateArrayTerm(BEEV::Kind, unsigned int, unsigned int, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) + 23
11 klee 0x0000000000e551ea BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 1466
12 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
13 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
14 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
15 klee 0x0000000000e556ee BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*) + 30
16 klee 0x0000000000dad0a1 BEEV::EstablishIntervals::topLevel_unsignedIntervals(BEEV::ASTNode const&) + 2769
17 klee 0x0000000000da1426 BEEV::STP::sizeReducing(BEEV::ASTNode, BEEV::BVSolver*, BEEV::PropagateEqualities*) + 2518
18 klee 0x0000000000da2886 BEEV::STP::TopLevelSTPAux(BEEV::SATSolver&, BEEV::ASTNode const&) + 1286
19 klee 0x0000000000da5957 BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 471
20 klee 0x0000000000d6d5bd vc_query_with_timeout + 301
21 klee 0x00000000005f45ac 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&) + 2524
22 klee 0x00000000005dea1e CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 238
23 klee 0x00000000005df70f CexCachingSolver::computeTruth(klee::Query const&, bool&) + 335
24 klee 0x00000000005dd410 CachingSolver::computeTruth(klee::Query const&, bool&) + 80
25 klee 0x00000000005ecd22 IndependentSolver::computeTruth(klee::Query const&, bool&) + 274
26 klee 0x00000000005ba6a6 klee::TimingSolver::mustBeTrue(klee::ExecutionState const&, klee::ref<klee::Expr>, bool&) + 358
27 klee 0x0000000000590b9b klee::Executor::getSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > >, std::allocator<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 1195
28 klee 0x0000000000588329
29 klee 0x00000000005916c5 klee::Executor::terminateStateOnError(klee::ExecutionState&, llvm::Twine const&, char const*, llvm::Twine const&) + 485
30 klee 0x0000000000597718 klee::Executor::executeAlloc(klee::ExecutionState&, klee::ref<klee::Expr>, bool, klee::KInstruction*, bool, klee::ObjectState const*) + 2008
31 klee 0x00000000005afcc7 klee::SpecialFunctionHandler::handleMalloc(klee::ExecutionState&, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 71
32 klee 0x00000000005b1a2f klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 191
33 klee 0x0000000000591a67 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 87
34 klee 0x0000000000598177 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 1927
35 klee 0x000000000059b807 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 13031
36 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
37 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
38 klee 0x0000000000576b03 main + 10115
39 libc.so.6 0x00002b1857be5ec5 __libc_start_main + 245
40 klee 0x0000000000585f66
ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited'
==================================================================================================
ginstall:
...
Try `(null) --help' for more information.
missing destination file operand after `\00'
(null): invalid option -- \00
Try `(null) --help' for more information.
Try `(null) --help' for more information.
missing destination file operand after `\00?'
Try `(null) --help' for more information.
Fatal Error: BVConstEvaluator:division by zero error
error: STP Error: BVConstEvaluator:division by zero error
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b38e0a06340
3 libc.so.6 0x00002b38e166ebb9 gsignal + 57
4 libc.so.6 0x00002b38e1671fc8 abort + 328
5 klee 0x00000000005f0439
6 klee 0x0000000000e30967
7 klee 0x0000000000e32290 BEEV::NonMemberBVConstEvaluator(BEEV::STPMgr*, BEEV::Kind, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&, unsigned int) + 6336
8 klee 0x0000000000e32680 BEEV::NonMemberBVConstEvaluator(BEEV::ASTNode const&) + 96
9 klee 0x0000000000d9931d SimplifyingNodeFactory::CreateTerm(BEEV::Kind, unsigned int, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) + 269
10 klee 0x0000000000d952d7 NodeFactory::CreateArrayTerm(BEEV::Kind, unsigned int, unsigned int, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) + 23
11 klee 0x0000000000e551ea BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 1466
12 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
13 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
14 klee 0x0000000000e556ee BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*) + 30
15 klee 0x0000000000dad0a1 BEEV::EstablishIntervals::topLevel_unsignedIntervals(BEEV::ASTNode const&) + 2769
16 klee 0x0000000000da1426 BEEV::STP::sizeReducing(BEEV::ASTNode, BEEV::BVSolver*, BEEV::PropagateEqualities*) + 2518
17 klee 0x0000000000da2886 BEEV::STP::TopLevelSTPAux(BEEV::SATSolver&, BEEV::ASTNode const&) + 1286
18 klee 0x0000000000da5957 BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 471
19 klee 0x0000000000d6d5bd vc_query_with_timeout + 301
20 klee 0x00000000005f45ac 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&) + 2524
21 klee 0x00000000005dea1e CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 238
22 klee 0x00000000005df70f CexCachingSolver::computeTruth(klee::Query const&, bool&) + 335
23 klee 0x00000000005dd410 CachingSolver::computeTruth(klee::Query const&, bool&) + 80
24 klee 0x00000000005ecd22 IndependentSolver::computeTruth(klee::Query const&, bool&) + 274
25 klee 0x00000000005ba6a6 klee::TimingSolver::mustBeTrue(klee::ExecutionState const&, klee::ref<klee::Expr>, bool&) + 358
26 klee 0x0000000000590b9b klee::Executor::getSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > >, std::allocator<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 1195
27 klee 0x0000000000588329
28 klee 0x00000000005911d6 klee::Executor::terminateStateOnExit(klee::ExecutionState&) + 38
29 klee 0x00000000005b1a2f klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 191
30 klee 0x0000000000591a67 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 87
31 klee 0x0000000000598177 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 1927
32 klee 0x000000000059b807 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 13031
33 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
34 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
35 klee 0x0000000000576b03 main + 10115
36 libc.so.6 0x00002b38e1659ec5 __libc_start_main + 245
37 klee 0x0000000000585f66
ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited'
==================================================================================================
ls:
...
: No such file or directorycannot access
: No such file or directory6684680 cannot access
: No such file or directoryKLEE: increased time budget from 2.387532e+01 to 3.539487e+01
cannot access ?/
: Not a directorycannot access
: No such file or directoryklee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:259: virtual bool CexCachingSolver::computeValidity(const klee::Query&, klee::Solver::Validity&): Assertion `a && "computeValidity() must have assignment"' failed.
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002ac30e0d8340
3 libc.so.6 0x00002ac30ed40bb9 gsignal + 57
4 libc.so.6 0x00002ac30ed43fc8 abort + 328
5 libc.so.6 0x00002ac30ed39a76
6 libc.so.6 0x00002ac30ed39b22
7 klee 0x00000000005df5c0 CexCachingSolver::computeTruth(klee::Query const&, bool&) + 0
8 klee 0x00000000005dd0ed CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 109
9 klee 0x00000000005ecf92 IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 274
10 klee 0x00000000005ba336 klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 358
11 klee 0x0000000000594257 klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 215
12 klee 0x0000000000599f69 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 6729
13 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
14 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
15 klee 0x0000000000576b03 main + 10115
16 libc.so.6 0x00002ac30ed2bec5 __libc_start_main + 245
17 klee 0x0000000000585f66
KLEE: watchdog exiting (no child)
==================================================================================================
pr:
...
(null): option `(null)' is ambiguous
Try `(null) --help' for more information.
invalid number of columns: `0'
page width too narrow
starting page number \AB exceeds page count starting page number \AB\AB exceeds page count 3
Try `(null) --help' for more information.
starting page number \AB\AB exceeds page count 3
1900-01-00 00:0\AB Page 1
invalid + argument `\00'
KLEE: increased time budget from 3.822312e+01 to 4.541657e+01
: Is a directoryklee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:259: virtual bool CexCachingSolver::computeValidity(const klee::Query&, klee::Solver::Validity&): Assertion `a && "computeValidity() must have assignment"' failed.
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b17a32d0340
3 libc.so.6 0x00002b17a3f38bb9 gsignal + 57
4 libc.so.6 0x00002b17a3f3bfc8 abort + 328
5 libc.so.6 0x00002b17a3f31a76
6 libc.so.6 0x00002b17a3f31b22
7 klee 0x00000000005df5c0 CexCachingSolver::computeTruth(klee::Query const&, bool&) + 0
8 klee 0x00000000005dd0ed CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 109
9 klee 0x00000000005ecf92 IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 274
10 klee 0x00000000005ba336 klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 358
11 klee 0x0000000000594257 klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 215
12 klee 0x0000000000599f69 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 6729
13 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
14 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
15 klee 0x0000000000576b03 main + 10115
16 libc.so.6 0x00002b17a3f23ec5 __libc_start_main + 245
17 klee 0x0000000000585f66
KLEE: watchdog exiting (no child)
==================================================================================================
stat:
...
Try `(null) --help' for more information.
KLEE: increased time budget from 2.558187e+01 to 3.493425e+01
80120496684686 10000---------- 10000755drwxr-xr-x 0 root 0`//'4096 8 4096 directory`\001'0 0 4096 regular empty fileKLEE: increased time budget from 3.493425e+01 to 4.006787e+01
`//'4096 8 4096 directory`//'4096 8 4096 directory0 4096 regular empty file80120496684686 11900-01-00 1900-01-00 cannot stat `'
: No such file or directory`//'4096 `-'0 0 4096 regular empty file(null): invalid option -- \00
Try `(null) --help' for more information.
`/'4096 8 4096 directory daemonerror: STP timed out(null): invalid option -- \00
Try `(null) --help' for more information.
`A'8 8 0 character special file`\001\001'8 8 4096 regular file binklee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:259: virtual bool CexCachingSolver::computeValidity(const klee::Query&, klee::Solver::Validity&): Assertion `a && "computeValidity() must have assignment"' failed.
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b5534263340
3 libc.so.6 0x00002b5534ecbbb9 gsignal + 57
4 libc.so.6 0x00002b5534ecefc8 abort + 328
5 libc.so.6 0x00002b5534ec4a76
6 libc.so.6 0x00002b5534ec4b22
7 klee 0x00000000005df5c0 CexCachingSolver::computeTruth(klee::Query const&, bool&) + 0
8 klee 0x00000000005dd0ed CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 109
9 klee 0x00000000005ecf92 IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 274
10 klee 0x00000000005ba336 klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 358
11 klee 0x0000000000594257 klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 215
12 klee 0x0000000000599f69 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 6729
13 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
14 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
15 klee 0x0000000000576b03 main + 10115
16 libc.so.6 0x00002b5534eb6ec5 __libc_start_main + 245
17 klee 0x0000000000585f66
KLEE: watchdog exiting (no child)
==================================================================================================
tsort:
...
Try `(null) --help' for more information.
extra operand `?'
Try `(null) --help' for more information.
KLEE: increased time budget from 1.669699e+01 to 2.014906e+01
KLEE: WARNING ONCE: calling external: __ctype_b_loc()
extra operand `\\00\00\00\''
Try `(null) --help' for more information.
\00: input contains an odd number of tokens
extra operand `\f?'
Try `(null) --help' for more information.
(null): invalid option -- \00
Try `(null) --help' for more information.
extra operand `\v\f'
Try `(null) --help' for more information.
-/
: Not a directoryklee: /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.
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002ab568c0e340
3 libc.so.6 0x00002ab569876bb9 gsignal + 57
4 libc.so.6 0x00002ab569879fc8 abort + 328
5 libc.so.6 0x00002ab56986fa76
6 libc.so.6 0x00002ab56986fb22
7 klee 0x00000000005dfb29 CexCachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 953
8 klee 0x00000000005ecab2 IndependentSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 274
9 klee 0x00000000005f2718 klee::Solver::getValue(klee::Query const&, klee::ref<klee::ConstantExpr>&) + 184
10 klee 0x00000000005bac5e klee::TimingSolver::getValue(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 558
11 klee 0x00000000005bc918 klee::AddressSpace::resolveOne(klee::ExecutionState&, klee::TimingSolver*, klee::ref<klee::Expr>, std::pair<klee::MemoryObject const*, klee::ObjectState const*>&, bool&) + 280
12 klee 0x00000000005963cc klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 220
13 klee 0x00000000005991b4 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 3220
14 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
15 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
16 klee 0x0000000000576b03 main + 10115
17 libc.so.6 0x00002ab569861ec5 __libc_start_main + 245
18 klee 0x0000000000585f66
KLEE: watchdog exiting (no child)
-------------- next part --------------
ginstall:
...
Try `(null) --help' for more information.
KLEE: WARNING: mkdir: ignoring (EIO)
missing destination file operand after `\'\v???\''
Try `(null) --help' for more information.
cannot stat `'
: No such file or directoryomitting directory `//'
missing destination file operand after `?\00'
Try `(null) --help' for more information.
Fatal Error: BVConstEvaluator:division by zero error
error: STP Error: BVConstEvaluator:division by zero error
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b5330e44340
3 libc.so.6 0x00002b5331aacbb9 gsignal + 57
4 libc.so.6 0x00002b5331aaffc8 abort + 328
5 klee 0x00000000005f0439
6 klee 0x0000000000e30967
7 klee 0x0000000000e32290 BEEV::NonMemberBVConstEvaluator(BEEV::STPMgr*, BEEV::Kind, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&, unsigned int) + 6336
8 klee 0x0000000000e32680 BEEV::NonMemberBVConstEvaluator(BEEV::ASTNode const&) + 96
9 klee 0x0000000000d9931d SimplifyingNodeFactory::CreateTerm(BEEV::Kind, unsigned int, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) + 269
10 klee 0x0000000000d952d7 NodeFactory::CreateArrayTerm(BEEV::Kind, unsigned int, unsigned int, std::vector<BEEV::ASTNode, std::allocator<BEEV::ASTNode> > const&) + 23
11 klee 0x0000000000e551ea BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 1466
12 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
13 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
14 klee 0x0000000000e54f46 BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*, bool, bool) + 790
15 klee 0x0000000000e556ee BEEV::SubstitutionMap::replace(BEEV::ASTNode const&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, std::unordered_map<BEEV::ASTNode, BEEV::ASTNode, BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual, std::allocator<std::pair<BEEV::ASTNode const, BEEV::ASTNode> > >&, NodeFactory*) + 30
16 klee 0x0000000000dad0a1 BEEV::EstablishIntervals::topLevel_unsignedIntervals(BEEV::ASTNode const&) + 2769
17 klee 0x0000000000da1426 BEEV::STP::sizeReducing(BEEV::ASTNode, BEEV::BVSolver*, BEEV::PropagateEqualities*) + 2518
18 klee 0x0000000000da2886 BEEV::STP::TopLevelSTPAux(BEEV::SATSolver&, BEEV::ASTNode const&) + 1286
19 klee 0x0000000000da5957 BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 471
20 klee 0x0000000000d6d5bd vc_query_with_timeout + 301
21 klee 0x00000000005f45ac 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&) + 2524
22 klee 0x00000000005dea1e CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 238
23 klee 0x00000000005df70f CexCachingSolver::computeTruth(klee::Query const&, bool&) + 335
24 klee 0x00000000005dd410 CachingSolver::computeTruth(klee::Query const&, bool&) + 80
25 klee 0x00000000005ecd22 IndependentSolver::computeTruth(klee::Query const&, bool&) + 274
26 klee 0x00000000005ba6a6 klee::TimingSolver::mustBeTrue(klee::ExecutionState const&, klee::ref<klee::Expr>, bool&) + 358
27 klee 0x0000000000590b9b klee::Executor::getSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > >, std::allocator<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 1195
28 klee 0x0000000000588329
29 klee 0x00000000005911d6 klee::Executor::terminateStateOnExit(klee::ExecutionState&) + 38
30 klee 0x00000000005b1a2f klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 191
31 klee 0x0000000000591a67 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 87
32 klee 0x0000000000598177 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 1927
33 klee 0x000000000059b807 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 13031
34 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
35 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
36 klee 0x0000000000576b03 main + 10115
37 libc.so.6 0x00002b5331a97ec5 __libc_start_main + 245
38 klee 0x0000000000585f66
ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited'
==================================================================================================
stat:
...
0cannot stat `'
: No such file or directorycannot stat `//\001'
`-'8 8 4096 regular file: No such file or directory`-'8 c 0 daemon 0cannot stat `///\001\001'
b 0 sys: No such file or directory`A'//4096841ed00801222001411447596141114249414113989104096 root 0 root000cannot stat `\001/'
cannot stat `'
: No such file or directory: No such file or directorycannot stat `'
: No such file or directory`A' -> `A.lnk'8 8 missing operand
Try `(null) --help' for more information.
80120492 220755drwxr-xr-x 0 sync 0 daemoncannot stat `\001/'
8 8 0 block special file001 b 0 daemon 0: No such file or directory`/'4096 klee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:259: virtual bool CexCachingSolver::computeValidity(const klee::Query&, klee::Solver::Validity&): Assertion `a && "computeValidity() must have assignment"' failed.
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b3c51ecf340
3 libc.so.6 0x00002b3c52b37bb9 gsignal + 57
4 libc.so.6 0x00002b3c52b3afc8 abort + 328
5 libc.so.6 0x00002b3c52b30a76
6 libc.so.6 0x00002b3c52b30b22
7 klee 0x00000000005df5c0 CexCachingSolver::computeTruth(klee::Query const&, bool&) + 0
8 klee 0x00000000005dd0ed CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 109
9 klee 0x00000000005ecf92 IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 274
10 klee 0x00000000005ba336 klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 358
11 klee 0x0000000000594257 klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) + 215
12 klee 0x0000000000599f69 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 6729
13 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
14 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
15 klee 0x0000000000576b03 main + 10115
16 libc.so.6 0x00002b3c52b22ec5 __libc_start_main + 245
17 klee 0x0000000000585f66
KLEE: watchdog exiting (no child)
==================================================================================================
tsort:
...
Try `(null) --help' for more information.
Try `(null) --help' for more information.
extra operand `\00\00'
-: input contains an odd number of tokens
Try `(null) --help' for more information.
extra operand `?\\'
Try `(null) --help' for more information.
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.
0 klee 0x0000000000d5773f
1 klee 0x0000000000d57c74
2 libpthread.so.0 0x00002b6d51f68340
3 libc.so.6 0x00002b6d52bd0bb9 gsignal + 57
4 libc.so.6 0x00002b6d52bd3fc8 abort + 328
5 libc.so.6 0x00002b6d52bc9a76
6 libc.so.6 0x00002b6d52bc9b22
7 klee 0x00000000005dfb29 CexCachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 953
8 klee 0x00000000005ecab2 IndependentSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 274
9 klee 0x00000000005f2718 klee::Solver::getValue(klee::Query const&, klee::ref<klee::ConstantExpr>&) + 184
10 klee 0x00000000005bac5e klee::TimingSolver::getValue(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 558
11 klee 0x00000000005bc918 klee::AddressSpace::resolveOne(klee::ExecutionState&, klee::TimingSolver*, klee::ref<klee::Expr>, std::pair<klee::MemoryObject const*, klee::ObjectState const*>&, bool&) + 280
12 klee 0x00000000005963cc klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 220
13 klee 0x00000000005991b4 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 3220
14 klee 0x000000000059d086 klee::Executor::run(klee::ExecutionState&) + 1654
15 klee 0x000000000059d931 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
16 klee 0x0000000000576b03 main + 10115
17 libc.so.6 0x00002b6d52bbbec5 __libc_start_main + 245
18 klee 0x0000000000585f66
KLEE: watchdog exiting (no child)
More information about the klee-dev
mailing list