about summary refs log tree commit diff homepage
path: root/lib/Core/MergeHandler.cpp
diff options
context:
space:
mode:
authorLukas Wölfer <lukas.woelfer@rwth-aachen.de>2017-06-24 19:31:04 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-05-15 15:18:36 +0100
commite5a18f47a8cdd37a5c2721e89df68ea7aafed8a0 (patch)
tree620bd0ab0ce7f737db5ab7f8f656d32ea0849f4a /lib/Core/MergeHandler.cpp
parent0cf0150da0f674c85f9eaccee8b487ed004c3edc (diff)
downloadklee-e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0.tar.gz
Implemented incomplete merging
Diffstat (limited to 'lib/Core/MergeHandler.cpp')
-rw-r--r--lib/Core/MergeHandler.cpp69
1 files changed, 67 insertions, 2 deletions
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp
index ad8ffd62..45373002 100644
--- a/lib/Core/MergeHandler.cpp
+++ b/lib/Core/MergeHandler.cpp
@@ -24,8 +24,65 @@ llvm::cl::opt<bool>
         llvm::cl::init(false),
         llvm::cl::desc("Enhanced verbosity for region based merge operations"));
 
+llvm::cl::opt<bool>
+    UseIncompleteMerge("use-incomplete-merge",
+        llvm::cl::init(false),
+        llvm::cl::desc("Heuristic based merging"));
+
+llvm::cl::opt<bool>
+    DebugLogIncompleteMerge("debug-log-incomplete-merge",
+        llvm::cl::init(false),
+        llvm::cl::desc("Debug info about incomplete merging"));
+
+double MergeHandler::getMean() {
+  if (closedStateCount == 0)
+    return 0;
+
+  return closeMean;
+}
+
+unsigned MergeHandler::getInstrDistance(ExecutionState *es){
+  return es->steppedInstructions - openInstruction;
+}
+
+ExecutionState *MergeHandler::getPrioritizeState(){
+  for (ExecutionState *cur_state : openStates) {
+    bool stateIsClosed = (executor->inCloseMerge.find(cur_state) !=
+                          executor->inCloseMerge.end());
+
+    if (!stateIsClosed && (getInstrDistance(cur_state) < 2 * getMean())) {
+      return cur_state;
+    }
+  }
+  return 0;
+}
+
+
+void MergeHandler::addOpenState(ExecutionState *es){
+  openStates.push_back(es);
+}
+
+void MergeHandler::removeOpenState(ExecutionState *es){
+  auto it = std::find(openStates.begin(), openStates.end(), es);
+  assert(it != openStates.end());
+  std::swap(*it, openStates.back());
+  openStates.pop_back();
+}
+
+void MergeHandler::removeFromCloseMergeSet(ExecutionState *es){
+  executor->inCloseMerge.erase(es);
+}
+
 void MergeHandler::addClosedState(ExecutionState *es,
                                          llvm::Instruction *mp) {
+  // Update stats
+  ++closedStateCount;
+  closeMean += (static_cast<double>(getInstrDistance(es)) - closeMean) /
+               closedStateCount;
+
+  // Remove from openStates
+  removeOpenState(es);
+
   auto closePoint = reachedMergeClose.find(mp);
 
   // If no other state has yet encountered this klee_close_merge instruction,
@@ -66,11 +123,19 @@ bool MergeHandler::hasMergedStates() {
   return (!reachedMergeClose.empty());
 }
 
-MergeHandler::MergeHandler(Executor *_executor)
-    : executor(_executor), refCount(0) {
+MergeHandler::MergeHandler(Executor *_executor, ExecutionState *es)
+    : executor(_executor), openInstruction(es->steppedInstructions),
+      closedStateCount(0), refCount(0) {
+  executor->mergeGroups.push_back(this);
+  addOpenState(es);
 }
 
 MergeHandler::~MergeHandler() {
+  auto it = std::find(executor->mergeGroups.begin(),
+                      executor->mergeGroups.end(), this);
+  std::swap(*it, executor->mergeGroups.back());
+  executor->mergeGroups.pop_back();
+
   releaseStates();
 }
 }