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