Removed merging searchers

5 files changed, 0 insertions, 287 deletions

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);
   }