| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
reference assigned.
|
|
|
|
TR1 implementation got replaced by the std::* equivalents with C++11.
Start to use the standard versions instead of the old ones.
|
|
|
|
|
|
* Port changes from .Dockerfile to this
* install emacs-nox and vim-nox instead of pulling all X dependencies
* Clean apt cache
|
|
|
|
|
|
|
|
Building older LLVM/libcxx versions under Ubuntu 18.04 requirer patches
|
|
LLVM changed from svn to github. Use the github mirror to have faster build times.
Patches were updated to follow the new structure.
Patches also support building underr Ubuntu 18.04
|
|
Build dependencies for different components were tied to a specific Ubuntu version (16.04).
Although, they are the same for newer versions as well.
By renaming `p-component-linux-ubuntu-16.04.inc` to `p-component-linux-ubuntu.inc`, the script can be used for newer Ubuntu versions as well.
Do some minor cleaning up.
|
|
|
|
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.
|
|
|
|
|
|
|
|
Added units for some of the data and
modified klee-stats source code to provide solver time
as a fraction of walltime along with fork, resolve
and cexcache time.
|
|
|
|
This Dockerfile provides a Grafana server with a preconfigured dashboard
and a datasource that will connect to klee-stats, as soon as klee-stats
is run.
|
|
|
|
Currently, arbitrary *.bc files or archives containing .bc files (.bca or .a) can
be linked using `--link-llvm-lib`. Change documentation of command line argument to make this clear.
This feature is useful to keep avoid linking the bitcode libraries with the application as bitcode file in the first place.
Fix error message in case library could not be loaded
|
|
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>
|
|
Python 2 should not be needed anymore, so we remove it from osx CI.
|
|
|
|
to function names.
|
|
|
|
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.
|
|
|
|
|
|
dependency.
|
|
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor
and move to support lib), so remove it.
|
|
Hoist increment of `sc` into the loop header.
Memory locations can only be written to if they are writeable.
Avoid concretising a value by writing it. If the location is not symbolic in the first place.
This avoids writing read-only memory locations.
|
|
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).
|
|
Fix multiple missing includes
|
