| Age | Commit message (Collapse) | Author |
|---|
|
cece05cadf6a624afd188e81720ae7701736a703
|
|
running the Configure script.
|
|
|
|
be included by tools that needs to link against MetaSMT. Apart from
making the Makefile code cleaner this allowed the Solver unit test
linking to succeed when not building with STP support.
Unfortunately when using MetaSMT as the core solver the Solver unit
tests do not pass. Clearly no one tried this before... :(
|
|
support
|
|
|
|
|
|
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.
|
|
Fix independence solver leak
|
|
Removed Language: Cpp Entry from .clang-format
|
|
Clang 3.4.2
|
|
``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
|
|
Implement support for lowering the ``llvm.objectsize`` intrinsic
|
|
Fix a leak detected by ASan in the KQuery parser where on destruction of
|
|
Fix duplication of klee::ArrayHashFn
|
|
introduced in LLVM 2.7. Previously KLEE would emit the following error
message when ``IntrinsicLowering::LowerIntrinsicCall()`` was called on
the intrinsic
```
LLVM ERROR: Code generator does not support intrinsic function 'llvm.objectsize.i64.p0i8'!
```
The ``IntrinsicCleaner`` pass now lowers this intrinsic to a constant
integer depending on the second argument to the intrinsic. This
corresponds to the case where the size of the object pointed to by the
first argument is unknown.
An alternative design would be to handle this intrinsic in the Executor
where is actually possible to know the size of objects during execution.
However that would be much more complicated because if the pointer is
symbolic we would have to fork for every object that could be pointed
to.
The implementation is similar to #260 but we handle the second argument
to the intrinsic correctly and also have a simple test case.
Unfortunately we have to have a different version of the test case
for LLVM 2.9 because the expected suffix for the intrinsic is different
in LLVM 2.9.
|
|
the ``ParserImpl`` it wouldn't free allocated ``Identifier``s
|
|
``include/klee/util/ArrayCache.h``.
|
|
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
|
|
due to fixes from #315 and #316.
|
|
Try to fix leaking Array objects detected by ASan.
|
|
Some of these leaks were introduced by the factory constructor for Array
objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have
been around for far longer.
This leak was fixed by introducing a ``ArrayCache`` object which has two
purposes
* Retains ownership of all created ``Array`` objects and destroys them when
the ``ArrayCache`` destructor is called.
* Mimic the caching behaviour for symbolic arrays that was introduced
by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same
name and size get "uniqued".
The Executor now maintains a ``arrayCache`` member that it uses and
passes by pointer to objects that need to construct ``Array`` objects (i.e.
``ObjectState``). This way when the Executor is destroyed all the
``Array`` objects get freed which seems like the right time to do this.
For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is
used for building ``Array`` objects. This means that the Parser must
live as long as the built expressions will be used otherwise we will
have a use after free. I'm not sure this is the right design choice.
It might be better to transfer ownership of the ``Array`` objects to
the root ``Decl`` returned by the parser.
|
|
helper functions.
|
|
for it
|
|
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
|
|
Fix a memory leak in ``UpdateList`` detected by AddressSanitizer.
|
|
The overloaded assignment operator previously only deleted the head
``UpdateNode`` if the ``UpdateList`` had exclusive ownership which left the remaining
list of ``UpdateNode``s dangling if those nodes had ``refCount`` of 1.
To fix this the logic that was previously in the ``UpdateList`` destructor
for deleting nodes that were exclusively referenced by the UpdateList
has been moved into ``UpdateList::tryFreeNodes()`` so that it can be
called from ``UpdateList::operator=()``.
It looks like this bug has been in KLEE since the beginning.
|
|
which is required to suppress all the leaks I'm currently seeing in KLEE
when running ``make unittests`` and ``make check``.
Ideally there should be no leaks but we aren't there yet. Hopefully
at some point we won't need to suppress any leaks and then we can
have a TravisCI build that builds with ASan.
The leak of the expression objects when running the executor is worrying
and I will investigate this next.
|
|
MemorySanitzer and ThreadSanitizer environment variables when running
lit tests.
This makes it easy suppress errors in sanitized versions of KLEE
|
|
build. Spotted by @domainexpert
|
|
|
|
template braces get reformatted the C++11 way and that breaks
compilation.
|
|
flag as suggested by @ccadar
|
|
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
|
|
infeasible assumptions.
|
|
``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.
|
|
|
|
Fixing klee-clang to strip all flags not understood by llvm-link
|
