diff options
Diffstat (limited to 'lib/Core/Searcher.cpp')
-rw-r--r-- | lib/Core/Searcher.cpp | 122 |
1 files changed, 71 insertions, 51 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 299bb89d..973057c3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -67,13 +67,14 @@ ExecutionState &DFSSearcher::selectState() { } void DFSSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.back()) { states.pop_back(); @@ -101,13 +102,14 @@ ExecutionState &BFSSearcher::selectState() { } void BFSSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.front()) { states.pop_front(); @@ -134,14 +136,16 @@ ExecutionState &RandomSearcher::selectState() { return *states[theRNG.getInt32()%states.size()]; } -void RandomSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +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::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; bool ok = false; @@ -224,20 +228,24 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { } } -void WeightedRandomSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { - if (current && updateWeights && !removedStates.count(current)) +void WeightedRandomSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + if (current && updateWeights && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) states->update(current, getWeight(current)); - - for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(), - ie = addedStates.end(); it != ie; ++it) { + + for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(), + ie = addedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; states->insert(es, getWeight(es)); } - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { states->remove(*it); } } @@ -277,9 +285,10 @@ ExecutionState &RandomPathSearcher::selectState() { return *n->data; } -void RandomPathSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +RandomPathSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { } bool RandomPathSearcher::empty() { @@ -358,9 +367,9 @@ entry: } } -void BumpMergingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void BumpMergingSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { baseSearcher->update(current, addedStates, removedStates); } @@ -472,18 +481,21 @@ ExecutionState &MergingSearcher::selectState() { return selectState(); } -void MergingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +MergingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { if (!removedStates.empty()) { - std::set<ExecutionState *> alt = removedStates; - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + 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 = statesAtMerge.find(es); if (it2 != statesAtMerge.end()) { statesAtMerge.erase(it2); - alt.erase(alt.find(es)); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -529,10 +541,12 @@ ExecutionState &BatchingSearcher::selectState() { } } -void BatchingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { - if (removedStates.count(lastState)) +void +BatchingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + if (std::find(removedStates.begin(), removedStates.end(), lastState) != + removedStates.end()) lastState = 0; baseSearcher->update(current, addedStates, removedStates); } @@ -554,20 +568,22 @@ ExecutionState &IterativeDeepeningTimeSearcher::selectState() { return res; } -void IterativeDeepeningTimeSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void IterativeDeepeningTimeSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { double elapsed = util::getWallTime() - startTime; if (!removedStates.empty()) { - std::set<ExecutionState *> alt = removedStates; - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + 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(alt.find(es)); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -575,7 +591,10 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, baseSearcher->update(current, addedStates, removedStates); } - if (current && !removedStates.count(current) && elapsed>time) { + if (current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end() && + elapsed > time) { pausedStates.insert(current); baseSearcher->removeState(current); } @@ -583,7 +602,8 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, if (baseSearcher->empty()) { time *= 2; llvm::errs() << "KLEE: increasing time budget to: " << time << "\n"; - baseSearcher->update(0, pausedStates, std::set<ExecutionState*>()); + std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); + baseSearcher->update(0, ps, std::vector<ExecutionState *>()); pausedStates.clear(); } } @@ -607,9 +627,9 @@ ExecutionState &InterleavedSearcher::selectState() { return s->selectState(); } -void InterleavedSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +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); |