| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
iostream injects static constructor function into every compilation unit.
Remove this to avoid it.
|
|
According to LLVM: lightweight and simpler implementation of streams.
|
|
it has been removed. From the LLVM 3.4 release notes:
"
The library call simplification pass has been removed. Its functionality
has been integrated into the instruction combiner and function attribute
marking passes.
"
|
|
of old V1 path API.
LLVM2.9 supports LLVM's V2 path API. Because that is the minimum
version we support we should just use this API everywhere so we
reduce the number of #if LLVM_VERSION_CODE macros and duplicated
code.
|
|
|
|
Old Path API was removed
|
|
of modules left because this information is no longer correct
(we no longer shrink the vector).
|
|
then clean up is performed.
|
|
because "RemovedSymbols" implies that the symbols have already been
removed which is misleading because we don't remove until the end.
|
|
|
|
Iterators get invalidated after elements of std::vector/set are
deleted. Avoid this by remembering which elements need to be
deleted and do it after iterating over the data structure.
|
|
KLEE intrinsics as undefined symbols
|
|
bitcode archive linker.
|
|
LLVM >= 3.3 by effectively reimplementing the linking algorithm
used in LLVM <= 3.2.
The LLVM specific bitcode archive format has been removed
from LLVM >= 3.3 . Now archives are normal system archives that can
contain LLVM bitcode modules as well as regular binary object files.
The previous commit implemented an approach where ALL the bitcode
modules get linked in which can be terribly slow when klee-uclibc gets
linked (~600 LLVM modules).
Here are the options that I considered to address this:
* Use LD with LLVM gold plug-in and call as an external program.
I Don't really want to add another dependency to KLEE. It already
has enough!
* Use the upcomming LLVM linker (lld). Not really an option
because at the time of writing there is no support for linking
archives of bitcode modules.
* Don't use archives at all and just work with modules (i.e.
replace uses of llvm-ar with llvm-link and tinker with the
flags a little). This isn't so great because the resulting
LLVM bitcode module we execute is bigger than it should be.
* Reimpelent bitcode archive linking ourselves in a slightly
better way.
I've gone for the last option
This implementation unfortunately loads all bitcode modules into memory
first so we can query the module symbols tables. I would prefer to read
the archive's index and link in modules on demand but unfortunately
although the new Object::Archive interface in LLVM allows iteration over
symbols it doesn't provide a way of knowing if that symbol is
defined/undefined.
This implementation is far from perfect!
|
|
With LLVM 3.3 the linker does not support reading of
archive files directly. This brings the support back
(based on llvm-mn).
Furthermore, linking single bc files or archives with
bc and object files mixed is supported as well.
|
|
In case linking of external libraries failed, user would
only be informed if KLEE is compiled with assertions enabled.
This fix lets KLEE always fail.
|
|
Existence of main() function is checked with assertion.
This check fails if KLEE is compiled in Release mode.
|
|
Feature klee internal functions
|
|
|
|
is actually available.
In addition if doing a DEBUG build then the command line flag
-debug-only=klee_missing_debug
shows the instructions missing debug information
and
-debug-only=klee_obtained_debug
show the instructions with debug information.
|
|
debug information is attached directly to most instructions so
the simpler algorithm added in 5ecfd6e2fd5becc10be355b3a20d014e76e40518
can be used.
Since support for LLVM version < 2.9 has been removed the old algorithm
should be removed.
This has been tested with LLVM 2.9 and LLVM 3.3
|
