| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
0 when overshifting
|
|
|
|
|
|
|
|
--with-metasmt-default-backend and improve the associated CXX flag
|
|
|
|
|
|
|
|
Fixed bug #375 in Kleaver's parser and added --clear-array-decls-after-query option to Kleaver.
|
|
|
|
|
|
The option now contains 4 different options:
1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst];
2) src:stderr, which logs all instructions to file in format [src, inst_id];
3) compact:stderr, which logs all instructions to file in format [inst_id];
4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst];
5) src:file, which logs all instructions to file in format [src, inst_id];
6) compact:file, which logs all instructions to file in format [inst_id];
Writing to file gives a speedup of ~50x.
|
|
Generate unique STP and Z3 array names deterministically
|
|
Bug fix in IndependentSolver
|
|
currently buggy, and we keep hitting this bug... See https://github.com/klee/klee/issues/334 for details.
|
|
Partial logging of queries
|
|
|
|
AllocaInst.
|
|
* ``-replay-out`` to ``-replay-ktest-file``
* ``-replay-out-dir`` to ``-replay-ktest-dir``
and also rename
* help descriptions
* global variables corresponding to these options.
* Names used in ``KleeHandler``, ``Interpreter``, ``Executor``
and in KLEE's ``main()`` function.
The old name for the options/code was very unhelpful as it wasn't
obvious that "out" files are ``.ktest`` files unless you examine KLEE's
source code.
|
|
@delcypher: Thanks a lot Dan!
|
|
|
|
|
|
``IndependentSolver::computeInitialValues(...)`` satisfies the whole
query. The previous commit only checked expressions evaluated to true
where there was an assignment for ``Array`` objects that the caller
asked for. This is incomplete and may miss problems with the assignment.
Instead in ``assertCreatedPointEvaluatesToTrue()`` augment the
``Assignment`` object with additional arrays in the ``retMap`` map.
|
|
The address of KLEE-internal data structures should not influence the
order arrays are printed out.
Order arrays by name.
|
|
The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the
IndependentSolver assumed that it would be given an assignment for every
array. If this wasn't the case the ``Assignment`` object by default
would just replace every read of an unknown array with a byte filled
with zeros.
This problem would appear if
``IndependentSolver::getInitialValues(...)`` was called without asking
for assignment for used arrays.
I saw two ways of fixing this
* Get an assignment for all arrays even if the client didn't ask
for them. This guarantees that is the query is satisfiable then
we can compute a concrete assignment.
* Just do a "best effort" check and only check expressions that can
be fully assigned to.
I chose the latter because the first option seems pretty wasteful,
especially for an assert.
The second option isn't ideal though as it would be possible to
compute an assignment that for the whole query leads to "unsat"
but we wouldn't notice.
|
|
|
|
error to use [] operator for accessing vector's elements after reserving. In such cases push_back/emplace methods should be used. But in this source code the usage of std::vector is redundant. So vector 'values' was iliminated.
|
|
of some.
|
|
Add support for tcmalloc
|
|
A few Expr related clean ups
|
|
|
|
|
|
Beside improving performance of KLEE,
tcmalloc allows to track used memory correctly.
If available, tcmalloc is automatically used during compile time.
This can be forced to be:
- disabled using --without-tcmalloc
- enabled using --with-tcmalloc
In the second case, configure will fail if tcmalloc
is not found or usable.
Both versions of tcmalloc a minimal and normal version.
|
|
|
|
a message stating this.
|
|
that it's possible to call it from gdb.
|
|
|
|
The implementation of the constructor calls a method on a ``ConstantExpr``
which means the type must be complete (i.e. a forward declaration of
``ConstantExpr`` is insufficient) which creates an unnecessary ordering
Dependency in ``Expr.h``.
|
|
CallInst::getOperand() uses incompatible operand orders across LLVM
versions. Use CallSite::hasArgument() instead. This bug prevented the
MD2U searcher from working correctly.
|
|
for the ``Z3_get_error_msg()`` function.
|
|
which is based on the work of Andrew Santosa (see PR #295) but fixes
many bugs in that implementation. The implementation communicates
with Z3 via it's C API.
This implementation is based of the STPSolver and STPBuilder and so it
inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped
out some of the optimisations (constructMulByConstant,
constructSDivByConstant and constructUDivByConstant) that were used in
the STPBuilder because
* I don't trust them
* Z3 can probably do these for us in the future if we use the
``Z3_simplify()``
At a glance its performance seems worse than STP but future work can
look at improving this.
|
|
|
|
|
|
|
|
The default core solver is STP if KLEE is built with STP otherwise
it is MetaSMT.
Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for
consistency.
|
|
a ``createCoreSolver()`` function. The solver used is set by the new
``--solver-backend`` command line argument. The default is STP.
This change necessitated refactoring the MetaSMT stuff. That clearly
didn't belong in the Executor! The MetaSMT command line option is
now ``--metasmt-backend`` as this only picks the MetaSMT backend.
In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed.
Note I don't have MetaSMT built on my development machine so I don't
know if the MetaSMT stuff even compiles...
|
|
|
|
their own file ``MetaSMTSolver.cpp``. Whilst I'm here also clang-format
the modified code.
This might not be a NFC (non functional change) as there's a good chance this
has broken the MetaSMT build of KLEE. I don't have a build of MetaSMT to hand
and there is no TravisCI build. At this point because there is no maintainer
for this code I think we should consider removing it as it is going bitrot.
|
