| Age | Commit message (Collapse) | Author |
|---|
|
Allows to provide 0 as an address to allocate deterministic memory
area at any free space.
|
|
Fix generation of STP shift operations with variable shift
|
|
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
|
|
Add support for deterministic allocation
|
|
|
|
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
|
|
Deterministic state addition and removing
|
|
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
|
|
Add options to dump istats and stats statistics every n instructions.
|
|
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.
|
|
Dockerfile: link binaries to /usr/bin
|
|
Signed-off-by: Domenico Fabio Marino <dfm114@ic.ac.uk>
|
|
Fix #416
|
|
have the same bv width
|
|
64, so that the first two arguments of the call bvVarRightShift(extend_npm, expr_shpost, 64) have the same bitwidth of 64.
|
|
Added error message for -run-in directory errors
|
|
Use klee_message for timeout information
|
|
Add metaSMT to Travis CI, fix metaSMTBuilder to pass all tests
|
|
|
|
|
|
|
|
|
|
|
|
|
|
0 when overshifting
|
|
|
|
|
|
|
|
--with-metasmt-default-backend and improve the associated CXX flag
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix Travis CI build - use alternative PPA for LLVM
|
|
|
|
|
|
Fixed the stub for times() not to dereference a NULL pointer when cal…
|
|
|
|
Fixed bug #375 in Kleaver's parser and added --clear-array-decls-after-query option to Kleaver.
|
|
|
