Implemented incomplete merging

2 files changed, 42 insertions, 1 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 6aec61ea..ceb07864 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -149,6 +149,9 @@ public:
   // The objects handling the klee_open_merge calls this state ran through
   std::vector<ref<MergeHandler> > openMergeStack;
 
+  // The numbers of times this state has run through Executor::stepInstruction
+  std::uint64_t steppedInstructions;
+
 private:
   ExecutionState() : ptreeNode(0) {}
 
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h
index 0c596825..79357d7c 100644
--- a/include/klee/MergeHandler.h
+++ b/include/klee/MergeHandler.h
@@ -67,6 +67,10 @@ extern llvm::cl::opt<bool> UseMerge;
 
 extern llvm::cl::opt<bool> DebugLogMerge;
 
+extern llvm::cl::opt<bool> UseIncompleteMerge;
+
+extern llvm::cl::opt<bool> DebugLogIncompleteMerge;
+
 class Executor;
 class ExecutionState;
 
@@ -76,6 +80,24 @@ class MergeHandler {
 private:
   Executor *executor;
 
+  /// @brief The instruction count when the state ran into the klee_open_merge
+  uint64_t openInstruction;
+
+  /// @brief The average number of instructions between the open and close merge of each
+  /// state that has finished so far
+  double closeMean;
+
+  /// @brief Number of states that are tracked by this MergeHandler, that ran
+  /// into a relevant klee_close_merge
+  unsigned closedStateCount;
+
+  /// @brief Get distance of state from the openInstruction
+  unsigned getInstrDistance(ExecutionState *es);
+
+  /// @brief States that ran through the klee_open_merge, but not yet into a
+  /// corresponding klee_close_merge
+  std::vector<ExecutionState *> openStates;
+
   /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into
   /// them
   std::map<llvm::Instruction *, std::vector<ExecutionState *> >
@@ -86,6 +108,18 @@ public:
   /// @brief Called when a state runs into a 'klee_close_merge()' call
   void addClosedState(ExecutionState *es, llvm::Instruction *mp);
 
+  /// @brief Return state that should be prioritized to complete this merge
+  ExecutionState *getPrioritizeState();
+
+  /// @brief Add state to the 'openStates' vector
+  void addOpenState(ExecutionState *es);
+
+  /// @brief Remove state from the 'openStates' vector
+  void removeOpenState(ExecutionState *es);
+
+  /// @brief Remove state from the 'inCloseMerge' set in the executor
+  void removeFromCloseMergeSet(ExecutionState *es);
+
   /// @brief True, if any states have run into 'klee_close_merge()' and have
   /// not been released yet
   bool hasMergedStates();
@@ -94,11 +128,15 @@ public:
   /// 'klee_merge_close()'
   void releaseStates();
 
+  // Return the mean time it takes for a state to get from klee_open_merge to
+  // klee_close_merge
+  double getMean();
+
   /// @brief Required by klee::ref objects
   unsigned refCount;
 
 
-  MergeHandler(Executor *_executor);
+  MergeHandler(Executor *_executor, ExecutionState *es);
   ~MergeHandler();
 };
 }