Removed merging searchers

10 files changed, 0 insertions, 358 deletions

diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h
index 41253383..e8ded725 100644
--- a/include/klee/Internal/Module/KModule.h
+++ b/include/klee/Internal/Module/KModule.h
@@ -82,9 +82,6 @@ namespace klee {
   public:
     llvm::Module *module;
     llvm::DataLayout *targetData;
-    
-    // Some useful functions to know the address of
-    llvm::Function *kleeMergeFn;
 
     // Our shadow versions of LLVM structures.
     std::vector<KFunction*> functions;
diff --git a/include/klee/klee.h b/include/klee/klee.h
index d0980395..bd3100b5 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -152,8 +152,6 @@ extern "C" {
   /* Print range for given argument and tagged with name */
   void klee_print_range(const char * name, int arg );
 
-  /* Merge current states together if possible */
-  void klee_merge();
 #ifdef __cplusplus
 }
 #endif
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 0e7aa685..b9f22538 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -301,217 +301,6 @@ bool RandomPathSearcher::empty() {
 
 ///
 
-BumpMergingSearcher::BumpMergingSearcher(Executor &_executor, Searcher *_baseSearcher) 
-  : executor(_executor),
-    baseSearcher(_baseSearcher),
-    mergeFunction(executor.kmodule->kleeMergeFn) {
-}
-
-BumpMergingSearcher::~BumpMergingSearcher() {
-  delete baseSearcher;
-}
-
-///
-
-Instruction *BumpMergingSearcher::getMergePoint(ExecutionState &es) {  
-  if (mergeFunction) {
-    Instruction *i = es.pc->inst;
-
-    if (i->getOpcode()==Instruction::Call) {
-      CallSite cs(cast<CallInst>(i));
-      if (mergeFunction==cs.getCalledFunction())
-        return i;
-    }
-  }
-
-  return 0;
-}
-
-ExecutionState &BumpMergingSearcher::selectState() {
-entry:
-  // out of base states, pick one to pop
-  if (baseSearcher->empty()) {
-    std::map<llvm::Instruction*, ExecutionState*>::iterator it = 
-      statesAtMerge.begin();
-    ExecutionState *es = it->second;
-    statesAtMerge.erase(it);
-    ++es->pc;
-
-    baseSearcher->addState(es);
-  }
-
-  ExecutionState &es = baseSearcher->selectState();
-
-  if (Instruction *mp = getMergePoint(es)) {
-    std::map<llvm::Instruction*, ExecutionState*>::iterator it = 
-      statesAtMerge.find(mp);
-
-    baseSearcher->removeState(&es);
-
-    if (it==statesAtMerge.end()) {
-      statesAtMerge.insert(std::make_pair(mp, &es));
-    } else {
-      ExecutionState *mergeWith = it->second;
-      if (mergeWith->merge(es)) {
-        // hack, because we are terminating the state we need to let
-        // the baseSearcher know about it again
-        baseSearcher->addState(&es);
-        executor.terminateState(es);
-      } else {
-        it->second = &es; // the bump
-        ++mergeWith->pc;
-
-        baseSearcher->addState(mergeWith);
-      }
-    }
-
-    goto entry;
-  } else {
-    return es;
-  }
-}
-
-void BumpMergingSearcher::update(
-    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
-    const std::vector<ExecutionState *> &removedStates) {
-  baseSearcher->update(current, addedStates, removedStates);
-}
-
-///
-
-MergingSearcher::MergingSearcher(Executor &_executor, Searcher *_baseSearcher) 
-  : executor(_executor),
-    baseSearcher(_baseSearcher),
-    mergeFunction(executor.kmodule->kleeMergeFn) {
-}
-
-MergingSearcher::~MergingSearcher() {
-  delete baseSearcher;
-}
-
-///
-
-Instruction *MergingSearcher::getMergePoint(ExecutionState &es) {
-  if (mergeFunction) {
-    Instruction *i = es.pc->inst;
-
-    if (i->getOpcode()==Instruction::Call) {
-      CallSite cs(cast<CallInst>(i));
-      if (mergeFunction==cs.getCalledFunction())
-        return i;
-    }
-  }
-
-  return 0;
-}
-
-ExecutionState &MergingSearcher::selectState() {
-  // FIXME: this loop is endless if baseSearcher includes RandomPathSearcher.
-  // The reason is that RandomPathSearcher::removeState() does nothing...
-  while (!baseSearcher->empty()) {
-    ExecutionState &es = baseSearcher->selectState();
-    if (getMergePoint(es)) {
-      baseSearcher->removeState(&es, &es);
-      statesAtMerge.insert(&es);
-    } else {
-      return es;
-    }
-  }
-  
-  // build map of merge point -> state list
-  std::map<Instruction*, std::vector<ExecutionState*> > merges;
-  for (std::set<ExecutionState*>::const_iterator it = statesAtMerge.begin(),
-         ie = statesAtMerge.end(); it != ie; ++it) {
-    ExecutionState &state = **it;
-    Instruction *mp = getMergePoint(state);
-    
-    merges[mp].push_back(&state);
-  }
-  
-  if (DebugLogMerge)
-    llvm::errs() << "-- all at merge --\n";
-  for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator
-         it = merges.begin(), ie = merges.end(); it != ie; ++it) {
-    if (DebugLogMerge) {
-      llvm::errs() << "\tmerge: " << it->first << " [";
-      for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(),
-             ie2 = it->second.end(); it2 != ie2; ++it2) {
-        ExecutionState *state = *it2;
-        llvm::errs() << state << ", ";
-      }
-      llvm::errs() << "]\n";
-    }
-
-    // merge states
-    std::set<ExecutionState*> toMerge(it->second.begin(), it->second.end());
-    while (!toMerge.empty()) {
-      ExecutionState *base = *toMerge.begin();
-      toMerge.erase(toMerge.begin());
-      
-      std::set<ExecutionState*> toErase;
-      for (std::set<ExecutionState*>::iterator it = toMerge.begin(),
-             ie = toMerge.end(); it != ie; ++it) {
-        ExecutionState *mergeWith = *it;
-        
-        if (base->merge(*mergeWith)) {
-          toErase.insert(mergeWith);
-        }
-      }
-      if (DebugLogMerge && !toErase.empty()) {
-        llvm::errs() << "\t\tmerged: " << base << " with [";
-        for (std::set<ExecutionState*>::iterator it = toErase.begin(),
-               ie = toErase.end(); it != ie; ++it) {
-          if (it!=toErase.begin()) llvm::errs() << ", ";
-          llvm::errs() << *it;
-        }
-        llvm::errs() << "]\n";
-      }
-      for (std::set<ExecutionState*>::iterator it = toErase.begin(),
-             ie = toErase.end(); it != ie; ++it) {
-        std::set<ExecutionState*>::iterator it2 = toMerge.find(*it);
-        assert(it2!=toMerge.end());
-        executor.terminateState(**it);
-        toMerge.erase(it2);
-      }
-
-      // step past merge and toss base back in pool
-      statesAtMerge.erase(statesAtMerge.find(base));
-      ++base->pc;
-      baseSearcher->addState(base);
-    }  
-  }
-  
-  if (DebugLogMerge)
-    llvm::errs() << "-- merge complete, continuing --\n";
-  
-  return selectState();
-}
-
-void
-MergingSearcher::update(ExecutionState *current,
-                        const std::vector<ExecutionState *> &addedStates,
-                        const std::vector<ExecutionState *> &removedStates) {
-  if (!removedStates.empty()) {
-    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(std::remove(alt.begin(), alt.end(), es), alt.end());
-      }
-    }    
-    baseSearcher->update(current, addedStates, alt);
-  } else {
-    baseSearcher->update(current, addedStates, removedStates);
-  }
-}
-
-///
-
 BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
                                    double _timeBudget,
                                    unsigned _instructionBudget) 
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 4ede3640..27c8aed1 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -180,52 +180,6 @@ namespace klee {
     }
   };
 
