klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Searcher.h
Go to the documentation of this file.
1 //===-- Searcher.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_SEARCHER_H
11 #define KLEE_SEARCHER_H
12 
13 #include "llvm/Support/raw_ostream.h"
14 #include <vector>
15 #include <set>
16 #include <map>
17 #include <queue>
18 
19 namespace llvm {
20  class BasicBlock;
21  class Function;
22  class Instruction;
23  class raw_ostream;
24 }
25 
26 namespace klee {
27  template<class T> class DiscretePDF;
28  class ExecutionState;
29  class Executor;
30 
31  class Searcher {
32  public:
33  virtual ~Searcher();
34 
35  virtual ExecutionState &selectState() = 0;
36 
37  virtual void update(ExecutionState *current,
38  const std::set<ExecutionState*> &addedStates,
39  const std::set<ExecutionState*> &removedStates) = 0;
40 
41  virtual bool empty() = 0;
42 
43  // prints name of searcher as a klee_message()
44  // TODO: could probably make prettier or more flexible
45  virtual void printName(llvm::raw_ostream &os) {
46  os << "<unnamed searcher>\n";
47  }
48 
49  // pgbovine - to be called when a searcher gets activated and
50  // deactivated, say, by a higher-level searcher; most searchers
51  // don't need this functionality, so don't have to override.
52  virtual void activate() {}
53  virtual void deactivate() {}
54 
55  // utility functions
56 
57  void addState(ExecutionState *es, ExecutionState *current = 0) {
58  std::set<ExecutionState*> tmp;
59  tmp.insert(es);
60  update(current, tmp, std::set<ExecutionState*>());
61  }
62 
63  void removeState(ExecutionState *es, ExecutionState *current = 0) {
64  std::set<ExecutionState*> tmp;
65  tmp.insert(es);
66  update(current, std::set<ExecutionState*>(), tmp);
67  }
68 
70  DFS,
71  BFS,
80  };
81  };
82 
83  class DFSSearcher : public Searcher {
84  std::vector<ExecutionState*> states;
85 
86  public:
88  void update(ExecutionState *current,
89  const std::set<ExecutionState*> &addedStates,
90  const std::set<ExecutionState*> &removedStates);
91  bool empty() { return states.empty(); }
92  void printName(llvm::raw_ostream &os) {
93  os << "DFSSearcher\n";
94  }
95  };
96 
97  class BFSSearcher : public Searcher {
98  std::deque<ExecutionState*> states;
99 
100  public:
102  void update(ExecutionState *current,
103  const std::set<ExecutionState*> &addedStates,
104  const std::set<ExecutionState*> &removedStates);
105  bool empty() { return states.empty(); }
106  void printName(llvm::raw_ostream &os) {
107  os << "BFSSearcher\n";
108  }
109  };
110 
111  class RandomSearcher : public Searcher {
112  std::vector<ExecutionState*> states;
113 
114  public:
116  void update(ExecutionState *current,
117  const std::set<ExecutionState*> &addedStates,
118  const std::set<ExecutionState*> &removedStates);
119  bool empty() { return states.empty(); }
120  void printName(llvm::raw_ostream &os) {
121  os << "RandomSearcher\n";
122  }
123  };
124 
126  public:
127  enum WeightType {
134  };
135 
136  private:
140 
141  double getWeight(ExecutionState*);
142 
143  public:
146 
148  void update(ExecutionState *current,
149  const std::set<ExecutionState*> &addedStates,
150  const std::set<ExecutionState*> &removedStates);
151  bool empty();
152  void printName(llvm::raw_ostream &os) {
153  os << "WeightedRandomSearcher::";
154  switch(type) {
155  case Depth : os << "Depth\n"; return;
156  case QueryCost : os << "QueryCost\n"; return;
157  case InstCount : os << "InstCount\n"; return;
158  case CPInstCount : os << "CPInstCount\n"; return;
159  case MinDistToUncovered : os << "MinDistToUncovered\n"; return;
160  case CoveringNew : os << "CoveringNew\n"; return;
161  default : os << "<unknown type>\n"; return;
162  }
163  }
164  };
165 
166  class RandomPathSearcher : public Searcher {
168 
169  public:
170  RandomPathSearcher(Executor &_executor);
172 
174  void update(ExecutionState *current,
175  const std::set<ExecutionState*> &addedStates,
176  const std::set<ExecutionState*> &removedStates);
177  bool empty();
178  void printName(llvm::raw_ostream &os) {
179  os << "RandomPathSearcher\n";
180  }
181  };
182 
183  class MergingSearcher : public Searcher {
185  std::set<ExecutionState*> statesAtMerge;
187  llvm::Function *mergeFunction;
188 
189  private:
190  llvm::Instruction *getMergePoint(ExecutionState &es);
191 
192  public:
195 
197  void update(ExecutionState *current,
198  const std::set<ExecutionState*> &addedStates,
199  const std::set<ExecutionState*> &removedStates);
200  bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
201  void printName(llvm::raw_ostream &os) {
202  os << "MergingSearcher\n";
203  }
204  };
205 
206  class BumpMergingSearcher : public Searcher {
208  std::map<llvm::Instruction*, ExecutionState*> statesAtMerge;
210  llvm::Function *mergeFunction;
211 
212  private:
213  llvm::Instruction *getMergePoint(ExecutionState &es);
214 
215  public:
218 
220  void update(ExecutionState *current,
221  const std::set<ExecutionState*> &addedStates,
222  const std::set<ExecutionState*> &removedStates);
223  bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
224  void printName(llvm::raw_ostream &os) {
225  os << "BumpMergingSearcher\n";
226  }
227  };
228 
229  class BatchingSearcher : public Searcher {
231  double timeBudget;
233 
237 
238  public:
240  double _timeBudget,
241  unsigned _instructionBudget);
243 
245  void update(ExecutionState *current,
246  const std::set<ExecutionState*> &addedStates,
247  const std::set<ExecutionState*> &removedStates);
248  bool empty() { return baseSearcher->empty(); }
249  void printName(llvm::raw_ostream &os) {
250  os << "<BatchingSearcher> timeBudget: " << timeBudget
251  << ", instructionBudget: " << instructionBudget
252  << ", baseSearcher:\n";
253  baseSearcher->printName(os);
254  os << "</BatchingSearcher>\n";
255  }
256  };
257 
260  double time, startTime;
261  std::set<ExecutionState*> pausedStates;
262 
263  public:
266 
268  void update(ExecutionState *current,
269  const std::set<ExecutionState*> &addedStates,
270  const std::set<ExecutionState*> &removedStates);
271  bool empty() { return baseSearcher->empty() && pausedStates.empty(); }
272  void printName(llvm::raw_ostream &os) {
273  os << "IterativeDeepeningTimeSearcher\n";
274  }
275  };
276 
277  class InterleavedSearcher : public Searcher {
278  typedef std::vector<Searcher*> searchers_ty;
279 
281  unsigned index;
282 
283  public:
284  explicit InterleavedSearcher(const searchers_ty &_searchers);
286 
288  void update(ExecutionState *current,
289  const std::set<ExecutionState*> &addedStates,
290  const std::set<ExecutionState*> &removedStates);
291  bool empty() { return searchers[0]->empty(); }
292  void printName(llvm::raw_ostream &os) {
293  os << "<InterleavedSearcher> containing "
294  << searchers.size() << " searchers:\n";
295  for (searchers_ty::iterator it = searchers.begin(), ie = searchers.end();
296  it != ie; ++it)
297  (*it)->printName(os);
298  os << "</InterleavedSearcher>\n";
299  }
300  };
301 
302 }
303 
304 #endif
std::set< ExecutionState * > pausedStates
Definition: Searcher.h:261
llvm::Instruction * getMergePoint(ExecutionState &es)
Definition: Searcher.cpp:378
double getWeight(ExecutionState *)
Definition: Searcher.cpp:187
MergingSearcher(Executor &executor, Searcher *baseSearcher)
Definition: Searcher.cpp:366
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:249
void removeState(ExecutionState *es, ExecutionState *current=0)
Definition: Searcher.h:63
ExecutionState & selectState()
Definition: Searcher.cpp:601
searchers_ty searchers
Definition: Searcher.h:280
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
virtual void activate()
Definition: Searcher.h:52
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
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
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
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:272
std::vector< ExecutionState * > states
Definition: Searcher.h:112
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:224
Executor & executor
Definition: Searcher.h:184
virtual ~Searcher()
Definition: Searcher.cpp:57
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:120
virtual void printName(llvm::raw_ostream &os)
Definition: Searcher.h:45
ExecutionState & selectState()
Definition: Searcher.cpp:314
unsigned lastStartInstructions
Definition: Searcher.h:236
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:106
llvm::Function * mergeFunction
Definition: Searcher.h:187
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:92
ExecutionState & selectState()
Definition: Searcher.cpp:130
BatchingSearcher(Searcher *baseSearcher, double _timeBudget, unsigned _instructionBudget)
Definition: Searcher.cpp:494
WeightedRandomSearcher(WeightType type)
Definition: Searcher.cpp:160
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:152
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:100
std::set< ExecutionState * > statesAtMerge
Definition: Searcher.h:185
std::deque< ExecutionState * > states
Definition: Searcher.h:98
ExecutionState * lastState
Definition: Searcher.h:234
RandomPathSearcher(Executor &_executor)
Definition: Searcher.cpp:248
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:292
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
std::vector< ExecutionState * > states
Definition: Searcher.h:84
ExecutionState & selectState()
Definition: Searcher.cpp:255
unsigned instructionBudget
Definition: Searcher.h:232
virtual bool empty()=0
ExecutionState & selectState()
Definition: Searcher.cpp:96
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
virtual void deactivate()
Definition: Searcher.h:53
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:178
void update(ExecutionState *current, const std::set< ExecutionState * > &addedStates, const std::set< ExecutionState * > &removedStates)
Definition: Searcher.cpp:224
InterleavedSearcher(const searchers_ty &_searchers)
Definition: Searcher.cpp:590
llvm::Function * mergeFunction
Definition: Searcher.h:210
void addState(ExecutionState *es, ExecutionState *current=0)
Definition: Searcher.h:57
std::vector< Searcher * > searchers_ty
Definition: Searcher.h:278
void printName(llvm::raw_ostream &os)
Definition: Searcher.h:201