Add core features for 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

README-UTBot.md

@@ -0,0 +1,68 @@
+## Get source code
+
+Our version of KLEE can be found at [link](https://github.com/UnitTestBot/klee/commits/luban-utbot-main).
+
+## Build
+
+There is a step-by-step [guide](https://klee.github.io/build-llvm11/) how to build KLEE by original authors.
+
+## Run
+
+The following flags should be used when calling klee binary.
+
+### Essential flags
+
+| KLEE flag | Description |
+|-----------|-------------|
+| --use-guided-search=error | Enables symbolic execution guidance by input errors from off-the-shelf static analyzer |
+| --mock-external-calls | All external calls will be treated symbolically |
+| --posix-runtime | POSIX environment is emulated |
+| --libc=klee | **To UtBotTeam: why not uclibc?** |
+| --skip-not-lazy-initialized | Lazy initialization optimization; crucial for performance |
+| --analysis-reproduce=/analyzer/result.json | Path of JSON file containing static analysis paths to be reproduced |
+
+### Nonessential flags
+
+| KLEE flag | Description |
+|-----------|-------------|
+| --output-dir=/path/to/some/folder.klee-out | Directory in which to write results. Note that it’s parent folder must exist (e.g., a folder /path/to/some must exist) and this folder must not exist (e.g., a folder /path/to/some/folder.klee-out must not exist). |
+
+#### Nonessential flags to control quality/time
+
+| KLEE flag | Description |
+|-----------|-------------|
+| --max-depth=N | Only allow N symbolic branches. Set to 0 to disable. |
+| --max-time=Ns | Halt execution after N seconds. Set to 0s to disable. |
+| --max-solver-time=Ns | N seconds is a maximum amount of time for a single SMT query. Set to 0s to disable. |
+| --max-instructions=N | Stop execution after N instructions. Set to 0 to disable. |
+| --max-forks=N | Only fork N times. Set to -1 to disable. |
+| --max-stack-frames=N | Terminate a symbolic state after N stack frames in symbolic state. Set to 0 to disable. |
+| --max-sym-alloc=N | Maximum available size for single array allocation. By default 10Mb. |
+| --mock-mutable-globals="none" or "primitive-fields" or "all" | Policy of symbolization mutable global objects |
+
+### Our KLEE reports results to **stderr** as lines of the form:
+
+`KLEE: WARNING: False Negative at: *filename*:*error line*:*error column*`
+
+where *filename*, *error line*, *error column* is an error address with program trace which does not match input source-sink request, which is proven to be reachable.
+
+`KLEE: WARNING: *verdict* at trace *number*`
+
+where
+
+* *verdict* is either: “False Positive” or “True Positive”
+* *number* is an id of the proved or refuted trace from JSON input
+
+### Known limitations
+
+Current version supports only `null dereference` type of errors. So, it does not support, e.g., `reverse null` type of errors.
+
+## Examples
+
+All example JSON inputs for `--analysis-reproduce` flag can be found [here](test/Industry).
+
+Examples can be run automatically with the following command
+
+```bash
+~/klee/build $ lit -a test/Industry
+```

convert_to_sarif.py

@@ -0,0 +1,73 @@
+import argparse
+from collections import defaultdict
+import json
+import os
+
+
+def get_args():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--input', type=str, required=True)
+    parser.add_argument('--output_dir', type=str, required=True)
+    return parser.parse_args()
+
+
+def convert_error(error):
+    converted_error = {}
+    locations = []
+    codeFlows = [{"threadFlows": [{"locations": locations}]}]
+    converted_error["codeFlows"] = codeFlows
+    for trace in error["trace"]:
+        traceLocation = trace["location"]
+        physicalLocation = {
+            "artifactLocation": {
+                "uri": traceLocation["file"]
+            },
+            "region": {
+                "startLine": traceLocation["reportLine"],
+                "startColumn": traceLocation.get("column")
+            }
+        }
+        location = {
+            "physicalLocation": physicalLocation
+        }
+        locations.append({"location": location})
+
+    trace = error["trace"][-1]
+    if trace["event"]["kind"] == "Error":
+        converted_error["ruleId"] = trace["event"]["error"]["sort"]
+    else:
+        converted_error["ruleId"] = "Reached"
+    converted_error["locations"] = [locations[-1]["location"]]
+
+
+    return converted_error
+
+
+def convert_file(input: str, output_dir: str):
+    with open(input, 'r') as f:
+        input_report = json.load(f)
+
+    output_report = {}
+    output_report["runs"] = [defaultdict(lambda: defaultdict(lambda: defaultdict(lambda: defaultdict(lambda: defaultdict(lambda: 0)))))]
+    run = output_report["runs"][0]
+    run["tool"]["driver"]["name"] = "huawei"
+    run["results"] = []
+    results = run["results"]
+
+    for error in input_report["errors"]:
+        results.append(convert_error(error))
+
+    with open(os.path.join(output_dir, os.path.basename(input)), 'w') as f:
+        json.dump(output_report, f, indent=4)
+
+def main():
+    args = get_args()
+    if os.path.isdir(args.input):
+        for f in os.listdir(args.input):
+            if f.endswith('.json'):
+                convert_file(os.path.join(args.input, f), args.output_dir)
+    else:
+        convert_file(args.input, args.output_dir)
+
+if __name__ == "__main__":
+    main()

filter_locations.py

@@ -0,0 +1,45 @@
+import argparse
+import json
+
+
+def get_args():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--input', type=str, required=True)
+    parser.add_argument('--output', type=str, required=True)
+    return parser.parse_args()
+
+def prepare_cppcheck(input: str, output: str):
+    with open(input, 'r') as file:
+        input_report = json.load(file)
+    run = input_report["runs"][0]
+    for i, result in enumerate(run["results"]):
+        result["id"] = i
+        if "codeFlows" in result:
+            locations = result["codeFlows"][0]["threadFlows"][0]["locations"]
+            new_locs = []
+            prev = -1
+            for i, loc in enumerate(locations):
+                if prev == -1:
+                    new_locs.append(loc)
+                    prev = i
+                else:
+                    if loc["location"]["physicalLocation"]["artifactLocation"]["uri"] == locations[prev]["location"]["physicalLocation"]["artifactLocation"]["uri"] and loc["location"]["physicalLocation"]["region"]["startLine"] == locations[prev]["location"]["physicalLocation"]["region"]["startLine"]:
+                        if "startColumn" in loc["location"]["physicalLocation"]["region"]:
+                            if loc["location"]["physicalLocation"]["region"]["startColumn"] != locations[prev]["location"]["physicalLocation"]["region"]["startColumn"]:
+                                new_locs.append(loc)
+                                prev = i
+                    else:
+                        new_locs.append(loc)
+                        prev = i
+
+            result["codeFlows"][0]["threadFlows"][0]["locations"] = new_locs
+    with open(output, 'w') as f:
+        json.dump({"runs": [run]}, f, indent=4) 
+
+
+def main():
+    args = get_args()
+    prepare_cppcheck(args.input, args.output)
+
+if __name__ == "__main__":
+    main()

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;