| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
DejaGNU testing used to have this flag in its substitution variable
but for llvm-lit this has not been done.
I could replicate what DejaGNU did but by forcing developers to be
explicit when creating LLVM bitcode
* Remove test suite inconsistentcies. Some tests explictly use
-emit-llvm
* Allows for tests to be written in the future that invoke
the compiler as a native compiler
|
|
in this directory. I don't know why these tests are here, they
weren't executed before by DejaGNU.
|
|
* Ignore lit.site.cfg file.
|
|
are now broken and will be fixed shortly.
|
|
seemed to causing problems for llvm-lit's parser.
|
|
properly at configure time at some point.
|
|
in test environment.
|
|
{ } quotes. I also add FileCheck lines but I've not added running
FileCheck because only new versions of FileCheck support the CHECK-DAG:
syntax.
|
|
a file created by KLEE exists. A big difference between
DejaGNU and llvm-lit is that in DejaGNU the working directory
is the test output directory (e.g. test/Feature/Output) but
in llvm-lit the working directory is the test directory
(e.g. test/Feature )
To fix this I have used the %T substitution variable for llvm-lit.
I have also improved some tests by using LLVM's FileCheck tool
and removing of hard coded constants for data type size in
some places.
This commit inevitably breaks running the tests under DejaGNU.
Although it is possible to hack by introducing the %T substitution
variable some tests would still be broken because the use of shell
pipes in DejaGNU doesn't seem to work properly. I could work around
this but it's really not worth the effort.
|
|
|
|
version that KLEE and llvm-as use is the same.
|
|
This is needed because the helper tool 'not' is used by some tests
|
|
|
|
|
