Target progress report

include/klee/Module/TargetHash.h

@@ -14,6 +14,7 @@
 
 #include <map>
 #include <unordered_map>
+#include <unordered_set>
 
 namespace llvm {
 class BasicBlock;
@@ -54,5 +55,12 @@ struct RefTargetLess {
   }
 };
 
+template <class T>
+class TargetHashMap
+    : public std::unordered_map<ref<Target>, T, RefTargetHash, RefTargetCmp> {};
+
+class TargetHashSet
+    : public std::unordered_set<ref<Target>, RefTargetHash, RefTargetCmp> {};
+
 } // namespace klee
 #endif /* KLEE_TARGETHASH_H */

lib/Core/DistanceCalculator.cpp

@@ -13,9 +13,26 @@
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/Target.h"
 
+#include <limits>
+
 using namespace llvm;
 using namespace klee;
 
+bool DistanceResult::operator<(const DistanceResult &b) const {
+  if (isInsideFunction != b.isInsideFunction)
+    return isInsideFunction;
+  if (result == WeightResult::Continue && b.result == WeightResult::Continue)
+    return weight < b.weight;
+  return result < b.result;
+}
+
+std::string DistanceResult::toString() const {
+  std::ostringstream out;
+  out << "(" << (int)!isInsideFunction << ", " << (int)result << ", " << weight
+      << ")";
+  return out.str();
+}
+
 DistanceResult DistanceCalculator::getDistance(ExecutionState &es,
                                                ref<Target> target) {
   return getDistance(es.pc, es.prevPC, es.initPC, es.stack, es.error, target);
@@ -55,14 +72,7 @@ DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC,
     if (distanceInCallGraph(sfi->kf, kb, callWeight, distanceToTargetFunction,
                             target)) {
       callWeight *= 2;
-      if (callWeight == 0 && target->shouldFailOnThisTarget()) {
-        return target->isTheSameAsIn(kb->getFirstInstruction()) &&
-                       target->isThatError(error)
-                   ? DistanceResult(Done)
-                   : DistanceResult(Continue);
-      } else {
-        callWeight += sfNum;
-      }
+      callWeight += sfNum;
 
       if (callWeight < minCallWeight) {
         minCallWeight = callWeight;

lib/Core/DistanceCalculator.h

@@ -21,9 +21,9 @@ class CodeGraphDistance;
 struct Target;
 
 enum WeightResult : std::uint8_t {
-  Continue,
-  Done,
-  Miss,
+  Done = 0U,
+  Continue = 1U,
+  Miss = 2U,
 };
 
 using weight_type = unsigned;
@@ -33,9 +33,14 @@ struct DistanceResult {
   weight_type weight;
   bool isInsideFunction;
 
-  explicit DistanceResult(WeightResult result_, weight_type weight_ = 0,
+  explicit DistanceResult(WeightResult result_ = WeightResult::Miss,
+                          weight_type weight_ = 0,
                           bool isInsideFunction_ = true)
-      : result(result_), weight(weight_), isInsideFunction(isInsideFunction_) {}
+      : result(result_), weight(weight_), isInsideFunction(isInsideFunction_){};
+
+  bool operator<(const DistanceResult &b) const;
+
+  std::string toString() const;
 };
 
 class DistanceCalculator {

lib/Core/Executor.cpp

@@ -4060,6 +4060,38 @@ void Executor::seed(ExecutionState &initialState) {
   }
 }
 
+void Executor::reportProgressTowardsTargets(std::string prefix,
+                                            const SetOfStates &states) const {
+  klee_message("%zu %sstates remaining", states.size(), prefix.c_str());
+  TargetHashMap<DistanceResult> distancesTowardsTargets;
+  for (auto &state : states) {
+    for (auto &p : *state->targetForest.getTargets()) {
+      auto target = p.first;
+      auto distance = distanceCalculator->getDistance(*state, target);
+      auto it = distancesTowardsTargets.find(target);
+      if (it == distancesTowardsTargets.end())
+        distancesTowardsTargets.insert(it, std::make_pair(target, distance));
+      else {
+        distance = std::min(distance, it->second);
+        distancesTowardsTargets[target] = distance;
+      }
+    }
+  }
+  klee_message("Distances from nearest %sstates to remaining targets:",
+               prefix.c_str());
+  for (auto &p : distancesTowardsTargets) {
+    auto target = p.first;
+    auto distance = p.second;
+    klee_message("%s for %s", distance.toString().c_str(),
+                 target->toString().c_str());
+  }
+}
+
+void Executor::reportProgressTowardsTargets() const {
+  reportProgressTowardsTargets("paused ", pausedStates);
+  reportProgressTowardsTargets("", states);
+}
+
 void Executor::run(std::vector<ExecutionState *> initialStates) {
   // Delay init till now so that ticks don't accrue during optimization and
   // such.
@@ -4098,6 +4130,7 @@ void Executor::run(std::vector<ExecutionState *> initialStates) {
   }
 
   if (guidanceKind == GuidanceKind::ErrorGuidance) {
+    reportProgressTowardsTargets();
     bool canReachNew1 = decreaseConfidenceFromStoppedStates(pausedStates);
     bool canReachNew2 =
         decreaseConfidenceFromStoppedStates(states, haltExecution);

lib/Core/Executor.h

@@ -593,6 +593,10 @@ class Executor : public Interpreter {
   void terminateStateOnUserError(ExecutionState &state,
                                  const llvm::Twine &message);
 
+  void reportProgressTowardsTargets(std::string prefix,
+                                    const SetOfStates &states) const;
+  void reportProgressTowardsTargets() const;
+
   /// bindModuleConstants - Initialize the module constant table.
   void bindModuleConstants(const llvm::APFloat::roundingMode &rm);
 

lib/Core/Searcher.h

@@ -158,14 +158,6 @@ class TargetedSearcher final : public Searcher {
 };
 
 class GuidedSearcher final : public Searcher {
-private:
-  template <class T>
-  class TargetHashMap
-      : public std::unordered_map<ref<Target>, T, RefTargetHash, RefTargetCmp> {
-  };
-  class TargetHashSet
-      : public std::unordered_set<ref<Target>, RefTargetHash, RefTargetCmp> {};
-
 public:
   using TargetToStateUnorderedSetMap =
       TargetHashMap<std::unordered_set<ExecutionState *>>;

lib/Module/KModule.cpp

@@ -728,6 +728,8 @@ std::string KBlock::getLabel() const {
   std::string _label;
   llvm::raw_string_ostream label_stream(_label);
   basicBlock->printAsOperand(label_stream, false);
+  label_stream << " (lines " << getFirstInstruction()->info->line << " to "
+               << getLastInstruction()->info->line << ")";
   std::string label = label_stream.str();
   return label;
 }

test/Industry/if2.c

@@ -13,4 +13,6 @@ int main(int x) {
 // 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 --max-stepped-instructions=19 --max-cycles=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
+// 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
+// CHECK-DISTANCE: KLEE: (0, 1, 1) for Target 1: error in %13 (lines 8 to 8) in function main

test/Industry/while_true.c

@@ -14,7 +14,12 @@ int main() {
 // 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 --max-stepped-instructions=10 --max-cycles=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: 0.00% NullPointerException False Positive at trace 1
+// RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-REACH-1
+// CHECK-REACH-1: (0, 1, 4) for Target 1: error in %17 (lines 8 to 8) in function main
+
 // 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 --max-stepped-instructions=5000 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-ALL
-// CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1
+// CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1
+// RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-REACH-2
+// CHECK-REACH-2: (0, 1, 1) for Target 1: error in %17 (lines 8 to 8) in function main