| Age | Commit message (Collapse) | Author |
|---|
|
and w/o seed extension) based on FP concretization.
|
|
|
|
Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
and tracks information such as branch type, termination
type or source location (asm) in nodes. Enabled with
-write-ptree
ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.
|
|
No need to re-create and re-alloc all the memory again after execution.
|
|
|
|
|
|
... for LLVM 14 in [1] and has already been removed from the LLVM 15
branch in [2].
Some changes are only temporary to silence the warning though, as
Type::getPointerElementType() is planned to be removed as well. [3]
[1] https://reviews.llvm.org/D117885/new/
[2] https://github.com/llvm/llvm-project/commit/d593cf7
[3] https://llvm.org/docs/OpaquePointers.html#migration-instructions
|
|
|
|
|
|
|
|
Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated.
|
|
Before, we reused the llvm::Function* value in the target program,
even though it stems from KLEE's own address space. This leads to
non-deterministic function pointers, even with --allocate-determ.
This issue was identified in the MoKLEE paper. Now, we allocate a
memory object per function, for its (potentially) deterministic
address. Mapping this address back to llvm::Functions is done by
the legalFunctions map.
Also, pointer width now depends on the target, not the host.
|
|
performed with one expressed in terms of number of forks.
|
|
the MaxStatic*Pct checks are performed.
|
|
|
|
restoring old behavior without EH support
|
|
See:
https://reviews.llvm.org/D75660
https://reviews.llvm.org/D75661
|
|
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>
|
|
* move global theRNG into Executor
* pass theRNG via ctor to searchers
* remove some type warnings from RNG.cpp
Fixes #1023.
|
|
|
|
* 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()).
|
|
|
|
|
|
* add getID()/setID()
* use ExecutionStateIDCompare in Executor::states set
* output state id in .err files
|
|
tly in lib/Core
|
|
using "../"
|
|
|
|
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
|
|
- 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.
|
|
|
|
|
|
This should not change the behaviour of KLEE and mimics the old API.
- functions moved from util into time namespace
- uses time points and time spans instead of double
- CLI arguments now have the form "3h5min8us"
Changed command line parameters:
- batch-time (double to string)
- istats-write-interval (double to string)
- max-instruction-time (double to string)
- max-solver-time (double to string)
- max-time (double to string)
- min-query-time-to-log (double to string)
- seed-time (double to string)
- stats-write-interval (double to string)
- uncovered-update-interval (double to string)
- added: log-timed-out-queries (replaces negative max-solver-time)
|
|
and introduce klee_open_compressed_output_file with similar behavior
along some other minor improvements
|
|
Don't pollute the project include directory with optimization specific
headers.
|
|
|
|
clang-format on patch)
|
|
Link intrinsic library before executing optimizations.
This makes sure that any optimization run by KLEE on the module
is executed for the intrinsic library as well.
Support .ll files as input for KLEE as well.
|
|
|
|
|
|
If an external function in KLEE is invoked, it might update errno.
Previously, the errno specific variable in a state was only updated
if it was part of the executed instructions.
That opened up a timeframe that increased the likelihood of errno being
overwritten by another method call.
This patch fixes two issues:
* the errno of the KLEE process state is updated before the external
function call allowing to detect changes to it later on
* after the external call, the memory object of errno is directly
updated
with its new value, reducing the likelihood to be overwritten by
another
call
Additional features:
* Add support for `errno()` for Darwin as well.
* Simplified errno handling in POSIX layer
|
|
|
|
|
|
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
|
|
evalConstantExpr also resides), as suggested by an old comment.
|
|
Request LLVM 3.4 as minimal requirement for KLEE
|
