From cfcc5f215bb1c1613c8f1af9ef104bf903a97e0d Mon Sep 17 00:00:00 2001
From: Aleksandr Misonizhnik <misonijnik@gmail.com>
Date: Mon, 18 Sep 2023 12:53:22 +0400
Subject: [PATCH] [fix] Make `isReachedTarget` consistent with
 `reportTruePositive`

---
 lib/Core/TargetManager.cpp            | 20 +++++++++++++++++---
 lib/Core/TargetedExecutionManager.cpp | 22 +++-------------------
 test/Industry/if2.c                   |  2 +-
 3 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp
index 58579130fb..8823bf3b72 100644
--- a/lib/Core/TargetManager.cpp
+++ b/lib/Core/TargetManager.cpp
@@ -270,9 +270,23 @@ bool TargetManager::isReachedTarget(const ExecutionState &state,
   }
 
   if (target->shouldFailOnThisTarget()) {
-    if (state.pc->parent == target->getBlock()) {
-      if (cast<ReproduceErrorTarget>(target)->isTheSameAsIn(state.prevPC) &&
-          cast<ReproduceErrorTarget>(target)->isThatError(state.error)) {
+    bool found = true;
+    auto possibleInstruction = state.prevPC;
+    int i = state.stack.size() - 1;
+
+    while (!cast<ReproduceErrorTarget>(target)->isTheSameAsIn(
+        possibleInstruction)) { // TODO: target->getBlock() ==
+                                // possibleInstruction should also be checked,
+                                // but more smartly
+      if (i <= 0) {
+        found = false;
+        break;
+      }
+      possibleInstruction = state.stack.callStack().at(i).caller;
+      i--;
+    }
+    if (found) {
+      if (cast<ReproduceErrorTarget>(target)->isThatError(state.error)) {
         result = Done;
       } else {
         result = Continue;
diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp
index 25357773ae..7799d5064b 100644
--- a/lib/Core/TargetedExecutionManager.cpp
+++ b/lib/Core/TargetedExecutionManager.cpp
@@ -530,6 +530,7 @@ void TargetedExecutionManager::reportFalseNegative(ExecutionState &state,
 bool TargetedExecutionManager::reportTruePositive(ExecutionState &state,
                                                   ReachWithError error) {
   bool atLeastOneReported = false;
+  state.error = error;
   for (auto target : state.targetForest.getTargets()) {
     if (!target->shouldFailOnThisTarget())
       continue;
@@ -539,27 +540,10 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state,
         reportedTraces.count(errorTarget->getId()))
       continue;
 
-    /// The following code checks if target is a `call ...` instruction and we
-    /// failed somewhere *inside* call
-    auto possibleInstruction = state.prevPC;
-    int i = state.stack.size() - 1;
-    bool found = true;
-
-    while (!errorTarget->isTheSameAsIn(
-        possibleInstruction)) { // TODO: target->getBlock() ==
-                                // possibleInstruction should also be checked,
-                                // but more smartly
-      if (i <= 0) {
-        found = false;
-        break;
-      }
-      possibleInstruction = state.stack.callStack().at(i).caller;
-      i--;
-    }
-    if (!found)
+    if (!targetManager.isReachedTarget(state, errorTarget)) {
       continue;
+    }
 
-    state.error = error;
     atLeastOneReported = true;
     assert(!errorTarget->isReported);
     if (errorTarget->isThatError(ReachWithError::Reachable)) {
diff --git a/test/Industry/if2.c b/test/Industry/if2.c
index 27f414ed01..d52edf529f 100644
--- a/test/Industry/if2.c
+++ b/test/Industry/if2.c
@@ -11,7 +11,7 @@ int main(int x) {
 // REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=19 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE
 // CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1
 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE