klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
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 "Common.h"
11 
12 #include "Searcher.h"
13 
14 #include "CoreStats.h"
15 #include "Executor.h"
16 #include "PTree.h"
17 #include "StatsTracker.h"
18 
19 #include "klee/ExecutionState.h"
20 #include "klee/Statistics.h"
25 #include "klee/Internal/ADT/RNG.h"
28 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
29 #include "llvm/IR/Constants.h"
30 #include "llvm/IR/Instructions.h"
31 #include "llvm/IR/Module.h"
32 #else
33 #include "llvm/Constants.h"
34 #include "llvm/Instructions.h"
35 #include "llvm/Module.h"
36 #endif
37 #include "llvm/Support/CallSite.h"
38 #include "llvm/Support/CFG.h"
39 #include "llvm/Support/CommandLine.h"
40 
41 #include <cassert>
42 #include <fstream>
43 #include <climits>
44 
45 using namespace klee;
46 using namespace llvm;
47 
48 namespace {
49  cl::opt<bool>
50  DebugLogMerge("debug-log-merge");
51 }
52 
53 namespace klee {
54  extern RNG theRNG;
55 }
56 
58 }
59 
61 
63  return *states.back();
64 }
65 
67  const std::set<ExecutionState*> &addedStates,
68  const std::set<ExecutionState*> &removedStates) {
69  states.insert(states.end(),
70  addedStates.begin(),
71  addedStates.end());
72  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
73  ie = removedStates.end(); it != ie; ++it) {
74  ExecutionState *es = *it;
75  if (es == states.back()) {
76  states.pop_back();
77  } else {
78  bool ok = false;
79 
80  for (std::vector<ExecutionState*>::iterator it = states.begin(),
81  ie = states.end(); it != ie; ++it) {
82  if (es==*it) {
83  states.erase(it);
84  ok = true;
85  break;
86  }
87  }
88 
89  assert(ok && "invalid state removed");
90  }
91  }
92 }
93 
95 
97  return *states.front();
98 }
99 
101  const std::set<ExecutionState*> &addedStates,
102  const std::set<ExecutionState*> &removedStates) {
103  states.insert(states.end(),
104  addedStates.begin(),
105  addedStates.end());
106  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
107  ie = removedStates.end(); it != ie; ++it) {
108  ExecutionState *es = *it;
109  if (es == states.front()) {
110  states.pop_front();
111  } else {
112  bool ok = false;
113 
114  for (std::deque<ExecutionState*>::iterator it = states.begin(),
115  ie = states.end(); it != ie; ++it) {
116  if (es==*it) {
117  states.erase(it);
118  ok = true;
119  break;
120  }
121  }
122 
123  assert(ok && "invalid state removed");
124  }
125  }
126 }
127 
129 
131  return *states[theRNG.getInt32()%states.size()];
132 }
133 
135  const std::set<ExecutionState*> &addedStates,
136  const std::set<ExecutionState*> &removedStates) {
137  states.insert(states.end(),
138  addedStates.begin(),
139  addedStates.end());
140  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
141  ie = removedStates.end(); it != ie; ++it) {
142  ExecutionState *es = *it;
143  bool ok = false;
144 
145  for (std::vector<ExecutionState*>::iterator it = states.begin(),
146  ie = states.end(); it != ie; ++it) {
147  if (es==*it) {
148  states.erase(it);
149  ok = true;
150  break;
151  }
152  }
153 
154  assert(ok && "invalid state removed");
155  }
156 }
157 
159 
161  : states(new DiscretePDF<ExecutionState*>()),
162  type(_type) {
163  switch(type) {
164  case Depth:
165  updateWeights = false;
166  break;
167  case InstCount:
168  case CPInstCount:
169  case QueryCost:
170  case MinDistToUncovered:
171  case CoveringNew:
172  updateWeights = true;
173  break;
174  default:
175  assert(0 && "invalid weight type");
176  }
177 }
178 
180  delete states;
181 }
182 
184  return *states->choose(theRNG.getDoubleL());
185 }
186 
188  switch(type) {
189  default:
190  case Depth:
191  return es->weight;
192  case InstCount: {
194  es->pc->info->id);
195  double inv = 1. / std::max((uint64_t) 1, count);
196  return inv * inv;
197  }
198  case CPInstCount: {
199  StackFrame &sf = es->stack.back();
200  uint64_t count = sf.callPathNode->statistics.getValue(stats::instructions);
201  double inv = 1. / std::max((uint64_t) 1, count);
202  return inv;
203  }
204  case QueryCost:
205  return (es->queryCost < .1) ? 1. : 1./es->queryCost;
206  case CoveringNew:
207  case MinDistToUncovered: {
208  uint64_t md2u = computeMinDistToUncovered(es->pc,
209  es->stack.back().minDistToUncoveredOnReturn);
210 
211  double invMD2U = 1. / (md2u ? md2u : 10000);
212  if (type==CoveringNew) {
213  double invCovNew = 0.;
214  if (es->instsSinceCovNew)
215  invCovNew = 1. / std::max(1, (int) es->instsSinceCovNew - 1000);
216  return (invCovNew * invCovNew + invMD2U * invMD2U);
217  } else {
218  return invMD2U * invMD2U;
219  }
220  }
221  }
222 }
223 
225  const std::set<ExecutionState*> &addedStates,
226  const std::set<ExecutionState*> &removedStates) {
227  if (current && updateWeights && !removedStates.count(current))
228  states->update(current, getWeight(current));
229 
230  for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(),
231  ie = addedStates.end(); it != ie; ++it) {
232  ExecutionState *es = *it;
233  states->insert(es, getWeight(es));
234  }
235 
236  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
237  ie = removedStates.end(); it != ie; ++it) {
238  states->remove(*it);
239  }
240 }
241 
243  return states->empty();
244 }
245 
247 
249  : executor(_executor) {
250 }
251 
253 }
254 
256  unsigned flips=0, bits=0;
258 
259  while (!n->data) {
260  if (!n->left) {
261  n = n->right;
262  } else if (!n->right) {
263  n = n->left;
264  } else {
265  if (bits==0) {
266  flips = theRNG.getInt32();
267  bits = 32;
268  }
269  --bits;
270  n = (flips&(1<<bits)) ? n->left : n->right;
271  }
272  }
273 
274  return *n->data;
275 }
276 
278  const std::set<ExecutionState*> &addedStates,
279  const std::set<ExecutionState*> &removedStates) {
280 }
281 
283  return executor.states.empty();
284 }
285 
287 
289  : executor(_executor),
290  baseSearcher(_baseSearcher),
291  mergeFunction(executor.kmodule->kleeMergeFn) {
292 }
293 
295  delete baseSearcher;
296 }
297 
299 
301  if (mergeFunction) {
302  Instruction *i = es.pc->inst;
303 
304  if (i->getOpcode()==Instruction::Call) {
305  CallSite cs(cast<CallInst>(i));
306  if (mergeFunction==cs.getCalledFunction())
307  return i;
308  }
309  }
310 
311  return 0;
312 }
313 
315 entry:
316  // out of base states, pick one to pop
317  if (baseSearcher->empty()) {
318  std::map<llvm::Instruction*, ExecutionState*>::iterator it =
319  statesAtMerge.begin();
320  ExecutionState *es = it->second;
321  statesAtMerge.erase(it);
322  ++es->pc;
323 
324  baseSearcher->addState(es);
325  }
326 
328 
329  if (Instruction *mp = getMergePoint(es)) {
330  std::map<llvm::Instruction*, ExecutionState*>::iterator it =
331  statesAtMerge.find(mp);
332 
334 
335  if (it==statesAtMerge.end()) {
336  statesAtMerge.insert(std::make_pair(mp, &es));
337  } else {
338  ExecutionState *mergeWith = it->second;
339  if (mergeWith->merge(es)) {
340  // hack, because we are terminating the state we need to let
341  // the baseSearcher know about it again
342  baseSearcher->addState(&es);
344  } else {
345  it->second = &es; // the bump
346  ++mergeWith->pc;
347 
348  baseSearcher->addState(mergeWith);
349  }
350  }
351 
352  goto entry;
353  } else {
354  return es;
355  }
356 }
357 
359  const std::set<ExecutionState*> &addedStates,
360  const std::set<ExecutionState*> &removedStates) {
361  baseSearcher->update(current, addedStates, removedStates);
362 }
363 
365 
367  : executor(_executor),
368  baseSearcher(_baseSearcher),
369  mergeFunction(executor.kmodule->kleeMergeFn) {
370 }
371 
373  delete baseSearcher;
374 }
375 
377 
379  if (mergeFunction) {
380  Instruction *i = es.pc->inst;
381 
382  if (i->getOpcode()==Instruction::Call) {
383  CallSite cs(cast<CallInst>(i));
384  if (mergeFunction==cs.getCalledFunction())
385  return i;
386  }
387  }
388 
389  return 0;
390 }
391 
393  while (!baseSearcher->empty()) {
395  if (getMergePoint(es)) {
396  baseSearcher->removeState(&es, &es);
397  statesAtMerge.insert(&es);
398  } else {
399  return es;
400  }
401  }
402 
403  // build map of merge point -> state list
404  std::map<Instruction*, std::vector<ExecutionState*> > merges;
405  for (std::set<ExecutionState*>::const_iterator it = statesAtMerge.begin(),
406  ie = statesAtMerge.end(); it != ie; ++it) {
407  ExecutionState &state = **it;
408  Instruction *mp = getMergePoint(state);
409 
410  merges[mp].push_back(&state);
411  }
412 
413  if (DebugLogMerge)
414  llvm::errs() << "-- all at merge --\n";
415  for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator
416  it = merges.begin(), ie = merges.end(); it != ie; ++it) {
417  if (DebugLogMerge) {
418  llvm::errs() << "\tmerge: " << it->first << " [";
419  for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(),
420  ie2 = it->second.end(); it2 != ie2; ++it2) {
421  ExecutionState *state = *it2;
422  llvm::errs() << state << ", ";
423  }
424  llvm::errs() << "]\n";
425  }
426 
427  // merge states
428  std::set<ExecutionState*> toMerge(it->second.begin(), it->second.end());
429  while (!toMerge.empty()) {
430  ExecutionState *base = *toMerge.begin();
431  toMerge.erase(toMerge.begin());
432 
433  std::set<ExecutionState*> toErase;
434  for (std::set<ExecutionState*>::iterator it = toMerge.begin(),
435  ie = toMerge.end(); it != ie; ++it) {
436  ExecutionState *mergeWith = *it;
437 
438  if (base->merge(*mergeWith)) {
439  toErase.insert(mergeWith);
440  }
441  }
442  if (DebugLogMerge && !toErase.empty()) {
443  llvm::errs() << "\t\tmerged: " << base << " with [";
444  for (std::set<ExecutionState*>::iterator it = toErase.begin(),
445  ie = toErase.end(); it != ie; ++it) {
446  if (it!=toErase.begin()) llvm::errs() << ", ";
447  llvm::errs() << *it;
448  }
449  llvm::errs() << "]\n";
450  }
451  for (std::set<ExecutionState*>::iterator it = toErase.begin(),
452  ie = toErase.end(); it != ie; ++it) {
453  std::set<ExecutionState*>::iterator it2 = toMerge.find(*it);
454  assert(it2!=toMerge.end());
455  executor.terminateState(**it);
456  toMerge.erase(it2);
457  }
458 
459  // step past merge and toss base back in pool
460  statesAtMerge.erase(statesAtMerge.find(base));
461  ++base->pc;
462  baseSearcher->addState(base);
463  }
464  }
465 
466  if (DebugLogMerge)
467  llvm::errs() << "-- merge complete, continuing --\n";
468 
469  return selectState();
470 }
471 
473  const std::set<ExecutionState*> &addedStates,
474  const std::set<ExecutionState*> &removedStates) {
475  if (!removedStates.empty()) {
476  std::set<ExecutionState *> alt = removedStates;
477  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
478  ie = removedStates.end(); it != ie; ++it) {
479  ExecutionState *es = *it;
480  std::set<ExecutionState*>::const_iterator it2 = statesAtMerge.find(es);
481  if (it2 != statesAtMerge.end()) {
482  statesAtMerge.erase(it2);
483  alt.erase(alt.find(es));
484  }
485  }
486  baseSearcher->update(current, addedStates, alt);
487  } else {
488  baseSearcher->update(current, addedStates, removedStates);
489  }
490 }
491 
493 
495  double _timeBudget,
496  unsigned _instructionBudget)
497  : baseSearcher(_baseSearcher),
498  timeBudget(_timeBudget),
499  instructionBudget(_instructionBudget),
500  lastState(0) {
501 
502 }
503 
505  delete baseSearcher;
506 }
507 
509  if (!lastState ||
512  if (lastState) {
513  double delta = util::getWallTime()-lastStartTime;
514  if (delta>timeBudget*1.1) {
515  llvm::errs() << "KLEE: increased time budget from " << timeBudget
516  << " to " << delta << "\n";
517  timeBudget = delta;
518  }
519  }
523  return *lastState;
524  } else {
525  return *lastState;
526  }
527 }
528 
530  const std::set<ExecutionState*> &addedStates,
531  const std::set<ExecutionState*> &removedStates) {
532  if (removedStates.count(lastState))
533  lastState = 0;
534  baseSearcher->update(current, addedStates, removedStates);
535 }
536 
537 /***/
538 
540  : baseSearcher(_baseSearcher),
541  time(1.) {
542 }
543 
545  delete baseSearcher;
546 }
547 
551  return res;
552 }
553 
555  const std::set<ExecutionState*> &addedStates,
556  const std::set<ExecutionState*> &removedStates) {
557  double elapsed = util::getWallTime() - startTime;
558 
559  if (!removedStates.empty()) {
560  std::set<ExecutionState *> alt = removedStates;
561  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
562  ie = removedStates.end(); it != ie; ++it) {
563  ExecutionState *es = *it;
564  std::set<ExecutionState*>::const_iterator it2 = pausedStates.find(es);
565  if (it2 != pausedStates.end()) {
566  pausedStates.erase(it);
567  alt.erase(alt.find(es));
568  }
569  }
570  baseSearcher->update(current, addedStates, alt);
571  } else {
572  baseSearcher->update(current, addedStates, removedStates);
573  }
574 
575  if (current && !removedStates.count(current) && elapsed>time) {
576  pausedStates.insert(current);
577  baseSearcher->removeState(current);
578  }
579 
580  if (baseSearcher->empty()) {
581  time *= 2;
582  llvm::errs() << "KLEE: increasing time budget to: " << time << "\n";
583  baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
584  pausedStates.clear();
585  }
586 }
587 
588 /***/
589 
590 InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers)
591  : searchers(_searchers),
592  index(1) {
593 }
594 
596  for (std::vector<Searcher*>::const_iterator it = searchers.begin(),
597  ie = searchers.end(); it != ie; ++it)
598  delete *it;
599 }
600 
602  Searcher *s = searchers[--index];
603  if (index==0) index = searchers.size();
604  return s->selectState();
605 }
606 
608  const std::set<ExecutionState*> &addedStates,
609  const std::set<ExecutionState*> &removedStates) {
610  for (std::vector<Searcher*>::const_iterator it = searchers.begin(),
611  ie = searchers.end(); it != ie; ++it)
612  (*it)->update(current, addedStates, removedStates);
613 }
std::set< ExecutionState * > pausedStates
Definition: Searcher.h:261
llvm::Instruction * getMergePoint(ExecutionState &es)
Definition: Searcher.cpp:378
bool merge(const ExecutionState &b)
double getWeight(ExecutionState *)
Definition: Searcher.cpp:187
MergingSearcher(Executor &executor, Searcher *baseSearcher)
Definition: Searcher.cpp:366
Definition: RNG.h:14
void removeState(ExecutionState *es, ExecutionState *current=0)
Definition: Searcher.h:63
std::set< ExecutionState * > states
Definition: Executor.h:110
uint64_t getValue(const Statistic &s) const
Definition: Statistics.h:120
ExecutionState & selectState()
Definition: Searcher.cpp:601
searchers_ty searchers
Definition: Searcher.h:280
StatisticManager * theStatisticManager
Definition: Statistics.cpp:57
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:358
ExecutionState & selectState()
Definition: Searcher.cpp:183
DiscretePDF< ExecutionState * > * states
Definition: Searcher.h:137
class PTreeNode Node
Definition: PTree.h:22
const InstructionInfo * info
Definition: KInstruction.h:31
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:554
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:277
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:607
RNG theRNG
Definition: Executor.cpp:271
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:472
ExecutionState & selectState()
Definition: Searcher.cpp:62
llvm::Instruction * getMergePoint(ExecutionState &es)
Definition: Searcher.cpp:300
std::map< llvm::Instruction *, ExecutionState * > statesAtMerge
Definition: Searcher.h:208
void terminateState(ExecutionState &state)
Definition: Executor.cpp:2695
BumpMergingSearcher(Executor &executor, Searcher *baseSearcher)
Definition: Searcher.cpp:288
virtual void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)=0
Searcher * baseSearcher
Definition: Searcher.h:230
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:66
Executor & executor
Definition: Searcher.h:184
double getWallTime()
Definition: Time.cpp:24
virtual ~Searcher()
Definition: Searcher.cpp:57
CallPathNode * callPathNode
Node * root
Definition: PTree.h:23
ExecutionState & selectState()
Definition: Searcher.cpp:314
unsigned lastStartInstructions
Definition: Searcher.h:236
uint64_t getIndexedValue(const Statistic &s, unsigned index) const
Definition: Statistics.h:142
PTree * processTree
Definition: Executor.h:115
llvm::Function * mergeFunction
Definition: Searcher.h:187
StatisticRecord statistics
ExecutionState & selectState()
Definition: Searcher.cpp:130
BatchingSearcher(Searcher *baseSearcher, double _timeBudget, unsigned _instructionBudget)
Definition: Searcher.cpp:494
WeightedRandomSearcher(WeightType type)
Definition: Searcher.cpp:160
uint64_t computeMinDistToUncovered(const KInstruction *ki, uint64_t minDistAtRA)
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:100
llvm::Instruction * inst
Definition: KInstruction.h:30
std::set< ExecutionState * > statesAtMerge
Definition: Searcher.h:185
ExecutionState * lastState
Definition: Searcher.h:234
RandomPathSearcher(Executor &_executor)
Definition: Searcher.cpp:248
virtual ExecutionState & selectState()=0
Searcher * baseSearcher
Definition: Searcher.h:186
ExecutionState & selectState()
Definition: Searcher.cpp:392
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:529
ExecutionState & selectState()
Definition: Searcher.cpp:508
ExecutionState & selectState()
Definition: Searcher.cpp:255
unsigned instructionBudget
Definition: Searcher.h:232
virtual bool empty()=0
ExecutionState & selectState()
Definition: Searcher.cpp:96
unsigned int getInt32()
Definition: RNG.cpp:69
IterativeDeepeningTimeSearcher(Searcher *baseSearcher)
Definition: Searcher.cpp:539
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:134
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:224
Statistic instructions
InterleavedSearcher(const searchers_ty &_searchers)
Definition: Searcher.cpp:590
double getDoubleL()
Definition: RNG.cpp:114
llvm::Function * mergeFunction
Definition: Searcher.h:210
void addState(ExecutionState *es, ExecutionState *current=0)
Definition: Searcher.h:57
Statistic states