| Age | Commit message (Collapse) | Author |
|---|
|
map added to ExecutionState); now storing addresses of MemoryObjects for easier cleanup
|
|
This feature implements tracking of and resolution of memory objects in the presence of
symbolic addresses.
For example, an expression like the following:
int x;
klee_make_symbolic(&x, sizeof(x), "x");
int* tmp = &b.y[x].z;
For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching
memory object - including the ones outside of the object "b".
This behaviour is consistent with symbex approach of exploring all execution paths.
However, from the point of view of security testing, we would only be interested to know if we are still
in-bounds or there is a buffer overflow.
The implemented feature creates and tracks (via the GEP instruction) the mapping between the current
symbolic offset and the base object it refers to: in our example we are able to tell that the reference
should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize
the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug.
The feature is turned on via the single-object-resolution command line flag.
A new test case was implemented to illustrate how the feature works.
|
|
|
|
Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
and tracks information such as branch type, termination
type or source location (asm) in nodes. Enabled with
-write-ptree
ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.
|
|
--external-call-warnings=none|once-per-function|all.
This eliminates the ambiguity when both of the old options were set.
Added test for the new option.
|
|
consistency
|
|
|
|
|
|
No need to re-create and re-alloc all the memory again after execution.
|
|
|
|
|
|
According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes.
Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes
were used.
This commit fixes the following out of bound pointer access.
```
$ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc
$ klee varalign.bc
KLEE: output directory is "/home/lukas/klee/klee-out-19"
KLEE: Using Z3 solver backend
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17
i1, i2, i3: 1, 2, 3
l1: 4
i4: 5
ld1: 6.000000
KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 499
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
```
|
|
|
|
|
|
|
|
|
|
... for LLVM 14 in [1] and has already been removed from the LLVM 15
branch in [2].
Some changes are only temporary to silence the warning though, as
Type::getPointerElementType() is planned to be removed as well. [3]
[1] https://reviews.llvm.org/D117885/new/
[2] https://github.com/llvm/llvm-project/commit/d593cf7
[3] https://llvm.org/docs/OpaquePointers.html#migration-instructions
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
... in Executor::callExternalFunction.
Fixes the following error reported in Feature/VarArg{Alignment,LongDouble}.c
tests:
lib/Expr/Expr.cpp:366:5: runtime error: store to misaligned address
0x7ffc011d3528 for type 'long double', which requires 16 byte alignment
|
|
|
|
Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.
|
|
|
|
Since KLEE requires C++14, we should prefer `nullptr` to plain `0`.
|
|
The vector variants are not implemented at the moment.
See: https://reviews.llvm.org/D84125
Co-authored-by: Lukas Zaoral <lzaoral@redhat.com>
Co-authored-by: Martin Nowack <m.nowack@imperial.ac.uk>
|
|
The vector variants are not implemented at the moment.
See: https://reviews.llvm.org/D84125
Co-authored-by: Lukas Zaoral <lzaoral@redhat.com>
Co-authored-by: Martin Nowack <m.nowack@imperial.ac.uk>
|
|
... and has already been removed from the LLVM 13 source tree.
See:
https://reviews.llvm.org/D78127
https://reviews.llvm.org/D95570
|
|
Before, we reused the llvm::Function* value in the target program,
even though it stems from KLEE's own address space. This leads to
non-deterministic function pointers, even with --allocate-determ.
This issue was identified in the MoKLEE paper. Now, we allocate a
memory object per function, for its (potentially) deterministic
address. Mapping this address back to llvm::Functions is done by
the legalFunctions map.
Also, pointer width now depends on the target, not the host.
|
|
stats when not dumping states
|
|
performed with one expressed in terms of number of forks.
|
|
|
|
reached
|
|
the MaxStatic*Pct checks are performed.
|
|
|
|
__cxa_throw and __cxa_rethrow were not handled by special function handlers in
the final version of #966 (which introduced support for C++ exception handling)
|
|
restoring old behavior without EH support
|
|
and should be replaced with CallBase::getParamAlign
|
|
See: https://reviews.llvm.org/D80368
|
|
See:
https://reviews.llvm.org/D75660
https://reviews.llvm.org/D75661
|
|
CallBase::getCalledValue has been deprecated by getCalledOperand since LLVM 8
and has been removed in LLVM 11
See: https://reviews.llvm.org/D78882
|
|
The same applies to SmallString.
See: llvm/llvm-project@777180a#diff-497ba4c0c527a125d382b51a34f32542
|
