diff options
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Searcher.cpp | 211 | ||||
| -rw-r--r-- | lib/Core/Searcher.h | 250 |
2 files changed, 215 insertions, 246 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 37c40897..e2f11a87 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -23,7 +23,6 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/Support/ErrorHandling.h" -#include "klee/Support/ModuleUtil.h" #include "klee/System/Time.h" #include "llvm/IR/Constants.h" @@ -32,17 +31,12 @@ #include "llvm/Support/CommandLine.h" #include <cassert> -#include <climits> #include <cmath> -#include <fstream> using namespace klee; using namespace llvm; -Searcher::~Searcher() { -} - /// ExecutionState &DFSSearcher::selectState() { @@ -52,28 +46,25 @@ ExecutionState &DFSSearcher::selectState() { void DFSSearcher::update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) { - states.insert(states.end(), - addedStates.begin(), - addedStates.end()); - for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); - it != ie; ++it) { - ExecutionState *es = *it; - if (es == states.back()) { + // insert states + states.insert(states.end(), addedStates.begin(), addedStates.end()); + + // remove states + for (const auto state : removedStates) { + if (state == states.back()) { states.pop_back(); } else { + __attribute__((unused)) bool ok = false; - for (std::vector<ExecutionState*>::iterator it = states.begin(), - ie = states.end(); it != ie; ++it) { - if (es==*it) { + for (auto it = states.begin(), ie = states.end(); it != ie; ++it) { + if (state == *it) { states.erase(it); ok = true; break; } } - (void) ok; assert(ok && "invalid state removed"); } } @@ -88,6 +79,7 @@ ExecutionState &BFSSearcher::selectState() { void BFSSearcher::update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) { + // update current state // Assumption: If new states were added KLEE forked, therefore states evolved. // constraints were added to the current state, it evolved. if (!addedStates.empty() && current && @@ -99,28 +91,25 @@ void BFSSearcher::update(ExecutionState *current, states.push_back(current); } - states.insert(states.end(), - addedStates.begin(), - addedStates.end()); - for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); - it != ie; ++it) { - ExecutionState *es = *it; - if (es == states.front()) { + // insert states + states.insert(states.end(), addedStates.begin(), addedStates.end()); + + // remove states + for (const auto state : removedStates) { + if (state == states.front()) { states.pop_front(); } else { + __attribute__((unused)) bool ok = false; - for (std::deque<ExecutionState*>::iterator it = states.begin(), - ie = states.end(); it != ie; ++it) { - if (es==*it) { + for (auto it = states.begin(), ie = states.end(); it != ie; ++it) { + if (state == *it) { states.erase(it); ok = true; break; } } - (void) ok; assert(ok && "invalid state removed"); } } @@ -129,32 +118,28 @@ void BFSSearcher::update(ExecutionState *current, /// ExecutionState &RandomSearcher::selectState() { - return *states[theRNG.getInt32()%states.size()]; + return *states[theRNG.getInt32() % states.size()]; } -void -RandomSearcher::update(ExecutionState *current, - const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates) { - states.insert(states.end(), - addedStates.begin(), - addedStates.end()); - for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); - it != ie; ++it) { - ExecutionState *es = *it; +void RandomSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + // insert states + states.insert(states.end(), addedStates.begin(), addedStates.end()); + + // remove states + for (const auto state : removedStates) { __attribute__((unused)) bool ok = false; - for (std::vector<ExecutionState*>::iterator it = states.begin(), - ie = states.end(); it != ie; ++it) { - if (es==*it) { + for (auto it = states.begin(), ie = states.end(); it != ie; ++it) { + if (state == *it) { states.erase(it); ok = true; break; } } - + assert(ok && "invalid state removed"); } } @@ -162,9 +147,10 @@ RandomSearcher::update(ExecutionState *current, /// WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng) - : states(new DiscretePDF<ExecutionState*, ExecutionStateIDCompare>()), + : states(std::make_unique<DiscretePDF<ExecutionState*, ExecutionStateIDCompare>>()), theRNG{rng}, type(type) { + switch(type) { case Depth: case RP: @@ -182,10 +168,6 @@ WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng) } } -WeightedRandomSearcher::~WeightedRandomSearcher() { - delete states; -} - ExecutionState &WeightedRandomSearcher::selectState() { return *states->choose(theRNG.getDoubleL()); } @@ -234,36 +216,28 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { void WeightedRandomSearcher::update( ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) { + + // update current if (current && updateWeights && std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) states->update(current, getWeight(current)); - for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(), - ie = addedStates.end(); - it != ie; ++it) { - ExecutionState *es = *it; - states->insert(es, getWeight(es)); - } + // insert states + for (const auto state : addedStates) + states->insert(state, getWeight(state)); - for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); - it != ie; ++it) { - states->remove(*it); - } + // remove states + for (const auto state : removedStates) + states->remove(state); } -bool WeightedRandomSearcher::empty() { - return states->empty(); +bool WeightedRandomSearcher::empty() { + return states->empty(); } /// -RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng) - : processTree{processTree}, theRNG{rng}, idBitMask{processTree.getNextId()} { -} -RandomPathSearcher::~RandomPathSearcher() { -} // Check if n is a valid pointer and a node belonging to us #define IS_OUR_NODE_VALID(n) \ (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0)) @@ -289,17 +263,17 @@ ExecutionState &RandomPathSearcher::selectState() { bits = 32; } --bits; - n = ((flips & (1 << bits)) ? n->left : n->right).getPointer(); + n = ((flips & (1U << bits)) ? n->left : n->right).getPointer(); } } return *n->state; } -void -RandomPathSearcher::update(ExecutionState *current, - const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates) { +void RandomPathSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + // insert states for (auto es : addedStates) { PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; PTreeNodePtr *childPtr; @@ -320,6 +294,7 @@ RandomPathSearcher::update(ExecutionState *current, } } + // remove states for (auto es : removedStates) { PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; @@ -344,13 +319,6 @@ bool RandomPathSearcher::empty() { /// -MergingSearcher::MergingSearcher(Searcher *_baseSearcher) - : baseSearcher(_baseSearcher){} - -MergingSearcher::~MergingSearcher() { - delete baseSearcher; -} - ExecutionState& MergingSearcher::selectState() { assert(!baseSearcher->empty() && "base searcher is empty"); @@ -382,20 +350,6 @@ ExecutionState& MergingSearcher::selectState() { /// -BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher, - time::Span _timeBudget, - unsigned _instructionBudget) - : baseSearcher(_baseSearcher), - timeBudget(_timeBudget), - instructionBudget(_instructionBudget), - lastState(0) { - -} - -BatchingSearcher::~BatchingSearcher() { - delete baseSearcher; -} - ExecutionState &BatchingSearcher::selectState() { if (!lastState || (((timeBudget.toSeconds() > 0) && @@ -420,26 +374,18 @@ ExecutionState &BatchingSearcher::selectState() { } } -void -BatchingSearcher::update(ExecutionState *current, - const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates) { +void BatchingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + // drop memoized state if it is marked for deletion if (std::find(removedStates.begin(), removedStates.end(), lastState) != removedStates.end()) - lastState = 0; + lastState = nullptr; + // update underlying searcher baseSearcher->update(current, addedStates, removedStates); } -/***/ - -IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *_baseSearcher) - : baseSearcher(_baseSearcher), - time(time::seconds(1)) { -} - -IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() { - delete baseSearcher; -} +/// ExecutionState &IterativeDeepeningTimeSearcher::selectState() { ExecutionState &res = baseSearcher->selectState(); @@ -453,17 +399,14 @@ void IterativeDeepeningTimeSearcher::update( const auto elapsed = time::getWallTime() - startTime; + // update underlying searcher (filter paused states unknown to underlying searcher) if (!removedStates.empty()) { std::vector<ExecutionState *> alt = removedStates; - for (std::vector<ExecutionState *>::const_iterator - it = removedStates.begin(), - ie = removedStates.end(); - it != ie; ++it) { - ExecutionState *es = *it; - std::set<ExecutionState*>::const_iterator it2 = pausedStates.find(es); - if (it2 != pausedStates.end()) { - pausedStates.erase(it2); - alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); + for (const auto state : removedStates) { + auto it = pausedStates.find(state); + if (it != pausedStates.end()) { + pausedStates.erase(it); + alt.erase(std::remove(alt.begin(), alt.end(), state), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -471,6 +414,7 @@ void IterativeDeepeningTimeSearcher::update( baseSearcher->update(current, addedStates, removedStates); } + // update current: pause if time exceeded if (current && std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end() && @@ -479,38 +423,35 @@ void IterativeDeepeningTimeSearcher::update( baseSearcher->removeState(current); } + // no states left in underlying searcher: fill with paused states if (baseSearcher->empty()) { time *= 2U; klee_message("increased time budget to %f\n", time.toSeconds()); std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); - baseSearcher->update(0, ps, std::vector<ExecutionState *>()); + baseSearcher->update(nullptr, ps, std::vector<ExecutionState *>()); pausedStates.clear(); } } -/***/ - -InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers) - : searchers(_searchers), - index(1) { -} +/// -InterleavedSearcher::~InterleavedSearcher() { - for (std::vector<Searcher*>::const_iterator it = searchers.begin(), - ie = searchers.end(); it != ie; ++it) - delete *it; +InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers) { + searchers.reserve(_searchers.size()); + for (auto searcher : _searchers) + searchers.emplace_back(searcher); } ExecutionState &InterleavedSearcher::selectState() { - Searcher *s = searchers[--index]; - if (index==0) index = searchers.size(); + Searcher *s = searchers[--index].get(); + if (index == 0) index = searchers.size(); return s->selectState(); } void InterleavedSearcher::update( ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) { - for (std::vector<Searcher*>::const_iterator it = searchers.begin(), - ie = searchers.end(); it != ie; ++it) - (*it)->update(current, addedStates, removedStates); + + // update underlying searchers + for (auto &searcher : searchers) + searcher->update(current, addedStates, removedStates); } diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 437cf01f..9243b69a 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -35,45 +35,44 @@ namespace klee { class ExecutionState; class Executor; + /// A Searcher implements an exploration strategy for the Executor by selecting + /// states for further exploration using different strategies or heuristics. class Searcher { public: - virtual ~Searcher(); + virtual ~Searcher() = default; + /// Selects a state for further exploration. + /// \return The selected state. virtual ExecutionState &selectState() = 0; + /// Notifies searcher about new or deleted states. + /// \param current The currently selected state for exploration. + /// \param addedStates The newly branched states with `current` as common ancestor. + /// \param removedStates The states that will be terminated. virtual void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) = 0; + /// \return True if no state left for exploration, False otherwise virtual bool empty() = 0; - // prints name of searcher as a klee_message() - // TODO: could probably make prettier or more flexible + /// Prints name of searcher as a `klee_message()`. + // TODO: could probably made prettier or more flexible virtual void printName(llvm::raw_ostream &os) { os << "<unnamed searcher>\n"; } - // pgbovine - to be called when a searcher gets activated and - // deactivated, say, by a higher-level searcher; most searchers - // don't need this functionality, so don't have to override. - virtual void activate() {} - virtual void deactivate() {} - // utility functions - void addState(ExecutionState *es, ExecutionState *current = 0) { - std::vector<ExecutionState *> tmp; - tmp.push_back(es); - update(current, tmp, std::vector<ExecutionState *>()); + void addState(ExecutionState *es, ExecutionState *current = nullptr) { + update(current, {es}, std::vector<ExecutionState *>()); } - void removeState(ExecutionState *es, ExecutionState *current = 0) { - std::vector<ExecutionState *> tmp; - tmp.push_back(es); - update(current, std::vector<ExecutionState *>(), tmp); + void removeState(ExecutionState *es, ExecutionState *current = nullptr) { + update(current, std::vector<ExecutionState *>(), {es}); } - enum CoreSearchType { + enum CoreSearchType : std::uint8_t { DFS, BFS, RandomState, @@ -88,53 +87,62 @@ namespace klee { }; }; - class DFSSearcher : public Searcher { + /// DFSSearcher implements depth-first exploration. All states are kept in + /// insertion order. The last state is selected for further exploration. + class DFSSearcher final : public Searcher { std::vector<ExecutionState*> states; public: - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty() { return states.empty(); } - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override { return states.empty(); } + void printName(llvm::raw_ostream &os) override { os << "DFSSearcher\n"; } }; - class BFSSearcher : public Searcher { + /// BFSSearcher implements breadth-first exploration. When KLEE branches multiple + /// times for a single instruction, all new states have the same depth. Keep in + /// mind that the process tree (PTree) is a binary tree and hence the depth of + /// a state in that tree and its branch depth during BFS are different. + class BFSSearcher final : public Searcher { std::deque<ExecutionState*> states; public: - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty() { return states.empty(); } - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override { return states.empty(); } + void printName(llvm::raw_ostream &os) override { os << "BFSSearcher\n"; } }; - class RandomSearcher : public Searcher { + /// RandomSearcher picks a state randomly. + class RandomSearcher final : public Searcher { std::vector<ExecutionState*> states; RNG &theRNG; public: explicit RandomSearcher(RNG &rng) : theRNG{rng} {} - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty() { return states.empty(); } - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override { return states.empty(); } + void printName(llvm::raw_ostream &os) override { os << "RandomSearcher\n"; } }; - class WeightedRandomSearcher : public Searcher { + /// The base class for all weighted searchers. Uses DiscretePDF as underlying + /// data structure. + class WeightedRandomSearcher final : public Searcher { public: - enum WeightType { + enum WeightType : std::uint8_t { Depth, RP, QueryCost, @@ -145,7 +153,7 @@ namespace klee { }; private: - DiscretePDF<ExecutionState*, ExecutionStateIDCompare> *states; + std::unique_ptr<DiscretePDF<ExecutionState*, ExecutionStateIDCompare>> states; RNG &theRNG; WeightType type; bool updateWeights; @@ -153,15 +161,17 @@ namespace klee { double getWeight(ExecutionState*); public: + /// \param type The WeightType that determines the underlying heuristic. + /// \param RNG A random number generator. WeightedRandomSearcher(WeightType type, RNG &rng); - ~WeightedRandomSearcher(); + ~WeightedRandomSearcher() override = default; - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty(); - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override; + void printName(llvm::raw_ostream &os) override { os << "WeightedRandomSearcher::"; switch(type) { case Depth : os << "Depth\n"; return; @@ -176,25 +186,22 @@ namespace klee { } }; - /* RandomPathSearcher performs a random walk of the PTree to - select a state. PTree is a global data structure, however - a searcher can sometimes only select from a subset of all states - (depending on the update calls). - - To support this RandomPathSearcher has a subgraph view of PTree, in that it - only - walks the PTreeNodes that it "owns". Ownership is stored in the - getInt method of PTreeNodePtr class (which hides it in the pointer itself). - - The current implementation of PTreeNodePtr supports only 3 instances of the - RandomPathSearcher. This is because current PTreeNodePtr implementation - conforms to C++ and only steals the last 3 alligment bits. This restriction - could be relaxed slightly by an architecture specific implementation of - PTreeNodePtr, that also steals the top bits of the pointer. - - The ownership bits are maintained in the update method. - */ - class RandomPathSearcher : public Searcher { + /// RandomPathSearcher performs a random walk of the PTree to select a state. + /// PTree is a global data structure, however, a searcher can sometimes only + /// select from a subset of all states (depending on the update calls). + /// + /// To support this, RandomPathSearcher has a subgraph view of PTree, in that it + /// only walks the PTreeNodes that it "owns". Ownership is stored in the + /// getInt method of the PTreeNodePtr class (which hides it in the pointer itself). + /// + /// The current implementation of PTreeNodePtr supports only 3 instances of the + /// RandomPathSearcher. This is because the current PTreeNodePtr implementation + /// conforms to C++ and only steals the last 3 alignment bits. This restriction + /// could be relaxed slightly by an architecture-specific implementation of + /// PTreeNodePtr that also steals the top bits of the pointer. + /// + /// The ownership bits are maintained in the update method. + class RandomPathSearcher final : public Searcher { PTree &processTree; RNG &theRNG; @@ -202,15 +209,20 @@ namespace klee { const uint8_t idBitMask; public: - RandomPathSearcher(PTree &processTree, RNG &rng); - ~RandomPathSearcher(); - - ExecutionState &selectState(); + /// \param processTree The process tree. + /// \param RNG A random number generator. + RandomPathSearcher(PTree &processTree, RNG &rng) : + processTree{processTree}, + theRNG{rng}, + idBitMask{processTree.getNextId()} {}; + ~RandomPathSearcher() override = default; + + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty(); - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override; + void printName(llvm::raw_ostream &os) override { os << "RandomPathSearcher\n"; } }; @@ -218,19 +230,20 @@ namespace klee { extern llvm::cl::opt<bool> UseIncompleteMerge; class MergeHandler; - class MergingSearcher : public Searcher { + class MergingSearcher final : public Searcher { friend class MergeHandler; private: - Searcher *baseSearcher; + std::unique_ptr<Searcher> baseSearcher; /// States that have been paused by the 'pauseState' function std::vector<ExecutionState*> pausedStates; public: - MergingSearcher(Searcher *baseSearcher); - ~MergingSearcher(); + /// \param baseSearcher The underlying searcher (takes ownership). + explicit MergingSearcher(Searcher *baseSearcher) : baseSearcher{baseSearcher} {}; + ~MergingSearcher() override = default; /// ExecutionStates currently paused from scheduling because they are /// waiting to be merged in a klee_close_merge instruction @@ -260,11 +273,11 @@ namespace klee { baseSearcher->addState(&state); } - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates) { + const std::vector<ExecutionState *> &removedStates) override { // We have to check if the current execution state was just deleted, as to // not confuse the nurs searchers if (std::find(pausedStates.begin(), pausedStates.end(), current) == @@ -273,33 +286,40 @@ namespace klee { } } - bool empty() { return baseSearcher->empty(); } - void printName(llvm::raw_ostream &os) { + bool empty() override { return baseSearcher->empty(); } + void printName(llvm::raw_ostream &os) override { os << "MergingSearcher\n"; } }; - class BatchingSearcher : public Searcher { - Searcher *baseSearcher; + /// BatchingSearcher selects a state from an underlying searcher and returns + /// that state for further exploration for a given time or a given number + /// of instructions. + class BatchingSearcher final : public Searcher { + std::unique_ptr<Searcher> baseSearcher; time::Span timeBudget; unsigned instructionBudget; - ExecutionState *lastState; + ExecutionState *lastState {nullptr}; time::Point lastStartTime; unsigned lastStartInstructions; public: - BatchingSearcher(Searcher *baseSearcher, - time::Span _timeBudget, - unsigned _instructionBudget); - ~BatchingSearcher(); - - ExecutionState &selectState(); + /// \param baseSearcher The underlying searcher (takes ownership). + /// \param timeBudget Time span a state gets selected before choosing a different one. + /// \param instructionBudget Number of instructions to re-select a state for. + BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget) : + baseSearcher{baseSearcher}, + timeBudget{timeBudget}, + instructionBudget{instructionBudget} {}; + ~BatchingSearcher() override = default; + + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty() { return baseSearcher->empty(); } - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override { return baseSearcher->empty(); } + void printName(llvm::raw_ostream &os) override { os << "<BatchingSearcher> timeBudget: " << timeBudget << ", instructionBudget: " << instructionBudget << ", baseSearcher:\n"; @@ -308,51 +328,59 @@ namespace klee { } }; - class IterativeDeepeningTimeSearcher : public Searcher { - Searcher *baseSearcher; + /// IterativeDeepeningTimeSearcher implements time-based deepening. States + /// are selected from an underlying searcher. When a state reaches its time + /// limit it is paused (removed from underlying searcher). When the underlying + /// searcher runs out of states, the time budget is increased and all paused + /// states are revived (added to underlying searcher). + class IterativeDeepeningTimeSearcher final : public Searcher { + std::unique_ptr<Searcher> baseSearcher; time::Point startTime; - time::Span time; + time::Span time {time::seconds(1)}; std::set<ExecutionState*> pausedStates; public: - IterativeDeepeningTimeSearcher(Searcher *baseSearcher); - ~IterativeDeepeningTimeSearcher(); + /// \param baseSearcher The underlying searcher (takes ownership). + explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher) : + baseSearcher{baseSearcher} {}; + ~IterativeDeepeningTimeSearcher() override = default; - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty() { return baseSearcher->empty() && pausedStates.empty(); } - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override { return baseSearcher->empty() && pausedStates.empty(); } + void printName(llvm::raw_ostream &os) override { os << "IterativeDeepeningTimeSearcher\n"; } }; - class InterleavedSearcher : public Searcher { - typedef std::vector<Searcher*> searchers_ty; - - searchers_ty searchers; - unsigned index; + /// InterleavedSearcher selects states from a set of searchers in round-robin + /// manner. It is used for KLEE's default strategy where it switches between + /// RandomPathSearcher and WeightedRandomSearcher with CoveringNew metric. + class InterleavedSearcher final : public Searcher { + std::vector<std::unique_ptr<Searcher>> searchers; + unsigned index {1}; public: - explicit InterleavedSearcher(const searchers_ty &_searchers); - ~InterleavedSearcher(); + /// \param searchers The underlying searchers (takes ownership). + explicit InterleavedSearcher(const std::vector<Searcher *> &searchers); + ~InterleavedSearcher() override = default; - ExecutionState &selectState(); + ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - const std::vector<ExecutionState *> &removedStates); - bool empty() { return searchers[0]->empty(); } - void printName(llvm::raw_ostream &os) { + const std::vector<ExecutionState *> &removedStates) override; + bool empty() override { return searchers[0]->empty(); } + void printName(llvm::raw_ostream &os) override { os << "<InterleavedSearcher> containing " << searchers.size() << " searchers:\n"; - for (searchers_ty::iterator it = searchers.begin(), ie = searchers.end(); - it != ie; ++it) - (*it)->printName(os); + for (const auto &searcher : searchers) + searcher->printName(os); os << "</InterleavedSearcher>\n"; } }; -} +} // klee namespace #endif /* KLEE_SEARCHER_H */ |