| Age | Commit message (Collapse) | Author |
|---|
|
This reverts commit 0aed7731210d0eb41c0ea767edb8067130cf6252.
|
|
Changes:
- IntrinsicCleaner accepts fshr/fshl as accepted intrinsics
- Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract
- Klee/main suppresses warnings about externals that are LLVM reserved
(i.e., begin with "llvm.")
- New test exercises 32 and 7 bit versions including oversize shift values
Test values are based on LLVM's test for fshl/fshr
- Changes that depend on existence of fshr/fshl are guarded by
#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
or
; REQUIRES: geq-llvm-7.0
|
|
* extend help messages for -max-memory and -max-memory-inhibit
* introduces branchingPermitted()
* enforces fork/branch limits in branch() (vector version)
* changes main loop
* calls updateStates() before checkMemoryUsage()
* calls updateStates() again in case we early terminate states
This should prevent double termination for now. Other solutions are
imho more expensive as we would have to compare possibly large
vectors of states (either states(arr) in checkMemoryUsage() or
removedStates in terminateState()).
|
|
|
|
|
|
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.
|
|
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++.
|
|
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
|
|
|
|
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.
|
|
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.
|
|
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`.
|
|
|
|
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>
|
|
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
|
|
|
|
|
|
|
|
|
|
* creates two new methods: dumpStates, dumpPTree
|
|
|
|
|
|
|
|
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
|
|
|
|
|
|
|
|
consistent naming convention
|
