| Age | Commit message (Collapse) | Author |
|---|
|
The rounding was removed because it was never needed:
llvm-mirror/llvm@ff278be
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.
|
|
|
|
reflect the fact that it simply returns a string
|
|
version that takes an argument a stream
|
|
|
|
dependency --output-istats is not
|
|
|
|
|
|
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
|
|
|
|
doDumpStates calls stepInstruction and therefore indirectly increases time and
instruction statistics for all dangling (dumped) states. This patch removes the
call, but now the timing stats for the last executed state are lost, as
StatsTracker::stepInstruction isn't called anymore.
|
|
|
|
|
|
llvm50 changed the semantics of SwitchInst::CaseIt and started using
"auto" variable type. So use it here too for all versions greater than
3.4 -- 3.4 does not support this semantics yet.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
|
|
on default searchers
|
|
Fixes klee/klee#717
delete on null pointer is always safe.
|
|
|
|
evalConstantExpr also resides), as suggested by an old comment.
|
|
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.
|
|
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.
|
|
Instead of using an id, use the assembly line number executed
|
|
llvm: get rid of static_casts from iterators
|
|
|
|
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.
|
|
|
|
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>
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
Moved printFileLine() to be part of KInstruction
|
|
|
|
|
|
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>
|
|
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.
|
|
too strict limitations (LLVM >= 3.0)
|
|
a…"
|
|
too strict limitations
|
|
Replaced an incorrect comma with a semicolon in the Executor constructor.
|
|
|
|
implement it in the solver.
|
