| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
`klee_open_output_file()` function so that it can be used by
the Z3Solver.
|
|
into `Z3Builder.cpp` so they can be called from in gdb.
|
|
|
|
to guess it means timeout but I'm not 100% sure about this.
|
|
Fixed some KLEE messages and added build to .gitignore
|
|
|
|
Previous changes for LLVM 3.6 using the MCJIT were incredibly hacky.
Those changes required creating and destroying the ExternalDispatcher
for every call to an external function. This is really bad
* It's very poor design. The Executor should not need to know
about the internal implementation details of the ExternalDispatcher.
* It's likely very inefficient to keep creating and destroying the
external dispatcher.
The new code does several things.
* Moves all of the implementation details into a `ExternalDispatcherImpl`
class so that implementation details are not exposed in
`ExternalDispatcher.h`.
* When using the MCJIT a module is compiled for every (instruction, function)
tuple. This is necessary because the MCJIT compiles whole modules at a
time and once a module is compiled it cannot be modified and
re-compiled. Doing this means we get to reuse already generated code
for call sites which hopefully will reduce the overhead of repeatedly
executing the same call site.
A consequence of this change is that now the dispatcher function name
needs to be unique across all modules. To do this we just append the
module name because we guarantee that the module name is unique by
construction.
The code has also been clang-formatted.
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
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>
|
|
|
|
It seems there are have been quite a few changes upstream that
change the way CMake is invoked. There doesn't seem to be any good
reason for doing this.
|
|
version and a metaSMT version that requires RTTI
|
|
version used by metaSMT and test it with the combination LLVM-2.9 + metaSMT
|
|
|
|
|
|
|
|
|
|
[TravisCI] Check if `METASMT_VERSION` is set
|
|
indentation and syntax highlighting.
|
|
This is useful for testing ranges. Especially when tests are run on
later LLVM versions.
This code is funny as it uses 2, 3, and 4 spaces for indentation :).
This is extensively used in #605.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
[CMake] bitcode build system fixes
|
|
[Docker] Unbreak build.
|
|
that its value not being `linux` implies `osx`.
|
|
The recent landing of macOS support in TravisCI
(3a8bc6a43073b98b58c8cf0c20a930cb2c953b5d) broke the Docker build due to
the `TRAVIS_OS_NAME` environment variable not being set by the Docker
build. Do the simplest fix for now which is to define the variable. This
isn't the cleanest fix but it will do for now.
|
|
to clean the runtime build.
Unfortuantely there is no way to have the `clean` target trigger the
`clean_runtime` target unfortunately.
|
|
`ExternalProject_Add_Step()` so that when using Ninja the output of the
bitcode build system is shown immediately.
|
|
This fixes a bug in the bitcode build system where the build would
fail if the build directory was a symbolic link (i.e. create a symbolic
link for the root of the build tree and try to do the build in that
directory).
The problem was that `DIR_SUFFIX` implicitly assumed that there was
only one way to refer to the build tree which is an incorrect assumption
in the presence of symbolic links. This has been fixed by using the
`$(realpath)` GNU make built in to resolve all symbolic links.
An additional sanity check has been added to check that `SRC_DIR`
exists.
|
|
It looks like older LLVM versions that were built from SVN/git didn't
have a patch version number (i.e. `3.4svn` rather than `3.4.0svn`).
|
|
the `cmake` directory breaks KLEE's CMake build.
Just copy across the STP library for now. This really sucks.
The script needs to do a better job of installing MetaSMT and
its dependencies.
For reference here's the error.
```
CMake Error at /usr/lib/cmake/STP/STPTargets.cmake:67 (message):
The imported target "stp_simple" references the file
"/usr/bin/stp_simple"
but this file does not exist. Possible reasons include:
* The file was deleted, renamed, or moved to another location.
* An install or uninstall procedure did not complete successfully.
* The installation package was faulty and contained
"/usr/lib/cmake/STP/STPTargets.cmake"
but not all the files it references.
Call Stack (most recent call first):
/usr/lib/cmake/STP/STPConfig.cmake:15 (include)
/home/travis/build/klee/build/metaSMT/build/metaSMTConfig.cmake:6 (find_package)
cmake/find_metasmt.cmake:10 (find_package)
CMakeLists.txt:360 (include)
```
|
|
runtime: POSIX, make it compile with glibc 2.25
|
|
Travis-CI target for macOS
|
|
|
|
|
|
delcypher/unbreak_build_assignment_validating_solver
[CMake] Unbreak build due to not adding AssignmentValidatingSolver.cpp
|
|
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.
|
|
It looks like `deps/stp-git-basic/lib` contains a directory named
`cmake` so use `-r` instead in the hack in the `metaSMT.sh`.
We didn't catch this before because the script previously just
carried on executing if a command failed.
|
|
set. Also exit if any of the commands in `.travis/metaSMT.sh` fail.
|
|
|
|
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
test: POSIX, stop FD_Fail to fail
|
|
fixed version of metaSMT with this flag being properly set)
|
|
|
