about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
authorLukas Wölfer <lukas.woelfer@rwth-aachen.de>2017-06-24 19:59:48 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2017-11-30 12:18:15 +0000
commit60b5c574ea565b3132cc60d946d87a4d1243801b (patch)
treec7b781fe9aa8c1fdf5b4753ddaa2c694d8878b99 /lib/Core
parentbc84fb1f642cbd15064c86d3839e278be536b254 (diff)
downloadklee-60b5c574ea565b3132cc60d946d87a4d1243801b.tar.gz
Implemented bounded merging functionality
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/CMakeLists.txt1
-rw-r--r--lib/Core/ExecutionState.cpp3
-rw-r--r--lib/Core/Executor.cpp7
-rw-r--r--lib/Core/Executor.h4
-rw-r--r--lib/Core/MergeHandler.cpp76
-rw-r--r--lib/Core/Searcher.cpp5
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp41
-rw-r--r--lib/Core/SpecialFunctionHandler.h2
-rw-r--r--lib/Core/UserSearcher.cpp17
9 files changed, 142 insertions, 14 deletions
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);
   }