| Age | Commit message (Collapse) | Author |
|---|
|
For performance reasons, if KLEE branches, one state is reused
and it is progressed by adding new constraints.
Make sure both new states end up at the end of the BFS searcher queue.
|
|
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.
|
|
Extended support for assembler raising
|
|
function) (#455)
|
|
POSIX runtime. If the check fails, exit with an error. (#457)
|
|
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.
|
|
Fix for klee_get_obj_size() crashing on 64-bit, resolves #446
|
|
|
|
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>
|
|
Added test case exposing division by zero failure reported by @kren1 and made division total in STP to fix it.
|
|
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>
|
|
Generated STP equality expressions have to be the same type.
If a shift with different types as operands was used,
therefore equality expressions of different width were generated.
Beside avoiding the different sizes, this patch restores the
original behavior to extract just the part involved in shifting
and therefore should generate smaller expressions.
Enable sdiv test case
|
|
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.
|
|
recently fixed in STP.
|
|
|
|
Fixed bug #375 in Kleaver's parser and added --clear-array-decls-after-query option to Kleaver.
|
|
|
|
|
|
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.
|
|
Bug fix in IndependentSolver
|
|
it after the division bug is fixed.
|
|
https://github.com/klee/klee/issues/334, which triggers a bug in solver-optimize-divides, and which is for now expected to fail.
|
|
* ``-replay-out`` to ``-replay-ktest-file``
* ``-replay-out-dir`` to ``-replay-ktest-dir``
and also rename
* help descriptions
* global variables corresponding to these options.
* Names used in ``KleeHandler``, ``Interpreter``, ``Executor``
and in KLEE's ``main()`` function.
The old name for the options/code was very unhelpful as it wasn't
obvious that "out" files are ``.ktest`` files unless you examine KLEE's
source code.
|
|
The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the
IndependentSolver assumed that it would be given an assignment for every
array. If this wasn't the case the ``Assignment`` object by default
would just replace every read of an unknown array with a byte filled
with zeros.
This problem would appear if
``IndependentSolver::getInitialValues(...)`` was called without asking
for assignment for used arrays.
I saw two ways of fixing this
* Get an assignment for all arrays even if the client didn't ask
for them. This guarantees that is the query is satisfiable then
we can compute a concrete assignment.
* Just do a "best effort" check and only check expressions that can
be fully assigned to.
I chose the latter because the first option seems pretty wasteful,
especially for an assert.
The second option isn't ideal though as it would be possible to
compute an assignment that for the whole query leads to "unsat"
but we wouldn't notice.
|
|
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.
|
|
a ``createCoreSolver()`` function. The solver used is set by the new
``--solver-backend`` command line argument. The default is STP.
This change necessitated refactoring the MetaSMT stuff. That clearly
didn't belong in the Executor! The MetaSMT command line option is
now ``--metasmt-backend`` as this only picks the MetaSMT backend.
In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed.
Note I don't have MetaSMT built on my development machine so I don't
know if the MetaSMT stuff even compiles...
|
|
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.
|
|
for it
|
|
MemorySanitzer and ThreadSanitizer environment variables when running
lit tests.
This makes it easy suppress errors in sanitized versions of KLEE
|
|
``--silent-klee-assume=0`` is no longer passed. This ensures that we
also check that ``--silent-klee-assume`` is off by default.
|
|
infeasible assumptions.
|
|
[STPBuilder] Generate SRrem expressions correctly
|
|
This causes problems on a shared machine where multiple users are running the
KLEE unit tests.
|
|
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.
|
|
Fix signed division by constant 1/ -1
|
|
|
|
Division by constant divisor get optimized
using shift and multiplication operations in STP builder.
The used method cannot be applied for divisor 1 and -1.
In that case use slow path.
|
|
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.
|
|
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant
to partially address issue #218.
There are a few problems with this commit
* It is possible for AShrExpr to not be abbreviated because the scan
methods will not see that we print the 0th child of the AShrExpr twice
* The added test case should really be run through an SMT solver (
i.e. STP) but that requires infrastructure changes.
|
|
Use correct definition and declaration of main function
|
|
Add some missing header to silence
compiler warnings
|
|
also test a negative constant as the lhs.
|
