Use vector instead of set to add/remove states

Deterministic adding/removing of states.

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);