Add error-guided search

.github/workflows/build.yaml

@@ -52,7 +52,7 @@ jobs:
                 "Latest klee-uclibc",
                 "Asserts enabled",
                 "No TCMalloc, optimised runtime",
-            ]
+              ]
         include:
           - name: "LLVM 13"
             env:
@@ -148,6 +148,8 @@ jobs:
     steps:
       - name: Checkout KLEE source code
         uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - name: Build KLEE
         env: ${{ matrix.env }}
         run: scripts/build/build.sh klee --docker --create-final-image
@@ -167,6 +169,8 @@ jobs:
         run: brew install bash
       - name: Checkout KLEE source code
         uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - name: Build KLEE
         run: scripts/build/build.sh klee --debug --install-system-deps
       - name: Run tests
@@ -177,6 +181,8 @@ jobs:
     steps:
       - name: Checkout KLEE Code
         uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - name: Build Docker image
         run: docker build .
 
@@ -189,6 +195,8 @@ jobs:
     steps:
       - name: Checkout KLEE source code
         uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - name: Build KLEE
         run: scripts/build/build.sh klee --docker --create-final-image
       - name: Run tests

.gitignore

@@ -31,6 +31,5 @@ autoconf/aclocal.m4
 autoconf/autom4te.cache/
 autom4te.cache/
 
-.vscode/launch.json
-.vscode/settings.json
+.vscode/
 .cache/

.gitmodules

@@ -0,0 +1,6 @@
+[submodule "json"]
+	path = json
+	url = https://github.com/nlohmann/json.git
+[submodule "optional"]
+	path = optional
+	url = https://github.com/martinmoene/optional-lite.git

CMakeLists.txt

@@ -724,6 +724,8 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
 ################################################################################
 include_directories("${CMAKE_BINARY_DIR}/include")
 include_directories("${CMAKE_SOURCE_DIR}/include")
+include_directories("${CMAKE_SOURCE_DIR}/json/include")
+include_directories("${CMAKE_SOURCE_DIR}/optional/include")
 
 ################################################################################
 # Set default location for targets in the build directory

include/klee/Core/Interpreter.h

@@ -9,15 +9,25 @@
 #ifndef KLEE_INTERPRETER_H
 #define KLEE_INTERPRETER_H
 
+#include "TerminationTypes.h"
+
+#include "klee/Module/SarifReport.h"
+
 #include <map>
 #include <memory>
 #include <set>
 #include <string>
+#include <unordered_map>
 #include <vector>
 
