Hi Ryan,
>
> I'm not sure where to begin debugging this—is there an option I should be
> using to dump state more thoroughly before the assertion is hit? It takes a
> long time to reach the assertion failure, so if there's an easier way to
> restore state to reproduce the problem it would be very helpful.
>
>
I don't know if there is a way to save/restore state, sorry.
I'm afraid I'm just lowly student working on KLEE so take everything I say
with some scepticism. However the work I'm doing at the moment involves
adding support other solvers (other than STP) so I might be able to offer
some advise.
I assume you have (but just in case you haven't) made sure your build of
KLEE passes the unit tests and other checks ($ make check and $ make
unittests). Here are a few suggestions...
* You've got several solvers chained together (based on the backtrace)
IndependentSolver, CachingSolver (the timing solver is just a wrapper which
we can probably ignore). Have you tried disabling them like so...
$ klee -use-independent-solver=0 -use-caching=0 your_program.bc
To see if it made any difference. I'm not convinced the caching solver is
the root of the problem but the Independent solver might.
* Something you could try is switching on core dumps in your shell so you
inspect the state of KLEE after the failed assert()
$ ulimit -c unlimited
# You may need to be root or change your settings in
/etc/security/limits.conf to do the above
$ klee --your-switches your_program.bc
...
Assertion failed: (hasSolution && "state has invalid constraint set"),
function computeValue, file /Users/rzg/Projects/llvm/
tools/klee/lib/Solver/Solver.cpp, line 540.
Aborted (core dumped)
$ gdb klee core
You can then inspect the value of various variables.
* Have you tried using the debugging solver..
$ klee -debug-validate-solver
This will run the normal solver and an un-optimised STPSolver (with no
other solvers on top) and check they are both outputting the same. If
something bad is happening this might catch the problem earlier. Take a
look at "constructSolverChain()" in lib/Core/Executor.cpp to get an idea of
what is happening.
* The bug could be in the solver or in KLEE itself. To check if the solver
is failing, a good place to start would be to actually record the
constraints that are causing the assertion failure.
In STPSolverImpl::computeValue() just before the assertion failure you
could add the following lines as a very hack-ish way of getting the
constraints out.
if(!hasSolution)
{
std::ofstream file("./failed-constraints.cvc");
char* log = this->getConstraintLog(query);
file << log;
file.close();
}
If you get this .cvc file you can run it on STP external, you should get
the same answer "Valid" which means that the constraints were NOT
satisfiable (no that's not a typo that's the language KLEE and STP use
which is very very confusing and silly...GRRRR...rant over). Conversely
"Invalid" means the constraints were satisfiable.
STP has an option --print-back-SMTLIBv2 which will let you print the .cvc
file in the SMTLIBv2 constraint language which are supported by several
solvers which are readily available in compiled form (e.g. Z3, SONOLAR,
Mathsat5, CVC3). You could then test this .cvc converted to SMTLIBv2
solvers and see if you get the same answer. In SMTLIBv2 the responces are
sensible ("sat" means satisfiable and "unsat" means unsatisfiable).
Of course this assumes that there isn't a bug in the way STP parses the
generated .cvc file and converts to SMTLIBv2. The only way to be really
sure is to get KLEE to generate SMTLIBv2 files natively (without using
STP), but this support hasn't been officially added yet. I've added support
for this in my own branch which you can play with. If you're interested
it's available here ( https://github.com/delcypher/klee/tree/smtlib). You
compile exactly in the same way
as normal KLEE. You could then print out a SMTLIBv2 file just before the
assert() like this...
#include "klee/util/ExprSMTLIBPrinter.h"
...
//just before assert()
if(!hasSolution)
{
std::ofstream file("./failed-constraints.smt2");
ExprSMTLIBPrinter p(file,query);
p.setHumanReadable(true);
p.generateOutput();
file.close();
}
Using my version of KLEE you can also use a different solver (must be
SMTLIBv2 compliant and support the "get-value" command) (other than STP)
but it is still highly experimental so I'm not sure it would help you much
finding the bug. But if you wanted to try it you can run it like this...
$ klee -solver=smtlibv2 -solver-path=sonolar your_program.bc
I hope some of this is useful to you. Happy bug hunting :)
Thanks,
Dan Liew.
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
