4 files changed, 55 insertions, 18 deletions
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h
index 79357d7c..75f4a3d1 100644
--- a/include/klee/MergeHandler.h
+++ b/include/klee/MergeHandler.h
@@ -48,6 +48,22 @@
  * reaches zero, every state which ran into the same `klee_open_merge()` is now
  * paused and waiting to be merged. The destructor of the MergeHandler
  * then continues the scheduling of the corresponding paused states.
+ *
+ * # Non-blocking State Merging
+ *
+ * This feature adds functionality to the BoundedMergingSearcher that will
+ * prioritize (e.g., immediately schedule) states running inside a bounded-merge
+ * region once a state has reached a corresponding klee_close_merge() call. The
+ * goal is to quickly gather all states inside the merging region in order to
+ * release the waiting states. However, states that are running for more than
+ * twice the mean number of instructions compared to the states that are already
+ * waiting, will not be prioritized anymore.
+ *
+ * Once no more states are available for prioritizing, but there are states
+ * waiting to be released, these states (which have already been merged as good as
+ * possible) will be continued without waiting for the remaining states. When a
+ * remaining state now enters a close-merge point, it will again wait for the
+ * other states, or until the 'timeout' is reached.
 */
 
 #ifndef KLEE_MERGEHANDLER_H
@@ -85,14 +101,14 @@ private:
 
   /// @brief The average number of instructions between the open and close merge of each
   /// state that has finished so far
-  double closeMean;
+  double closedMean;
 
   /// @brief Number of states that are tracked by this MergeHandler, that ran
   /// into a relevant klee_close_merge
   unsigned closedStateCount;
 
   /// @brief Get distance of state from the openInstruction
-  unsigned getInstrDistance(ExecutionState *es);
+  unsigned getInstructionDistance(ExecutionState *es);
 
   /// @brief States that ran through the klee_open_merge, but not yet into a
   /// corresponding klee_close_merge
@@ -101,7 +117,7 @@ private:
   /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into
   /// them
   std::map<llvm::Instruction *, std::vector<ExecutionState *> >
-      reachedMergeClose;
+      reachedCloseMerge;
 
 public:
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 852aaf3c..a0174ab7 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -134,10 +134,14 @@ private:
   std::vector<TimerInfo*> timers;
   PTree *processTree;
 
+  /// Keeps track of all currently ongoing merges.
+  /// An ongoing merge is a set of states which branched from a single state
+  /// which ran into a klee_open_merge(), and not all states in the set have
+  /// reached the corresponding klee_close_merge() yet.
   std::vector<MergeHandler *> mergeGroups;
 
-  // Set of vectors that are currently paused from scheduling because they are
-  // waiting to be merged in a klee_close_merge instruction
+  /// ExecutionStates currently paused from scheduling because they are
+  /// waiting to be merged in a klee_close_merge instruction
   std::set<ExecutionState *> inCloseMerge;
 
   /// Used to track states that have been added during the current
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp
index 45373002..67c24912 100644
--- a/lib/Core/MergeHandler.cpp
+++ b/lib/Core/MergeHandler.cpp
@@ -38,10 +38,10 @@ double MergeHandler::getMean() {
   if (closedStateCount == 0)
     return 0;
 
-  return closeMean;
+  return closedMean;
 }
 
-unsigned MergeHandler::getInstrDistance(ExecutionState *es){
+unsigned MergeHandler::getInstructionDistance(ExecutionState *es){
   return es->steppedInstructions - openInstruction;
 }
 
@@ -50,7 +50,7 @@ ExecutionState *MergeHandler::getPrioritizeState(){
     bool stateIsClosed = (executor->inCloseMerge.find(cur_state) !=
                           executor->inCloseMerge.end());
 
-    if (!stateIsClosed && (getInstrDistance(cur_state) < 2 * getMean())) {
+    if (!stateIsClosed && (getInstructionDistance(cur_state) < 2 * getMean())) {
       return cur_state;
     }
   }
@@ -77,18 +77,21 @@ void MergeHandler::addClosedState(ExecutionState *es,
                                          llvm::Instruction *mp) {
   // Update stats
   ++closedStateCount;
-  closeMean += (static_cast<double>(getInstrDistance(es)) - closeMean) /
+
+  // Incremental update of mean (travelling mean)
+  // https://math.stackexchange.com/a/1836447
+  closedMean += (static_cast<double>(getInstructionDistance(es)) - closedMean) /
                closedStateCount;
 
   // Remove from openStates
   removeOpenState(es);
 
-  auto closePoint = reachedMergeClose.find(mp);
+  auto closePoint = reachedCloseMerge.find(mp);
 
   // If no other state has yet encountered this klee_close_merge instruction,
   // add a new element to the map
-  if (closePoint == reachedMergeClose.end()) {
-    reachedMergeClose[mp].push_back(es);
+  if (closePoint == reachedCloseMerge.end()) {
+    reachedCloseMerge[mp].push_back(es);
     executor->pauseState(*es);
   } else {
     // Otherwise try to merge with any state in the map element for this
@@ -111,16 +114,16 @@ void MergeHandler::addClosedState(ExecutionState *es,
 }
 
 void MergeHandler::releaseStates() {
-  for (auto& curMergeGroup: reachedMergeClose) {
+  for (auto& curMergeGroup: reachedCloseMerge) {
     for (auto curState: curMergeGroup.second) {
       executor->continueState(*curState);
     }
   }
-  reachedMergeClose.clear();
+  reachedCloseMerge.clear();
 }
 
 bool MergeHandler::hasMergedStates() {
-  return (!reachedMergeClose.empty());
+  return (!reachedCloseMerge.empty());
 }
 
 MergeHandler::MergeHandler(Executor *_executor, ExecutionState *es)
diff --git a/test/Merging/incomplete_merge.c b/test/Merging/incomplete_merge.c
index 1962cfaa..bb5e4f37 100644
--- a/test/Merging/incomplete_merge.c
+++ b/test/Merging/incomplete_merge.c
@@ -16,6 +16,11 @@
 // CHECK: close merge:
 // CHECK: close merge:
 
+// This test merges branches with vastly different instruction counts.
+// The incomplete merging heuristic merges preemptively if a branch takes too long.
+// It might occur that the random branch selection completes the heavy branch first,
+// which results in the branches being merged completely.
+
 #include <klee/klee.h>
 
 int main(int argc, char **args) {
@@ -31,15 +36,24 @@ int main(int argc, char **args) {
   if (a == 0) {
     klee_open_merge();
 
+    for (int i = 0; i < 5; ++i){
+      foo += 2;
+    }
     if (x == 1) {
-      foo = 5;
+      foo += 5;
     } else if (x == 2) {
-      foo = 6;
+      for (int i = 0; i < 10; ++i) {
+        foo += foo;
+      }
     } else {
-      foo = 7;
+      foo += 7;
     }
 
     klee_close_merge();
+  } else if (a == 1) {
+    foo = 4;
+  } else {
+    foo = 3;
   }
   klee_close_merge();