| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
mainly range-based for, code deduplication
|
|
|
|
|
|
This is the same check used in Executor::setModule. Without this check,
KLEE will segfault in StatisticsManager::incrementIndexedValue,
getIndexedValue, and setIndexedValue when `-output-stats=false` or
`-output-istats=false` because StatisticsManager::indexedStats has not
been allocated.
|
|
|
|
* add getID()/setID()
* use ExecutionStateIDCompare in Executor::states set
* output state id in .err files
|
|
|
|
|
|
"Instruction *i" declared at the beginning of the function. Reformatted this function.
|
|
values
Inline asm used for memory barriers might use their operands and propagate them as
return value.
This is currently not supported. Tighten check for this condition and do not to
lift those inline asm instructions.
Fixes #1252
|
|
Array names used for STP queries used to be restricted to 32 characters,
with the last characters replaced by a unique number.
Similarly, an array is made unique by `klee_make_symbolic`.
Unfortunately, both combined can lead to the generation of the same STP array name for different arrays.
This leads to wrong queries with invalid results.
This is more likely be triggered with longer names for `klee_make_symbolic`
Fixes #1257
|
|
appropriate existing directories and a new directory Statistics; a few missing renames.
|
|
|
|
tly in lib/Core
|
|
using "../"
|
|
|
|
The code assumed that the passed pointer points at the beginning
of the object. Remove this assumption and support any (constant)
pointer. The string is read util either the end of the object
is hit (in which case a warning is issued as the string
was not zero terminated) or until the terminating zero is found.
|
|
The code is simpler and more in the spirit of C++.
|
|
|
|
|
|
|
|
constraints
|
|
ArrayHashTime
* fix binding order for assignments when KLEE_ARRAY_DEBUG enabled
* always write ArrayHashTime column to run.stats, assign -1 when KLEE_ARRAY_DEBUG disabled
* remove unused NumObjects column from run.stats
* remove NumObjects panel from Grafana
|
|
introduced during the optimization step
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
