| Age | Commit message (Collapse) | Author |
|---|
|
with another solver. For example the core solver can be STP and the
cross checking solver can be Z3.
Unfortunately a few fragile tests don't pass when actually using this
option.
|
|
|
|
In some Solver sources, some error outputs were missing \n. Instead of
adding a new line to all of them, convert the fprintf's to
klee_warning which adds \n automatically.
ErrorHandling.h had to be included in MetaSMTSolver.cpp to have
klee_warning declared there.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Added test case exposing division by zero failure reported by @kren1 and made division total in STP to fix it.
|
|
|
|
Generated STP equality expressions have to be the same type.
If a shift with different types as operands was used,
therefore equality expressions of different width were generated.
Beside avoiding the different sizes, this patch restores the
original behavior to extract just the part involved in shifting
and therefore should generate smaller expressions.
Enable sdiv test case
|
|
Provide initial zlib-based compression support for
raw_outstreams. Replacing llvm::raw_fd_outstreams
with compressed_fd_outstreams automatically compresses
data in gzip format before writing to file.
Options added:
* --compress-log to compress all query log files (e.g. *.pc, *.smt2) on
the fly. Every query log file gets extended with .gz.
* --debug-compress-instructions to compress logfile for instruction
stream on the fly.
|
|
have the same bv width
|
|
64, so that the first two arguments of the call bvVarRightShift(extend_npm, expr_shpost, 64) have the same bitwidth of 64.
|
|
|
|
|
|
|
|
|
|
|
|
0 when overshifting
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Generate unique STP and Z3 array names deterministically
|
|
Bug fix in IndependentSolver
|
|
|
|
@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 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.
|
|
|
|
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.
|
|
own file ``STPSolver.cpp``. Whilst I'm here also clang-format the
modified code.
|
|
``DummySolver.cpp``. Whilst I'm here also clang-format the modified code.
|
|
``ValidatingSolver.cpp``. Whilst I'm here also clang-format the modified
code.
|
|
(SolverImpl.cpp). Whilst I'm here also clang-format the modified
code.
|
|
``IndependentSolver::computeInitialValues()`` was called where at least
one of the constraint sets computed by
``getAllIndependentConstraintsSets()`` is either unsatisfiable or
the solver failed.
To make things (a little) clearer I've made it so that no
``std::list<>*`` is passed to``getAllIndependentConstraintsSets()``.
Instead ``getAllIndependentConstraintsSets()`` now returns a
``std::list<>*`` that the caller is responsible for cleaning up. The
behaviour previously was really confusing because it was unclear if the
caller or callee was responsible for the clean up.
This fixes #322
|
|
Reformat ``getAllIndependentConstraintsSets()`` using clang-format.
It was not formatted correctly and was consequently a little hard
to read. Also add braces around a for loop body.
The original code for this function came from
d9bcbba2c94086039c11c86200670639ee2ec19f
|
|
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
|
|
Use "-debug-dump-stp-queries" argument for KLEE/Kleaver
to print out each STP query sent to the STP Solver.
Queries have the format which `stp` frontend can understand.
|
|
|
|
|
|
Support directory
|
|
``stp/stplog.h`` header file in the current version of STP
and no support in the build system for setting this define so
this code is completly dead.
|
