| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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>
|
|
recently fixed in STP.
|
|
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
|
|
|
|
|
|
|
|
|
