| Age | Commit message (Collapse) | Author |
|---|
|
to have only solver options.
|
|
|
|
* also adds klee-replay as dependency for systemtests
|
|
LLVM 4 renamed and splitted some headers. Take this into account in
includes.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
To enable the POSIX support, the former implementation instrumented the
main function and inserted a call to `klee_init_env` at the beginning.
This has multiple disadvantages:
* debugging information was not correctly propagated leaving the call to
`klee_init_env` without debug information
* the main function always required `int arg, char**` as part of the
function definition of `main`
Based on the new linking infrastructure, we can now add an additional
wrapper `__klee_posix_wraper(int, char**)` that gets always called when
POSIX support is enabled. It executes `klee_init_env` and after that
calls the `main` function.
Enabling POSIX support only requires the renaming of the user provided
`main` into `__klee_posix_wrapped_main` in addition to linking.
|
|
|
|
Replace the remaining occurrences of `Inst::Create()` with
`llvm::Builder` to manage metadata automatically and to fold
instructions.
C++11 it and clang-format
|
|
No need to flush it, see llvm-mirror/llvm@d4177b2
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Link intrinsic library before executing optimizations.
This makes sure that any optimization run by KLEE on the module
is executed for the intrinsic library as well.
Support .ll files as input for KLEE as well.
|
|
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
If an external function in KLEE is invoked, it might update errno.
Previously, the errno specific variable in a state was only updated
if it was part of the executed instructions.
That opened up a timeframe that increased the likelihood of errno being
overwritten by another method call.
This patch fixes two issues:
* the errno of the KLEE process state is updated before the external
function call allowing to detect changes to it later on
* after the external call, the memory object of errno is directly
updated
with its new value, reducing the likelihood to be overwritten by
another
call
Additional features:
* Add support for `errno()` for Darwin as well.
* Simplified errno handling in POSIX layer
|
|
|
|
Signed-off-by: Domenico Fabio Marino <nospamdomi@hotmail.it>
|
|
|
|
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.
|
|
Fixes klee/klee#717
delete on null pointer is always safe.
|
|
|
|
KLEE was always incremented, even if a symbolic solution was not found.
|
|
https://github.com/klee/klee/commit/db29a0bba74b672cdf4b8fef4d94ffa6ab845e6d
__fprintf_chk has a different prototype than fprintf
|
|
Request LLVM 3.4 as minimal requirement for KLEE
|
|
llvm: get rid of static_casts from iterators
|
|
- 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 commit b7a6aec4eeb4 (convert iterators using static_cast), I switched
all implicit casts to static_cast. It turned out that llvm 4.0 banned
casting via static_cast. See e.g. 1e2bc42eb988 in the llvm repo what
they do.
So similarly to the above commit, change all the casts of iterators to
"&*" which is what they do in LLVM.
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>
|
|
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>
|
|
`klee_open_output_file()` function so that it can be used by
the Z3Solver.
|
|
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>
|
|
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
Newer versions of LLVM do not allow to implicitly cast iterators to
pointers where they point. So convert all such uses to explicit
static_cast, the same as LLVM code does.
Otherwise we see errors like:
lib/Core/Executor.cpp:548:15: error: no viable conversion from 'Module::iterator' (aka 'ilist_iterator<llvm::Function>') to 'llvm::Function *'
Function *f = i;
^ ~
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
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>
|
|
This was a proposal from #500.
@andreamattavelli pointed out that the lit tests are really
system tests rather than integration tests so this commit fixes
the inappropriate naming that I chose.
|
|
|
|
|
|
|
|
|
|
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.
|
|
Links in the correct LLVM libraries when using the MCJIT. No effect for LLVM
versions less than 3.6
|
|
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.
|
|
In the description, --sym-argv and --sym-argvs should have instead been --sym-arg and --sym-args
|
|
klee_warning, and klee_error
|
|
function) (#455)
|
|
POSIX runtime. If the check fails, exit with an error. (#457)
|
|
|
|
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.
|
|
Added error message for -run-in directory errors
|
