| Age | Commit message (Collapse) | Author |
|---|
|
|
|
New compilers warn about using 'register' as follows:
ConstantDivision.cpp:66:3: warning: 'register' storage class specifier is deprecated and incompatible with C++1z [-Wdeprecated-register]
Remove the register specifier -- the compilers are clever enough to know
what to do.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
transitive dependencies on KLEE's libraries rather than on the final
binaries. This is better because it means we can build
other tools that use KLEE's libraries and not need to express the
needed LLVM dependencies.
It also makes it clearer what the dependencies are between KLEE
libraries. This has illustrated a problem with the `kleeBasic`
library. It contains `ConstructSolverChain.cpp` which clearly
belongs in `kleaverSolver` not in `kleeBasic`. This will be fixed
later.
|
|
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.
|
|
|
|
|
|
|
|
runAndGetCexForked())
|
|
|
|
|
|
operators
|
|
klee_warning, and klee_error
|
|
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.
|
