| Age | Commit message (Collapse) | Author |
|---|
|
assignments against the corresponding `Query` object and check the
assignment evaluates correctly.
This can be switched on using `-debug-assignment-validating-solver`
on the command line.
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
|
|
It was marked as deprecated long time ago and finally removed in LLVM
3.9. Remove all uses of getGlobalContext and create our own context.
Propagate it all over the code then.
[v2] use ctx, not C as name
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Pass the list as reference. Otherwise we can get errors with newer LLVM
like:
lib/Basic/ConstructSolverChain.cpp:26:19: error: call to deleted constructor of 'llvm::cl::list<QueryLoggingSolverType>'
if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) {
^~~~~~~~~~~~~~~~~~~
llvm/Support/CommandLine.h:1466:3: note: 'list' has been explicitly marked deleted here
list(const list &) = delete;
^
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
controlled by a new parameter `moduleIsFullyLinked`. When
true the linkage type of a weak alias is ignored. It is legal to do
this when the module is fully linked because there won't be another
function that could override the weak alias.
This fixes a previous assertion failure in `klee::getDirectCallTarget()`
triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
|
|
|
|
width greater than 64
|
|
|
|
compiler warnings, one by adding an assert, and the other by refactoring the choose() function.
|
|
This was confusing because it would emit something like
`v1.0.0-290-g08d4716` because the 1.1.0 and 1.2.0 releases
didn't have a tag on the master branch so `git describe --tags`
would just find the `v1.0.0` tag and report based on that tag.
|
|
* Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving
its implementation into `Expr.cpp`.
* Document `Expr::compare(const Expr&)`.
This partially addresses #515 .
|
|
and make it a pure virtual method. Also make it protected rather than
public because it is an implementation detail of `Expr::compare()`.
This means that sub classes must implement it so this commit also
provides implementations. The comparision behaves as before except
for `ConcatExpr` where its `width` attribute is now used (previously
it wasn't).
This commit also documents the semantics of `Expr::compareContents(const Expr&)`
which was clearly needed because it has been incorrectly implemented
in the past and has gone unnoticed for several years.
This partially addresses #515 .
|
|
`compareContents()`.
This bug would not have affected correctness but it would have
affected performance because if `Expr::compare()` was called on
two structually equal `NotExpr` then its children would be
checked for structually equality twice - once in
NotExpr::compareContents()` and once in `Expr::compare()`.
This partially addresses #515 .
|
|
|
|
This is done as a separate commit because it imports
third party code. It's under the Boost license though
so it "should be" fine.
|
|
This is based off intial work by @jirislaby in #481. However it
has been substantially modified.
Notably it includes a separate build sytem to build the runtimes which
is inspired by the old build system. The reason for doing this is
because CMake is not well suited for building the runtime:
* CMake is configured to use the host compiler, not the bitcode
compiler. These are not the same thing.
* Building the runtime using `add_custom_command()` is flawed
because we can't automatically get transitive depencies (i.e.
header file dependencies) unless the CMake generator is makefiles.
(See `IMPLICIT_DEPENDS` of `add_custom_command()` in CMake).
So for now we have a very simple build system for building the runtimes.
In the future we can replace this with something more sophisticated if
we need it.
Support for all features of the old build system are implemented apart
from recording the git revision and showing it in the output of
`klee --help`.
Another notable change is the CMake build system works much better with
LLVM installs which don't ship with testing tools. The build system
will download the sources for `FileCheck` and `not` tools if the
corresponding binaries aren't available and will build them. However
`lit` (availabe via `pip install lit`) and GTest must already be
installed.
Apart from better support for testing a significant advantage of the
new CMake build system compared to the existing "Autoconf/Makefile"
build system is that it is **not** coupled to LLVM's build system
(unlike the existing build system). This means that LLVM's
autoconf/Makefiles don't need to be installed somewhere on the system.
Currently all tests pass.
Support has been implemented in TravisCI and the Dockerfile for
building with CMake.
The existing "Autoconf/Makefile" build system has been left intact
and so both build systems can coexist for a short while. We should
remove the old build system as soon as possible though because it
creates an unnecessary maintance burden.
|
|
* Add unittest to check that the `Assignment` class can evaluate
expressions containing a `NotOptimizedExpr`.
* Fix the `AssignmentTest.FoldNotOptimized` unit test by
teaching the `ExprEvaluator` to fold `NotOptimizedExpr` nodes.
|
|
The previous change altered .ac files, regenerate the scripts.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
function) (#455)
|
|
functions.
|
|
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.
|
|
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.
|
|
|
|
|
|
* ``-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.
|
|
in the range of ``BinaryKindFirst`` and ``BinaryKindLast``. ``NotExpr``
is a unary expr not a binary expression.
|
|
The SELinux function signatures have changed between version 2.2 and
2.3. In particular, the type of the "security context" parameter was
changed from char * to const char *, with the following patch:
SELinuxProject/selinux@9eb9c9327563014ad6a807814e7975424642d5b9.
Recent Linux distributions (e.g. Ubuntu 15.10) ship with the updated
version of libselinux. This change makes the SELinux runtime compatible
with the newer versions of the library by replacing security_context_t
with its original char * definition and defining it as const only if the
installed library does so. Whether the system uses const char * types is
detected with the configure script.
Fixes klee/klee#303.
|
|
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.
|
|
|
|
that it's possible to call it from gdb.
|
|
sub-class rather than the first. Whilst I'm here clang-format the
moved code.
The motivation for this is that ``ConstantExpr`` may need to refer to a
type that cannot be forward declared (e.g. some kind of enum) in the
other ``Expr`` sub-classes.
For example if an Expr sub-class is ever introduced that has contains an
enum that is used for its constructor then the previous ordering would prevent
a Constant evaluation method (e.g. ``ConstantExpr::MyNewExprType(const
ref<ConstantExpr> &RHS, MyNewType::SpecialEnum p)``) from being
implemented because the ``MyNewType::SpecialEnum`` type has not yet been
declared.
|
|
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``.
|
|
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.
|
|
|
|
solver using the new ``--with-z3=`` option.
|
|
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...
|
|
``include/klee/util/ArrayCache.h``.
|
|
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
|
|
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.
|
|
|
|
|
|
Support directory
|
|
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.
|
|
New version of the get initial values functionality which makes use of the independent solver.
|
|
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
|
