about summary refs log tree commit diff homepage
path: root/lib/Core/Searcher.cpp
AgeCommit message (Collapse)Author
2024-01-12new: persistent ptree (-write-ptree) and klee-ptreeFrank Busse
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.
2023-06-05make BatchingSearcher more readableJulian Büning
2023-06-05fix BatchingSearcher's disabled time budgetJulian Büning
The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own.
2023-04-06Support disabling compiler warnings; Use with external headersMartin Nowack
2020-10-12searchers: more consistent formattingFrank Busse
2020-10-12DFS/BFS/RandomSearcher: replace loop with std::findFrank Busse
2020-10-12searchers: move implementations from .h to .cppFrank Busse
2020-10-12Searcher: remove addState/removeState functionsFrank Busse
2020-10-12searchers: clean up, add documentationFrank Busse
2020-09-26Replace llvm::CallSite with llvm::CallBase on LLVM 8+Lukas Zaoral
This is in preparation for LLVM 11 as the llvm:CallSite class has been removed.
2020-08-19DiscretePDF: use IDs instead of pointers (see PR #739)Frank Busse
2020-07-30introduce --rng-initial-seed=<unsigned>Frank Busse
* move global theRNG into Executor * pass theRNG via ctor to searchers * remove some type warnings from RNG.cpp Fixes #1023.
2020-07-01Use constraint sets and separate metadata for timing solver invocationMartin Nowack
Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints)
2020-06-29Enable subsets for RandomPathSearcherTimotej Kapus
2020-06-29[PTree] Replace left/right with PointerIntPairTimotej Kapus
2020-06-29Revert "refactor PTree: use unique_ptr"Timotej Kapus
This reverts commit 0aed7731210d0eb41c0ea767edb8067130cf6252.
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Created include/klee/Core directory and moved appropriate files direc\Cristian Cadar
tly in lib/Core
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2019-12-12[Searchers] Remove weight from es, add nurs_depthTimotej Kapus
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).
2019-11-28Move merging related code from Executor into MergingSearcherLukas Wölfer
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
2019-09-20refactor PTree: use unique_ptrFrank Busse
2019-09-20refactor PTree: remove split(), add attach() methodFrank Busse
2019-03-21drop support for LLVM <= 3.7Julian Büning
2019-03-16Added support for disabling --batch-instructions and --batch-time by setting ↵Cristian Cadar
them to 0
2019-03-12time: add double type for span multiplicationsFrank Busse
2018-10-30Base time API upon std::chronoFrank Busse
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)
2018-07-04Fix compiler warnings if assertions are disabledMartin Nowack
2018-05-15Implemented incomplete mergingLukas Wölfer
2017-11-30Implemented bounded merging functionalityLukas Wölfer
2017-10-15Fixed assert in BFSSearcher that does not hold as part of interleaved searcherJulian Büning
2017-10-03Silenced some warnings about unused variables when assertions are disabled.Cristian Cadar
2017-08-04Removed merging searchersLukas Wölfer
2017-07-23Remove support for LLVM < 3.4Martin Nowack
Request LLVM 3.4 as minimal requirement for KLEE
2017-05-24Remove redundant KLEE prefix while loggingJörg Thalheim
2016-11-19Merge branch 'fix_bfs2' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-fix_bfs2
2016-11-09Fix BFS searcherMartin Nowack
For performance reasons, if KLEE branches, one state is reused and it is progressed by adding new constraints. Make sure both new states end up at the end of the BFS searcher queue.
2016-11-08add nicer error messages for --use-merge and add explanation why it ↵Hoang M. Le
currently cannot be used with random-path
2016-09-26Modified logging information to steer the usage of klee_message, ↵Andrea Mattavelli
klee_warning, and klee_error
2016-07-08Use vector instead of set to add/remove statesMartin Nowack
Deterministic adding/removing of states.
2016-07-08IterativeDeepeningTimeSearcher: Fix using wrong iteratorMartin Nowack
2015-12-17Refactoring: Moving klee_warning/_error functions to ErrorHandling in ↵Martin Nowack
Support directory
2014-09-14[LLVM3.5] Update for move of CFG.h into IR.Daniel Dunbar
- Mostly fixed by removing unnecessary references.
2014-09-14[LLVM3.5] Update for CallSite.h move into IR/.Daniel Dunbar
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-04-24Removed ununsed Executor field in WeightedRandomSearcher to silenceDan Liew
clang warning.
2013-08-27Port to LLVM 3.3Martin Nowack
Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful
2013-07-23BFS searcher.Lei Zhang
2010-07-15Reduce variable shadowing.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108405 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-01Update for LLVM ostream changes.Daniel Dunbar
- Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-11 07:02:51 +0000