[feat] Return confidence and give advise

include/klee/Core/Interpreter.h

@@ -15,6 +15,8 @@
 #include <string>
 #include <vector>
 
+#include "TerminationTypes.h"
+
 struct KTest;
 struct TestCase;
 
@@ -32,6 +34,7 @@ class ExecutionState;
 struct PathForest;
 class Interpreter;
 class TreeStreamWriter;
+struct LocatedEvent;
 
 class InterpreterHandler {
 public:
@@ -176,7 +179,7 @@ class Interpreter {
                                  char **envp) = 0;
   /*** Runtime options ***/
 
-  virtual void setHaltExecution(bool value) = 0;
+  virtual void setHaltExecution(HaltExecution::Reason value) = 0;
 
   virtual void setInhibitForking(bool value) = 0;
 

include/klee/Core/TargetedExecutionReporter.h

@@ -0,0 +1,37 @@
+//===-- TargetedExecutionReporter.h ------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_TARGETEDEXECUTIONREPORTER_H
+#define KLEE_TARGETEDEXECUTIONREPORTER_H
+
+#include "klee/Module/Locations.h"
+
+namespace klee {
+
+namespace confidence {
+  using ty = double;
+  static ty MinConfidence = 0.0;
+  static ty MaxConfidence = 100.0;
+  static ty Confident = 90.0;
+  static ty VeryConfident = 99.0;
+  bool isConfident(ty conf);
+  bool isVeryConfident(ty conf);
+  bool isNormal(ty conf);
+  std::string toString(ty conf);
+  ty min(ty left, ty right);
+};
+
+void reportFalsePositive(
+  confidence::ty confidence,
+  LocatedEvent &event,
+  std::string whatToIncrease);
+
+}
+
+#endif

include/klee/Core/TerminationTypes.h

@@ -55,4 +55,23 @@ enum class StateTerminationType : std::uint8_t {
 #undef MARK
 };
 
+namespace HaltExecution {
+  enum Reason {
+    NotHalt = 0,
+    MaxTests,
+    MaxInstructions,
+    MaxSteppedInstructions,
+    MaxTime,
+    BCovCheckInterval,
+    NoMoreStates,
+    ReachedTarget,
+    ErrorOnWhichShouldExit,
+    Interrupt,
+    MaxDepth,
+    MaxStackFrames,
+    MaxSolverTime,
+    Unspecified
+  };
+};
+
 #endif

include/klee/Module/Locations.h

@@ -17,6 +17,7 @@
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
 #include "klee/Module/InstructionInfoTable.h"
+#include "klee/ADT/Ref.h"
 
 
 namespace klee {
@@ -49,6 +50,9 @@ class Location {
   const std::string function;
   const std::string filename;
 
+  /// @brief Required by klee::ref-managed objects
+  class ReferenceCounter _refCount;
+
   Location(const std::string &f, const std::string &function, unsigned line, unsigned offset, unsigned column, unsigned instructionOpcode)
     : line(line), offset(offset), column(column), instructionOpcode(instructionOpcode), function(function), filename(f) {}
   Location(const std::string &f, const std::string &function)
@@ -68,19 +72,14 @@ class Location {
 
   std::set<KInstruction *> initInstructions(KModule *origModule, KModule *kleeModule, std::ostringstream &error);
 
+  int compare(const Location &other) const;
+
   friend bool operator <(const Location& lhs, const Location& rhs) {
-    return
-            lhs.line < rhs.line     ||     (lhs.line == rhs.line &&
-         (lhs.offset < rhs.offset   ||   (lhs.offset == rhs.offset &&
-       (lhs.filename < rhs.filename || (lhs.filename == rhs.filename &&
-       (lhs.function < rhs.function || (lhs.function == rhs.function &&
-    (lhs.instructions < rhs.instructions))))))));
+    return lhs.compare(rhs) < 0;
   }
 
   friend bool operator==(const Location &lhs, const Location &rhs) {
-    return lhs.line == rhs.line && lhs.offset == rhs.offset &&
-           lhs.filename == rhs.filename && lhs.function == rhs.function &&
-           lhs.instructions == rhs.instructions;
+    return lhs.compare(rhs) == 0;
   }
 
   friend bool operator!=(const Location &lhs, const Location &rhs) {
@@ -89,16 +88,37 @@ class Location {
 };
 
 struct LocatedEvent {
-  Location location;
+private:
+  ref<Location> location;
   ReachWithError error;
-  unsigned id = 0;
+  unsigned id;
+
+public:
+  LocatedEvent(Location *location, ReachWithError error, unsigned id)
+    : location(location), error(error), id(id) {}
+
+  LocatedEvent(Location *location, unsigned id)
+    : LocatedEvent(location, ReachWithError::None, id) {}
 
-  LocatedEvent(Location location, ReachWithError error) : location(location), error(error) {}
+  LocatedEvent(Location *location)
+    : LocatedEvent(location, 0) {}
+
+  explicit LocatedEvent() : LocatedEvent(nullptr) {}
 
   bool hasFunctionWithOffset() {
-    return location.hasFunctionWithOffset();
+    return location->hasFunctionWithOffset();
   }
 
+  int compare(const LocatedEvent &other) const;
+  bool operator<(const LocatedEvent &other) const;
+  bool operator==(const LocatedEvent &other) const;
+  ReachWithError getError() const { return error; }
+  const char *getErrorString() const { return ReachWithErrorNames[error]; }
+  unsigned getId() const { return id; }
+  ref<Location> getLocation() const { return location; }
+  bool shouldFailOnThisTarget() const { return error != ReachWithError::None; }
+  void setErrorReachableIfNone();
+
   std::string toString() const;
 };
 

lib/Core/CMakeLists.txt

@@ -14,6 +14,7 @@ klee_add_component(kleeCore
   CoreStats.cpp
   CXXTypeSystem/CXXTypeManager.cpp
   ExecutionState.cpp
+  TargetedExecutionReporter.cpp
   TargetForest.cpp
   TargetedExecutionManager.cpp
   Executor.cpp

lib/Core/ExecutionState.h

@@ -18,6 +18,7 @@
 
 #include "klee/ADT/ImmutableSet.h"
 #include "klee/ADT/TreeStream.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
@@ -287,6 +288,8 @@ class ExecutionState {
 
   ReachWithError error = ReachWithError::None;
 
+  HaltExecution::Reason terminationReasonType = HaltExecution::NotHalt;
+
   ExprHashMap<std::pair<ref<Expr>, llvm::Type *>> gepExprBases;
 
 public: