| Age | Commit message (Collapse) | Author |
|---|
|
klee_warning, and klee_error
|
|
Extended support for assembler raising
|
|
function) (#455)
|
|
Allow cross checking of solvers
|
|
`-debug-crosscheck-core-solver` as requested by Cristian
|
|
functions.
|
|
with another solver. For example the core solver can be STP and the
cross checking solver can be Z3.
Unfortunately a few fragile tests don't pass when actually using this
option.
|
|
|
|
POSIX runtime. If the check fails, exit with an error. (#457)
|
|
Try to unbreak the TravisCI and Docker builds.
|
|
GTest has moved from googlecode to GitHub so update URL and directory
name used in source archive as appropriate.
|
|
Document -save-all-writes to klee_init_env help message
|
|
|
|
[Klee Web] Link libkleeRuntest library to fix coverage report
|
|
|
|
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
|
|
|
|
Fix to #449 by using sys::StrError(errno) to print error messages.
|
|
|
|
Fix to #445
|
|
|
|
add --exit-on-error-type option
|
|
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>
|
|
fprintf: convert to klee_warning
|
|
In some Solver sources, some error outputs were missing \n. Instead of
adding a new line to all of them, convert the fprintf's to
klee_warning which adds \n automatically.
ErrorHandling.h had to be included in MetaSMTSolver.cpp to have
klee_warning declared there.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
MemoryUsage: handle ill-designed mallinfo
|
|
The mallinfo() interface is ill-designed. It returns 'int' as occupied
memory. This means at most 2G. This causes troubles when capping the
memory to 3G by -max-memory=3000 for example.
We cannot fix the interface, but we can at least extend the space to
4G. So cast those 'int's to 'unsigned int's to avoid sign extension.
Then do the addition on 'size_t' to count on 64bit values (on 64 bit).
Apart from that, the original 'int' + 'int' led to overflow which is
undefined on 'signed int's in C.
Also, when klee is run under valgrind, generic.current_allocated_bytes
from gperftools does not touch the passed pointer and in that case, we
return garbage from GetTotalMallocUsage. So initialize 'value' to 0 to
avoid the problem.
And since GetNumericProperty accepts 'size_t', let's define 'value' as
such. It was 'uint64_t' previously and they differ on 32 bit.
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.
|
|
|
|
Executor: do not crash on non-sized globals
|
|
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>
|
|
Fix parsing of the address for the deterministic memory area.
|
|
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.
|
