diff options
| -rw-r--r-- | lib/Core/Searcher.cpp | 130 | ||||
| -rw-r--r-- | lib/Core/Searcher.h | 114 |
2 files changed, 156 insertions, 88 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index f8fd2aea..0dffcf2c 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -70,6 +70,15 @@ void DFSSearcher::update(ExecutionState *current, } } +bool DFSSearcher::empty() { + return states.empty(); +} + +void DFSSearcher::printName(llvm::raw_ostream &os) { + os << "DFSSearcher\n"; +} + + /// ExecutionState &BFSSearcher::selectState() { @@ -115,8 +124,19 @@ void BFSSearcher::update(ExecutionState *current, } } +bool BFSSearcher::empty() { + return states.empty(); +} + +void BFSSearcher::printName(llvm::raw_ostream &os) { + os << "BFSSearcher\n"; +} + + /// +RandomSearcher::RandomSearcher(RNG &rng) : theRNG{rng} {} + ExecutionState &RandomSearcher::selectState() { return *states[theRNG.getInt32() % states.size()]; } @@ -144,6 +164,15 @@ void RandomSearcher::update(ExecutionState *current, } } +bool RandomSearcher::empty() { + return states.empty(); +} + +void RandomSearcher::printName(llvm::raw_ostream &os) { + os << "RandomSearcher\n"; +} + + /// WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng) @@ -236,12 +265,32 @@ bool WeightedRandomSearcher::empty() { return states->empty(); } +void WeightedRandomSearcher::printName(llvm::raw_ostream &os) { + os << "WeightedRandomSearcher::"; + switch(type) { + case Depth : os << "Depth\n"; return; + case RP : os << "RandomPath\n"; return; + case QueryCost : os << "QueryCost\n"; return; + case InstCount : os << "InstCount\n"; return; + case CPInstCount : os << "CPInstCount\n"; return; + case MinDistToUncovered : os << "MinDistToUncovered\n"; return; + case CoveringNew : os << "CoveringNew\n"; return; + default : os << "<unknown type>\n"; return; + } +} + + /// // 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)) +RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng) + : processTree{processTree}, + theRNG{rng}, + idBitMask{processTree.getNextId()} {}; + ExecutionState &RandomPathSearcher::selectState() { unsigned flips=0, bits=0; assert(processTree.root.getInt() & idBitMask && @@ -317,8 +366,29 @@ bool RandomPathSearcher::empty() { return !IS_OUR_NODE_VALID(processTree.root); } +void RandomPathSearcher::printName(llvm::raw_ostream &os) { + os << "RandomPathSearcher\n"; +} + + /// +MergingSearcher::MergingSearcher(Searcher *baseSearcher) + : baseSearcher{baseSearcher} {}; + +void MergingSearcher::pauseState(ExecutionState &state) { + assert(std::find(pausedStates.begin(), pausedStates.end(), &state) == pausedStates.end()); + pausedStates.push_back(&state); + baseSearcher->update(nullptr, {}, {&state}); +} + +void MergingSearcher::continueState(ExecutionState &state) { + auto it = std::find(pausedStates.begin(), pausedStates.end(), &state); + assert(it != pausedStates.end()); + pausedStates.erase(it); + baseSearcher->update(nullptr, {&state}, {}); +} + ExecutionState& MergingSearcher::selectState() { assert(!baseSearcher->empty() && "base searcher is empty"); @@ -348,8 +418,32 @@ ExecutionState& MergingSearcher::selectState() { return baseSearcher->selectState(); } +void MergingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + // 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) == pausedStates.end()) { + baseSearcher->update(current, addedStates, removedStates); + } +} + +bool MergingSearcher::empty() { + return baseSearcher->empty(); +} + +void MergingSearcher::printName(llvm::raw_ostream &os) { + os << "MergingSearcher\n"; +} + + /// +BatchingSearcher::BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget) + : baseSearcher{baseSearcher}, + timeBudget{timeBudget}, + instructionBudget{instructionBudget} {}; + ExecutionState &BatchingSearcher::selectState() { if (!lastState || (((timeBudget.toSeconds() > 0) && @@ -385,8 +479,24 @@ void BatchingSearcher::update(ExecutionState *current, baseSearcher->update(current, addedStates, removedStates); } +bool BatchingSearcher::empty() { + return baseSearcher->empty(); +} + +void BatchingSearcher::printName(llvm::raw_ostream &os) { + os << "<BatchingSearcher> timeBudget: " << timeBudget + << ", instructionBudget: " << instructionBudget + << ", baseSearcher:\n"; + baseSearcher->printName(os); + os << "</BatchingSearcher>\n"; +} + + /// +IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *baseSearcher) + : baseSearcher{baseSearcher} {}; + ExecutionState &IterativeDeepeningTimeSearcher::selectState() { ExecutionState &res = baseSearcher->selectState(); startTime = time::getWallTime(); @@ -433,6 +543,15 @@ void IterativeDeepeningTimeSearcher::update( } } +bool IterativeDeepeningTimeSearcher::empty() { + return baseSearcher->empty() && pausedStates.empty(); +} + +void IterativeDeepeningTimeSearcher::printName(llvm::raw_ostream &os) { + os << "IterativeDeepeningTimeSearcher\n"; +} + + /// InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers) { @@ -455,3 +574,14 @@ void InterleavedSearcher::update( for (auto &searcher : searchers) searcher->update(current, addedStates, removedStates); } + +bool InterleavedSearcher::empty() { + return searchers[0]->empty(); +} + +void InterleavedSearcher::printName(llvm::raw_ostream &os) { + os << "<InterleavedSearcher> containing " << searchers.size() << " searchers:\n"; + for (const auto &searcher : searchers) + searcher->printName(os); + os << "</InterleavedSearcher>\n"; +} diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index e7f146e0..4eda838d 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -58,9 +58,7 @@ namespace klee { /// 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"; - } + virtual void printName(llvm::raw_ostream &os) = 0; enum CoreSearchType : std::uint8_t { DFS, @@ -87,10 +85,8 @@ namespace klee { void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) override; - bool empty() override { return states.empty(); } - void printName(llvm::raw_ostream &os) override { - os << "DFSSearcher\n"; - } + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; /// BFSSearcher implements breadth-first exploration. When KLEE branches multiple @@ -105,10 +101,8 @@ namespace klee { void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) override; - bool empty() override { return states.empty(); } - void printName(llvm::raw_ostream &os) override { - os << "BFSSearcher\n"; - } + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; /// RandomSearcher picks a state randomly. @@ -117,15 +111,13 @@ namespace klee { RNG &theRNG; public: - explicit RandomSearcher(RNG &rng) : theRNG{rng} {} + explicit RandomSearcher(RNG &rng); ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) override; - bool empty() override { return states.empty(); } - void printName(llvm::raw_ostream &os) override { - os << "RandomSearcher\n"; - } + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; /// The base class for all weighted searchers. Uses DiscretePDF as underlying @@ -161,19 +153,7 @@ namespace klee { const std::vector<ExecutionState *> &addedStates, 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; - case RP : os << "RandomPath\n"; return; - case QueryCost : os << "QueryCost\n"; return; - case InstCount : os << "InstCount\n"; return; - case CPInstCount : os << "CPInstCount\n"; return; - case MinDistToUncovered : os << "MinDistToUncovered\n"; return; - case CoveringNew : os << "CoveringNew\n"; return; - default : os << "<unknown type>\n"; return; - } - } + void printName(llvm::raw_ostream &os) override; }; /// RandomPathSearcher performs a random walk of the PTree to select a state. @@ -201,10 +181,7 @@ namespace klee { public: /// \param processTree The process tree. /// \param RNG A random number generator. - RandomPathSearcher(PTree &processTree, RNG &rng) : - processTree{processTree}, - theRNG{rng}, - idBitMask{processTree.getNextId()} {}; + RandomPathSearcher(PTree &processTree, RNG &rng); ~RandomPathSearcher() override = default; ExecutionState &selectState() override; @@ -212,9 +189,7 @@ namespace klee { const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) override; bool empty() override; - void printName(llvm::raw_ostream &os) override { - os << "RandomPathSearcher\n"; - } + void printName(llvm::raw_ostream &os) override; }; @@ -232,7 +207,7 @@ namespace klee { public: /// \param baseSearcher The underlying searcher (takes ownership). - explicit MergingSearcher(Searcher *baseSearcher) : baseSearcher{baseSearcher} {}; + explicit MergingSearcher(Searcher *baseSearcher); ~MergingSearcher() override = default; /// ExecutionStates currently paused from scheduling because they are @@ -249,37 +224,18 @@ namespace klee { /// Remove state from the searcher chain, while keeping it in the executor. /// This is used here to 'freeze' a state while it is waiting for other /// states in its merge group to reach the same instruction. - void pauseState(ExecutionState &state) { - assert(std::find(pausedStates.begin(), pausedStates.end(), &state) == pausedStates.end()); - pausedStates.push_back(&state); - baseSearcher->update(nullptr, {}, {&state}); - } + void pauseState(ExecutionState &state); /// Continue a paused state - void continueState(ExecutionState &state) { - auto it = std::find(pausedStates.begin(), pausedStates.end(), &state); - assert(it != pausedStates.end()); - pausedStates.erase(it); - baseSearcher->update(nullptr, {&state}, {}); - } + void continueState(ExecutionState &state); ExecutionState &selectState() override; - void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, - 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) == - pausedStates.end()) { - baseSearcher->update(current, addedStates, removedStates); - } - } - - bool empty() override { return baseSearcher->empty(); } - void printName(llvm::raw_ostream &os) override { - os << "MergingSearcher\n"; - } + const std::vector<ExecutionState *> &removedStates) override; + + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; /// BatchingSearcher selects a state from an underlying searcher and returns @@ -298,24 +254,15 @@ namespace klee { /// \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(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget); ~BatchingSearcher() override = default; ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, 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"; - baseSearcher->printName(os); - os << "</BatchingSearcher>\n"; - } + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; /// IterativeDeepeningTimeSearcher implements time-based deepening. States @@ -331,18 +278,15 @@ namespace klee { public: /// \param baseSearcher The underlying searcher (takes ownership). - explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher) : - baseSearcher{baseSearcher} {}; + explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher); ~IterativeDeepeningTimeSearcher() override = default; ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) override; - bool empty() override { return baseSearcher->empty() && pausedStates.empty(); } - void printName(llvm::raw_ostream &os) override { - os << "IterativeDeepeningTimeSearcher\n"; - } + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; /// InterleavedSearcher selects states from a set of searchers in round-robin @@ -361,14 +305,8 @@ namespace klee { void update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, 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 (const auto &searcher : searchers) - searcher->printName(os); - os << "</InterleavedSearcher>\n"; - } + bool empty() override; + void printName(llvm::raw_ostream &os) override; }; } // klee namespace |