diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-22 16:39:28 +0100 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-08 21:56:28 +0200 |
commit | f3ff3b06318cae93db4d682e6451ddbca4760328 (patch) | |
tree | b984df4d0ab09629ef423831f542ff746ff8e34c /lib/Core | |
parent | 07632e75e21e3c61f1ab46f76618cb1b807bd6c3 (diff) | |
download | klee-f3ff3b06318cae93db4d682e6451ddbca4760328.tar.gz |
Use vector instead of set to add/remove states
Deterministic adding/removing of states.
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 18 | ||||
-rw-r--r-- | lib/Core/Executor.h | 4 | ||||
-rw-r--r-- | lib/Core/ExecutorTimers.cpp | 4 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 122 | ||||
-rw-r--r-- | lib/Core/Searcher.h | 56 |
5 files changed, 114 insertions, 90 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2c4e5202..49cba67f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -665,7 +665,7 @@ void Executor::branch(ExecutionState &state, for (unsigned i=1; i<N; ++i) { ExecutionState *es = result[theRNG.getInt32() % i]; ExecutionState *ns = es->branch(); - addedStates.insert(ns); + addedStates.push_back(ns); result.push_back(ns); es->ptreeNode->data = 0; std::pair<PTree::Node*,PTree::Node*> res = @@ -883,7 +883,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { ++stats::forks; falseState = trueState->branch(); - addedStates.insert(falseState); + addedStates.push_back(falseState); if (RandomizeFork && theRNG.getBool()) std::swap(trueState, falseState); @@ -2467,9 +2467,9 @@ void Executor::updateStates(ExecutionState *current) { states.insert(addedStates.begin(), addedStates.end()); addedStates.clear(); - - for (std::set<ExecutionState*>::iterator - it = removedStates.begin(), ie = removedStates.end(); + + for (std::vector<ExecutionState *>::iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::iterator it2 = states.find(es); @@ -2674,7 +2674,8 @@ void Executor::run(ExecutionState &initialState) { searcher = constructUserSearcher(*this); - searcher->update(0, states, std::set<ExecutionState*>()); + std::vector<ExecutionState *> newStates(states.begin(), states.end()); + searcher->update(0, newStates, std::vector<ExecutionState *>()); while (!states.empty() && !haltExecution) { ExecutionState &state = searcher->selectState(); @@ -2753,11 +2754,12 @@ void Executor::terminateState(ExecutionState &state) { interpreterHandler->incPathsExplored(); - std::set<ExecutionState*>::iterator it = addedStates.find(&state); + std::vector<ExecutionState *>::iterator it = + std::find(addedStates.begin(), addedStates.end(), &state); if (it==addedStates.end()) { state.pc = state.prevPC; - removedStates.insert(&state); + removedStates.push_back(&state); } else { // never reached searcher, just delete immediately std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 = diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 99f5921b..92edc364 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -122,12 +122,12 @@ private: /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> addedStates; + std::vector<ExecutionState *> addedStates; /// Used to track states that have been removed during the current /// instructions step. /// \invariant \ref removedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> removedStates; + std::vector<ExecutionState *> removedStates; /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 480f1cde..f1c45105 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -179,7 +179,9 @@ void Executor::processTimers(ExecutionState *current, dumpStates = 0; } - if (maxInstTime>0 && current && !removedStates.count(current)) { + if (maxInstTime > 0 && current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) { if (timerTicks*kSecondsPerTick > maxInstTime) { klee_warning("max-instruction-time exceeded: %.2fs", timerTicks*kSecondsPerTick); 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); diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index d866f521..4ede3640 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -35,8 +35,8 @@ namespace klee { virtual ExecutionState &selectState() = 0; virtual void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) = 0; + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) = 0; virtual bool empty() = 0; @@ -55,15 +55,15 @@ namespace klee { // utility functions void addState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, tmp, std::set<ExecutionState*>()); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, tmp, std::vector<ExecutionState *>()); } void removeState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, std::set<ExecutionState*>(), tmp); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, std::vector<ExecutionState *>(), tmp); } enum CoreSearchType { @@ -86,8 +86,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; @@ -100,8 +100,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; @@ -114,8 +114,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; @@ -146,8 +146,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "WeightedRandomSearcher::"; @@ -172,8 +172,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; @@ -195,8 +195,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; @@ -218,8 +218,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; @@ -243,8 +243,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty(); } void printName(llvm::raw_ostream &os) { os << "<BatchingSearcher> timeBudget: " << timeBudget @@ -266,8 +266,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; @@ -286,8 +286,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return searchers[0]->empty(); } void printName(llvm::raw_ostream &os) { os << "<InterleavedSearcher> containing " |