1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
//===-- PTree.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_PTREE_H
#define KLEE_PTREE_H
#include "PTreeWriter.h"
#include "UserSearcher.h"
#include "klee/Core/BranchTypes.h"
#include "klee/Core/TerminationTypes.h"
#include "klee/Expr/Expr.h"
#include "klee/Support/ErrorHandling.h"
#include "llvm/ADT/PointerIntPair.h"
#include "llvm/Support/Casting.h"
#include <cstdint>
#include <variant>
namespace klee {
class ExecutionState;
class Executor;
class InMemoryPTree;
class InterpreterHandler;
class PTreeNode;
class Searcher;
/* PTreeNodePtr is used by the Random Path Searcher object to efficiently
record which PTreeNode belongs to it. PTree is a global structure that
captures all states, whereas a Random Path Searcher might only care about
a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which
Random Path Searchers PTreeNode belongs to. */
constexpr std::uint8_t PtrBitCount = 3;
using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
class PTreeNode {
public:
enum class NodeType : std::uint8_t { Basic, Annotated };
PTreeNode *parent{nullptr};
PTreeNodePtr left;
PTreeNodePtr right;
ExecutionState *state{nullptr};
PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
virtual ~PTreeNode() = default;
PTreeNode(const PTreeNode &) = delete;
PTreeNode &operator=(PTreeNode const &) = delete;
PTreeNode(PTreeNode &&) = delete;
PTreeNode &operator=(PTreeNode &&) = delete;
[[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; }
static bool classof(const PTreeNode *N) { return true; }
};
class AnnotatedPTreeNode : public PTreeNode {
inline static std::uint32_t nextID{1};
public:
std::uint32_t id{0};
std::uint32_t stateID{0};
std::uint32_t asmLine{0};
std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
~AnnotatedPTreeNode() override = default;
[[nodiscard]] NodeType getType() const override { return NodeType::Annotated; }
static bool classof(const PTreeNode *N) {
return N->getType() == NodeType::Annotated;
}
};
class PTree {
public:
enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent };
/// Branch from PTreeNode and attach states, convention: rightState is
/// parent
virtual void attach(PTreeNode *node, ExecutionState *leftState,
ExecutionState *rightState, BranchType reason) = 0;
/// Dump process tree in .dot format into os (debug)
virtual void dump(llvm::raw_ostream &os) = 0;
/// Remove node from tree
virtual void remove(PTreeNode *node) = 0;
/// Set termination type (on state removal)
virtual void setTerminationType(ExecutionState &state,
StateTerminationType type){}
virtual ~PTree() = default;
PTree(PTree const &) = delete;
PTree &operator=(PTree const &) = delete;
PTree(PTree &&) = delete;
PTree &operator=(PTree &&) = delete;
[[nodiscard]] virtual PTreeType getType() const = 0;
static bool classof(const PTreeNode *N) { return true; }
protected:
explicit PTree() noexcept = default;
};
/// @brief A pseudo process tree that does not maintain any nodes.
class NoopPTree final : public PTree {
public:
NoopPTree() noexcept = default;
~NoopPTree() override = default;
void attach(PTreeNode *node, ExecutionState *leftState,
ExecutionState *rightState,
BranchType reason) noexcept override{}
void dump(llvm::raw_ostream &os) noexcept override;
void remove(PTreeNode *node) noexcept override{}
[[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; };
static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; }
};
/// @brief An in-memory process tree required by RandomPathSearcher
class InMemoryPTree : public PTree {
public:
PTreeNodePtr root;
private:
/// Number of registered IDs ("users", e.g. RandomPathSearcher)
std::uint8_t registeredIds = 0;
virtual PTreeNode *createNode(PTreeNode *parent, ExecutionState *state);
virtual void updateBranchingNode(PTreeNode &node, BranchType reason){}
virtual void updateTerminatingNode(PTreeNode &node){}
public:
InMemoryPTree() noexcept = default;
explicit InMemoryPTree(ExecutionState &initialState) noexcept;
~InMemoryPTree() override = default;
void attach(PTreeNode *node, ExecutionState *leftState,
ExecutionState *rightState, BranchType reason) noexcept override;
void dump(llvm::raw_ostream &os) noexcept override;
std::uint8_t getNextId() noexcept;
void remove(PTreeNode *node) noexcept override;
[[nodiscard]] PTreeType getType() const override { return PTreeType::InMemory; };
static bool classof(const PTree *T) {
return (T->getType() == PTreeType::InMemory) || (T->getType() == PTreeType::Persistent);
}
};
/// @brief An in-memory process tree that also writes its nodes into an SQLite
/// database (ptree.db) with a PTreeWriter
class PersistentPTree : public InMemoryPTree {
PTreeWriter writer;
PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override;
void updateBranchingNode(PTreeNode &node, BranchType reason) override;
void updateTerminatingNode(PTreeNode &node) override;
public:
explicit PersistentPTree(ExecutionState &initialState,
InterpreterHandler &ih) noexcept;
~PersistentPTree() override = default;
void dump(llvm::raw_ostream &os) noexcept override;
void setTerminationType(ExecutionState &state,
StateTerminationType type) override;
[[nodiscard]] PTreeType getType() const override { return PTreeType::Persistent; };
static bool classof(const PTree *T) { return T->getType() == PTreeType::Persistent; }
};
std::unique_ptr<PTree> createPTree(ExecutionState &initialState, bool inMemory,
InterpreterHandler &ih);
} // namespace klee
#endif /* KLEE_PTREE_H */
|
