| Age | Commit message (Collapse) | Author |
|---|
|
Add the ability to control whether the pretty printer uses line breaks
|
|
This change makes it possible to more reliably write unit tests which check
that an expression is equivalent to an expected pretty printed string.
|
|
Modify the SMT-LIB printer to declare arrays in a deterministic (alphabetical) order.
|
|
(alphabetical) order.
|
|
|
|
instruction in main().
|
|
|
|
optimizations are enabled.
|
|
Overshift fixes
|
|
that is the samw width of the "expr" expression.
It probably is the same width (it defintely is in SMT-LIB but I'm not
sure about STP) but it is probably better to be explicit.
|
|
|
|
behaviour for arithmetic right shift are identical.
|
|
overshifts to zero. Test case is included.
|
|
to zero. Test case is included.
|
|
behaviour for logical right shift are identical.
|
|
overshifts to zero. Test case is included.
|
|
to zero. Test case is included.
|
|
behaviour for left shift are identical.
|
|
zero. A test case was added for this.
In addition the use to vc_bvExtract() was removed for shifting left by an
expression because we don't want/need bitmasked behaviour anymore.
|
|
a bug in the previous commit where 32-bit width was assumed.
|
|
The other shift operators still need to be changed
|
|
Upstream STP's libstp now depends on boost.
|
|
Add support for archive and single bc file linking
|
|
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.
|
|
|
|
|
|
Allow passing arbitrary command line flags to klee and kleaver when running llvm-lit
|
|
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
|
|
that clients can access HandlerInfo nicely.
|
|
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.
|
|
variables in llvm-lit. This should hopefully fix the build bot.
The propagation of environmental variables was also slightly refactored.
|
|
Fix Runtime/POSIX/Isatty.c test under LLVM3.3.
|
|
a call fprintf(stderr,...). llvm-gcc transforms this to a call to
fwrite() however clang does not so klee-uclibc's fprintf will be
called instead and if klee-uclibc is compiled with KLEE_SYM_PRINTF
then output will always go stdout if the FILE is stdout or stderr.
The end result of this is that when we build with Clang under LLVM3.3
is that the fprintf(stderr,...) print outs go to standard output instead
and so the test would fail because it expects the fprintf(stderr,...)
to be on stderr.
This test sort of fixes this by having the test check stdout for
the fprintf(stderr,...) statements too.
|
|
when running llvm-lit. This is done by doing something like
$ cd test/
$ llvm-lit --param klee_opts=--xxx --param kleaver_opts=--yyy .
This would pass "--xxx" as an extra option to KLEE when running
tests and would pass "--yyy" as an extra option to kleaver when
running tests.
This feature has been added to make it easy to pass different flags to
KLEE or Kleaver without needing to modify tests or recompile KLEE with
different defaults (yuck!).
|
|
the configure script to detect this by first trying to link without
boost and if that fails then trying to link libstp with boost.
This also updates the relevant Makefiles so that the klee and kleaver
executables link in STP's boost dependencies if necessary.
|
|
Move testing infrastructure to llvm-lit and completly remove all DejaGNU support
|
|
e.g.
$ make check VERBOSE=1 # Shows command and shows more detail
$ make check # Does not show command and shows summary
|
|
We need to fix the test suite so we can run it in parallel.
|
|
|
|
support.
|
|
The problem is newer LLVM versions (e.g. 3.3) detect python at
their configure time whereas older versions don't (i.e. 2.9). So
I don't want to add python detection to KLEE's configure if LLVM
already does the work for us. We need to move off llvm 2.9 anyway.
|
|
Say hello to our new friend, llvm-lit :)
|
|
standing FIXME:
|
|
time.
|
|
tests from being executed if not enabled at configure time.
|
