Skip to content

Commit 37f0da6

Browse files
ladisginmisonijnik
authored andcommitted
Memory optimize, remove InstructionInfoTable, add immutable list for symbolics
1 parent f5f7574 commit 37f0da6

33 files changed

+3585
-810
lines changed

include/klee/ADT/ImmutableList.h

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
//===---- ImmutableList.h ---------------------------------------*- C++ -*-===//
2+
//
3+
// The KLEE Symbolic Virtual Machine
4+
//
5+
// This file is distributed under the University of Illinois Open Source
6+
// License. See LICENSE.TXT for details.
7+
//
8+
//===----------------------------------------------------------------------===//
9+
10+
#ifndef KLEE_IMMUTABLELIST_H
11+
#define KLEE_IMMUTABLELIST_H
12+
13+
#include <memory>
14+
#include <vector>
15+
16+
namespace klee {
17+
18+
template <typename T> class ImmutableList {
19+
struct ImmutableListNode {
20+
std::shared_ptr<ImmutableListNode> prev;
21+
const size_t prev_len;
22+
std::vector<T> values;
23+
24+
[[nodiscard]] size_t size() const { return prev_len + values.size(); }
25+
26+
ImmutableListNode() : prev(nullptr), prev_len(0), values() {}
27+
28+
explicit ImmutableListNode(const ImmutableList<T> &il)
29+
: prev_len(il.size()), values() {
30+
std::shared_ptr<ImmutableListNode> pr = il.node;
31+
while (pr && pr->values.empty()) {
32+
pr = pr->prev;
33+
}
34+
if (pr && pr->size()) {
35+
prev = pr;
36+
} else {
37+
prev = nullptr;
38+
}
39+
}
40+
};
41+
42+
std::shared_ptr<ImmutableListNode> node;
43+
44+
public:
45+
[[nodiscard]] size_t size() const { return node ? node->size() : 0; }
46+
47+
struct iterator {
48+
const ImmutableListNode *rootNode;
49+
std::unique_ptr<iterator> it;
50+
size_t get;
51+
52+
public:
53+
explicit iterator(const ImmutableListNode *p)
54+
: rootNode(p), it(nullptr), get(0) {
55+
if (rootNode && rootNode->prev.get()) {
56+
it = std::make_unique<iterator>(rootNode->prev.get());
57+
}
58+
}
59+
60+
bool operator==(const iterator &b) const {
61+
return rootNode == b.rootNode && get == b.get;
62+
}
63+
64+
bool operator!=(const iterator &b) const { return !(*this == b); }
65+
66+
iterator &operator++() {
67+
++get;
68+
if (get < rootNode->prev_len) {
69+
it->operator++();
70+
}
71+
return *this;
72+
}
73+
74+
const T &operator*() const {
75+
if (get < rootNode->prev_len) {
76+
return **it;
77+
}
78+
return rootNode->values[get - rootNode->prev_len];
79+
}
80+
81+
const T &operator->() const { return **this; }
82+
};
83+
84+
[[nodiscard]] iterator begin() const { return iterator(node.get()); }
85+
86+
[[nodiscard]] iterator end() const {
87+
auto it = iterator(node.get());
88+
it.get = size();
89+
return it;
90+
}
91+
92+
void push_back(T &&value) {
93+
if (!node) {
94+
node = std::make_shared<ImmutableListNode>();
95+
}
96+
node->values.push_back(std::move(value));
97+
}
98+
99+
ImmutableList() : node(){};
100+
ImmutableList(const ImmutableList<T> &il)
101+
: node(std::make_shared<ImmutableListNode>(il)) {}
102+
};
103+
104+
} // namespace klee
105+
106+
#endif /* KLEE_IMMUTABLELIST_H */

include/klee/Core/Interpreter.h

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,6 @@ class ExecutionState;
4141
struct SarifReport;
4242
class Interpreter;
4343
class TreeStreamWriter;
44-
class InstructionInfoTable;
4544

4645
class InterpreterHandler {
4746
public:
@@ -61,6 +60,12 @@ class InterpreterHandler {
6160
const char *suffix, bool isError = false) = 0;
6261
};
6362

