| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This is too generic and llvm 6.0 defines DEBUG as follows:
#define DEBUG(X) DEBUG_WITH_TYPE(DEBUG_TYPE, X)
This then results in various build failures where once the macro is
defined, once it is not.
So rename this generic macro to KLEE_ARRAY_DEBUG.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
compile flags accordingly
|
|
|
|
configuration, TravisCI scripts and Dockerfile build appropriately.
There are a bunch of clean ups this enables but this commit doesn't
attempt them. We can do that in future commits.
|
|
|
|
|
|
MetaSMTSolver.cpp so that the backend headers only need to be included once there
|
|
|
|
option.
This lets us see what Z3 is doing execution (e.g. which tactic is being
applied) which is very useful for debugging.
|
|
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.
Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.
This partially addresses #653. We still need to try rolling our
own custom tactic.
[1] https://github.com/Z3Prover/z3/issues/1035
|
|
solver. This is to avoid tampering with the cache of the builder the
solver is using.
|
|
Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be
logged to a file. The files logged by this option can be replayed by the
`z3` binary (using its `-log` option). This is incredibly useful because
it allows to exactly replay Z3's behaviour outside of KLEE.
|
|
This can be enabled by passing the command line option `-debug-z3-validate-models`.
Although Z3 has a global parameter `model_validate` (off by default) I don't trust it
so do the validation manually. This also means we can potentially do
validation on a per Z3Solver instance basis rather than globally.
When failing to validate a Z3 model the solver state and model are
dumped to standard error.
|
|
is useful for getting access to the constraints being stored in the Z3
solver in the SMT-LIBv2.5 format.
|
|
into `Z3Builder.cpp` so they can be called from in gdb.
|
|
|
|
to guess it means timeout but I'm not 100% sure about this.
|
|
Based on work by @ccadeptic23 and @delcypher.
Formatting fixed by @snf.
Fix compiler warning by @martijnthe.
Further fixes by @mchalupa.
Refactored, so that changes can be reviewed -- no massive changes in
whitespace and in the surrounding code.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
to list of source files.
The cause of the breakage was me being to eager and merging #468
before forcing tests to re-run. That PR was written before the CMake
build system existed.
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