+#include <nonstd/optional.hpp>
+
+using nonstd::optional;
+
 struct KTest;
 
 namespace llvm {
+class BasicBlock;
 class Function;
 class LLVMContext;
 class Module;
@@ -27,8 +37,10 @@ class raw_fd_ostream;
 
 namespace klee {
 class ExecutionState;
+struct SarifReport;
 class Interpreter;
 class TreeStreamWriter;
+class InstructionInfoTable;
 
 class InterpreterHandler {
 public:
@@ -50,25 +62,36 @@ class InterpreterHandler {
 
 class Interpreter {
 public:
+  enum class GuidanceKind {
+    NoGuidance,       // Default symbolic execution
+    CoverageGuidance, // Use GuidedSearcher and guidedRun to maximize full code
+                      // coverage
+    ErrorGuidance     // Use GuidedSearcher and guidedRun to maximize specified
+                      // targets coverage
+  };
+
   /// ModuleOptions - Module level options which can be set when
   /// registering a module with the interpreter.
   struct ModuleOptions {
     std::string LibraryDir;
     std::string EntryPoint;
     std::string OptSuffix;
     bool Optimize;
+    bool Simplify;
     bool CheckDivZero;
     bool CheckOvershift;
     bool WithFPRuntime;
+    bool WithPOSIXRuntime;
 
     ModuleOptions(const std::string &_LibraryDir,
                   const std::string &_EntryPoint, const std::string &_OptSuffix,
-                  bool _Optimize, bool _CheckDivZero, bool _CheckOvershift,
-                  bool _WithFPRuntime)
+                  bool _Optimize, bool _Simplify, bool _CheckDivZero,
+                  bool _CheckOvershift, bool _WithFPRuntime,
+                  bool _WithPOSIXRuntime)
         : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
-          OptSuffix(_OptSuffix), Optimize(_Optimize),
+          OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify),
           CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift),
-          WithFPRuntime(_WithFPRuntime) {}
+          WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
   };
 
   enum LogType {
@@ -84,12 +107,16 @@ class Interpreter {
     /// symbolic values. This is used to test the correctness of the
     /// symbolic execution on concrete programs.
     unsigned MakeConcreteSymbolic;
+    GuidanceKind Guidance;
+    nonstd::optional<SarifReport> Paths;
 
-    InterpreterOptions() : MakeConcreteSymbolic(false) {}
+    InterpreterOptions(nonstd::optional<SarifReport> Paths)
+        : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
+          Paths(std::move(Paths)) {}
   };
 
 protected:
-  const InterpreterOptions interpreterOpts;
+  const InterpreterOptions &interpreterOpts;
 
   Interpreter(const InterpreterOptions &_interpreterOpts)
       : interpreterOpts(_interpreterOpts) {}
@@ -112,7 +139,8 @@ class Interpreter {
   setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
             std::vector<std::unique_ptr<llvm::Module>> &libsModules,
             const ModuleOptions &opts,
-            const std::vector<std::string> &mainModuleFunctions) = 0;
+            const std::vector<std::string> &mainModuleFunctions,
+            std::unique_ptr<InstructionInfoTable> origInfos) = 0;
 
   // supply a tree stream writer which the interpreter will use
   // to record the concrete path (as a stream of '0' and '1' bytes).
@@ -140,12 +168,14 @@ class Interpreter {
 
   /*** Runtime options ***/
 
-  virtual void setHaltExecution(bool value) = 0;
+  virtual void setHaltExecution(HaltExecution::Reason value) = 0;
 
   virtual void setInhibitForking(bool value) = 0;
 
   virtual void prepareForEarlyExit() = 0;
 
+  virtual bool hasTargetForest() const = 0;
+
   /*** State accessor methods ***/
 
   virtual unsigned getPathStreamID(const ExecutionState &state) = 0;

include/klee/Core/TargetedExecutionReporter.h

@@ -0,0 +1,38 @@
+//===-- 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/SarifReport.h"
+
+#include <unordered_set>
+
+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);
+}; // namespace confidence
+
+void reportFalsePositive(confidence::ty confidence,
+                         const std::unordered_set<ReachWithError> &errors,
+                         unsigned id, std::string whatToIncrease);
+
+} // namespace klee
+
+#endif

include/klee/Core/TerminationTypes.h

@@ -33,7 +33,8 @@
   TTYPE(ReadOnly, 17U, "read_only.err")                                        \
   TTYPE(ReportError, 18U, "report_error.err")                                  \
   TTYPE(UndefinedBehavior, 19U, "undefined_behavior.err")                      \
-  MARK(PROGERR, 19U)                                                           \
+  TTYPE(InternalOutOfMemory, 20U, "out_of_memory.er")                          \
+  MARK(PROGERR, 20U)                                                           \
   TTYPE(User, 23U, "user.err")                                                 \
   MARK(USERERR, 23U)                                                           \
   TTYPE(Execution, 25U, "exec.err")                                            \
@@ -42,7 +43,8 @@
   TTYPE(Replay, 27U, "")                                                       \
   TTYPE(Merge, 28U, "")                                                        \
   TTYPE(SilentExit, 29U, "")                                                   \
