| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Replaced an incorrect comma with a semicolon in the Executor constructor.
|
|
|
|
implement it in the solver.
|
|
|
|
MartinNowack-fix_bfs2
|
|
add nicer error messages for --use-merge and add explanation why it currently cannot be used with random-path
|
|
|
|
transitive dependencies on KLEE's libraries rather than on the final
binaries. This is better because it means we can build
other tools that use KLEE's libraries and not need to express the
needed LLVM dependencies.
It also makes it clearer what the dependencies are between KLEE
libraries. This has illustrated a problem with the `kleeBasic`
library. It contains `ConstructSolverChain.cpp` which clearly
belongs in `kleaverSolver` not in `kleeBasic`. This will be fixed
later.
|
|
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.
|
|
currently cannot be used with random-path
|
|
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.
|
|
klee_warning, and klee_error
|
|
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 to PTree pointer use-after-delete
|
|
|
|
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>
|
|
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>
|
|
Allows to provide 0 as an address to allocate deterministic memory
area at any free space.
|
|
|
|
Deterministic allocation provides an internal allocator which
mmaps memory to a fixed static address.
This way, same allocation is assured across different KLEE runs
for the same application assuming a deterministic searcher.
In addition, this patch provides following options:
-allocate-determ: switch on/off deterministic allocation
-allocate-determ-size: adjust preallocated memory
-null-on-zero-malloc: returns null pointer in case a malloc
of size 0 was requested. According to standard, also a non-null pointer
can be returned (which happens with the default glibc malloc implementation)
-allocation-space: space between allocations can be adjusted. KLEE is not able
to detect out-of-bound accesses which are inside another but wrong object.
Due the implementation of typical allocators adjacent mallocs have space
in between for management purposes. This spaces helped KLEE to detect off-by-1/2 accesses.
For higher numbers, the allocation space has to be increased.
-allocate-determ-start-address: adjust deterministic start address. The addres
has to be page aligned. KLEE fails if it cannot acquire this address
|
|
For vararg handling, arguments of size bigger than 64 bit need
to be handled 128bit aligned according to AMD calling conventions
AMD64-ABI 3.5.7p5.
To handle that case correctly, we do:
1) make sure that every argument is aligned correctly in
an allocation for function arguments
2) the allocation itself is aligned correctly
|
|
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.
|
|
|
|
|
|
Support gzip-based compression of raw_outstreams
|
|
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.
|
|
Add -stats-write-after-instructions and -istats-write-after-instructions
to update each statistic after n steps.
Furthermore, the metric "minimal distance to uncovered state" is now
updated independently if statistics are enabled or not.
This metric is needed i.e. by weighted random searchers directed towards
uncovered instructions.
Remove some dead code.
|
|
|
|
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.
|
|
AllocaInst.
|
|
* ``-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.
|
|
of some.
|
|
|
|
|
|
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...
|
|
so that it is possible to ``#include "klee/util/ArrayExprHash.h"``
|
|
Some of these leaks were introduced by the factory constructor for Array
objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have
been around for far longer.
This leak was fixed by introducing a ``ArrayCache`` object which has two
purposes
* Retains ownership of all created ``Array`` objects and destroys them when
the ``ArrayCache`` destructor is called.
* Mimic the caching behaviour for symbolic arrays that was introduced
by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same
name and size get "uniqued".
The Executor now maintains a ``arrayCache`` member that it uses and
passes by pointer to objects that need to construct ``Array`` objects (i.e.
``ObjectState``). This way when the Executor is destroyed all the
``Array`` objects get freed which seems like the right time to do this.
For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is
used for building ``Array`` objects. This means that the Parser must
live as long as the built expressions will be used otherwise we will
have a use after free. I'm not sure this is the right design choice.
It might be better to transfer ownership of the ``Array`` objects to
the root ``Decl`` returned by the parser.
|
|
helper functions.
|
|
for it
|
|
Support directory
|
|
flag as suggested by @ccadar
|
|
infeasible assumptions.
|
|
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
|
|
Previously, default Klee would go through every byte in a test case
and attempt to bound it to be between 0 and 127, making it human
readable. While this may be useful when attempting to understand Klee,
it also means that the time required to create large test suites was
greatly increased. By making this behavior default off, unsuspecting
users won't incur these additional costs.
|
|
when they are given the --version command line option.
Unfortunately to make the build type and git revision available we
need to check this for every build which means KLEE's support library
will be rebuilt for every build which will slow down incremental builds.
This addresses issue #231
|
|
|
