[feat] Adds support for reporting errors in SARIF format:

  * Introduces `CodeEvent` as a base unit for storing information about event in code.
  * `CodeEvent`s are managed with `EventRecorder`, capable of serializing recorded trace.
  * `termianateStateOnProgramError` receives an `ErrorEvent` object contatining all required information about error.
[feat] Enhances `gepExprBases`:
  * Bases for addresses stored for constant expressions.
  * Precalculates bases for `llvm::ConstantExpr` (i.e. for `getElementPtr` in arguments of instructions).
[perf] Removes checks on `baseInBounds` during memory operations.
[fix] Adds hacks for managing objects with neighboring addresses (in some cases `gepExprBases` could assume that the beginning of one object is the end of another).
[fix] Fixes ODR violation with `llvm::APFloat::RoundingMode`.

include/klee/ADT/ImmutableList.h

@@ -97,9 +97,9 @@ template <typename T> class ImmutableList {
     node->values.push_back(value);
   }
 
-  bool empty() { return size() == 0; }
+  bool empty() const { return size() == 0; }
 
-  const T &back() {
+  const T &back() const {
     assert(node && "requiers not empty list");
     auto it = iterator(node.get());
     it.get = size() - 1;
@@ -109,6 +109,10 @@ template <typename T> class ImmutableList {
   ImmutableList() : node(){};
   ImmutableList(const ImmutableList<T> &il)
       : node(std::make_shared<ImmutableListNode>(il)) {}
+  ImmutableList &operator=(const ImmutableList<T> &il) {
+    node = std::make_shared<ImmutableListNode>(il);
+    return *this;
+  }
 };
 
 } // namespace klee

include/klee/Core/Interpreter.h

@@ -38,6 +38,7 @@ class raw_fd_ostream;
 namespace klee {
 class ExecutionState;
 struct SarifReport;
+struct ToolJson;
 class Interpreter;
 class TreeStreamWriter;
 
@@ -57,6 +58,8 @@ class InterpreterHandler {
 
   virtual void processTestCase(const ExecutionState &state, const char *message,
                                const char *suffix, bool isError = false) = 0;
+
+  virtual ToolJson info() const = 0;
 };
 
 /// [File][Line][Column] -> Opcode
@@ -228,6 +231,10 @@ class Interpreter {
 
   virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0;
 
+  virtual void addSARIFReport(const ExecutionState &state) = 0;
+
+  virtual SarifReportJson getSARIFReport() const = 0;
+
   virtual void logState(const ExecutionState &state, int id,
                         std::unique_ptr<llvm::raw_fd_ostream> &f) = 0;
 

include/klee/Expr/SourceBuilder.h

@@ -5,8 +5,8 @@
 
 namespace klee {
 
-class KInstruction;
-class KGlobalVariable;
+struct KInstruction;
+struct KGlobalVariable;
 
 template <typename T, typename Eq> class SparseStorage;
 template <typename T> class ref;

include/klee/Module/KModule.h

@@ -381,6 +381,8 @@ class KModule {
 
   KBlock *getKBlock(const llvm::BasicBlock *bb);
 
+  bool inMainModule(const llvm::Instruction &i);
+
   bool inMainModule(const llvm::Function &f);
 
   bool inMainModule(const llvm::GlobalVariable &v);

include/klee/Module/LocationInfo.h

@@ -1,16 +1,18 @@
-////===-- LocationInfo.h ----------------------------------*- C++ -*-===//
-////
-////                     The KLEE Symbolic Virtual Machine
-////
-//// This file is distributed under the University of Illinois Open Source
-//// License. See LICENSE.TXT for details.
-////
-////===----------------------------------------------------------------------===//
+////===-- LocationInfo.h ----------------------------------------*- C++ -*-===//
+//
+//                     The KLEEF Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
 
 #ifndef KLEE_LOCATIONINFO_H
 #define KLEE_LOCATIONINFO_H
 
+#include <cstdint>
 #include <memory>
+#include <optional>
 #include <string>
 
 namespace llvm {
@@ -21,11 +23,27 @@ class Module;
 } // namespace llvm
 
 namespace klee {
+struct PhysicalLocationJson;
+}
 
+namespace klee {
+
+/// @brief Immutable struct representing location in source code.
 struct LocationInfo {
-  std::string file;
-  size_t line;
-  size_t column;
+  /// @brief Path to source file for that location.
+  const std::string file;
+
+  /// @brief Code line in source file.
+  const uint64_t line;
+
+  /// @brief Column number in source file.
+  const std::optional<uint64_t> column;
+
+  /// @brief Converts location info to SARIFs representation
+  /// of location.
+  /// @param location location info in source code.
+  /// @return SARIFs representation of location.
+  PhysicalLocationJson serialize() const;
 };
 
 LocationInfo getLocationInfo(const llvm::Function *func);

include/klee/Module/SarifReport.h

@@ -58,6 +58,11 @@ std::string getErrorsString(const std::vector<ReachWithError> &errors);
 
 struct FunctionInfo;
 struct KBlock;
+struct LocationInfo;
+
+struct Message {
+  std::string text;
+};
 
 struct ArtifactLocationJson {
   std::optional<std::string> uri;
@@ -76,6 +81,7 @@ struct PhysicalLocationJson {
 };
 
 struct LocationJson {
+  std::optional<Message> message;
   std::optional<PhysicalLocationJson> physicalLocation;
 };
 
@@ -92,10 +98,6 @@ struct CodeFlowJson {
   std::vector<ThreadFlowJson> threadFlows;
 };
 
-struct Message {
-  std::string text;
-};
-
 struct Fingerprints {
   std::string cooddy_uid;
 };
@@ -110,15 +112,25 @@ static void from_json(const json &j, Fingerprints &p) {
 
 struct ResultJson {
   std::optional<std::string> ruleId;
+  std::optional<std::string> level;
   std::optional<Message> message;
   std::optional<unsigned> id;
   std::optional<Fingerprints> fingerprints;
   std::vector<LocationJson> locations;
   std::vector<CodeFlowJson> codeFlows;
 };
 
+struct RuleJson {
+  std::string id;
+  std::optional<std::string> name;
+  std::optional<Message> shortDescription;
+  std::optional<std::string> helpUri;
+};
+
 struct DriverJson {
   std::string name;
+  std::optional<std::string> informationUri;
+  std::vector<RuleJson> rules;
 };
 
 struct ToolJson {
@@ -131,9 +143,13 @@ struct RunJson {
 };
 
 struct SarifReportJson {
+  std::string version;
   std::vector<RunJson> runs;
 };
 
+NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(RuleJson, id, name,
+                                                shortDescription, helpUri)
+
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ArtifactLocationJson, uri)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(RegionJson, startLine, endLine,
@@ -142,7 +158,8 @@ NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(RegionJson, startLine, endLine,
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(PhysicalLocationJson,
                                                 artifactLocation, region)
 
-NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(LocationJson, physicalLocation)
+NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(LocationJson, message,
+                                                physicalLocation)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ThreadFlowLocationJson,
                                                 location, metadata)
@@ -153,17 +170,18 @@ NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(CodeFlowJson, threadFlows)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(Message, text)
 
-NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ResultJson, ruleId, message, id,
-                                                fingerprints, codeFlows,
-                                                locations)
+NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ResultJson, ruleId, level,
+                                                message, id, fingerprints,
+                                                codeFlows, locations)
 
-NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(DriverJson, name)
+NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(DriverJson, name,
+                                                informationUri, rules)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ToolJson, driver)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(RunJson, results, tool)
 
-NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(SarifReportJson, runs)
+NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(SarifReportJson, version, runs)
 
 struct Location {
   struct LocationHash {

lib/Core/CMakeLists.txt

@@ -10,10 +10,12 @@ add_library(kleeCore
   AddressManager.cpp
   AddressSpace.cpp
   CallPathManager.cpp
+  CodeLocation.cpp
   Context.cpp
   CoreStats.cpp
   CXXTypeSystem/CXXTypeManager.cpp
   DistanceCalculator.cpp
+  EventRecorder.cpp
   ExecutionState.cpp
   Executor.cpp
   ExecutorUtil.cpp