Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions include/klee/ADT/ImmutableList.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand Down
7 changes: 7 additions & 0 deletions include/klee/Core/Interpreter.h
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ class raw_fd_ostream;
namespace klee {
class ExecutionState;
struct SarifReport;
struct ToolJson;
class Interpreter;
class TreeStreamWriter;

Expand All @@ -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
Expand Down Expand Up @@ -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;

Expand Down
4 changes: 2 additions & 2 deletions include/klee/Expr/SourceBuilder.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 2 additions & 0 deletions include/klee/Module/KModule.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
40 changes: 29 additions & 11 deletions include/klee/Module/LocationInfo.h
Original file line number Diff line number Diff line change
@@ -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 {
Expand All @@ -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);
Expand Down
38 changes: 28 additions & 10 deletions include/klee/Module/SarifReport.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -76,6 +81,7 @@ struct PhysicalLocationJson {
};

struct LocationJson {
std::optional<Message> message;
std::optional<PhysicalLocationJson> physicalLocation;
};

Expand All @@ -92,10 +98,6 @@ struct CodeFlowJson {
std::vector<ThreadFlowJson> threadFlows;
};

struct Message {
std::string text;
};

struct Fingerprints {
std::string cooddy_uid;
};
Expand All @@ -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 {
Expand All @@ -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,
Expand All @@ -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)
Expand All @@ -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 {
Expand Down
2 changes: 2 additions & 0 deletions lib/Core/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading