| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Fix signed division by constant 1/ -1
|
|
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
New version of the get initial values functionality which makes use of the independent solver.
|
|
The super-set check in the CexCachingSolver takes MUCH longer than the
sub-set check. Upon closer inspection, the super-set check gets slower
and slower as more counterexamples fill the UBTree. Pretty quickly,
the cost of the super-set check becomes larger than the time required
to simply bypass it and go to the Solver.
|
|
This function should be used solely in assertion statements and is
intended as a sanity check to make sure that the solution constructed
by IndependentSolver::getInitialValues() produces and answer that in
fact satisfies the the query.
|
|
Previous implementation simply passed the entire constraint forward
without any factoring of the constraint at all. This is a problem
since it is highly likely that there are cached solutions to pieces
of the constraint. The new implementation breaks the entire
constraint down into its requisite factors and passes each piece
forward, one by one, down the solver chain. After an answer is
returned, it is integrated into a larger solution. Since, by
definition, no factor can affect another, we can safely create a
solution to the larger constraint from the answers of its smaller
pieces.
The reconstruction of the solution is done by analyzing which parts of
an array a factor touches. If the factor is the only one to reference
a particular array, then all of the values calculated in the solution
for that array are included in the final answer. If the factor
references a particular element of the array (for example, arr[1]),
then only the value in index 1 of array arr will be included in the
solution.
|
