Provide API for KLEE to verify execution traces

[korifey]

One of unique advantages of UTBOT-KLEE is ability to verify execution trace of defect (e.g. in SARIF format) is True Positive or False Positive.
But the only way to start UTBOT-KLEE is from CLI (command line interface).

Can we provide API to be able to use UTBOT-KLEE as library.

We can discuss here the format of this API.

[misonijnik]

The current version of KLEE accepts a path to a .bc file, a path to a set of traces in SARIF format, and a list of options as input on the command line to verify traces for correctness. Similar input data will be needed to use KLEE as a library.

We propose a class TraceVerifier, which takes an llvm::Module and a structure containing option values as constructor arguments. The llvm::Module should be an unmodified module obtained after loading the .bc file of the program to be analyzed. An important limitation is that the .bc file must contain debug information that links LLVM-IR instructions to their source code. A documentation describing the list of options and default values will be provided along with the option values.

After creating an object of the TraceVerifier class, the verifyTraces function can be called to verify the traces. The verifyTraces function takes an object of the SarifReport class as input and returns an object of the AnalysisReport class. The SarifReport class describes the set of traces, while the AnalysisReport class contains the results of the analysis. The function works in a single-threaded synchronous mode.

Below is a description of SarifReport class.

enum ReachWithError { // supported vulnerability types
  DoubleFree = 0,
  UseAfterFree,
  NullPointerException,
  NullCheckAfterDerefException,
  Reachable,
  None,
};

struct Location { // structure describing an event from a trace
  // Mandatory fields
  std::string filename; // the name of the source file
  unsigned int startLine; // the line number in the source code
  // Optional fields
  std::optional<unsigned int> endLine; // the end of the range in which the event occurs. If not set, it is equal to startLine
  std::optional<unsigned int> startColumn; // the column in which the event occurs
  std::optional<unsigned int> endColumn; // the end of the column range in which the event occurs. If not set, it is equal to startColumn
  // If startColumn and endColumn are not set simultaneously, the range is considered unlimited
};

struct Result { // structure representing a single trace
  std::vector<std::reference_wrapper<const Location>> locations; // list of events from the trace
  unsigned id; // unique identifier of the trace
  std::unordered_set<ReachWithError> errors; // list of vulnerabilities associated with this trace
};

struct SarifReport {
  std::vector<Result> results; // list of traces
};

Description of the AnalysisReport class.

enum Verdict {
  FalsePositive,
  TruePositive
};

struct AnalysisResult { // structure representing the result of checking a trace
  unsigned id; // unique identifier of the trace
  Verdict v; // the verdict on the trace (FP or TP)
  double confidence; // confidence in the verdict
};

struct AnalysisReport {
  std::vector<AnalysisResult> results; // list of check results
};

What do you think of such an API?

[ocelaiwo]

What versions of LLVM are in use in projects that intend to use KLEE as a library? If you want the API to accept an instance of llvm::Module, then you have to build both KLEE and your project with the same version of LLVM. As of now, KLEE supports LLVM versions from 6 up to 13. If you have to use some different version of LLVM, we can provide an API that accepts a path to an LLVM bitcode file and loads it independently of your project using a version of LLVM that KLEE supports.

[misonijnik]

We are working on a solution in this branch. Now there is a prototype that we tested on a test project. This is not a finished version of the solution yet.