klee
Searcher.cpp
Go to the documentation of this file.
1//===-- Searcher.cpp ------------------------------------------------------===//
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#include "Searcher.h"
11
12#include "CoreStats.h"
13#include "ExecutionState.h"
14#include "Executor.h"
15#include "MergeHandler.h"
16#include "PTree.h"
17#include "StatsTracker.h"
18
20#include "klee/ADT/RNG.h"
24#include "klee/Module/KModule.h"
26#include "klee/System/Time.h"
27
28#include "llvm/IR/Constants.h"
29#include "llvm/IR/Instructions.h"
30#include "llvm/IR/Module.h"
31#include "llvm/Support/CommandLine.h"
32
33#include <cassert>
34#include <cmath>
35
36using namespace klee;
37using namespace llvm;
38
39
41
42ExecutionState &DFSSearcher::selectState() {
43 return *states.back();
44}
45
47 const std::vector<ExecutionState *> &addedStates,
48 const std::vector<ExecutionState *> &removedStates) {
49 // insert states
50 states.insert(states.end(), addedStates.begin(), addedStates.end());
51
52 // remove states
53 for (const auto state : removedStates) {
54 if (state == states.back()) {
55 states.pop_back();
56 } else {
57 auto it = std::find(states.begin(), states.end(), state);
58 assert(it != states.end() && "invalid state removed");
59 states.erase(it);
60 }
61 }
62}
63
65 return states.empty();
66}
67
68void DFSSearcher::printName(llvm::raw_ostream &os) {
69 os << "DFSSearcher\n";
70}
71
72
74
76 return *states.front();
77}
78
80 const std::vector<ExecutionState *> &addedStates,
81 const std::vector<ExecutionState *> &removedStates) {
82 // update current state
83 // Assumption: If new states were added KLEE forked, therefore states evolved.
84 // constraints were added to the current state, it evolved.
85 if (!addedStates.empty() && current &&
86 std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) {
87 auto pos = std::find(states.begin(), states.end(), current);
88 assert(pos != states.end());
89 states.erase(pos);
90 states.push_back(current);
91 }
92
93 // insert states
94 states.insert(states.end(), addedStates.begin(), addedStates.end());
95
96 // remove states
97 for (const auto state : removedStates) {
98 if (state == states.front()) {
99 states.pop_front();
100 } else {
101 auto it = std::find(states.begin(), states.end(), state);
102 assert(it != states.end() && "invalid state removed");
103 states.erase(it);
104 }
105 }
106}
107
109 return states.empty();
110}
111
112void BFSSearcher::printName(llvm::raw_ostream &os) {
113 os << "BFSSearcher\n";
114}
115
116
118
120
122 return *states[theRNG.getInt32() % states.size()];
123}
124
126 const std::vector<ExecutionState *> &addedStates,
127 const std::vector<ExecutionState *> &removedStates) {
128 // insert states
129 states.insert(states.end(), addedStates.begin(), addedStates.end());
130
131 // remove states
132 for (const auto state : removedStates) {
133 auto it = std::find(states.begin(), states.end(), state);
134 assert(it != states.end() && "invalid state removed");
135 states.erase(it);
136 }
137}
138
140 return states.empty();
141}
142
143void RandomSearcher::printName(llvm::raw_ostream &os) {
144 os << "RandomSearcher\n";
145}
146
147
149
152 theRNG{rng},
153 type(type) {
154
155 switch(type) {
156 case Depth:
157 case RP:
158 updateWeights = false;
159 break;
160 case InstCount:
161 case CPInstCount:
162 case QueryCost:
164 case CoveringNew:
165 updateWeights = true;
166 break;
167 default:
168 assert(0 && "invalid weight type");
169 }
170}
171
173 return *states->choose(theRNG.getDoubleL());
174}
175
177 switch(type) {
178 default:
179 case Depth:
180 return es->depth;
181 case RP:
182 return std::pow(0.5, es->depth);
183 case InstCount: {
185 es->pc->info->id);
186 double inv = 1. / std::max((uint64_t) 1, count);
187 return inv * inv;
188 }
189 case CPInstCount: {
190 StackFrame &sf = es->stack.back();
192 double inv = 1. / std::max((uint64_t) 1, count);
193 return inv;
194 }
195 case QueryCost:
196 return (es->queryMetaData.queryCost.toSeconds() < .1)
197 ? 1.
198 : 1. / es->queryMetaData.queryCost.toSeconds();
199 case CoveringNew:
200 case MinDistToUncovered: {
201 uint64_t md2u = computeMinDistToUncovered(es->pc,
202 es->stack.back().minDistToUncoveredOnReturn);
203
204 double invMD2U = 1. / (md2u ? md2u : 10000);
205 if (type == CoveringNew) {
206 double invCovNew = 0.;
207 if (es->instsSinceCovNew)
208 invCovNew = 1. / std::max(1, (int) es->instsSinceCovNew - 1000);
209 return (invCovNew * invCovNew + invMD2U * invMD2U);
210 } else {
211 return invMD2U * invMD2U;
212 }
213 }
214 }
215}
216
218 const std::vector<ExecutionState *> &addedStates,
219 const std::vector<ExecutionState *> &removedStates) {
220
221 // update current
222 if (current && updateWeights &&
223 std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end())
224 states->update(current, getWeight(current));
225
226 // insert states
227 for (const auto state : addedStates)
228 states->insert(state, getWeight(state));
229
230 // remove states
231 for (const auto state : removedStates)
232 states->remove(state);
233}
234
236 return states->empty();
237}
238
239void WeightedRandomSearcher::printName(llvm::raw_ostream &os) {
240 os << "WeightedRandomSearcher::";
241 switch(type) {
242 case Depth : os << "Depth\n"; return;
243 case RP : os << "RandomPath\n"; return;
244 case QueryCost : os << "QueryCost\n"; return;
245 case InstCount : os << "InstCount\n"; return;
246 case CPInstCount : os << "CPInstCount\n"; return;
247 case MinDistToUncovered : os << "MinDistToUncovered\n"; return;
248 case CoveringNew : os << "CoveringNew\n"; return;
249 default : os << "<unknown type>\n"; return;
250 }
251}
252
253
255
256// Check if n is a valid pointer and a node belonging to us
257#define IS_OUR_NODE_VALID(n) \
258 (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
259
261 : processTree{processTree},
262 theRNG{rng},
263 idBitMask{processTree.getNextId()} {};
264
266 unsigned flips=0, bits=0;
267 assert(processTree.root.getInt() & idBitMask && "Root should belong to the searcher");
268 PTreeNode *n = processTree.root.getPointer();
269 while (!n->state) {
270 if (!IS_OUR_NODE_VALID(n->left)) {
271 assert(IS_OUR_NODE_VALID(n->right) && "Both left and right nodes invalid");
272 assert(n != n->right.getPointer());
273 n = n->right.getPointer();
274 } else if (!IS_OUR_NODE_VALID(n->right)) {
275 assert(IS_OUR_NODE_VALID(n->left) && "Both right and left nodes invalid");
276 assert(n != n->left.getPointer());
277 n = n->left.getPointer();
278 } else {
279 if (bits==0) {
280 flips = theRNG.getInt32();
281 bits = 32;
282 }
283 --bits;
284 n = ((flips & (1U << bits)) ? n->left : n->right).getPointer();
285 }
286 }
287
288 return *n->state;
289}
290
292 const std::vector<ExecutionState *> &addedStates,
293 const std::vector<ExecutionState *> &removedStates) {
294 // insert states
295 for (auto es : addedStates) {
296 PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
297 PTreeNodePtr *childPtr;
298
299 childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
300 : &parent->right)
301 : &processTree.root;
302 while (pnode && !IS_OUR_NODE_VALID(*childPtr)) {
303 childPtr->setInt(childPtr->getInt() | idBitMask);
304 pnode = parent;
305 if (pnode)
306 parent = pnode->parent;
307
308 childPtr = parent
309 ? ((parent->left.getPointer() == pnode) ? &parent->left
310 : &parent->right)
311 : &processTree.root;
312 }
313 }
314
315 // remove states
316 for (auto es : removedStates) {
317 PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
318
319 while (pnode && !IS_OUR_NODE_VALID(pnode->left) &&
320 !IS_OUR_NODE_VALID(pnode->right)) {
321 auto childPtr =
322 parent ? ((parent->left.getPointer() == pnode) ? &parent->left
323 : &parent->right)
324 : &processTree.root;
325 assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours");
326 childPtr->setInt(childPtr->getInt() & ~idBitMask);
327 pnode = parent;
328 if (pnode)
329 parent = pnode->parent;
330 }
331 }
332}
333
336}
337
338void RandomPathSearcher::printName(llvm::raw_ostream &os) {
339 os << "RandomPathSearcher\n";
340}
341
342
344
346 : baseSearcher{baseSearcher} {};
347
349 assert(std::find(pausedStates.begin(), pausedStates.end(), &state) == pausedStates.end());
350 pausedStates.push_back(&state);
351 baseSearcher->update(nullptr, {}, {&state});
352}
353
355 auto it = std::find(pausedStates.begin(), pausedStates.end(), &state);
356 assert(it != pausedStates.end());
357 pausedStates.erase(it);
358 baseSearcher->update(nullptr, {&state}, {});
359}
360
362 assert(!baseSearcher->empty() && "base searcher is empty");
363
365 return baseSearcher->selectState();
366
367 // Iterate through all MergeHandlers
368 for (auto cur_mergehandler: mergeGroups) {
369 // Find one that has states that could be released
370 if (!cur_mergehandler->hasMergedStates()) {
371 continue;
372 }
373 // Find a state that can be prioritized
374 ExecutionState *es = cur_mergehandler->getPrioritizeState();
375 if (es) {
376 return *es;
377 } else {
379 llvm::errs() << "Preemptively releasing states\n";
380 }
381 // If no state can be prioritized, they all exceeded the amount of time we
382 // are willing to wait for them. Release the states that already arrived at close_merge.
383 cur_mergehandler->releaseStates();
384 }
385 }
386 // If we were not able to prioritize a merging state, just return some state
387 return baseSearcher->selectState();
388}
389
391 const std::vector<ExecutionState *> &addedStates,
392 const std::vector<ExecutionState *> &removedStates) {
393 // We have to check if the current execution state was just deleted, as to
394 // not confuse the nurs searchers
395 if (std::find(pausedStates.begin(), pausedStates.end(), current) == pausedStates.end()) {
396 baseSearcher->update(current, addedStates, removedStates);
397 }
398}
399
401 return baseSearcher->empty();
402}
403
404void MergingSearcher::printName(llvm::raw_ostream &os) {
405 os << "MergingSearcher\n";
406}
407
408
410
411BatchingSearcher::BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget)
412 : baseSearcher{baseSearcher},
413 timeBudget{timeBudget},
414 instructionBudget{instructionBudget} {};
415
417 if (!lastState ||
418 (((timeBudget.toSeconds() > 0) &&
420 ((instructionBudget > 0) &&
422 if (lastState) {
424 auto t = timeBudget;
425 t *= 1.1;
426 if (delta > t) {
427 klee_message("increased time budget from %f to %f\n", timeBudget.toSeconds(), delta.toSeconds());
428 timeBudget = delta;
429 }
430 }
431 lastState = &baseSearcher->selectState();
434 return *lastState;
435 } else {
436 return *lastState;
437 }
438}
439
441 const std::vector<ExecutionState *> &addedStates,
442 const std::vector<ExecutionState *> &removedStates) {
443 // drop memoized state if it is marked for deletion
444 if (std::find(removedStates.begin(), removedStates.end(), lastState) != removedStates.end())
445 lastState = nullptr;
446 // update underlying searcher
447 baseSearcher->update(current, addedStates, removedStates);
448}
449
451 return baseSearcher->empty();
452}
453
454void BatchingSearcher::printName(llvm::raw_ostream &os) {
455 os << "<BatchingSearcher> timeBudget: " << timeBudget
456 << ", instructionBudget: " << instructionBudget
457 << ", baseSearcher:\n";
458 baseSearcher->printName(os);
459 os << "</BatchingSearcher>\n";
460}
461
462
464
466 : baseSearcher{baseSearcher} {};
467
469 ExecutionState &res = baseSearcher->selectState();
471 return res;
472}
473
475 const std::vector<ExecutionState *> &addedStates,
476 const std::vector<ExecutionState *> &removedStates) {
477
478 const auto elapsed = time::getWallTime() - startTime;
479
480 // update underlying searcher (filter paused states unknown to underlying searcher)
481 if (!removedStates.empty()) {
482 std::vector<ExecutionState *> alt = removedStates;
483 for (const auto state : removedStates) {
484 auto it = pausedStates.find(state);
485 if (it != pausedStates.end()) {
486 pausedStates.erase(it);
487 alt.erase(std::remove(alt.begin(), alt.end(), state), alt.end());
488 }
489 }
490 baseSearcher->update(current, addedStates, alt);
491 } else {
492 baseSearcher->update(current, addedStates, removedStates);
493 }
494
495 // update current: pause if time exceeded
496 if (current &&
497 std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end() &&
498 elapsed > time) {
499 pausedStates.insert(current);
500 baseSearcher->update(nullptr, {}, {current});
501 }
502
503 // no states left in underlying searcher: fill with paused states
504 if (baseSearcher->empty()) {
505 time *= 2U;
506 klee_message("increased time budget to %f\n", time.toSeconds());
507 std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
508 baseSearcher->update(nullptr, ps, std::vector<ExecutionState *>());
509 pausedStates.clear();
510 }
511}
512
514 return baseSearcher->empty() && pausedStates.empty();
515}
516
517void IterativeDeepeningTimeSearcher::printName(llvm::raw_ostream &os) {
518 os << "IterativeDeepeningTimeSearcher\n";
519}
520
521
523
524InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers) {
525 searchers.reserve(_searchers.size());
526 for (auto searcher : _searchers)
527 searchers.emplace_back(searcher);
528}
529
531 Searcher *s = searchers[--index].get();
532 if (index == 0) index = searchers.size();
533 return s->selectState();
534}
535
537 const std::vector<ExecutionState *> &addedStates,
538 const std::vector<ExecutionState *> &removedStates) {
539
540 // update underlying searchers
541 for (auto &searcher : searchers)
542 searcher->update(current, addedStates, removedStates);
543}
544
546 return searchers[0]->empty();
547}
548
549void InterleavedSearcher::printName(llvm::raw_ostream &os) {
550 os << "<InterleavedSearcher> containing " << searchers.size() << " searchers:\n";
551 for (const auto &searcher : searchers)
552 searcher->printName(os);
553 os << "</InterleavedSearcher>\n";
554}
Implementation of the region based merging.
#define IS_OUR_NODE_VALID(n)
Definition: Searcher.cpp:257
bool empty() override
Definition: Searcher.cpp:108
std::deque< ExecutionState * > states
Definition: Searcher.h:97
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:112
ExecutionState & selectState() override
Definition: Searcher.cpp:75
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:79
ExecutionState & selectState() override
Definition: Searcher.cpp:416
std::unique_ptr< Searcher > baseSearcher
Definition: Searcher.h:245
unsigned lastStartInstructions
Definition: Searcher.h:251
BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget)
Definition: Searcher.cpp:411
ExecutionState * lastState
Definition: Searcher.h:249
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:440
bool empty() override
Definition: Searcher.cpp:450
time::Span timeBudget
Definition: Searcher.h:246
unsigned instructionBudget
Definition: Searcher.h:247
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:454
time::Point lastStartTime
Definition: Searcher.h:250
StatisticRecord statistics
std::vector< ExecutionState * > states
Definition: Searcher.h:81
bool empty() override
Definition: Searcher.cpp:64
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:68
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:46
ExecutionState representing a path under exploration.
stack_ty stack
Stack representing the current instruction stream.
SolverQueryMetaData queryMetaData
Statistics and information.
std::uint32_t depth
Exploration depth, i.e., number of times KLEE branched for this state.
std::uint32_t instsSinceCovNew
Counts how many instructions were executed since the last new instruction was covered.
KInstIterator pc
Pointer to instruction to be executed after the current instruction.
ExecutionState & selectState() override
Definition: Searcher.cpp:530
std::vector< std::unique_ptr< Searcher > > searchers
Definition: Searcher.h:296
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:549
bool empty() override
Definition: Searcher.cpp:545
InterleavedSearcher(const std::vector< Searcher * > &searchers)
Definition: Searcher.cpp:524
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:536
std::unique_ptr< Searcher > baseSearcher
Definition: Searcher.h:274
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:517
std::set< ExecutionState * > pausedStates
Definition: Searcher.h:277
ExecutionState & selectState() override
Definition: Searcher.cpp:468
IterativeDeepeningTimeSearcher(Searcher *baseSearcher)
Definition: Searcher.cpp:465
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:474
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:390
std::unique_ptr< Searcher > baseSearcher
Definition: Searcher.h:203
ExecutionState & selectState() override
Definition: Searcher.cpp:361
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:404
MergingSearcher(Searcher *baseSearcher)
Definition: Searcher.cpp:345
std::vector< MergeHandler * > mergeGroups
Definition: Searcher.h:222
void continueState(ExecutionState &state)
Continue a paused state.
Definition: Searcher.cpp:354
std::vector< ExecutionState * > pausedStates
States that have been paused by the 'pauseState' function.
Definition: Searcher.h:206
bool empty() override
Definition: Searcher.cpp:400
void pauseState(ExecutionState &state)
Definition: Searcher.cpp:348
ExecutionState * state
Definition: PTree.h:35
PTreeNode * parent
Definition: PTree.h:31
PTreeNodePtr right
Definition: PTree.h:34
PTreeNodePtr left
Definition: PTree.h:33
PTreeNodePtr root
Definition: PTree.h:47
Definition: RNG.h:14
double getDoubleL()
Definition: RNG.cpp:127
unsigned int getInt32()
Definition: RNG.cpp:82
ExecutionState & selectState() override
Definition: Searcher.cpp:265
RandomPathSearcher(PTree &processTree, RNG &rng)
Definition: Searcher.cpp:260
const uint8_t idBitMask
Definition: Searcher.h:179
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:338
bool empty() override
Definition: Searcher.cpp:334
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:291
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:125
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:143
bool empty() override
Definition: Searcher.cpp:139
RandomSearcher(RNG &rng)
Definition: Searcher.cpp:119
std::vector< ExecutionState * > states
Definition: Searcher.h:110
ExecutionState & selectState() override
Definition: Searcher.cpp:121
virtual ExecutionState & selectState()=0
uint64_t getIndexedValue(const Statistic &s, unsigned index) const
Definition: Statistics.h:142
uint64_t getValue(const Statistic &s) const
Definition: Statistics.h:120
void update(ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override
Definition: Searcher.cpp:217
ExecutionState & selectState() override
Definition: Searcher.cpp:172
WeightedRandomSearcher(WeightType type, RNG &rng)
Definition: Searcher.cpp:150
void printName(llvm::raw_ostream &os) override
Prints name of searcher as a klee_message().
Definition: Searcher.cpp:239
std::unique_ptr< DiscretePDF< ExecutionState *, ExecutionStateIDCompare > > states
Definition: Searcher.h:138
double getWeight(ExecutionState *)
Definition: Searcher.cpp:176
Statistic states
Statistic instructions
Point getWallTime()
Returns point in time using a monotonic steady clock.
Definition: Time.cpp:206
Definition: main.cpp:291
uint64_t computeMinDistToUncovered(const KInstruction *ki, uint64_t minDistAtRA)
llvm::PointerIntPair< PTreeNode *, PtrBitCount, uint8_t > PTreeNodePtr
Definition: PTree.h:27
llvm::cl::opt< bool > DebugLogIncompleteMerge
void klee_message(const char *msg,...) __attribute__((format(printf
llvm::cl::opt< bool > UseIncompleteMerge
StatisticManager * theStatisticManager
Definition: Statistics.cpp:57
unsigned id
The instruction id.
const InstructionInfo * info
Definition: KInstruction.h:35
time::Span queryCost
Costs for all queries issued for this state.
Definition: Solver.h:29
CallPathNode * callPathNode
double toSeconds() const
Definition: Time.cpp:163