Skip to content

Commit

Permalink
Memory optimize, remove InstructionInfoTable, add immutable list for …
Browse files Browse the repository at this point in the history
…symbolics
  • Loading branch information
ladisgin committed Oct 4, 2023
1 parent 390866f commit c5c898f
Show file tree
Hide file tree
Showing 33 changed files with 3,585 additions and 810 deletions.
106 changes: 106 additions & 0 deletions include/klee/ADT/ImmutableList.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
//===---- ImmutableList.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_IMMUTABLELIST_H
#define KLEE_IMMUTABLELIST_H

#include <memory>
#include <vector>

namespace klee {

template <typename T> class ImmutableList {
struct ImmutableListNode {
std::shared_ptr<ImmutableListNode> prev;
const size_t prev_len;
std::vector<T> values;

[[nodiscard]] size_t size() const { return prev_len + values.size(); }

ImmutableListNode() : prev(nullptr), prev_len(0), values() {}

explicit ImmutableListNode(const ImmutableList<T> &il)
: prev_len(il.size()), values() {
std::shared_ptr<ImmutableListNode> pr = il.node;
while (pr && pr->values.empty()) {
pr = pr->prev;
}
if (pr && pr->size()) {
prev = pr;
} else {
prev = nullptr;
}
}
};

std::shared_ptr<ImmutableListNode> node;

public:
[[nodiscard]] size_t size() const { return node ? node->size() : 0; }

struct iterator {
const ImmutableListNode *rootNode;
std::unique_ptr<iterator> it;
size_t get;

public:
explicit iterator(const ImmutableListNode *p)
: rootNode(p), it(nullptr), get(0) {
if (rootNode && rootNode->prev.get()) {
it = std::make_unique<iterator>(rootNode->prev.get());
}
}

bool operator==(const iterator &b) const {
return rootNode == b.rootNode && get == b.get;
}

bool operator!=(const iterator &b) const { return !(*this == b); }

iterator &operator++() {
++get;
if (get < rootNode->prev_len) {
it->operator++();
}
return *this;
}

const T &operator*() const {
if (get < rootNode->prev_len) {
return **it;
}
return rootNode->values[get - rootNode->prev_len];
}

const T &operator->() const { return **this; }
};

[[nodiscard]] iterator begin() const { return iterator(node.get()); }

[[nodiscard]] iterator end() const {
auto it = iterator(node.get());
it.get = size();
return it;
}

void push_back(T &&value) {
if (!node) {
node = std::make_shared<ImmutableListNode>();
}
node->values.push_back(std::move(value));
}

ImmutableList() : node(){};
ImmutableList(const ImmutableList<T> &il)
: node(std::make_shared<ImmutableListNode>(il)) {}
};

} // namespace klee

#endif /* KLEE_IMMUTABLELIST_H */
15 changes: 10 additions & 5 deletions include/klee/Core/Interpreter.h
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,6 @@ class ExecutionState;
struct SarifReport;
class Interpreter;
class TreeStreamWriter;
class InstructionInfoTable;

class InterpreterHandler {
public:
Expand All @@ -61,6 +60,12 @@ class InterpreterHandler {
const char *suffix, bool isError = false) = 0;
};

/// [File][Line][Column] -> Opcode
using FLCtoOpcode = std::unordered_map<
std::string,
std::unordered_map<
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;