-  class MergingSearcher : public Searcher {
-    Executor &executor;
-    std::set<ExecutionState*> statesAtMerge;
-    Searcher *baseSearcher;
-    llvm::Function *mergeFunction;
-
-  private:
-    llvm::Instruction *getMergePoint(ExecutionState &es);
-
-  public:
-    MergingSearcher(Executor &executor, Searcher *baseSearcher);
-    ~MergingSearcher();
-
-    ExecutionState &selectState();
-    void update(ExecutionState *current,
-                const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
-    void printName(llvm::raw_ostream &os) {
-      os << "MergingSearcher\n";
-    }
-  };
-
-  class BumpMergingSearcher : public Searcher {
-    Executor &executor;
-    std::map<llvm::Instruction*, ExecutionState*> statesAtMerge;
-    Searcher *baseSearcher;
-    llvm::Function *mergeFunction;
-
-  private:
-    llvm::Instruction *getMergePoint(ExecutionState &es);
-
-  public:
-    BumpMergingSearcher(Executor &executor, Searcher *baseSearcher);
-    ~BumpMergingSearcher();
-
-    ExecutionState &selectState();
-    void update(ExecutionState *current,
-                const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
-    void printName(llvm::raw_ostream &os) {
-      os << "BumpMergingSearcher\n";
-    }
-  };
-
   class BatchingSearcher : public Searcher {
     Searcher *baseSearcher;
     double timeBudget;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index aaa26922..74d36f27 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -93,7 +93,6 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_is_symbolic", handleIsSymbolic, true),
   add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
-  add("klee_merge", handleMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
   add("klee_posix_prefer_cex", handlePosixPreferCex, false),
   add("klee_print_expr", handlePrintExpr, false),
@@ -325,12 +324,6 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
 				 readStringAtAddress(state, arguments[3]).c_str());
 }
 
-void SpecialFunctionHandler::handleMerge(ExecutionState &state,
-                           KInstruction *target,
-                           std::vector<ref<Expr> > &arguments) {
-  // nop
-}
-
 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 2dfdde43..394b649a 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -116,7 +116,6 @@ namespace klee {
     HANDLER(handleMakeSymbolic);
     HANDLER(handleMalloc);
     HANDLER(handleMarkGlobal);
-    HANDLER(handleMerge);
     HANDLER(handleNew);
     HANDLER(handleNewArray);
     HANDLER(handlePreferCex);
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 2bbbe747..4275f3a5 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -52,15 +52,6 @@ namespace {
             cl::desc("Amount of time to batch when using --use-batching-search"),
             cl::init(5.0));
 
-
-  cl::opt<bool>
-  UseMerge("use-merge", 
-           cl::desc("Enable support for klee_merge() (experimental)"));
- 
-  cl::opt<bool>
-  UseBumpMerge("use-bump-merge", 
-           cl::desc("Enable support for klee_merge() (extra experimental)"));
-
 }
 
 
@@ -115,19 +106,6 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
     searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
   }
 
-  // merge support is experimental
-  if (UseMerge) {
-    if (UseBumpMerge)
-      klee_error("use-merge and use-bump-merge cannot be used together");
-    // RandomPathSearcher cannot be used in conjunction with MergingSearcher,
-    // see MergingSearcher::selectState() for explanation.
-    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");
-    searcher = new MergingSearcher(executor, searcher);
-  } else if (UseBumpMerge) {
-    searcher = new BumpMergingSearcher(executor, searcher);
-  }
-  
   if (UseIterativeDeepeningTimeSearch) {
     searcher = new IterativeDeepeningTimeSearcher(searcher);
   }
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 751776b9..bb34dcad 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -54,9 +54,6 @@ namespace {
     eSwitchTypeLLVM,
     eSwitchTypeInternal
   };
-
-  cl::list<std::string>
-  MergeAtExit("merge-at-exit");
     
   cl::opt<bool>
   NoTruncateSourceLines("no-truncate-source-lines",
@@ -91,7 +88,6 @@ namespace {
 KModule::KModule(Module *_module) 
   : module(_module),
     targetData(new DataLayout(module)),
-    kleeMergeFn(0),
     infos(0),
     constantTable(0) {
 }
@@ -206,53 +202,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
                       InterpreterHandler *ih) {
   LLVMContext &ctx = module->getContext();
 
-  if (!MergeAtExit.empty()) {
-    Function *mergeFn = module->getFunction("klee_merge");
-    if (!mergeFn) {
-      llvm::FunctionType *Ty =
-          FunctionType::get(Type::getVoidTy(ctx), std::vector<Type *>(), false);
-      mergeFn = Function::Create(Ty, GlobalVariable::ExternalLinkage,
-				 "klee_merge",
-				 module);
-    }
-
-    for (cl::list<std::string>::iterator it = MergeAtExit.begin(), 
-           ie = MergeAtExit.end(); it != ie; ++it) {
-      std::string &name = *it;
-      Function *f = module->getFunction(name);
-      if (!f) {
-        klee_error("cannot insert merge-at-exit for: %s (cannot find)",
-                   name.c_str());
-      } else if (f->isDeclaration()) {
-        klee_error("cannot insert merge-at-exit for: %s (external)",
-                   name.c_str());
-      }
-
-      BasicBlock *exit = BasicBlock::Create(ctx, "exit", f);
-      PHINode *result = 0;
-      if (f->getReturnType() != Type::getVoidTy(ctx))
-        result = PHINode::Create(f->getReturnType(), 0, "retval", exit);
-      CallInst::Create(mergeFn, "", exit);
-      ReturnInst::Create(ctx, result, exit);
-
-      llvm::errs() << "KLEE: adding klee_merge at exit of: " << name << "\n";
-      for (llvm::Function::iterator bbit = f->begin(), bbie = f->end(); 
-           bbit != bbie; ++bbit) {
-	BasicBlock *bb = &*bbit;
-        if (bb != exit) {
-          Instruction *i = bbit->getTerminator();
-          if (i->getOpcode()==Instruction::Ret) {
-            if (result) {
-              result->addIncoming(i->getOperand(0), bb);
-            }
-            i->eraseFromParent();
-	    BranchInst::Create(exit, bb);
-          }
-        }
-      }
-    }
-  }
-
   // Inject checks prior to optimization... we also perform the
   // invariant transformations that we will end up doing later so that
   // optimize is seeing what is as close as possible to the final
@@ -373,8 +322,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     delete f;
   }
 
-  kleeMergeFn = module->getFunction("klee_merge");
-
   /* Build shadow structures */
 
   infos = new InstructionInfoTable(module);  
diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
index 284020eb..9e0bc722 100644
--- a/test/Feature/Searchers.c
+++ b/test/Feature/Searchers.c
@@ -18,16 +18,6 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --search=random-path --search=nurs:qc %t2.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-merge --search=dfs --debug-log-merge --debug-log-state-merge %t2.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=dfs %t2.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=random-state %t2.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=nurs:depth %t2.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-merge --use-batching-search --search=nurs:qc %t2.bc
-// RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search %t2.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc
@@ -49,12 +39,10 @@ int validate(char *buf, int N) {
 
   for (i=0; i<N; i++) {
     if (buf[i]==0) {
-      klee_merge();
       return 0;
     }
   }
   
-  klee_merge();
   return 1;
 }
 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 26ec6c7f..05ba54d3 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -718,7 +718,6 @@ static const char *modelledExternals[] = {
   "klee_is_symbolic",
   "klee_make_symbolic",
   "klee_mark_global",
-  "klee_merge",
   "klee_prefer_cex",
   "klee_posix_prefer_cex",
   "klee_print_expr",