| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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>
|
|
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>
|
|
Module: simplify is_object checks
|
|
|
|
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>
|
|
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>
|
|
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.
|
|
Reported by @jirislaby in #507.
|
|
This has shown that there is another circular dependency
(added by me! sigh...) between `kleeCore` and `kleeModule`.
|
|
|
|
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.
|
|
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.
|
|
|
|
`dirty` flag if we remove `llvm.trap` from the module.
|
|
Extended support for assembler raising
|
|
function) (#455)
|
|
Improved support for assembler handling.
Providing additional triple information
to raise assembler for supported architectures
only.
Implemented support for raising full assembly
memory fence.
Added initial support for memory fences in Executor.
|
|
|
|
error to use [] operator for accessing vector's elements after reserving. In such cases push_back/emplace methods should be used. But in this source code the usage of std::vector is redundant. So vector 'values' was iliminated.
|
|
CallInst::getOperand() uses incompatible operand orders across LLVM
versions. Use CallSite::hasArgument() instead. This bug prevented the
MD2U searcher from working correctly.
|
|
introduced in LLVM 2.7. Previously KLEE would emit the following error
message when ``IntrinsicLowering::LowerIntrinsicCall()`` was called on
the intrinsic
```
LLVM ERROR: Code generator does not support intrinsic function 'llvm.objectsize.i64.p0i8'!
```
The ``IntrinsicCleaner`` pass now lowers this intrinsic to a constant
integer depending on the second argument to the intrinsic. This
corresponds to the case where the size of the object pointed to by the
first argument is unknown.
An alternative design would be to handle this intrinsic in the Executor
where is actually possible to know the size of objects during execution.
However that would be much more complicated because if the pointer is
symbolic we would have to fork for every object that could be pointed
to.
The implementation is similar to #260 but we handle the second argument
to the intrinsic correctly and also have a simple test case.
Unfortunately we have to have a different version of the test case
for LLVM 2.9 because the expected suffix for the intrinsic is different
in LLVM 2.9.
|
|
Support directory
|
|
It failed when the function being called is a bitcasted alias.
|
|
|
|
Instead of checking for every possible casse which result in overflow,
it is much simpler to perform the operation using integers with bigger
dimension and check if the result overflow
|
|
Previously the check was done as
unsigned int a, b, c;
c = a * b;
if (c < a)
// error
but it is wrong, since it catches only a subset of all the
possible overflows.
This patch improves the check as
unsigned int a, b, c;
if ((a > 1) && (b > 1){
if ((UINT_MAX/a) < b)
// error
}
An additional case has been added to the tests, with two 32-bit
values that cause overflow and are not detected by the old check.
It is also necessary to break the lowering procedure in case the current
BasicBlock is splitted; in this case it was necessary in order not to
trigger the division by 0 error.
|
|
This requires clang with -fsanitize=unsigned-integer-overflow
tested with clang and llvm 3.4.2
|
|
Will redo the merge to preserve original commits.
This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
|
|
and mul operations. Refactored tests into two main cases, and
disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
|
|
assertion entirely?
|
|
|
|
|
|
|
|
|
|
- Mostly fixed by removing unnecessary references.
|
|
|
|
|
|
- This makes KCachegrind output look nicer, as otherwise it assumes
instructions without debug info were inlined and shows some message to that
effect.
- This does however we might be lying a bit about the source line that an
instruction came from.
- This also adds a test case for our istats output, yay!
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
|
- The change in 6829fb9 caused us to not allocation InstructionInfo objects for
instructions without source-level debug info, however, that means that all
such instructions end up sharing the one dummy InstructionInfo object, which
really breaks statistics tracking.
- This commit basically reverts that change, and also changes the code so we
don't ever use the dummy InstructionInfo object for instructions, so that
this problem can't be hit in other ways (e.g., if someone modifies the module
after the InstructionInfoTable construction). There is a FIXME for checking
the same thing for functions.
- Fixes #144.
|
