Receive instrumented revision number

6 files changed, 25 insertions, 0 deletions

diff --git a/include/klee/klee.h b/include/klee/klee.h
index 07528595..04cb75c8 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -118,6 +118,7 @@ extern "C" {
   void klee_prefer_cex(void *object, uintptr_t condition);
   void klee_posix_prefer_cex(void *object, uintptr_t condition);
   void klee_mark_global(void *object);
+  void klee_mark_patch(uint64_t patch_number);
 
   /* Return a possible constant value for the input expression. This
      allows programs to forcibly concretize values on their own. */
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);
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 82c638c2..58379e38 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -514,6 +514,10 @@ void klee_mark_global(void *object) {
   ;
 }
 
+void klee_mark_patch(uint64_t patch_number) {
+  ;
+}
+
 /*** HELPER FUNCTIONS ***/
 
 static void __emit_error(const char *msg) {
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 18e67fe6..3c6c81ca 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -771,6 +771,7 @@ static const char *modelledExternals[] = {
   "klee_is_symbolic",
   "klee_make_symbolic",
   "klee_mark_global",
+  "klee_mark_patch",
   "klee_open_merge",
   "klee_close_merge",
   "klee_prefer_cex",