| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
It allows stopping the execution on some conditions like assertions.
The use is like:
klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm
This is especially useful in the SV-COMP.
A test to cover the new parameter was added too.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Sometimes, globals are not sized and ->getTypeStoreSize on such type
crashes inside the LLVM. Check whether type is sized prior to calling
the function above.
A minimalistic example of Y being unsized with no effect on the actual
code is put to tests.
[v2]
Use klee_warning for printing. And use %.*s formatting string given
StringRef.data() need not be null terminated.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
This patch generates the states based on the order of switch-cases.
Before, switch-constraints were randomly assigned to forked states.
As generated code might be different between LLVM versions,
we use the case values, order them, and iterate in that order
over the cases.
This way we can also support deterministic execution of older LLVM
versions.
|
|
Deterministic adding/removing of states.
|
|
Provide initial zlib-based compression support for
raw_outstreams. Replacing llvm::raw_fd_outstreams
with compressed_fd_outstreams automatically compresses
data in gzip format before writing to file.
Options added:
* --compress-log to compress all query log files (e.g. *.pc, *.smt2) on
the fly. Every query log file gets extended with .gz.
* --debug-compress-instructions to compress logfile for instruction
stream on the fly.
|
|
The option now contains 4 different options:
1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst];
2) src:stderr, which logs all instructions to file in format [src, inst_id];
3) compact:stderr, which logs all instructions to file in format [inst_id];
4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst];
5) src:file, which logs all instructions to file in format [src, inst_id];
6) compact:file, which logs all instructions to file in format [inst_id];
Writing to file gives a speedup of ~50x.
|
|
This allows a user to invoke klee with specific libraries to load from
command line. This is an attempt to allow klee to run on applications
linked to external libraries.
The libraries still have to be compiled specially for klee, in a manner
similar to klee-uclibc, i.e. archives (build with llvm-ar) of llvm IR
files.
|
|
``test/Feature/SolverTimeout.c`` test fails there.
The error message I see in TravisCI is
```
Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc"
Command 2 Result: -11
Command 2 Output:
Command 2 Stderr:
KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out"
KLEE: WARNING: undefined reference to function: printf
KLEE: ERROR: (location information missing) divide by zero
KLEE: NOTE: now ignoring this error at this location
0 klee 0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1 klee 0x0000000000da85c9
2 libpthread.so.0 0x00007fca19936cb0
3 libz3.so 0x00007fca19079826
4 librt.so.1 0x00007fca1747640c
5 libpthread.so.0 0x00007fca1992ee9a
6 libc.so.6 0x00007fca1776c38d clone + 109
```
The issue appears to be racey as I had to run several copies of KLEE in
parallel for the bug to occur using Z3 4.4.1. I managed to get a
coredump and got the backtrace from gdb for the crash which is
```
#0 0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112
#1 0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63
#2 0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312
#3 0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111
```
The crash appears to be in Z3 itself but I can't reproduce the issue when using the
version of Z3 from the master branch.
For now we simply workaround the issue by not running the
``test/Feature/SolverTimeout.c`` test when using Z3 as the solver.
We should revisit this issue when another stable release of Z3 is made.
|
|
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
|
|
infeasible assumptions.
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
|
Added option to specify a different entry point from main(). Remove some whitespaces.
|
|
|
|
It failed when the function being called is a bitcasted alias.
|
|
compilation.
|
|
|
|
The test contains the program proposed by Eric Rizzi in https://github.com/klee/klee/issues/227, and shows a case in which a constant constraint results after the optimisation.
|
|
also test a negative constant as the lhs.
|
|
between arrays created at the same location but with different sizes
|
|
|
|
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.
|
|
|
|
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.
|
|
Fix va args passing for big types
|
|
unconstrained buf[3]
|
|
Removed XFAIL tag from the Feature/VarArgLongDouble.c test
Fixed Executor to (more) correctly handle the alignment of types larger than 64bit (such as long double) when those are passed in var_args on x86_64.
Specifically:
From http://www.x86-64.org/documentation/abi.pdf
AMD64-ABI 3.5.7p5: Step 7.
Align l->overflow_arg_area upwards to a 16 byte boundary if alignment needed by type exceeds 8 byte boundary.
|
|
varargs on x86_64.
|
|
- KCachegrind appears to expect the first function name to be preceeded by the
name of the file it appears in. Otherwise, it will end up creating two
different records for the function, one of which has no file name and won't
have any statistics.
|
|
- 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!
|
|
- I suspect no one is using this feature, and I'm not sure it is well conceived
either. Ripping it out for now in lieu of bothering to maintain it.
|
|
|
|
- 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.
|
|
path.
- Otherwise this test takes a long time just hammering on the allocator trying
to get to the memory limit.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
|
|
instruction in main().
|
|
optimizations are enabled.
|
|
behaviour for arithmetic right shift are identical.
|
|
to zero. Test case is included.
|
|
behaviour for logical right shift are identical.
|
|
behaviour for left shift are identical.
|
|
Say hello to our new friend, llvm-lit :)
|
|
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
|
|
seemed to causing problems for llvm-lit's parser.
|
|
{ } 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.
|
|
Fixed bug where divide by zero bugs would only be detected once in a program
|