-  MARK(END, 29U)
+  TTYPE(Paused, 30U, "")                                                       \
+  MARK(END, 30U)
 
 ///@brief Reason an ExecutionState got terminated.
 enum class StateTerminationType : std::uint8_t {
@@ -53,4 +55,23 @@ enum class StateTerminationType : std::uint8_t {
 #undef MARK
 };
 
+namespace HaltExecution {
+enum Reason {
+  NotHalt = 0,
+  MaxTests,
+  MaxInstructions,
+  MaxSteppedInstructions,
+  MaxTime,
+  CovCheck,
+  NoMoreStates,
+  ReachedTarget,
+  ErrorOnWhichShouldExit,
+  Interrupt,
+  MaxDepth,
+  MaxStackFrames,
+  MaxSolverTime,
+  Unspecified
+};
+};
+
 #endif

include/klee/Expr/Assignment.h

@@ -36,17 +36,14 @@ class Assignment {
   Assignment(const bindings_ty &_bindings, bool _allowFreeValues = false)
       : allowFreeValues(_allowFreeValues), bindings(_bindings) {}
   Assignment(const std::vector<const Array *> &objects,
-             std::vector<SparseStorage<unsigned char>> &values,
+             const std::vector<SparseStorage<unsigned char>> &values,
              bool _allowFreeValues = false)
       : allowFreeValues(_allowFreeValues) {
-    std::vector<SparseStorage<unsigned char>>::iterator valIt = values.begin();
-    for (std::vector<const Array *>::const_iterator it = objects.begin(),
-                                                    ie = objects.end();
-         it != ie; ++it) {
-      const Array *os = *it;
-      SparseStorage<unsigned char> &arr = *valIt;
+    assert(objects.size() == values.size());
+    for (unsigned i = 0; i < values.size(); ++i) {
+      const Array *os = objects.at(i);
+      const SparseStorage<unsigned char> &arr = values.at(i);
       bindings.insert(std::make_pair(os, arr));
-      ++valIt;
     }
   }
 

include/klee/Expr/SourceBuilder.h

@@ -10,7 +10,10 @@ class SourceBuilder {
 private:
   static ref<SymbolicSource> constantSource;
   static ref<SymbolicSource> makeSymbolicSource;
-  static ref<SymbolicSource> lazyInitializationMakeSymbolicSource;
+  static ref<SymbolicSource> symbolicAddressSource;
+  static ref<SymbolicSource> lazyInitializationSymbolicSource;
+  static ref<SymbolicSource> irreproducibleSource;
+  static ref<SymbolicSource> symbolicValueSource;
 
 public:
   SourceBuilder() = delete;
@@ -20,7 +23,9 @@ class SourceBuilder {
   static ref<SymbolicSource> makeSymbolic();
   static ref<SymbolicSource> symbolicAddress();
   static ref<SymbolicSource> symbolicSize();
-  static ref<SymbolicSource> lazyInitializationMakeSymbolic();
+  static ref<SymbolicSource> lazyInitializationSymbolic();
+  static ref<SymbolicSource> irreproducible();
+  static ref<SymbolicSource> symbolicValue();
 };
 
 }; // namespace klee

include/klee/Expr/SymbolicSource.h

@@ -19,7 +19,9 @@ class SymbolicSource {
     LazyInitializationSymbolic,
     MakeSymbolic,
     SymbolicAddress,
-    SymbolicSize
+    SymbolicSize,
+    Irreproducible,
+    SymbolicValue
   };
 
 public:
@@ -120,7 +122,7 @@ class LazyInitializationSymbolicSource : public SymbolicSource {
 public:
   Kind getKind() const override { return Kind::LazyInitializationSymbolic; }
   virtual std::string getName() const override {
-    return "lazyInitializationMakeSymbolic";
+    return "lazyInitializationSymbolic";
   }
   virtual bool isSymcrete() const override { return false; }
 
@@ -129,6 +131,30 @@ class LazyInitializationSymbolicSource : public SymbolicSource {
   }
 };
 
+class IrreproducibleSource : public SymbolicSource {
+public:
+  Kind getKind() const override { return Kind::Irreproducible; }
+  virtual std::string getName() const override { return "irreproducible"; }
+  virtual bool isSymcrete() const override { return false; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::Irreproducible;
+  }
+  static bool classof(const IrreproducibleSource *) { return true; }
+};
+
+class SymbolicValueSource : public SymbolicSource {
+public:
+  Kind getKind() const override { return Kind::SymbolicValue; }
+  virtual std::string getName() const override { return "symbolicValue"; }
+  virtual bool isSymcrete() const override { return false; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::SymbolicValue;
+  }
+  static bool classof(const SymbolicValueSource *) { return true; }
+};
+
 } // namespace klee
 
 #endif /* KLEE_SYMBOLICSOURCE_H */