63+
/// [File][Line][Column] -> Opcode
64+
using FLCtoOpcode = std::unordered_map<
65+
std::string,
66+
std::unordered_map<
67+
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
68+
6469
class Interpreter {
6570
public:
6671
enum class GuidanceKind {
@@ -140,9 +145,9 @@ class Interpreter {
140145
setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
141146
std::vector<std::unique_ptr<llvm::Module>> &libsModules,
142147
const ModuleOptions &opts,
143-
const std::unordered_set<std::string> &mainModuleFunctions,
144-
const std::unordered_set<std::string> &mainModuleGlobals,
145-
std::unique_ptr<InstructionInfoTable> origInfos) = 0;
148+
std::set<std::string> &&mainModuleFunctions,
149+
std::set<std::string> &&mainModuleGlobals,
150+
FLCtoOpcode &&origInstructions) = 0;
146151

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

195200
virtual void
196201
getCoveredLines(const ExecutionState &state,
197-
std::map<const std::string *, std::set<unsigned>> &res) = 0;
202+
std::map<std::string, std::set<unsigned>> &res) = 0;
198203

199204
virtual void getBlockPath(const ExecutionState &state,
200205
std::string &blockPath) = 0;

include/klee/Module/InstructionInfoTable.h

Lines changed: 0 additions & 113 deletions
This file was deleted.

include/klee/Module/KInstruction.h

Lines changed: 43 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -10,16 +10,17 @@
1010
#ifndef KLEE_KINSTRUCTION_H
1111
#define KLEE_KINSTRUCTION_H
1212

13+
#include "KModule.h"
1314
#include "klee/Config/Version.h"
14-
#include "klee/Module/InstructionInfoTable.h"
15-
1615
#include "klee/Support/CompilerWarning.h"
16+
1717
DISABLE_WARNING_PUSH
1818
DISABLE_WARNING_DEPRECATED_DECLARATIONS
1919
#include "llvm/Support/DataTypes.h"
2020
#include "llvm/Support/raw_ostream.h"
2121
DISABLE_WARNING_POP
2222

23+
#include <unordered_map>
2324
#include <vector>
2425

2526
namespace llvm {
@@ -28,34 +29,57 @@ class Instruction;
2829

2930
namespace klee {
3031
class Executor;
31-
struct InstructionInfo;
3232
class KModule;
3333
struct KBlock;
3434

3535
/// KInstruction - Intermediate instruction representation used
3636
/// during execution.
3737
struct KInstruction {
3838
llvm::Instruction *inst;
39-
const InstructionInfo *info;
4039

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

47+
private:
5048
// Instruction index in the basic block
51-
unsigned index;
49+
const unsigned globalIndex;
5250

5351
public:
54-
KInstruction() = default;
55-
explicit KInstruction(const KInstruction &ki);
52+
/// Unique index for KFunction and KInstruction inside KModule
53+
/// from 0 to [KFunction + KInstruction]
54+
[[nodiscard]] unsigned getGlobalIndex() const;
55+
/// Instruction index in the basic block
56+
[[nodiscard]] unsigned getIndex() const;
57+
/// Destination register index.
58+
[[nodiscard]] unsigned getDest() const;
59+
60+
KInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
61+
&_instructionToRegisterMap,
62+
llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
63+
unsigned &_globalIndexInc);
64+
65+
KInstruction() = delete;
66+
explicit KInstruction(const KInstruction &ki) = delete;
5667
virtual ~KInstruction();
57-
std::string getSourceLocation() const;
58-
std::string toString() const;
68+
69+
[[nodiscard]] size_t getLine() const;
70+
[[nodiscard]] size_t getColumn() const;
71+
[[nodiscard]] std::string getSourceFilepath() const;
72+
73+
[[nodiscard]] std::string getSourceLocationString() const;
74+
[[nodiscard]] std::string toString() const;
75+
76+
[[nodiscard]] inline KBlock *getKBlock() const { return parent; }
77+
[[nodiscard]] inline KFunction *getKFunction() const {
78+
return getKBlock()->parent;
79+
}
80+
[[nodiscard]] inline KModule *getKModule() const {
81+
return getKFunction()->parent;
82+
}
5983
};
6084

6185
struct KGEPInstruction : KInstruction {
@@ -70,8 +94,14 @@ struct KGEPInstruction : KInstruction {
7094
uint64_t offset;
7195

7296
public:
73-
KGEPInstruction() = default;
74-
explicit KGEPInstruction(const KGEPInstruction &ki);
97+
KGEPInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
98+
&_instructionToRegisterMap,
99+
llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
100+
unsigned &_globalIndexInc)
101+
: KInstruction(_instructionToRegisterMap, _inst, _km, _kb,
102+
_globalIndexInc) {}
103+
KGEPInstruction() = delete;
104+
explicit KGEPInstruction(const KGEPInstruction &ki) = delete;
75105
};
76106
} // namespace klee
77107

0 commit comments

Comments
 (0)