| Age | Commit message (Collapse) | Author |
|---|
|
Propagate ExternalCallPolicy to allow user-based selection.
|
|
Provide an additional argument to select the concretisation policy.
Fix a bug where the concretisation of a shared memory object was visible
across different states by retrieving a writable object state first.
|
|
Use existing `Executor::toConstant()` function to transform a symbolic
byte of an `ObjectState` to its concrete representation.
This will also add constraints if required.
|
|
Before, only partially symbolic variables have been concretized.
Now, every object that is not fully concrete is concretized correctly
this includes fully symbolic objects.
|
|
Before, external changes to symbolic variables have not been propagated
back to their internal representation.
Do a byte-by-byte comparison and update object state if required.
|
|
|
|
|
|
whether the expression is concretised. Also changed a C string argument to std::string.
|
|
with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf.
|
|
--compress-execution-tree to --compress-exec-tree. Fix an incorrect reference to --write-exec-tree.
|
|
|
|
|
|
Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com>
(cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308)
|
|
Handle like `memalign` for now.
|
|
|
|
|
|
|
|
callers
|
|
|
|
This reworked logic also fixes a buffer overflow which could be triggered during seed extension.
|
|
|
|
|
|
Added a test case.
|
|
and w/o seed extension) based on FP concretization.
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The functionality of the batching searcher that increases the time
budget if it is shorter than the time between two calls to
`selectState()` ignored the disabled time budget. Effectively, the
batching searcher thus picks a very arbitrary time budget on its own.
|
|
available since CMake version 3.14
|
|
|
|
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
```
|
|
|
