| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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>
|
|
|
|
|
|
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.
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
Core: explicitly create CallSite from Instruction
|
|
Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only.
|
|
Core: MCJIT functions need unique names
|
|
Module: simplify is_object checks
|
|
Moved printFileLine() to be part of KInstruction
|
|
|
|
Fix internal fork without new pathOS.id
|
|
|
|
|
|
Newer LLVMs do not allow implicit conversion from Instruction to
CallSite. We see this error:
Internal/Support/ModuleUtil.h:36:19: note: candidate function not viable: no known conversion from 'llvm::Instruction *' to 'llvm::CallSite' for 1st argument
llvm::Function *getDirectCallTarget(llvm::CallSite);
^
So explicitly create a CallSite from Instruction.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
to warnings.txt only. Disabled by default.
|
|
We will use newer MCJIT with newer LLVM versions. But it needs unique
names of functions or a wrong function can be called. So prepend
"dispatcher_" to function names (even for older LLVMs).
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
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>
|
|
object::Binary has isObject method, which can be used to check whether
it is an object::ObjectFile. Use that, since dyn_casting of
object::Binary is not allowed in newer LLVMs:
lib/Module/ModuleUtil.cpp:304:78: error: cannot convert ‘llvm::object::ObjectFile’ to ‘llvm::object::ObjectFile*’ in initialization
else if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(child.get()))
^
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Teach KLEE to respect the requested memory alignment of allocated memory
|
|
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>
|
|
variables when possible.
Previously an alignment 8 was always used which did not faithfully
emulate what was either explicitly requested in the LLVM IR or what
the default alignment was for the target.
|
|
New compilers warn about using 'register' as follows:
ConstantDivision.cpp:66:3: warning: 'register' storage class specifier is deprecated and incompatible with C++1z [-Wdeprecated-register]
Remove the register specifier -- the compilers are clever enough to know
what to do.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
controlled by a new parameter `moduleIsFullyLinked`. When
true the linkage type of a weak alias is ignored. It is legal to do
this when the module is fully linked because there won't be another
function that could override the weak alias.
This fixes a previous assertion failure in `klee::getDirectCallTarget()`
triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
|
|
too strict limitations (LLVM >= 3.0)
|
|
ReadExpr::create() was missing an opportunity to constant fold
|
|
constant arrays.
|
|
|
|
|
|
Modify scripts and a test to allow ASan/UBSan builds.
|
|
compiler warnings, one by adding an assert, and the other by refactoring the choose() function.
|
|
a…"
|
|
too strict limitations
|
|
When building with ASan the `mallinfo()` function is intercepted.
However the currently implementation is just a stub that always
returns 0. So instead use the public API of the sanitizer runtime
to get the amount of currently allocated memory when KLEE is built
with ASan.
Unfortunately it appears that the way to detect building with ASan
differs between Clang and GCC. There was also a sanitizer runtime
API change too.
This was tested with
* Clang 3.4, 3.5, and 3.9.0
* GCC 4.8, 4.9, 5.2, 5.4 and, 6.2.1.
|
|
|
|
Replaced an incorrect comma with a semicolon in the Executor constructor.
|
|
This was confusing because it would emit something like
`v1.0.0-290-g08d4716` because the 1.1.0 and 1.2.0 releases
didn't have a tag on the master branch so `git describe --tags`
would just find the `v1.0.0` tag and report based on that tag.
|
|
* Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving
its implementation into `Expr.cpp`.
* Document `Expr::compare(const Expr&)`.
This partially addresses #515 .
|
|
|
|
Reported by @jirislaby in #507.
|
|
This has shown that there is another circular dependency
(added by me! sigh...) between `kleeCore` and `kleeModule`.
|
|
implement it in the solver.
|
|
|
|
MartinNowack-fix_bfs2
|
|
add nicer error messages for --use-merge and add explanation why it currently cannot be used with random-path
|
|
|
|
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.
|
|
For performance reasons, if KLEE branches, one state is reused
and it is progressed by adding new constraints.
Make sure both new states end up at the end of the BFS searcher queue.
|
