Receive instrumented revision number

3 files changed, 19 insertions, 0 deletions

diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 0e28e04f..74c33a4c 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -226,6 +226,9 @@ public:
   /// @brief The objects handling the klee_open_merge calls this state ran through
   std::vector<ref<MergeHandler>> openMergeStack;
 
+  /// @ brief The patch number, starting from 1; 0 being the original.
+  std::uint64_t patchNo = 0;
+
   /// @brief The numbers of times this state has run through Executor::stepInstruction
   std::uint64_t steppedInstructions = 0;
 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index b0c28fbc..784bb8f1 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -109,6 +109,7 @@ static constexpr std::array handlerInfo = {
   add("klee_is_symbolic", handleIsSymbolic, true),
   add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
+  add("klee_mark_patch", handleMarkPatch, false),
   add("klee_open_merge", handleOpenMerge, false),
   add("klee_close_merge", handleCloseMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
@@ -840,3 +841,17 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
     mo->isGlobal = true;
   }
 }
+
+void SpecialFunctionHandler::handleMarkPatch(ExecutionState &state,
+                                             KInstruction *target,
+                                             std::vector<ref<Expr>> &arguments) {
+  assert(arguments.size() == 1 &&
+         "invalid number of arguments to klee_mark_patch");
+  assert(isa<ConstantExpr>(arguments[0]) &&
+         "expect constant patch number argument to klee_mark_patch");
+  if (state.patchNo)
+    executor.terminateStateEarly(state, "ignore patch combination",
+                                 StateTerminationType::SilentExit);
+  else
+    state.patchNo = cast<ConstantExpr>(arguments[0])->getLimitedValue();
+}
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 3fdbf8f8..be0bc7d2 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -101,6 +101,7 @@ namespace klee {
     HANDLER(handleMalloc);
     HANDLER(handleMemalign);
     HANDLER(handleMarkGlobal);
+    HANDLER(handleMarkPatch);
     HANDLER(handleOpenMerge);
     HANDLER(handleCloseMerge);
     HANDLER(handleNew);