Implemented bounded merging functionality

21 files changed, 579 insertions, 14 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 78ebddac..6aec61ea 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -13,6 +13,7 @@
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Internal/ADT/TreeStream.h"
+#include "klee/MergeHandler.h"
 
 // FIXME: We do not want to be exposing these? :(
 #include "../../lib/Core/AddressSpace.h"
@@ -145,6 +146,9 @@ public:
   void addFnAlias(std::string old_fn, std::string new_fn);
   void removeFnAlias(std::string fn);
 
+  // The objects handling the klee_open_merge calls this state ran through
+  std::vector<ref<MergeHandler> > openMergeStack;
+
 private:
   ExecutionState() : ptreeNode(0) {}
 
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h
new file mode 100644
index 00000000..d374e168
--- /dev/null
+++ b/include/klee/MergeHandler.h
@@ -0,0 +1,110 @@
+//===-- MergeHandler.h --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/** 
+ * @file MergeHandler.h
+ * @brief Implementation of the region based merging
+ *
+ * ## Basic usage:
+ * 
+ * @code{.cpp}
+ * klee_open_merge();
+ * 
+ * code containing branches etc. 
+ * 
+ * klee_close_merge();
+ * @endcode
+ * 
+ * Will lead to all states that forked from the state that executed the
+ * klee_open_merge() being merged in the klee_close_merge(). This allows for
+ * fine-grained regions to be specified for merging.
+ * 
+ * # Implementation Structure
+ * 
+ * The main part of the new functionality is implemented in the class
+ * klee::MergeHandler. The Special Function Handler generates an instance of
+ * this class every time a state runs into a klee_open_merge() call.
+ * 
+ * This instance is appended to a `std::vector<klee::ref<klee::MergeHandler>>`
+ * in the ExecutionState that passed the merge open point. This stack is also
+ * copied during forks. We use a stack instead of a single instance to support
+ * nested merge regions.
+ * 
+ * Once a state runs into a `klee_close_merge()`, the Special Function Handler
+ * notifies the top klee::MergeHandler in the state's stack, pauses the state
+ * from scheduling, and tries to merge it with all other states that already
+ * arrived at the same close merge point. This top instance is then popped from
+ * the stack, resulting in a decrease of the ref count of the
+ * klee::MergeHandler.
+ * 
+ * Since the only references to this MergeHandler are in the stacks of
+ * the ExecutionStates currently in the merging region, once the ref count
+ * 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.
+*/
+
+#ifndef KLEE_MERGEHANDLER_H
+#define KLEE_MERGEHANDLER_H
+
+#include <vector>
+#include <map>
+#include <stdint.h>
+#include "llvm/Support/CommandLine.h"
+
+namespace llvm {
+class Instruction;
+}
+
+namespace klee {
+extern llvm::cl::opt<bool> UseMerge;
+
+extern llvm::cl::opt<bool> DebugLogMerge;
+
+class Executor;
+class ExecutionState;
+
+/// @brief Represents one `klee_open_merge()` call. 
+/// Handles merging of states that branched from it
+class MergeHandler {
+private:
+  Executor *executor;
+
+  /// @brief Number of states that are tracked by this MergeHandler, that ran
+  /// into a relevant klee_close_merge
+  unsigned closedStateCount;
+
+  /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into
+  /// them
+  std::map<llvm::Instruction *, std::vector<ExecutionState *> >
+      reachedMergeClose;
+
+public:
+
+  /// @brief Called when a state runs into a 'klee_close_merge()' call
+  void addClosedState(ExecutionState *es, llvm::Instruction *mp);
+
+  /// @brief True, if any states have run into 'klee_close_merge()' and have
+  /// not been released yet
+  bool hasMergedStates();
+  
+  /// @brief Immediately release the merged states that have run into a
+  /// 'klee_merge_close()'
+  void releaseStates();
+
+  /// @brief Required by klee::ref objects
+  unsigned refCount;
+
+
+  MergeHandler(Executor *_executor);
+  ~MergeHandler();
+};
+}
+
+#endif	/* KLEE_MERGEHANDLER_H */
diff --git a/include/klee/klee.h b/include/klee/klee.h
index bd3100b5..644c498e 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -152,6 +152,11 @@ extern "C" {
   /* Print range for given argument and tagged with name */
   void klee_print_range(const char * name, int arg );
 
+  /* Open a merge */
+  void klee_open_merge();
+
+  /* Merge all paths of the state that went through klee_open_merge */
+  void klee_close_merge();
 #ifdef __cplusplus
 }
 #endif
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 86ce3cfc..4b14df36 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -8,6 +8,7 @@
 #===------------------------------------------------------------------------===#
 klee_add_component(kleeCore
   AddressSpace.cpp
+  MergeHandler.cpp
   CallPathManager.cpp
   Context.cpp
   CoreStats.cpp
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 20b1a162..522bdd15 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -116,7 +116,8 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     coveredLines(state.coveredLines),
     ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
-    arrayNames(state.arrayNames)
+    arrayNames(state.arrayNames),
+    openMergeStack(state.openMergeStack)
 {
   for (unsigned int i=0; i<symbolics.size(); i++)
     symbolics[i].first->refCount++;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index e79d6a2c..be92b16a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2456,7 +2456,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 void Executor::updateStates(ExecutionState *current) {
   if (searcher) {
     searcher->update(current, addedStates, removedStates);
-    searcher->update(0, continuedStates, pausedStates);
+    searcher->update(nullptr, continuedStates, pausedStates);
     pausedStates.clear();
     continuedStates.clear();
   }
@@ -2745,7 +2745,7 @@ std::string Executor::getAddressInfo(ExecutionState &state,
 }
 
 void Executor::pauseState(ExecutionState &state){
-  std::vector<ExecutionState *>::iterator it = std::find(continuedStates.begin(), continuedStates.end(), &state);
+  auto it = std::find(continuedStates.begin(), continuedStates.end(), &state);
   // If the state was to be continued, but now gets paused again
   if (it != continuedStates.end()){
     // ...just don't continue it
@@ -2757,7 +2757,7 @@ void Executor::pauseState(ExecutionState &state){
 }
 
 void Executor::continueState(ExecutionState &state){
-  std::vector<ExecutionState *>::iterator it = std::find(pausedStates.begin(), pausedStates.end(), &state);
+  auto it = std::find(pausedStates.begin(), pausedStates.end(), &state);
   // If the state was to be paused, but now gets continued again
   if (it != pausedStates.end()){
     // ...don't pause it
@@ -2768,7 +2768,6 @@ void Executor::continueState(ExecutionState &state){
   }
 }
 
-
 void Executor::terminateState(ExecutionState &state) {
   if (replayKTest && replayPosition!=replayKTest->numObjects) {
     klee_warning_once(replayKTest,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index c6f01179..71b1f5f7 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -69,6 +69,7 @@ namespace klee {
   class StatsTracker;
   class TimingSolver;
   class TreeStreamWriter;
+  class MergeHandler;
   template<class T> class ref;
 
 
@@ -78,13 +79,12 @@ namespace klee {
   /// removedStates, and haltExecution, among others.
 
 class Executor : public Interpreter {
-  friend class BumpMergingSearcher;
-  friend class MergingSearcher;
   friend class RandomPathSearcher;
   friend class OwningSearcher;
   friend class WeightedRandomSearcher;
   friend class SpecialFunctionHandler;
   friend class StatsTracker;
+  friend class MergeHandler;
 
 public:
   class Timer {
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp
new file mode 100644
index 00000000..ad8ffd62
--- /dev/null
+++ b/lib/Core/MergeHandler.cpp
@@ -0,0 +1,76 @@
+//===-- MergeHandler.cpp --------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/MergeHandler.h"
+
+#include "CoreStats.h"
+#include "Executor.h"
+#include "klee/ExecutionState.h"
+
+namespace klee {
+llvm::cl::opt<bool>
+    UseMerge("use-merge",
+        llvm::cl::init(false),
+        llvm::cl::desc("Enable support for klee_open_merge() and klee_close_merge() (experimental)"));
+
+llvm::cl::opt<bool>
+    DebugLogMerge("debug-log-merge",
+        llvm::cl::init(false),
+        llvm::cl::desc("Enhanced verbosity for region based merge operations"));
+
+void MergeHandler::addClosedState(ExecutionState *es,
+                                         llvm::Instruction *mp) {
+  auto closePoint = reachedMergeClose.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);
+    executor->pauseState(*es);
+  } else {
+    // Otherwise try to merge with any state in the map element for this
+    // instruction
+    auto &cpv = closePoint->second;
+    bool mergedSuccessful = false;
+
+    for (auto& mState: cpv) {
+      if (mState->merge(*es)) {
+        executor->terminateState(*es);
+        mergedSuccessful = true;
+        break;
+      }
+    }
+    if (!mergedSuccessful) {
+      cpv.push_back(es);
+      executor->pauseState(*es);
+    }
+  }
+}
+
+void MergeHandler::releaseStates() {
+  for (auto& curMergeGroup: reachedMergeClose) {
+    for (auto curState: curMergeGroup.second) {
+      executor->continueState(*curState);
+    }
+  }
+  reachedMergeClose.clear();
+}
+
+bool MergeHandler::hasMergedStates() {
+  return (!reachedMergeClose.empty());
+}
+
+MergeHandler::MergeHandler(Executor *_executor)
+    : executor(_executor), refCount(0) {
+}
+
+MergeHandler::~MergeHandler() {
+  releaseStates();
+}
+}
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index d5d35e8f..05ebe6a6 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -42,11 +42,6 @@
 using namespace klee;
 using namespace llvm;
 
-namespace {
-  cl::opt<bool>
-  DebugLogMerge("debug-log-merge");
-}
-
 namespace klee {
   extern RNG theRNG;
 }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 1c2b245c..a8d6edec 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -10,6 +10,7 @@
 #include "Memory.h"
 #include "SpecialFunctionHandler.h"
 #include "TimingSolver.h"
+#include "klee/MergeHandler.h"
 
 #include "klee/ExecutionState.h"
 
@@ -28,6 +29,7 @@
 #include "llvm/IR/DataLayout.h"
 
 #include <errno.h>
+#include <sstream>
 
 using namespace llvm;
 using namespace klee;
@@ -92,6 +94,8 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_is_symbolic", handleIsSymbolic, true),
   add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
+  add("klee_open_merge", handleOpenMerge, false),
+  add("klee_close_merge", handleCloseMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
   add("klee_posix_prefer_cex", handlePosixPreferCex, false),
   add("klee_print_expr", handlePrintExpr, false),
@@ -324,6 +328,43 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
 				 readStringAtAddress(state, arguments[3]).c_str());
 }
 
+void SpecialFunctionHandler::handleOpenMerge(ExecutionState &state,
+    KInstruction *target,
+    std::vector<ref<Expr> > &arguments) {
+  if (!UseMerge) {
+    klee_warning_once(0, "klee_open_merge ignored, use '-use-merge'");
+    return;
+  }
+
+  state.openMergeStack.push_back(
+      ref<MergeHandler>(new MergeHandler(&executor)));
+
+  if (DebugLogMerge)
+    llvm::errs() << "open merge: " << &state << "\n";
+}
+
+void SpecialFunctionHandler::handleCloseMerge(ExecutionState &state,
+    KInstruction *target,
+    std::vector<ref<Expr> > &arguments) {
+  if (!UseMerge) {
+    klee_warning_once(0, "klee_close_merge ignored, use '-use-merge'");
+    return;
+  }
+  Instruction *i = target->inst;
+
+  if (DebugLogMerge)
+    llvm::errs() << "close merge: " << &state << " at " << i << '\n';
+
+  if (state.openMergeStack.empty()) {
+    std::ostringstream warning;
+    warning << &state << " ran into a close at " << i << " without a preceding open\n";
+    klee_warning(warning.str().c_str());
+  } else {
+    state.openMergeStack.back()->addClosedState(&state, i);
+    state.openMergeStack.pop_back();
+  }
+}
+
 void SpecialFunctionHandler::handleNew(ExecutionState &state,
                          KInstruction *target,
                          std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 394b649a..7e58018f 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -116,6 +116,8 @@ namespace klee {
     HANDLER(handleMakeSymbolic);
     HANDLER(handleMalloc);
     HANDLER(handleMarkGlobal);
+    HANDLER(handleOpenMerge);
+    HANDLER(handleCloseMerge);
     HANDLER(handleNew);
     HANDLER(handleNewArray);
     HANDLER(handlePreferCex);
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 6158f722..f0b2f85a 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -13,6 +13,8 @@
 #include "Executor.h"
 
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/CommandLine.h"
+
 #include "llvm/Support/CommandLine.h"
 
 using namespace llvm;
@@ -58,8 +60,13 @@ namespace {
 void klee::initializeSearchOptions() {
   // default values
   if (CoreSearch.empty()) {
-    CoreSearch.push_back(Searcher::RandomPath);
-    CoreSearch.push_back(Searcher::NURS_CovNew);
+    if (UseMerge){
+      CoreSearch.push_back(Searcher::NURS_CovNew);
+      klee_warning("--use-merge enabled. Using NURS_CovNew as default searcher.");
+    } else {
+      CoreSearch.push_back(Searcher::RandomPath);
+      CoreSearch.push_back(Searcher::NURS_CovNew);
+    }
   }
 }
 
@@ -104,6 +111,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
     searcher = new InterleavedSearcher(s);
   }
 
+  if (UseMerge) {
+    if (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end()){
+      klee_error("use-merge currently does not support random-path, please use another search strategy");
+    }
+  }
+
   if (UseBatchingSearch) {
     searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
   }
diff --git a/test/Merging/batching_break.c b/test/Merging/batching_break.c
new file mode 100644
index 00000000..67570734
--- /dev/null
+++ b/test/Merging/batching_break.c
@@ -0,0 +1,42 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s
+
+// CHECK: open merge:
+// CHECK: close merge:
+// CHECK: KLEE: done: generated tests = 3{{$}}
+
+#include <klee/klee.h>
+
+int main(int argc, char** args){
+
+  int x;
+  int p;
+  int i;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  x = x % 20;
+
+  klee_open_merge();
+  for (i = 0; i < x; ++i){
+    if (x % 3 == 0){
+      klee_close_merge();
+      if (x > 10){
+        return 1;
+      } else {
+        return 2;
+      }
+    }
+  }
+  klee_close_merge();
+
+  klee_open_merge();
+  if (x > 10){
+    p = 1;
+  } else {
+    p = 2;
+  }
+  klee_close_merge();
+  return p;
+
+}
diff --git a/test/Merging/easy_merge.c b/test/Merging/easy_merge.c
new file mode 100644
index 00000000..b9c634dc
--- /dev/null
+++ b/test/Merging/easy_merge.c
@@ -0,0 +1,44 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge %t.bc 2>&1 | FileCheck %s
+
+// CHECK: open merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: generated tests = 2{{$}}
+#include <klee/klee.h>
+
+int main(int argc, char** args){
+
+  int x;
+  int a;
+  int foo = 0;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  if (a == 0){
+    klee_open_merge();
+
+    if (x == 1) {
+      foo = 5;
+    } else if (x == 2) {
+      foo = 6;
+    } else {
+      foo = 7;
+    }
+
+    klee_close_merge();
+  }
+
+  return foo;
+}
diff --git a/test/Merging/indirect_value.c b/test/Merging/indirect_value.c
new file mode 100644
index 00000000..ffea14ec
--- /dev/null
+++ b/test/Merging/indirect_value.c
@@ -0,0 +1,32 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s
+
+// CHECK: generated tests = 2{{$}}
+#include <stdlib.h>
+#include <stdio.h>
+
+#include <klee/klee.h>
+
+int main(int argc, char** argv) {
+
+  int sym = klee_int("sym");
+  int* heap_int = calloc(1, sizeof(*heap_int));
+
+  klee_open_merge();
+
+  if(sym != 0) {
+    *heap_int = 1;
+  }
+
+  klee_close_merge();
+
+  klee_print_expr("*heap_int: ", *heap_int);
+  if(*heap_int != 0) {
+    printf("true\n");
+  } else {
+    printf("false\n");
+  }
+
+  return 0;
+}
diff --git a/test/Merging/loop_merge.c b/test/Merging/loop_merge.c
new file mode 100644
index 00000000..4a38d98f
--- /dev/null
+++ b/test/Merging/loop_merge.c
@@ -0,0 +1,38 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s
+
+// CHECK: open merge:
+// There will be 20 'close merge' statements. Only checking a few, the generated
+// test count will confirm that the merge was closed correctly
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: generated tests = 2{{$}}
+
+#include <klee/klee.h>
+
+int main(int argc, char** args){
+
+  int x;
+  int i;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  x = x % 20;
+
+  klee_open_merge();
+  for (i = 0; i < x; ++i){
+    if (x % 3 == 0){
+      klee_close_merge();
+      return 1;
+    }
+  }
+  klee_close_merge();
+
+  return 0;
+}
diff --git a/test/Merging/merge_fail.c b/test/Merging/merge_fail.c
new file mode 100644
index 00000000..5cd9f782
--- /dev/null
+++ b/test/Merging/merge_fail.c
@@ -0,0 +1,36 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s
+
+// CHECK: open merge:
+// CHECK: generated tests = 2{{$}}
+
+// This test will not merge because we cannot merge states when they allocated memory.
+
+#include <klee/klee.h>
+
+int main(int argc, char **args) {
+
+  int* arr = 0;
+  int a = 0;
+
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  klee_open_merge();
+  if (a == 0) {
+    arr = (int*) malloc(7 * sizeof(int));
+    arr[0] = 7;
+  } else {
+    arr = (int*) malloc(8 * sizeof(int));
+    arr[0] = 8;
+  }
+  klee_close_merge();
+  a = arr[0];
+  free(arr);
+
+  return a;
+}
diff --git a/test/Merging/nested_merge.c b/test/Merging/nested_merge.c
new file mode 100644
index 00000000..027c72d3
--- /dev/null
+++ b/test/Merging/nested_merge.c
@@ -0,0 +1,48 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s
+
+// CHECK: open merge:
+// 5 close merges
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: generated tests = 1{{$}}
+
+#include <klee/klee.h>
+
+int main(int argc, char **args) {
+
+  int x;
+  int a;
+  int foo = 0;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  klee_open_merge();
+  if (a == 0) {
+    klee_open_merge();
+
+    if (x == 1) {
+      foo = 5;
+    } else if (x == 2) {
+      foo = 6;
+    } else {
+      foo = 7;
+    }
+
+    klee_close_merge();
+  }
+  klee_close_merge();
+
+  return foo;
+}
diff --git a/test/Merging/split_merge.c b/test/Merging/split_merge.c
new file mode 100644
index 00000000..bca8a5a2
--- /dev/null
+++ b/test/Merging/split_merge.c
@@ -0,0 +1,41 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s
+
+
+// CHECK: open merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: close merge:
+// CHECK: generated tests = 2{{$}}
+
+#include <klee/klee.h>
+
+int main(int argc, char** args){
+
+  int x;
+  int foo = 0;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  klee_open_merge();
+
+  if (x == 1){
+    foo = 5;
+  } else if (x == 2){
+    klee_close_merge();
+    return 6;
+  } else {
+    foo = 7;
+  }
+
+  klee_close_merge();
+
+  return foo;
+}
diff --git a/test/Merging/unexpected_close.c b/test/Merging/unexpected_close.c
new file mode 100644
index 00000000..b4994de1
--- /dev/null
+++ b/test/Merging/unexpected_close.c
@@ -0,0 +1,35 @@
+// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s
+// RUN: rm -rf %t.klee-out
+// RUN: klee --output-dir=%t.klee-out --use-merge --search=nurs:covnew --max-time=2 %t.bc
+
+// CHECK: ran into a close at
+// CHECK: generated tests = 2{{$}}
+
+#include <klee/klee.h>
+
+int main(int argc, char **args) {
+
+  int x;
+  int a;
+  int foo = 0;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&a, sizeof(a), "a");
+
+  if (a == 0) {
+    klee_open_merge();
+
+    if (x == 1) {
+      foo = 5;
+    } else if (x == 2) {
+      foo = 6;
+    } else {
+      foo = 7;
+    }
+
+    klee_close_merge();
+  }
+  klee_close_merge();
+
+  return foo;
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index f1def38c..2b2fe3eb 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -718,6 +718,8 @@ static const char *modelledExternals[] = {
   "klee_is_symbolic",
   "klee_make_symbolic",
   "klee_mark_global",
+  "klee_open_merge",
+  "klee_close_merge",
   "klee_prefer_cex",
   "klee_posix_prefer_cex",
   "klee_print_expr",