Implemented incomplete merging

1 files changed, 38 insertions, 2 deletions

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 05ebe6a6..dfeb15de 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -15,6 +15,7 @@
 #include "StatsTracker.h"
 
 #include "klee/ExecutionState.h"
+#include "klee/MergeHandler.h"
 #include "klee/Statistics.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
 #include "klee/Internal/Module/KInstruction.h"
@@ -42,6 +43,7 @@
 using namespace klee;
 using namespace llvm;
 
+
 namespace klee {
   extern RNG theRNG;
 }
@@ -257,7 +259,6 @@ bool WeightedRandomSearcher::empty() {
 }
 
 ///
-
 RandomPathSearcher::RandomPathSearcher(Executor &_executor)
   : executor(_executor) {
 }
@@ -268,7 +269,6 @@ RandomPathSearcher::~RandomPathSearcher() {
 ExecutionState &RandomPathSearcher::selectState() {
   unsigned flips=0, bits=0;
   PTree::Node *n = executor.processTree->root;
-  
   while (!n->data) {
     if (!n->left) {
       n = n->right;
@@ -299,6 +299,42 @@ bool RandomPathSearcher::empty() {
 
 ///
 
+MergingSearcher::MergingSearcher(Executor &_executor, Searcher *_baseSearcher)
+  : executor(_executor),
+  baseSearcher(_baseSearcher){}
+
+MergingSearcher::~MergingSearcher() {
+  delete baseSearcher;
+}
+
+ExecutionState& MergingSearcher::selectState() {
+  assert(!baseSearcher->empty() && "base searcher is empty");
+
+  // Iterate through all MergeHandlers
+  for (auto cur_mergehandler: executor.mergeGroups) {
+    // Find one that has states that could be released
+    if (!cur_mergehandler->hasMergedStates()) {
+      continue;
+    }
+    // Find a state that can be prioritized
+    ExecutionState *es = cur_mergehandler->getPrioritizeState();
+    if (es) {
+      return *es;
+    } else {
+      if (DebugLogIncompleteMerge){
+        llvm::errs() << "Preemptively releasing states\n";
+      }
+      // If no state can be prioritized, they all exceeded the amount of time we
+      // are willing to wait for them. Release the states that already arrived at close_merge.
+      cur_mergehandler->releaseStates();
+    }
+  }
+  // If we were not able to prioritize a merging state, just return some state
+  return baseSearcher->selectState();
+}
+
+///
+
 BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
                                    double _timeBudget,
                                    unsigned _instructionBudget)