| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Added support for hiding command-line options
|
|
Fixes klee/klee#717
delete on null pointer is always safe.
|
|
|
|
|
|
|
|
Added checks for div/mod by zero and overshifts in constant expressio…
|
|
|
|
Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268.
|
|
|
|
On FreeBSD <sys/capabilities.h> is present in libc, so we don't require libcap there.
Close and write functions are located in <unistd.h>.
|
|
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
|
|
location as a string. Also added const qualifier to the printFileLine functions
|
|
|
|
Refactored some code related to constant evaluation
|
|
evalConstantExpr also resides), as suggested by an old comment.
|
|
|
|
follow up of c9c90a0ecdce10172fd5318aea60a9ff4057679f
|
|
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.
|
|
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>
|
|
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
|
|
|
|
- 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>
|
|
|
|
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.
|
|
|
|
|
|
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.
|
