about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2013-08-07 13:22:06 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2013-08-07 13:22:06 +0100
commit363e7ab2d7bfa790b666eac1b48b7b7daf02e5e3 (patch)
tree6716b850795baa8ae09312e7cc6952f24627624f
parent357ecb515baaa018a5b4b611f7cb4000e91315d3 (diff)
parent939d6874d114f5a39396f28aeb6ebc17a0dc652b (diff)
downloadklee-363e7ab2d7bfa790b666eac1b48b7b7daf02e5e3.tar.gz
Merge branch 'bfs' of https://github.com/antiAgainst/klee into antiAgainst-bfs
-rw-r--r--lib/Core/Searcher.cpp34
-rw-r--r--lib/Core/Searcher.h17
-rw-r--r--lib/Core/UserSearcher.cpp2
-rw-r--r--[-rwxr-xr-x]runtime/Makefile0
-rw-r--r--[-rwxr-xr-x]unittests/Makefile0
5 files changed, 52 insertions, 1 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index d08cd1b1..778ef0ef 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -88,6 +88,40 @@ void DFSSearcher::update(ExecutionState *current,
 
 ///
 
+ExecutionState &BFSSearcher::selectState() {
+  return *states.front();
+}
+
+void BFSSearcher::update(ExecutionState *current,
+                         const std::set<ExecutionState*> &addedStates,
+                         const std::set<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) {
+    ExecutionState *es = *it;
+    if (es == states.front()) {
+      states.pop_front();
+    } else {
+      bool ok = false;
+
+      for (std::deque<ExecutionState*>::iterator it = states.begin(),
+             ie = states.end(); it != ie; ++it) {
+        if (es==*it) {
+          states.erase(it);
+          ok = true;
+          break;
+        }
+      }
+
+      assert(ok && "invalid state removed");
+    }
+  }
+}
+
+///
+
 ExecutionState &RandomSearcher::selectState() {
   return *states[theRNG.getInt32()%states.size()];
 }
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 58772bbb..79c233c4 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -68,7 +68,8 @@ namespace klee {
     }
 
     enum CoreSearchType {
-      DFS,                
+      DFS,
+      BFS,
       RandomState,
       RandomPath,
       NURS_CovNew,
@@ -94,6 +95,20 @@ namespace klee {
     }
   };
 
+  class BFSSearcher : public Searcher {
+    std::deque<ExecutionState*> states;
+
+  public:
+    ExecutionState &selectState();
+    void update(ExecutionState *current,
+                const std::set<ExecutionState*> &addedStates,
+                const std::set<ExecutionState*> &removedStates);
+    bool empty() { return states.empty(); }
+    void printName(std::ostream &os) {
+      os << "BFSSearcher\n";
+    }
+  };
+
   class RandomSearcher : public Searcher {
     std::vector<ExecutionState*> states;
 
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 361092d2..a20ae968 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -23,6 +23,7 @@ namespace {
   cl::list<Searcher::CoreSearchType>
   CoreSearch("search", cl::desc("Specify the search heuristic (default=random-path interleaved with nurs:covnew)"),
 	     cl::values(clEnumValN(Searcher::DFS, "dfs", "use Depth First Search (DFS)"),
+			clEnumValN(Searcher::BFS, "bfs", "use Breadth First Search (BFS)"),
 			clEnumValN(Searcher::RandomState, "random-state", "randomly select a state to explore"),
 			clEnumValN(Searcher::RandomPath, "random-path", "use Random Path Selection (see OSDI'08 paper)"),
 			clEnumValN(Searcher::NURS_CovNew, "nurs:covnew", "use Non Uniform Random Search (NURS) with Coverage-New"),
@@ -77,6 +78,7 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
   Searcher *searcher = NULL;
   switch (type) {
   case Searcher::DFS: searcher = new DFSSearcher(); break;
+  case Searcher::BFS: searcher = new BFSSearcher(); break;
   case Searcher::RandomState: searcher = new RandomSearcher(); break;
   case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
   case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CoveringNew); break;
diff --git a/runtime/Makefile b/runtime/Makefile
index 24824d08..24824d08 100755..100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
diff --git a/unittests/Makefile b/unittests/Makefile
index 761987d6..761987d6 100755..100644
--- a/unittests/Makefile
+++ b/unittests/Makefile