[feat] Output number of reached events instead of confidence rate

lib/Core/TargetForest.cpp

@@ -280,6 +280,7 @@ void TargetForest::stepTo(ref<Target> loc) {
   } else {
     history = history->add(loc);
     forest = forest->replaceChildWith(loc, res->second.get());
+    loc->isReported = true;
   }
   if (forest->empty() && !loc->shouldFailOnThisTarget()) {
     history = History::create();
@@ -407,3 +408,19 @@ TargetForest::Layer *TargetForest::Layer::divideConfidenceBy(std::multiset<ref<T
   }
   return result;
 }
+
+void TargetForest::Layer::collectHowManyEventsInTracesWereReached(
+  std::unordered_map<unsigned, std::pair<unsigned, unsigned>> &trace2eventCount,
+  unsigned reached,
+  unsigned total) const {
+  total++;
+  for (const auto &p : forest) {
+    auto target = p.first;
+    auto child = p.second;
+    auto reachedCurrent = target->isReported ? reached + 1 : reached;
+    if (target->shouldFailOnThisTarget()) {
+      trace2eventCount[target->getId()] = std::make_pair(reachedCurrent, total);
+    }
+    child->collectHowManyEventsInTracesWereReached(trace2eventCount, reachedCurrent, total);
+  }
+}

lib/Core/TargetForest.h

@@ -56,6 +56,11 @@ class TargetForest {
       std::unordered_map<LocatedEvent *, TargetsSet *> &loc2Targets,
       std::unordered_set<unsigned> &broken_traces);
 
+    void collectHowManyEventsInTracesWereReached(
+      std::unordered_map<unsigned, std::pair<unsigned, unsigned>> &trace2eventCount,
+      unsigned reached,
+      unsigned total) const;
+
   public:
     using iterator = InternalLayer::const_iterator;
 
@@ -90,6 +95,9 @@ class TargetForest {
     void divideConfidenceBy(unsigned factor);
     Layer *divideConfidenceBy(std::multiset<ref<Target> > &reachableStatesOfTarget);
     confidence_ty getConfidence() const { return getConfidence(MAX_CONFIDENCE); }
+    void collectHowManyEventsInTracesWereReached(std::unordered_map<unsigned, std::pair<unsigned, unsigned>> &trace2eventCount) const {
+      collectHowManyEventsInTracesWereReached(trace2eventCount, 0, 0);
+    }
   };
 
   ref<Layer> forest;
@@ -187,6 +195,9 @@ class TargetForest {
   void divideConfidenceBy(std::multiset<ref<Target> > &reachableStatesOfTarget) {
     forest = forest->divideConfidenceBy(reachableStatesOfTarget);
   }
+  void collectHowManyEventsInTracesWereReached(std::unordered_map<unsigned, std::pair<unsigned, unsigned>> &trace2eventCount) const {
+    forest->collectHowManyEventsInTracesWereReached(trace2eventCount);
+  }
 };
 
 struct TargetsHistoryHash {

lib/Core/TargetedExecutionManager.cpp

@@ -255,6 +255,8 @@ TargetedExecutionManager::prepareTargets(KModule *origModule, KModule *kmodule,
 void TargetedExecutionManager::reportFalsePositives(ref<TargetForest> &targets, bool canReachSomeTarget) {
   if (targets.isNull())
     return;
+  std::unordered_map<unsigned, std::pair<unsigned, unsigned>> trace2eventCount;
+  targets->collectHowManyEventsInTracesWereReached(trace2eventCount);
   auto leafs = targets->leafs();
   for (const auto &targetWithConfidence : *leafs) {
     auto target = targetWithConfidence.first;
@@ -263,18 +265,23 @@ void TargetedExecutionManager::reportFalsePositives(ref<TargetForest> &targets,
       continue;
     if (target->isReported)
       continue;
-    if (canReachSomeTarget && confidence > 99.0) // We should not be so sure if there are states that can reach some targets
-      confidence = 99.00;
-    klee_warning("%.2f%% %s False Positive at trace %u", confidence,
-                 ReachWithErrorNames[target->getError()], target->getId());
+    if (canReachSomeTarget) {
+      if (confidence > 99.0) // We should not be so sure if there are states that can reach some targets
+        confidence = 99.00;
+      auto eventCount = trace2eventCount[target->getId()];
+      klee_warning("Time limit; reached only %u out of %u events at trace %u", eventCount.first, eventCount.second, target->getId());
+    } else {
+      klee_warning("%s False Positive at trace %u",
+                   ReachWithErrorNames[target->getError()], target->getId());
+    }
     target->isReported = true;
   }
   delete leafs;
 }
 
 void TargetedExecutionManager::reportFalseNegative(ExecutionState &state,
                                                    ReachWithError error) {
-  klee_warning("100.00%% %s False Negative at: %s", ReachWithErrorNames[error],
+  klee_warning("%s False Negative at: %s", ReachWithErrorNames[error],
                state.prevPC->getSourceLocation().c_str());
 }
 
@@ -306,9 +313,9 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, ReachWi
     atLeastOneReported = true;
     assert(!target->isReported);
     if (target->getError() == ReachWithError::Reachable) {
-      klee_warning("100.00%% %s Reachable at trace %u", ReachWithErrorNames[target->getError()], target->getId());
+      klee_warning("%s Reachable at trace %u", ReachWithErrorNames[target->getError()], target->getId());
     } else {
-      klee_warning("100.00%% %s True Positive at trace %u", ReachWithErrorNames[target->getError()], target->getId());
+      klee_warning("%s True Positive at trace %u", ReachWithErrorNames[target->getError()], target->getId());
     }
     target->isReported = true;
   }

lib/Runner/run_klee.cpp

@@ -1328,7 +1328,6 @@ static Interpreter *theInterpreter = 0;
 static PathForest *pathTree = 0;
 
 static std::atomic_bool interrupted{false};
-static std::atomic_bool reported{false};
 
 // Pulled out so it can be easily called from a debugger.
 extern "C"
@@ -1358,7 +1357,7 @@ static void interrupt_handle() {
           auto nextTree = p.second;
           if (nextTree->empty()) {
             if (event->error != ReachWithError::None) {
-              klee_warning("0.00%% False Positive at trace %u", event->id);
+              klee_warning("Time limit; not started investigating at trace %u", event->id);
             }
           } else {
             q.push_back(nextTree);