| Age | Commit message (Collapse) | Author |
|---|
|
This uses the `ref<>`-based memory handling of MemoryObjects.
This makes it explicit that references are held in:
- ExecutionState::symbolics
- ObjectState
|
|
Remove additional reference counting as part of UpdateNodeList and
UpdateNode. Simplifies code.
|
|
Using KLEE's `ref<>` shared ptr requires the referenced object
to contain a reference counter to be added and initialised to 0
as part of the constructor.
To support better reuse of the `ref<>` ptr add a `ReferenceCounter`
struct.
Just adding this struct to a new class/struct as member enables
reference counting with `ref<>` - no additional counter management
needed.
|
|
TR1 implementation got replaced by the std::* equivalents with C++11.
Start to use the standard versions instead of the old ones.
|
|
|
|
Statistics encoded in `run.istats` were limited to a maximum number of 13 due to encoding in a `uint64_t` variable.
This approach has multiple limitations:
- a maximum number of 13 statistics were allowed
- a subtle bug can be triggered if many more statistics are added - independent of the selected statistics for `run.istats`
Depending on the linking order, statistics will get a different ID. Previously, the ID was used to shift a `1` to its position marking the statistic as being used.
This will lead to undefined behaviour if more than 63 statistics are used.
Using an llvm::SmallBitVector instead fixes both problems.
|
|
Tracking function locations separately correctly without prefixing
it with a directory.
|
|
Assuming a `klee-out-*` directory is moved to a different path location, subsequent analysis of the run.istats with KCachegrind focusing on assembly is impossible as the `assembly.ll` cannot be found.
The reason is that the absolute path of the object file (assembly.ll) is hard-coded as part of the generated run.istats.
To fix this, assume that the file is local to the `run.istats`.
|
|
|
|
Value transformation operates on word instead of byte arrays.
That means the Read indicies need to be adjusted to reflect that.
Previously IndexCleanerVisitor tried to remove the multiplications in the index
to covert byte indicies to word indicies. However as the two added test cases show
this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide
the index with word size which should always be correct.
|
|
buildMixedSelectExpr was using the byte index for holes in the
select condition instead of the word based one. This only occured
if there was more than 1 hole.
|
|
The caching maps in ArrayExpr are broken, they only consider hashes
and don't check for structural equality. This can lead to hash collisions
and invalid Expr replacement. This is especially potetent for UpdateLists, who
only put the array name in the hash, so there can be a lot of colisions.
|
|
ArrayExprOptimizer read the UpdateList in the wrong order, which
meant that it used least recent update instead of the most recent one.
This patch fixes this as well as adds a test to illustrate the issue.
|
|
Having both weight and depth in execution state is wasteful,
therefore this patch removes weight.
The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute
the weight
A new nurs:depth searcher is introduced that biases the search with depth,
making it the only other searcher that prefers to go deep (similar to dfs).
|
|
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
|
|
|
|
llvm.objectsize is used in several optimisation during compile time. Lowering
these intrinsics took a conservative approach returning always the value for
unknown. Instead, lower to the object's real size, if possible. Otherwise,
a conservative value is used.
Since LLVM 4.0, the function `llvm::lowerObjectSizeCall()` does exactly
this. Use this function or preserve the old behaviour for older LLVM versions.
|
|
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor
and move to support lib), so remove it.
|
|
Fixes #264.
We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory.
After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic).
|
|
|
|
|
|
|
|
|
|
- moves timer handling from Executor into support lib
- introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes
- removes ExecutorTimers.cpp and ExecutorTimerInfo.h
- removes -max-instruction-time flag (see #1114)
|
|
- adds -timer-interval threshold for timer checks
- fixes #831
|
|
|
|
|
|
|
|
|
|
|
|
|
|
header SolverCmdLine.h) and moved it to the Solver library.
|
|
* creates two new methods: dumpStates, dumpPTree
|
|
|
|
|
|
|
|
|
|
|
|
|
|
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
|
|
Eliminates -Wdeprecated-copy warnings
Performed clang-format on touched file
|
|
Eliminates -Wdeprecated-copy warnings
Performed partia clang-format on touched file
|
|
|
|
|
|
|
|
consistent naming convention
|
|
|
|
|
|
|
|
|