class Interpreter {
public:
enum class GuidanceKind {
Expand Down Expand Up @@ -140,9 +145,9 @@ class Interpreter {
setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
std::vector<std::unique_ptr<llvm::Module>> &libsModules,
const ModuleOptions &opts,
const std::unordered_set<std::string> &mainModuleFunctions,
const std::unordered_set<std::string> &mainModuleGlobals,
std::unique_ptr<InstructionInfoTable> origInfos) = 0;
std::set<std::string> &&mainModuleFunctions,
std::set<std::string> &&mainModuleGlobals,
FLCtoOpcode &&origInstructions) = 0;

// supply a tree stream writer which the interpreter will use
// to record the concrete path (as a stream of '0' and '1' bytes).
Expand Down Expand Up @@ -194,7 +199,7 @@ class Interpreter {

virtual void
getCoveredLines(const ExecutionState &state,
std::map<const std::string *, std::set<unsigned>> &res) = 0;
std::map<std::string, std::set<unsigned>> &res) = 0;

virtual void getBlockPath(const ExecutionState &state,
std::string &blockPath) = 0;
Expand Down
113 changes: 0 additions & 113 deletions include/klee/Module/InstructionInfoTable.h

This file was deleted.

56 changes: 43 additions & 13 deletions include/klee/Module/KInstruction.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,17 @@
#ifndef KLEE_KINSTRUCTION_H
#define KLEE_KINSTRUCTION_H

#include "KModule.h"
#include "klee/Config/Version.h"
#include "klee/Module/InstructionInfoTable.h"

#include "klee/Support/CompilerWarning.h"

DISABLE_WARNING_PUSH
DISABLE_WARNING_DEPRECATED_DECLARATIONS
#include "llvm/Support/DataTypes.h"
#include "llvm/Support/raw_ostream.h"
DISABLE_WARNING_POP

#include <unordered_map>
#include <vector>

namespace llvm {
Expand All @@ -28,34 +29,57 @@ class Instruction;

namespace klee {
class Executor;
struct InstructionInfo;
class KModule;
struct KBlock;

/// KInstruction - Intermediate instruction representation used
/// during execution.
struct KInstruction {
llvm::Instruction *inst;
const InstructionInfo *info;

/// Value numbers for each operand. -1 is an invalid value,
/// otherwise negative numbers are indices (negated and offset by
/// 2) into the module constant table and positive numbers are
/// register indices.
int *operands;
/// Destination register index.
unsigned dest;
KBlock *parent;

private:
// Instruction index in the basic block
unsigned index;
const unsigned globalIndex;

public:
KInstruction() = default;
explicit KInstruction(const KInstruction &ki);
/// Unique index for KFunction and KInstruction inside KModule
/// from 0 to [KFunction + KInstruction]
[[nodiscard]] unsigned getGlobalIndex() const;
/// Instruction index in the basic block
[[nodiscard]] unsigned getIndex() const;
/// Destination register index.
[[nodiscard]] unsigned getDest() const;

KInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
&_instructionToRegisterMap,
llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
unsigned &_globalIndexInc);

KInstruction() = delete;
explicit KInstruction(const KInstruction &ki) = delete;
virtual ~KInstruction();
std::string getSourceLocation() const;
std::string toString() const;

[[nodiscard]] size_t getLine() const;
[[nodiscard]] size_t getColumn() const;
[[nodiscard]] std::string getSourceFilepath() const;

[[nodiscard]] std::string getSourceLocationString() const;
[[nodiscard]] std::string toString() const;

[[nodiscard]] inline KBlock *getKBlock() const { return parent; }
[[nodiscard]] inline KFunction *getKFunction() const {
return getKBlock()->parent;
}
[[nodiscard]] inline KModule *getKModule() const {
return getKFunction()->parent;
}
};

struct KGEPInstruction : KInstruction {
Expand All @@ -70,8 +94,14 @@ struct KGEPInstruction : KInstruction {
uint64_t offset;

public:
KGEPInstruction() = default;
explicit KGEPInstruction(const KGEPInstruction &ki);
KGEPInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
&_instructionToRegisterMap,
llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
unsigned &_globalIndexInc)
: KInstruction(_instructionToRegisterMap, _inst, _km, _kb,
_globalIndexInc) {}
KGEPInstruction() = delete;
explicit KGEPInstruction(const KGEPInstruction &ki) = delete;
};
} // namespace klee

Expand Down
Loading

0 comments on commit c5c898f

Please sign in to comment.