| Age | Commit message (Collapse) | Author |
|---|
|
This is useful on systems like NixOS, where python3 is not in
/usr/bin/python3 as well as for people using alternative ways to
install python such as virtualenv/pyenv.
Some scripts where already using '/usr/bin/env'. With this pull request
it gets more consistent. For background information see also:
https://github.com/systemd/systemd/pull/5816
|
|
follow up of c9c90a0ecdce10172fd5318aea60a9ff4057679f
|
|
A few runtime build system fixes
|
|
Remove support for LLVM < 3.4
|
|
provide a better error message (and stop earlier) when no C source
files are found.
|
|
archive/modules when the list of source files that constitute it
changes.
To fix this a file is written in the build directory that contains
the list of `.bc` files. This file is updated whenever the list of
`.bc` files for a module changes and then the rule that builds the
module/archive depends on that file.
This fixes a bug reported by @ccadar in #718.
|
|
|
|
|
|
|
|
|
|
Request LLVM 3.4 as minimal requirement for KLEE
|
|
|
|
|
|
Implement basic support for vectorized instructions.
|
|
pass that checks these assertions. This improves several things.
* This pass provides more friendly messages than assertions in that it
just emits a warning and carries on checking the rest of the
instructions.
* The takes the checks outside of the Executor's hot path and so avoids
checking the same instruction multiple times. Now each instruction
is only checked once just before execution starts.
The disadvantage of this approach is the check for invariants we expect
to hold have been pulled far away from where we expect them to hold.
After discussion with @ccadar and @MartinNowack it was decided we will
take this hit to readability for better performance and simpler code in
the Executor.
|
|
Core: TimingSolver, use WallTimer
|
|
Do not opencode what we already have in TimerStatIncrementer. This
simplifies the code a lot and makes transition to LLVM 4.0 a lot easier.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Fixes bug in TreeStreamWriter::write reported by @gladtbx in #562. A…
|
|
other a regression test for #562
|
|
We use LLVM's Scalarizer pass to remove most vectorized code so that the
Executor only needs to support the InsertElement and ExtractElement
instructions.
This pass was not available in LLVM 3.4 so to support that LLVM version
the pass has been back ported.
To check that the Executor is not receiving vector operand types
that it can't handle assertions have been added.
There are a few limitations to this implementation.
* The InsertElement and ExtractElement index cannot be symbolic.
* There is no support for LLVM < 3.4.
|
|
removes commented out code from that function.
|
|
Instead of using an id, use the assembly line number executed
|
|
llvm: get rid of static_casts from iterators
|
|
Added caching of Homebrew downloads
|
|
|
|
|
|
- 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>
|
|
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>
|
|
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.
|
