| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- having an explicit function which is defined for multiple llvm
versions separately increases readability.
- also: error handling was simplified
- Personal motivation: being able to use this functionality in unit tests
fixes #561
related to #656
|
|
In LLVM 3.7, PassManager was moved to the legacy:: namespace. Introduce
a type for it and use it in the code.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
llvm37: do not copy DILocation to getDSPIPath
|
|
DILocation is not copyable in LLVM 3.7. So, pass it as reference and
make it const given we do not write to it.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
It became unnecessary when defining options and mainly undefined.
So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Fixed typos in comments related to vararg support.
|
|
Removing flaky test Vararg.c from Darwin build until we find a proper…
|
|
|
|
|
|
ExitOnError collides with llvm::ExitOnError from LLVM 4:
tools/klee/main.cpp:430:23: error: reference to 'ExitOnError' is ambiguous
if (errorMessage && ExitOnError) {
^
/usr/include/llvm/Support/Error.h:938:7: note: candidate found by name lookup is 'llvm::ExitOnError'
class ExitOnError {
^
klee/tools/klee/main.cpp:141:3: note: candidate found by name lookup is '(anonymous namespace)::ExitOnError'
ExitOnError("exit-on-error",
^
1 error generated.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Fix test failure on systems with libstdc++ corresponding to gcc7.
|
|
|
|
This fixes #664.
As reported by @jirislaby the `test/Feature/LongDouble.cpp` test
fails to compile with Clang 3.4 due to new changes the libstdc++
headers. This ends up giving errors like
```
In file included from /home/abuild/rpmbuild/BUILD/klee-1.3.0+20170409/test/Feature/LongDouble.cpp:12:
In file included from /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/cstdlib:77:
/usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:101:3: error: unknown type name '__float128'
__float128
^
/usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:102:7: error: unknown type name '__float128'
abs(__float128 __x)
^
2 errors generated.
```
Clang 4.0 seems fine with this source file so the problem has already
been addressed upstream so we don't need to file a bug. We just need
to move to a newer LLVM version to fix this properly!
To work around this the test has been made into a C program rather than
a C++ program to avoid including the C++ headers. The program wasn't
using any important C++ features anyway so this seems like a sensible change.
|
|
|
|
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.
|
|
`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.
|
