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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
|
//===-- Searcher.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_SEARCHER_H
#define KLEE_SEARCHER_H
#include "ExecutionState.h"
#include "PTree.h"
#include "klee/ADT/RNG.h"
#include "klee/System/Time.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/raw_ostream.h"
#include <map>
#include <queue>
#include <set>
#include <vector>
namespace llvm {
class BasicBlock;
class Function;
class Instruction;
class raw_ostream;
}
namespace klee {
template<class T, class Comparator> class DiscretePDF;
class ExecutionState;
class Executor;
/// A Searcher implements an exploration strategy for the Executor by selecting
/// states for further exploration using different strategies or heuristics.
class Searcher {
public:
virtual ~Searcher() = default;
/// Selects a state for further exploration.
/// \return The selected state.
virtual ExecutionState &selectState() = 0;
/// Notifies searcher about new or deleted states.
/// \param current The currently selected state for exploration.
/// \param addedStates The newly branched states with `current` as common ancestor.
/// \param removedStates The states that will be terminated.
virtual void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) = 0;
/// \return True if no state left for exploration, False otherwise
virtual bool empty() = 0;
/// Prints name of searcher as a `klee_message()`.
// TODO: could probably made prettier or more flexible
virtual void printName(llvm::raw_ostream &os) = 0;
enum CoreSearchType : std::uint8_t {
DFS,
BFS,
RandomState,
RandomPath,
NURS_CovNew,
NURS_MD2U,
NURS_Depth,
NURS_RP,
NURS_ICnt,
NURS_CPICnt,
NURS_QC
};
};
/// DFSSearcher implements depth-first exploration. All states are kept in
/// insertion order. The last state is selected for further exploration.
class DFSSearcher final : public Searcher {
std::vector<ExecutionState*> states;
public:
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// BFSSearcher implements breadth-first exploration. When KLEE branches multiple
/// times for a single instruction, all new states have the same depth. Keep in
/// mind that the process tree (PTree) is a binary tree and hence the depth of
/// a state in that tree and its branch depth during BFS are different.
class BFSSearcher final : public Searcher {
std::deque<ExecutionState*> states;
public:
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// RandomSearcher picks a state randomly.
class RandomSearcher final : public Searcher {
std::vector<ExecutionState*> states;
RNG &theRNG;
public:
explicit RandomSearcher(RNG &rng);
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// The base class for all weighted searchers. Uses DiscretePDF as underlying
/// data structure.
class WeightedRandomSearcher final : public Searcher {
public:
enum WeightType : std::uint8_t {
Depth,
RP,
QueryCost,
InstCount,
CPInstCount,
MinDistToUncovered,
CoveringNew
};
private:
std::unique_ptr<DiscretePDF<ExecutionState*, ExecutionStateIDCompare>> states;
RNG &theRNG;
WeightType type;
bool updateWeights;
double getWeight(ExecutionState*);
public:
/// \param type The WeightType that determines the underlying heuristic.
/// \param RNG A random number generator.
WeightedRandomSearcher(WeightType type, RNG &rng);
~WeightedRandomSearcher() override = default;
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// RandomPathSearcher performs a random walk of the PTree to select a state.
/// PTree is a global data structure, however, a searcher can sometimes only
/// select from a subset of all states (depending on the update calls).
///
/// To support this, RandomPathSearcher has a subgraph view of PTree, in that it
/// only walks the PTreeNodes that it "owns". Ownership is stored in the
/// getInt method of the PTreeNodePtr class (which hides it in the pointer itself).
///
/// The current implementation of PTreeNodePtr supports only 3 instances of the
/// RandomPathSearcher. This is because the current PTreeNodePtr implementation
/// conforms to C++ and only steals the last 3 alignment bits. This restriction
/// could be relaxed slightly by an architecture-specific implementation of
/// PTreeNodePtr that also steals the top bits of the pointer.
///
/// The ownership bits are maintained in the update method.
class RandomPathSearcher final : public Searcher {
PTree &processTree;
RNG &theRNG;
// Unique bitmask of this searcher
const uint8_t idBitMask;
public:
/// \param processTree The process tree.
/// \param RNG A random number generator.
RandomPathSearcher(PTree &processTree, RNG &rng);
~RandomPathSearcher() override = default;
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
extern llvm::cl::opt<bool> UseIncompleteMerge;
class MergeHandler;
class MergingSearcher final : public Searcher {
friend class MergeHandler;
private:
std::unique_ptr<Searcher> baseSearcher;
/// States that have been paused by the 'pauseState' function
std::vector<ExecutionState*> pausedStates;
public:
/// \param baseSearcher The underlying searcher (takes ownership).
explicit MergingSearcher(Searcher *baseSearcher);
~MergingSearcher() override = default;
/// ExecutionStates currently paused from scheduling because they are
/// waiting to be merged in a klee_close_merge instruction
std::set<ExecutionState *> inCloseMerge;
/// Keeps track of all currently ongoing merges.
/// An ongoing merge is a set of states (stored in a MergeHandler object)
/// which branched from a single state which ran into a klee_open_merge(),
/// and not all states in the set have reached the corresponding
/// klee_close_merge() yet.
std::vector<MergeHandler *> mergeGroups;
/// Remove state from the searcher chain, while keeping it in the executor.
/// This is used here to 'freeze' a state while it is waiting for other
/// states in its merge group to reach the same instruction.
void pauseState(ExecutionState &state);
/// Continue a paused state
void continueState(ExecutionState &state);
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// BatchingSearcher selects a state from an underlying searcher and returns
/// that state for further exploration for a given time or a given number
/// of instructions.
class BatchingSearcher final : public Searcher {
std::unique_ptr<Searcher> baseSearcher;
bool timeBudgetEnabled;
time::Span timeBudget;
bool instructionBudgetEnabled;
unsigned instructionBudget;
ExecutionState *lastState {nullptr};
time::Point lastStartTime;
unsigned lastStartInstructions;
bool withinTimeBudget() const;
bool withinInstructionBudget() const;
public:
/// \param baseSearcher The underlying searcher (takes ownership).
/// \param timeBudget Time span a state gets selected before choosing a different one.
/// \param instructionBudget Number of instructions to re-select a state for.
BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget);
~BatchingSearcher() override = default;
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// IterativeDeepeningTimeSearcher implements time-based deepening. States
/// are selected from an underlying searcher. When a state reaches its time
/// limit it is paused (removed from underlying searcher). When the underlying
/// searcher runs out of states, the time budget is increased and all paused
/// states are revived (added to underlying searcher).
class IterativeDeepeningTimeSearcher final : public Searcher {
std::unique_ptr<Searcher> baseSearcher;
time::Point startTime;
time::Span time {time::seconds(1)};
std::set<ExecutionState*> pausedStates;
public:
/// \param baseSearcher The underlying searcher (takes ownership).
explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher);
~IterativeDeepeningTimeSearcher() override = default;
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
/// InterleavedSearcher selects states from a set of searchers in round-robin
/// manner. It is used for KLEE's default strategy where it switches between
/// RandomPathSearcher and WeightedRandomSearcher with CoveringNew metric.
class InterleavedSearcher final : public Searcher {
std::vector<std::unique_ptr<Searcher>> searchers;
unsigned index {1};
public:
/// \param searchers The underlying searchers (takes ownership).
explicit InterleavedSearcher(const std::vector<Searcher *> &searchers);
~InterleavedSearcher() override = default;
ExecutionState &selectState() override;
void update(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const std::vector<ExecutionState *> &removedStates) override;
bool empty() override;
void printName(llvm::raw_ostream &os) override;
};
} // klee namespace
#endif /* KLEE_SEARCHER_H */
|