| 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.
|
|
|
|
|
|
|
|
... by initialising all members of fundamental types of the ExecutionState
class.
Fixes the following error in SearcherTest.{Two,}RandomPath unit tests:
lib/Core/ExecutionState.cpp:114:22: runtime error: load of value 254, which is not a valid value for type 'bool'
|
|
|
|
|
|
We implement the Itanium ABI unwinding base-API, and leave the
C++-specific parts to libcxxabi.
Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
|
|
This constructor has been a hack and was wrongly used, use ConstraintManager instead.
Allow copy-constructing states only via `ExecutionState::branch()` call.
|
|
Decouple ExecutionState from TimingSolver
Instead of providing an execution state to the timing solver use a set of
constraints and an additional object for metadata.
Fixes:
* correct accounting of metadata to a specific state
* accounting of all solver invocations (e.g. solver-getRange was not
accounted)
* allows to invoke the solver without a state (avoids costly copying of
states/constraints)
|
|
|
|
|
|
* add getID()/setID()
* use ExecutionStateIDCompare in Executor::states set
* output state id in .err files
|
|
|
|
tly in lib/Core
|
