 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
43.6% |
228 / 523 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
50.9% |
266 / 523 |
| |
|
Line Coverage: |
52.8% |
322 / 610 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Common.h"
4 :
5 : #include "Searcher.h"
6 :
7 : #include "CoreStats.h"
8 : #include "Executor.h"
9 : #include "PTree.h"
10 : #include "StatsTracker.h"
11 :
12 : #include "klee/ExecutionState.h"
13 : #include "klee/Statistics.h"
14 : #include "klee/Internal/Module/InstructionInfoTable.h"
15 : #include "klee/Internal/Module/KInstruction.h"
16 : #include "klee/Internal/Module/KModule.h"
17 : #include "klee/Internal/ADT/DiscretePDF.h"
18 : #include "klee/Internal/ADT/RNG.h"
19 : #include "klee/Internal/Support/ModuleUtil.h"
20 : #include "klee/Internal/System/Time.h"
21 :
22 : #include "llvm/Constants.h"
23 : #include "llvm/Instructions.h"
24 : #include "llvm/Module.h"
25 : #include "llvm/Support/CallSite.h"
26 : #include "llvm/Support/CFG.h"
27 : #include "llvm/Support/CommandLine.h"
28 :
29 : #include <cassert>
30 : #include <fstream>
31 : #include <climits>
32 :
33 : #include "klee/Internal/FIXME/sugar.h"
34 :
35 : using namespace klee;
36 : using namespace llvm;
37 :
38 : namespace {
39 : cl::opt<bool>
40 103: DebugLogMerge("debug-log-merge");
41 : }
42 :
43 : namespace klee {
44 : extern RNG theRNG;
45 : }
46 :
47 140: Searcher::~Searcher() {
140: branch 0 taken
140: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
140: branch 7 taken
48 140: }
49 :
50 : ///
51 :
52 10381031: ExecutionState &DFSSearcher::selectState() {
53 20762062: return *states.back();
54 : }
55 :
56 : void DFSSearcher::update(ExecutionState *current,
57 : const std::set<ExecutionState*> &addedStates,
58 10382870: const std::set<ExecutionState*> &removedStates) {
59 : states.insert(states.end(),
60 : addedStates.begin(),
61 20765740: addedStates.end());
512: branch 1 taken
10382870: branch 2 taken
62 10383894: foreach(it, removedStates.begin(), removedStates.end()) {
63 512: ExecutionState *es = *it;
497: branch 0 taken
15: branch 1 taken
64 1024: if (es == states.back()) {
65 497: states.pop_back();
66 : } else {
67 15: bool ok = false;
68 :
15: branch 0 taken
0: branch 1 not taken
69 45: foreach(it, states.begin(), states.end()) {
15: branch 0 taken
0: branch 1 not taken
70 15: if (es==*it) {
71 15: states.erase(it);
72 15: ok = true;
73 15: break;
74 : }
75 : }
76 :
0: branch 0 not taken
15: branch 1 taken
77 15: assert(ok && "invalid state removed");
78 : }
79 : }
80 10382870: }
81 :
82 : ///
83 :
84 : // FIXME: This stuff should not be here in this fashion. All we need
85 : // is some sort of observation interface so the searcher can watch
86 : // what happens to the execution state. Then PGSearcher can use
87 : // auxiliary tables for all the extra information it wants.
88 :
89 : // pgbovine - kinda gross, but dunno where else to put it:
90 : // only used if klee::userSearcherRequiresBranchSequences()
91 : // Key: two-branch pair of <branch instruction ID, TRUE side taken?>
92 : // Value: Keep a running tally (need a SIGNED int):
93 : // +1 if this pair has been seen in a terminated state
94 : // that has covered new code,
95 : // -1 if seen in terminated state that has NOT covered new code
96 : std::map< std::pair< std::pair<unsigned, bool>,
97 : std::pair<unsigned, bool> >,
98 103: int > termStatesBranchPairTally;
99 :
100 : // only used if klee::userSearcherRequiresBranchSequences()
101 : // contains two-branch adjacent sequences that have been seen thus
102 : // during ANY state that has TERMINATED
103 : // (implemented as a multiset so can count the number of terminated
104 : // states that has seen a particular branch pair)
105 : std::multiset< std::pair< std::pair<unsigned, bool>,
106 103: std::pair<unsigned, bool> > > seenBranchPairs;
107 :
108 0: ExecutionState &PGSearcher::selectState() {
0: branch 0 not taken
0: branch 1 not taken
109 0: assert(isActive);
110 :
111 0: const bool debug_print = false;
112 :
113 : // true iff you want original 'more random' behavior
114 0: const bool original_behavior = false;
115 :
116 : // continue running currentlyRunning until termination if possible;
0: branch 0 not taken
0: branch 1 not taken
117 0: if (!currentlyRunning) {
118 :
119 : // original behavior (phase out if new behavior works significantly
120 : // better)
121 : //
122 : // otherwise pick the one with the highest numbers of unseen branch
123 : // pairs (to break ties, choose the one with the fewest branches)
124 : //
125 : // implement an optimization whereby we only see whether the LAST
126 : // branch pair was novel since all other branch pairs will have
127 : // been seen before in SOME previously-terminated state
128 : if (original_behavior) {
129 : ExecutionState* curWinner = NULL;
130 : unsigned maxNumUnseenBranchPairs = 0;
131 : unsigned minNumBranches = 0;
132 :
133 : foreach(it, states.begin(), states.end()) {
134 : ExecutionState* curState = *it;
135 : bool lastBranchPairSeen = curState->isLastBranchPairSeen();
136 : unsigned numBranches = curState->branchDecisionsSequence.size();
137 :
138 : unsigned numUnseenBranchPairs = lastBranchPairSeen ? 0 : 1;
139 :
140 : // gotta start somewhere
141 : if (!curWinner) {
142 : curWinner = curState;
143 : maxNumUnseenBranchPairs = numUnseenBranchPairs;
144 : minNumBranches = numBranches;
145 : }
146 : else {
147 : // the PRIMARY key to compare is the number of unseen
148 : // branch pairs
149 : if (numUnseenBranchPairs > maxNumUnseenBranchPairs) {
150 : curWinner = curState;
151 : maxNumUnseenBranchPairs = numUnseenBranchPairs;
152 : minNumBranches = numBranches;
153 : }
154 : // in case of a TIE,
155 : // the SECONDARY key to compare is number of branches
156 : else if (numUnseenBranchPairs == maxNumUnseenBranchPairs) {
157 : if (numBranches < minNumBranches) {
158 : curWinner = curState;
159 : maxNumUnseenBranchPairs = numUnseenBranchPairs;
160 : minNumBranches = numBranches;
161 : }
162 : }
163 : }
164 : }
165 :
166 : // sanity check:
167 : assert(curWinner->branchDecisionsSequence.size() == minNumBranches);
168 :
169 : if (debug_print) {
170 : klee_message("selectState: pick new state from %u CANDIDATES",
171 : (unsigned) states.size());
172 : klee_message(" %u total seen branch pairs",
173 : (unsigned) seenBranchPairs.size());
174 : foreach(it, states.begin(), states.end()) {
175 : klee_message(" state: %p, %u branches, last branch pair seen %u",
176 : (void*)*it,
177 : (unsigned) (*it)->branchDecisionsSequence.size(),
178 : (*it)->isLastBranchPairSeen());
179 : }
180 :
181 : klee_message("NEW STATE TO RUN: %p, %u branches, last branch pair seen %u",
182 : (void*)curWinner,
183 : (unsigned) curWinner->branchDecisionsSequence.size(),
184 : curWinner->isLastBranchPairSeen());
185 : }
186 :
187 : // pick the new winner now!
188 : currentlyRunning = curWinner;
189 : }
190 : // pick the state to run whose branches pairs have the HIGHEST TALLY
191 : // (might be a crazy idea, but let's try it!) ... that is, the state
192 : // whose set of branch pairs have been seen the most by previously
193 : // terminated states that have achieved new coverage
194 : else {
195 : // List of ExecutionState* with maxTally
196 : std::vector<ExecutionState*> maxTallyStates;
197 :
198 0: int maxTally = INT_MIN;
199 :
0: branch 0 not taken
0: branch 1 not taken
200 0: foreach(it, states.begin(), states.end()) {
201 0: ExecutionState* curState = *it;
202 0: int curTally = curState->getBranchPairsTally();
203 :
0: branch 0 not taken
0: branch 1 not taken
204 0: if (curTally > maxTally) {
205 : maxTallyStates.clear();
206 0: maxTallyStates.push_back(curState);
207 0: maxTally = curTally;
208 : }
0: branch 0 not taken
0: branch 1 not taken
209 0: else if (curTally == maxTally) {
210 0: maxTallyStates.push_back(curState);
211 : }
212 : // else don't do anything
213 :
214 : if (debug_print) {
215 : klee_message(" candidate state %p tally %d",
216 : (void*)curState, curTally);
217 : }
218 : }
219 :
220 : // now select from amongst those with maximal tally
221 :
222 : // TODO: as an alternative, pick the one with the SMALLEST num.
223 : // branches rather than picking one at random
224 :
225 0: unsigned numStatesWithMaxTally = maxTallyStates.size();
226 0: unsigned dice_roll_res = theRNG.getInt32() % numStatesWithMaxTally;
227 :
228 0: currentlyRunning = maxTallyStates[dice_roll_res];
229 :
230 : if (debug_print) {
231 : klee_message(" dice-roll %u/%u - maxTally: %d, new state to run: %p, %u branches",
232 : dice_roll_res + 1,
233 : numStatesWithMaxTally,
234 : maxTally,
235 : (void*)currentlyRunning,
236 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
237 0: }
238 : }
239 : }
240 :
241 0: return *currentlyRunning;
242 : }
243 :
244 : void PGSearcher::update(ExecutionState *current,
245 : const std::set<ExecutionState*> &addedStates,
246 0: const std::set<ExecutionState*> &removedStates) {
247 0: const bool debug_print = false;
248 :
249 : // true iff you want original 'more random' behavior
250 0: const bool original_behavior = false;
251 :
252 0: unsigned num_added_states = addedStates.size();
253 :
254 : if (debug_print) {
255 : if ((num_added_states > 0) || (removedStates.size() > 0)) {
256 : klee_message("update - %d added, %u removed (current: %p), currentlyRunning: %p",
257 : num_added_states, (unsigned) removedStates.size(),
258 : (void*)current, (void*)currentlyRunning);
259 : }
260 : }
261 :
262 : // need to make sure that update() works properly even when PGSearcher
263 : // isn't active at the moment, since if this is chained together with
264 : // other searchers, update() still gets called even when it's inactive
265 : //
266 : // if !isActive, then don't bother doing path selection:
0: branch 0 not taken
0: branch 1 not taken
267 0: if (isActive) {
268 : // don't indent yet so don't screw up svn diffs ...
269 :
270 : // gotta start somewhere (beginning of execution):
0: branch 0 not taken
0: branch 1 not taken
271 0: if (!currentlyRunning && !current) {
0: branch 0 not taken
0: branch 1 not taken
272 0: assert(num_added_states == 1);
273 0: currentlyRunning = *(addedStates.begin());
274 : }
275 : else {
276 : // if one state forks into multiple states, then the
277 : // branchDecisionsSequence of each forked variant should be
278 : // IDENTICAL except for the FINAL pair (since they share
279 : // a common prefix), so pick the one whose FINAL pair has
280 : // not been seen before. If all final pairs have been
281 : // seen before, then pick one at random
0: branch 0 not taken
0: branch 1 not taken
282 0: if (num_added_states > 0) {
0: branch 0 not taken
0: branch 1 not taken
283 0: assert(currentlyRunning);
284 0: unsigned curNumBranches = currentlyRunning->branchDecisionsSequence.size();
285 :
286 : // if you've forked, you better have more than one branch
287 : // under your belt ...
0: branch 0 not taken
0: branch 1 not taken
288 0: assert(curNumBranches > 1);
289 :
290 : std::pair< std::pair<unsigned, bool>, std::pair<unsigned, bool> > curFinalPair =
291 : std::make_pair(currentlyRunning->branchDecisionsSequence[curNumBranches - 2],
292 0: currentlyRunning->branchDecisionsSequence[curNumBranches - 1]);
293 :
294 0: unsigned curFinalPairNumSeen = seenBranchPairs.count(curFinalPair);
295 0: bool curFinalPairUnseen = (curFinalPairNumSeen == 0);
296 :
297 : // by far the common case is that there is 1 added state, so
298 : // optimize for it:
0: branch 0 not taken
0: branch 1 not taken
299 0: if (num_added_states == 1) {
300 : // it's a competition between picking currentlyRunning and
301 : // newForkedState, which is forked off of currentlyRunning
302 0: ExecutionState* newForkedState = *(addedStates.begin());
303 0: unsigned newForkedStateNumBranches = newForkedState->branchDecisionsSequence.size();
304 :
305 : // they're forks of one another, so better be the same length!
0: branch 0 not taken
0: branch 1 not taken
306 0: assert(curNumBranches == newForkedStateNumBranches);
307 :
308 : // now grab the FINAL branch pair:
309 : std::pair< std::pair<unsigned, bool>, std::pair<unsigned, bool> > newFinalPair =
310 : std::make_pair(newForkedState->branchDecisionsSequence[newForkedStateNumBranches - 2],
311 0: newForkedState->branchDecisionsSequence[newForkedStateNumBranches - 1]);
312 :
313 0: unsigned newFinalPairNumSeen = seenBranchPairs.count(newFinalPair);
314 0: bool newFinalPairUnseen = (newFinalPairNumSeen == 0);
315 :
316 : // do a coin flip because it's a tie
0: branch 0 not taken
0: branch 1 not taken
317 0: if (curFinalPairUnseen == newFinalPairUnseen) {
318 : // the original behavior is to simply consider whether the final
319 : // pair has been seen or not; new behavior is to take
320 : // termStatesBranchPairTally into account
321 : if (original_behavior) {
322 : bool coin_toss_res = theRNG.getBool();
323 : if (coin_toss_res) {
324 : currentlyRunning = newForkedState;
325 : }
326 :
327 : if (debug_print) {
328 : klee_message(" unseen:(cur,new) (%u,%u) count:(%u,%u) tally:(%d,%d) FAST-CASE coin-toss %u - post-fork run state: %p, %u branches",
329 : curFinalPairUnseen,
330 : newFinalPairUnseen,
331 : curFinalPairNumSeen,
332 : newFinalPairNumSeen,
333 : termStatesBranchPairTally[curFinalPair],
334 : termStatesBranchPairTally[newFinalPair],
335 : coin_toss_res,
336 : (void*)currentlyRunning,
337 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
338 : }
339 : }
340 : else {
341 0: int curTally = termStatesBranchPairTally[curFinalPair];
342 0: int newTally = termStatesBranchPairTally[newFinalPair];
343 :
344 : // pick the pair with the higher tally since that's been
345 : // seen more by states that have achieved new coverage
0: branch 0 not taken
0: branch 1 not taken
346 0: if (newTally > curTally) {
347 0: currentlyRunning = newForkedState;
348 :
349 : if (debug_print) {
350 : klee_message(" unseen:(cur,new) (%u,%u) count:(%u,%u) tally:(%d,%d) FAST-CASE PICK NEW by tally - post-fork run state: %p, %u branches",
351 : curFinalPairUnseen,
352 : newFinalPairUnseen,
353 : curFinalPairNumSeen,
354 : newFinalPairNumSeen,
355 : curTally,
356 : newTally,
357 : (void*)currentlyRunning,
358 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
359 : }
360 : }
0: branch 0 not taken
0: branch 1 not taken
361 0: else if (newTally == curTally) {
362 0: bool coin_toss_res = theRNG.getBool();
0: branch 0 not taken
0: branch 1 not taken
363 0: if (coin_toss_res) {
364 0: currentlyRunning = newForkedState;
365 : }
366 :
367 : if (debug_print) {
368 : klee_message(" unseen:(cur,new) (%u,%u) count:(%u,%u) tally:(%d,%d) FAST-CASE coin-toss %u - post-fork run state: %p, %u branches",
369 : curFinalPairUnseen,
370 : newFinalPairUnseen,
371 : curFinalPairNumSeen,
372 : newFinalPairNumSeen,
373 : curTally,
374 : newTally,
375 : coin_toss_res,
376 : (void*)currentlyRunning,
377 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
378 : }
379 : }
380 : else {
381 : // maintain status quo
382 : if (debug_print) {
383 : klee_message(" unseen:(cur,new) (%u,%u) count:(%u,%u) tally:(%d,%d) FAST-CASE KEEP CUR by tally - post-fork run state: %p, %u branches",
384 : curFinalPairUnseen,
385 : newFinalPairUnseen,
386 : curFinalPairNumSeen,
387 : newFinalPairNumSeen,
388 : curTally,
389 : newTally,
390 : (void*)currentlyRunning,
391 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
392 : }
393 : }
394 : }
395 : }
396 : // newForkedState is more 'novel', so pick it to run:
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
397 0: else if (newFinalPairUnseen && (!curFinalPairUnseen)) {
398 0: currentlyRunning = newForkedState;
399 :
400 : if (debug_print) {
401 : klee_message(" unseen:(cur,new) (%u,%u) count:(%u,%u) tally:(%d,%d) PICK NEW post-fork run state: %p, %u branches",
402 : curFinalPairUnseen,
403 : newFinalPairUnseen,
404 : curFinalPairNumSeen,
405 : newFinalPairNumSeen,
406 : termStatesBranchPairTally[curFinalPair],
407 : termStatesBranchPairTally[newFinalPair],
408 : (void*)currentlyRunning,
409 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
410 : }
411 : }
412 : else {
413 : // else do nothing and maintain status quo
414 : if (debug_print) {
415 : klee_message(" unseen:(cur,new) (%u,%u) count:(%u,%u) tally:(%d,%d) KEEP CUR post-fork run state: %p, %u branches",
416 : curFinalPairUnseen,
417 : newFinalPairUnseen,
418 : curFinalPairNumSeen,
419 : newFinalPairNumSeen,
420 : termStatesBranchPairTally[curFinalPair],
421 : termStatesBranchPairTally[newFinalPair],
422 : (void*)currentlyRunning,
423 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
424 : }
425 : }
426 : }
427 : // slow path that always works in the general case:
428 : else {
429 : // TODO: implement tally behavior here too, except that
430 : // all these branches are always identical (for some weird
431 : // reason, maybe in how Klee handles multiway branches
432 : // - switch stmts - so we'll always resort to coin flip!
433 :
434 : // should end up containing all ExecutionState objects with
435 : // the final pair of branches unseen
436 : std::vector<ExecutionState*> statesWithFinalPairUnseen;
437 : // ... and already seen
438 : std::vector<ExecutionState*> statesWithFinalPairAlreadySeen;
439 :
440 : // start with the incumbent:
0: branch 0 not taken
0: branch 1 not taken
441 0: if (curFinalPairUnseen) {
442 0: statesWithFinalPairUnseen.push_back(currentlyRunning);
443 : }
444 : else {
445 0: statesWithFinalPairAlreadySeen.push_back(currentlyRunning);
446 : }
447 :
0: branch 1 not taken
0: branch 2 not taken
448 0: foreach(it, addedStates.begin(), addedStates.end()) {
449 0: ExecutionState* newForkedState = *it;
450 :
451 0: unsigned newForkedStateNumBranches = newForkedState->branchDecisionsSequence.size();
452 :
453 : // they're forks of one another, so better be the same length!
0: branch 0 not taken
0: branch 1 not taken
454 0: assert(curNumBranches == newForkedStateNumBranches);
455 :
456 : // now grab the FINAL branch pair:
457 : std::pair< std::pair<unsigned, bool>, std::pair<unsigned, bool> > newFinalPair =
458 : std::make_pair(newForkedState->branchDecisionsSequence[newForkedStateNumBranches - 2],
459 0: newForkedState->branchDecisionsSequence[newForkedStateNumBranches - 1]);
460 :
461 0: bool newFinalPairUnseen = (seenBranchPairs.count(newFinalPair) == 0);
462 :
0: branch 0 not taken
0: branch 1 not taken
463 0: if (newFinalPairUnseen) {
464 0: statesWithFinalPairUnseen.push_back(newForkedState);
465 : }
466 : else {
467 0: statesWithFinalPairAlreadySeen.push_back(newForkedState);
468 : }
469 : }
470 :
471 0: unsigned numStatesWithFinalPairUnseen = statesWithFinalPairUnseen.size();
472 0: unsigned numStatesWithFinalPairAlreadySeen = statesWithFinalPairAlreadySeen.size();
473 :
474 : // sanity check
475 : assert((numStatesWithFinalPairAlreadySeen + numStatesWithFinalPairUnseen) ==
0: branch 0 not taken
0: branch 1 not taken
476 0: (num_added_states + 1));
477 :
478 : // prefer states with final pair unseen if any exist ...
479 : // otherwise defer to states with final pair already seen
0: branch 0 not taken
0: branch 1 not taken
480 0: if (numStatesWithFinalPairUnseen > 0) {
481 0: unsigned dice_roll_res = theRNG.getInt32() % numStatesWithFinalPairUnseen;
482 0: currentlyRunning = statesWithFinalPairUnseen[dice_roll_res];
483 :
484 : if (debug_print) {
485 : klee_message(" FINAL PAIR UNSEEN dice-roll %u/%u - post-fork run state: %p, %u branches",
486 : dice_roll_res + 1,
487 : numStatesWithFinalPairUnseen,
488 : (void*)currentlyRunning,
489 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
490 : }
491 : }
492 : else {
0: branch 0 not taken
0: branch 1 not taken
493 0: assert(numStatesWithFinalPairAlreadySeen > 0);
494 0: unsigned dice_roll_res = theRNG.getInt32() % numStatesWithFinalPairAlreadySeen;
495 0: currentlyRunning = statesWithFinalPairAlreadySeen[dice_roll_res];
496 :
497 : if (debug_print) {
498 : klee_message(" FINAL PAIR ALREADY SEEN dice-roll %u/%u - post-fork run state: %p, %u branches",
499 : dice_roll_res + 1,
500 : numStatesWithFinalPairAlreadySeen,
501 : (void*)currentlyRunning,
502 : (unsigned) currentlyRunning->branchDecisionsSequence.size());
503 : }
504 0: }
505 : }
0: branch 0 not taken
0: branch 1 not taken
506 0: assert(currentlyRunning);
507 : }
508 : }
509 :
510 : // don't indent yet so don't screw up svn diffs ...
511 : }
512 : // !isActive
513 : else {
0: branch 0 not taken
0: branch 1 not taken
514 0: assert(!currentlyRunning);
515 : }
516 :
517 : // do all of this stuff below regardless of isActive
518 :
519 : // add new states ...
520 : states.insert(states.end(),
521 : addedStates.begin(),
522 0: addedStates.end());
523 : // remove old states and update statistics ...
0: branch 1 not taken
0: branch 2 not taken
524 0: foreach(it, removedStates.begin(), removedStates.end()) {
525 0: ExecutionState *es = *it;
526 :
527 : // dump all of its mySeenBranchPairs into the global
528 : // seenBranchPairs, so that the we can pick the next
529 : // state (in PGSearcher::selectState()) to run based
530 : // on who has the fewest number of already-seen branches:
531 : //
532 : // note that because seenBranchPairs is a multiset,
533 : // we want to insert elements from mySeenBranchPairs,
534 : // which is a set, so that we only count each branch
535 : // pair ONCE for every terminated state
536 : seenBranchPairs.insert(es->mySeenBranchPairs.begin(),
537 0: es->mySeenBranchPairs.end());
538 :
539 : // depending on whether es->coveredNew,
540 : // either increment or decrement termStatesBranchPairTally
0: branch 0 not taken
0: branch 1 not taken
541 0: foreach(it, es->mySeenBranchPairs.begin(), es->mySeenBranchPairs.end()) {
0: branch 0 not taken
0: branch 1 not taken
542 0: if (es->coveredNew) {
543 0: termStatesBranchPairTally[*it]++;
544 : }
545 : else {
546 0: termStatesBranchPairTally[*it]--;
547 : }
548 : }
549 :
550 : if (debug_print) {
551 : klee_message("--- JUST TERMINATED state %p - covnew: %u",
552 : (void*)es, es->coveredNew);
553 : /*
554 : foreach(it,
555 : termStatesBranchPairTally.begin(),
556 : termStatesBranchPairTally.end()) {
557 : std::pair< std::pair<unsigned, bool>, std::pair<unsigned, bool> > p = it->first;
558 : int tally = it->second;
559 : klee_message(" <(%u,%u), (%u,%u)> : %d tally",
560 : p.first.first,
561 : p.first.second,
562 : p.second.first,
563 : p.second.second,
564 : tally);
565 : }
566 : klee_message("---");
567 : */
568 : }
569 :
570 : // uh oh! we're done running our current state now ...
0: branch 0 not taken
0: branch 1 not taken
571 0: if (es == currentlyRunning) {
572 0: currentlyRunning = NULL;
573 : }
574 :
575 0: bool ok = false;
0: branch 0 not taken
0: branch 1 not taken
576 0: foreach(it, states.begin(), states.end()) {
0: branch 0 not taken
0: branch 1 not taken
577 0: if (es==*it) {
578 0: states.erase(it);
579 0: ok = true;
580 0: break;
581 : }
582 : }
583 :
0: branch 0 not taken
0: branch 1 not taken
584 0: assert(ok && "invalid state removed");
585 : }
586 0: }
587 :
588 : // keep currentlyRunning as NULL, and selectState should do the
589 : // right thing and choose a new state to set to currentlyRunning
590 0: void PGSearcher::activate() {
0: branch 0 not taken
0: branch 1 not taken
591 0: assert(!isActive);
0: branch 0 not taken
0: branch 1 not taken
592 0: assert(!currentlyRunning);
593 0: isActive = true;
594 0: klee_message("PGSearcher::activate()");
595 0: }
596 :
597 0: void PGSearcher::deactivate() {
0: branch 0 not taken
0: branch 1 not taken
598 0: assert(isActive);
599 0: isActive = false;
600 0: currentlyRunning = NULL;
601 0: klee_message("PGSearcher::deactivate()");
602 0: }
603 :
604 : ///
605 :
606 0: PGSupervisedSearcher::PGSupervisedSearcher(const std::vector<Searcher*> &_searchers)
607 : : searchers(_searchers),
608 : index(0),
609 : numTerminatedStates(0),
610 : numTerminatedCovnewStates(0),
611 : numTerminatedStatesCurSearcher(0),
612 : numTerminatedCovnewStatesCurSearcher(0),
613 0: numTermStatesSinceNewCov(0) {
614 0: approxStartTime = lastTimeTermStateHadNewCov = util::getWallTime();
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
615 0: foreach(it, searchers.begin(), searchers.end()) {
616 0: numTerminatedCovnewStatesLastSearcher.push_back(0);
617 : // start with these values for timeouts:
618 0: timeoutForSearcher.push_back(60);
619 : }
620 0: }
621 :
622 0: PGSupervisedSearcher::~PGSupervisedSearcher() {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
623 0: foreach(it, searchers.begin(), searchers.end())
0: branch 0 not taken
0: branch 1 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
0: branch 7 not taken
624 0: delete *it;
0: branch 4 not taken
0: branch 5 not taken
0: branch 11 not taken
0: branch 12 not taken
0: branch 18 not taken
0: branch 19 not taken
625 0: }
626 :
627 0: ExecutionState &PGSupervisedSearcher::selectState() {
628 : //const bool debug_print = false;
629 :
630 0: double curTime = util::getWallTime();
631 :
632 : // if current searcher sucks too much, switch to the next one:
633 : // the simplest thing is to get number of seconds since last time we
634 : // made progress in terms of reaching new coverage:
0: branch 0 not taken
0: branch 1 not taken
635 0: if ((curTime - lastTimeTermStateHadNewCov) > timeoutForSearcher[index]) {
636 0: searchers[index]->deactivate(); // PGSearcher needs this
637 :
638 0: numTerminatedCovnewStatesLastSearcher[index] = numTerminatedCovnewStatesCurSearcher;
639 :
640 0: index++;
641 :
642 0: unsigned num_searchers = searchers.size();
643 :
0: branch 0 not taken
0: branch 1 not taken
644 0: assert(num_searchers == numTerminatedCovnewStatesLastSearcher.size());
0: branch 0 not taken
0: branch 1 not taken
645 0: assert(num_searchers == timeoutForSearcher.size());
646 :
647 : // done making one round over all searchers:
0: branch 0 not taken
0: branch 1 not taken
648 0: if (index == num_searchers) {
649 0: unsigned max_new_states = 0;
650 0: unsigned max_ind = 0;
0: branch 0 not taken
0: branch 1 not taken
651 0: for (unsigned i = 0; i < num_searchers; i++) {
652 0: unsigned NTcnS = numTerminatedCovnewStatesLastSearcher[i];
0: branch 0 not taken
0: branch 1 not taken
653 0: if (NTcnS > max_new_states) {
654 0: max_new_states = NTcnS;
655 0: max_ind = i;
656 : }
657 : }
658 :
659 : // if SOMEBODY has gotten new coverage, reward the one
660 : // that got the most coverage ...
0: branch 0 not taken
0: branch 1 not taken
661 0: if (max_new_states > 0) {
662 0: timeoutForSearcher[max_ind] = (unsigned) (1.2 * timeoutForSearcher[max_ind]);
663 :
664 : // optionally, punish all other ones:
665 : /*
666 : for(unsigned i = 0; i < num_searchers; i++) {
667 : if (i == max_ind) {
668 : timeoutForSearcher[i] *= 1.5;
669 : }
670 : else {
671 : timeoutForSearcher[i] /= 1.2;
672 : }
673 : }
674 : */
675 : }
676 : // if NOBODY has gotten any new coverage,
677 : // then reset everything to baseline ...
678 : else {
0: branch 0 not taken
0: branch 1 not taken
679 0: for (unsigned i = 0; i < num_searchers; i++) {
680 0: timeoutForSearcher[i] = 60;
681 : }
682 : }
683 :
684 : // reset to beginning:
685 0: index = 0;
686 : }
687 :
688 0: searchers[index]->activate(); // PGSearcher needs this
689 :
690 : klee_message("PGSupervisedSearcher SWITCHING to searcher %u | time=%.4g NTS=%u NTcnS=%u csNTS=%u csNTcnS=%u NTSsnc=%u TFS_0=%u TFS_1=%u",
691 : index, curTime - approxStartTime,
692 : numTerminatedStates, numTerminatedCovnewStates,
693 : numTerminatedStatesCurSearcher, numTerminatedCovnewStatesCurSearcher,
694 : numTermStatesSinceNewCov,
695 : timeoutForSearcher[0],
696 0: timeoutForSearcher[1]);
697 :
698 : // TODO: this is hack to not make the switcher keep switching
699 : // indefinitely ... gotta come up with a cleaner solution
700 0: lastTimeTermStateHadNewCov = curTime;
701 : // reset:
702 0: numTerminatedStatesCurSearcher = 0;
703 0: numTerminatedCovnewStatesCurSearcher = 0;
704 : }
705 :
706 0: Searcher *s = searchers[index];
707 0: return s->selectState();
708 : }
709 :
710 : void PGSupervisedSearcher::update(ExecutionState *current,
711 : const std::set<ExecutionState*> &addedStates,
712 0: const std::set<ExecutionState*> &removedStates) {
713 0: const bool debug_print = false;
714 :
0: branch 1 not taken
0: branch 2 not taken
715 0: foreach(it, removedStates.begin(), removedStates.end()) {
716 0: numTerminatedStates++;
717 0: numTerminatedStatesCurSearcher++;
0: branch 0 not taken
0: branch 1 not taken
718 0: if ((*it)->coveredNew) {
719 0: numTerminatedCovnewStates++;
720 0: numTerminatedCovnewStatesCurSearcher++;
721 0: numTermStatesSinceNewCov = 0;
722 0: lastTimeTermStateHadNewCov = util::getWallTime();
723 : }
724 : else {
725 0: numTermStatesSinceNewCov++;
726 : }
727 : }
728 :
729 : if (debug_print) {
730 : double curTime = util::getWallTime();
731 : if (removedStates.size() > 0) {
732 : klee_message("PGSupervisedSearcher::update removed %d: NTS=%u (%u) NTcnS=%u (%u) propCovNew=%.3g (%.3g) NTSsnc=%u deltaLastCovTime=%.4g",
733 : (unsigned) removedStates.size(),
734 : numTerminatedStates,
735 : numTerminatedStatesCurSearcher,
736 : numTerminatedCovnewStates,
737 : numTerminatedCovnewStatesCurSearcher,
738 : float(numTerminatedCovnewStates) / numTerminatedStates,
739 : float(numTerminatedCovnewStatesCurSearcher) / numTerminatedStatesCurSearcher,
740 : numTermStatesSinceNewCov,
741 : curTime - lastTimeTermStateHadNewCov);
742 : }
743 : }
744 :
745 : // always keep all searchers up-to-date as to which states are
746 : // available to be run:
0: branch 0 not taken
0: branch 1 not taken
747 0: foreach(it, searchers.begin(), searchers.end())
748 0: (*it)->update(current, addedStates, removedStates);
749 0: }
750 :
751 : ///
752 :
753 3012: ExecutionState &RandomSearcher::selectState() {
754 9036: return *states[theRNG.getInt32()%states.size()];
755 : }
756 :
757 : void RandomSearcher::update(ExecutionState *current,
758 : const std::set<ExecutionState*> &addedStates,
759 4770: const std::set<ExecutionState*> &removedStates) {
760 : states.insert(states.end(),
761 : addedStates.begin(),
762 9540: addedStates.end());
117: branch 1 taken
4770: branch 2 taken
763 5004: foreach(it, removedStates.begin(), removedStates.end()) {
764 117: ExecutionState *es = *it;
765 117: bool ok = false;
766 :
377: branch 0 taken
0: branch 1 not taken
767 728: foreach(it, states.begin(), states.end()) {
117: branch 0 taken
260: branch 1 taken
768 377: if (es==*it) {
769 117: states.erase(it);
770 117: ok = true;
771 117: break;
772 : }
773 : }
774 :
0: branch 0 not taken
117: branch 1 taken
775 117: assert(ok && "invalid state removed");
776 : }
777 4770: }
778 :
779 : ///
780 :
781 : WeightedRandomSearcher::WeightedRandomSearcher(Executor &_executor,
782 10: WeightType _type)
783 : : executor(_executor),
784 : states(new DiscretePDF<ExecutionState*>()),
785 30: type(_type) {
5: branch 0 taken
5: branch 1 taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
786 10: switch(type) {
787 : case Depth:
788 5: updateWeights = false;
789 5: break;
790 : case InstCount:
791 : case CPInstCount:
792 : case QueryCost:
793 : case MinDistToUncovered:
794 : case CoveringNew:
795 5: updateWeights = true;
796 5: break;
797 : default:
798 0: assert(0 && "invalid weight type");
799 : }
800 10: }
801 :
802 10: WeightedRandomSearcher::~WeightedRandomSearcher() {
10: branch 0 taken
0: branch 1 not taken
10: branch 4 taken
10: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
803 10: delete states;
10: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
804 10: }
805 :
806 1112: ExecutionState &WeightedRandomSearcher::selectState() {
807 1112: return *states->choose(theRNG.getDoubleL());
808 : }
809 :
810 2336: double WeightedRandomSearcher::getWeight(ExecutionState *es) {
82: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
2254: branch 3 taken
0: branch 4 not taken
811 2336: switch(type) {
812 : default:
813 : case Depth:
814 82: return es->weight;
815 : case InstCount: {
816 : uint64_t count = theStatisticManager->getIndexedValue(stats::instructions,
817 0: es->pc->info->id);
818 0: double inv = 1. / std::max((uint64_t) 1, count);
819 0: return inv * inv;
820 : }
821 : case CPInstCount: {
822 0: StackFrame &sf = es->stack.back();
823 0: uint64_t count = sf.callPathNode->statistics.getValue(stats::instructions);
824 0: double inv = 1. / std::max((uint64_t) 1, count);
825 0: return inv;
826 : }
827 : case QueryCost:
2254: branch 0 taken
0: branch 1 not taken
828 2254: return (es->queryCost < .1) ? 1. : 1./es->queryCost;
829 : case CoveringNew:
830 : case MinDistToUncovered: {
831 : uint64_t md2u = computeMinDistToUncovered(es->pc,
832 0: es->stack.back().minDistToUncoveredOnReturn);
833 :
0: branch 0 not taken
0: branch 1 not taken
834 0: double invMD2U = 1. / (md2u ? md2u : 10000);
0: branch 0 not taken
0: branch 1 not taken
835 0: if (type==CoveringNew) {
836 0: double invCovNew = 0.;
0: branch 0 not taken
0: branch 1 not taken
837 0: if (es->instsSinceCovNew)
838 0: invCovNew = 1. / std::max(1, (int) es->instsSinceCovNew - 1000);
839 0: return (invCovNew * invCovNew + invMD2U * invMD2U);
840 : } else {
841 0: return invMD2U * invMD2U;
842 : }
843 : }
844 : }
845 : }
846 :
847 : void WeightedRandomSearcher::update(ExecutionState *current,
848 : const std::set<ExecutionState*> &addedStates,
849 4624: const std::set<ExecutionState*> &removedStates) {
4508: branch 0 taken
116: branch 1 taken
2254: branch 2 taken
2254: branch 3 taken
2172: branch 4 taken
82: branch 5 taken
2172: branch 6 taken
2452: branch 7 taken
850 6878: if (current && updateWeights && !removedStates.count(current))
851 2172: states->update(current, getWeight(current));
852 :
164: branch 1 taken
4624: branch 2 taken
853 4952: foreach(it, addedStates.begin(), addedStates.end()) {
854 164: ExecutionState *es = *it;
855 164: states->insert(es, getWeight(es));
856 : }
857 :
164: branch 1 taken
4624: branch 2 taken
858 4952: foreach(it, removedStates.begin(), removedStates.end()) {
859 164: states->remove(*it);
860 : }
861 4624: }
862 :
863 1672: bool WeightedRandomSearcher::empty() {
864 3344: return states->empty();
865 : }
866 :
867 : ///
868 :
869 0: RandomPathSearcher::RandomPathSearcher(Executor &_executor)
870 0: : executor(_executor) {
871 0: }
872 :
873 0: RandomPathSearcher::~RandomPathSearcher() {
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
874 0: }
875 :
876 0: ExecutionState &RandomPathSearcher::selectState() {
877 0: unsigned flips=0, bits=0;
878 0: PTree::Node *n = executor.processTree->root;
879 :
0: branch 0 not taken
0: branch 1 not taken
880 0: while (!n->data) {
0: branch 0 not taken
0: branch 1 not taken
881 0: if (!n->left) {
882 0: n = n->right;
0: branch 0 not taken
0: branch 1 not taken
883 0: } else if (!n->right) {
884 0: n = n->left;
885 : } else {
0: branch 0 not taken
0: branch 1 not taken
886 0: if (bits==0) {
887 0: flips = theRNG.getInt32();
888 0: bits = 32;
889 : }
890 0: --bits;
0: branch 0 not taken
0: branch 1 not taken
891 0: n = (flips&(1<<bits)) ? n->left : n->right;
892 : }
893 : }
894 :
895 0: return *n->data;
896 : }
897 :
898 : void RandomPathSearcher::update(ExecutionState *current,
899 : const std::set<ExecutionState*> &addedStates,
900 0: const std::set<ExecutionState*> &removedStates) {
901 0: }
902 :
903 0: bool RandomPathSearcher::empty() {
904 0: return executor.states.empty();
905 : }
906 :
907 : ///
908 :
909 0: BumpMergingSearcher::BumpMergingSearcher(Executor &_executor, Searcher *_baseSearcher)
910 : : executor(_executor),
911 : baseSearcher(_baseSearcher),
912 0: mergeFunction(executor.kmodule->kleeMergeFn) {
913 0: }
914 :
915 0: BumpMergingSearcher::~BumpMergingSearcher() {
0: branch 0 not taken
0: branch 1 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
0: branch 7 not taken
916 0: delete baseSearcher;
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
917 0: }
918 :
919 : ///
920 :
921 0: Instruction *BumpMergingSearcher::getMergePoint(ExecutionState &es) {
0: branch 0 not taken
0: branch 1 not taken
922 0: if (mergeFunction) {
923 0: Instruction *i = es.pc->inst;
924 :
0: branch 0 not taken
0: branch 1 not taken
925 0: if (i->getOpcode()==Instruction::Call) {
926 0: CallSite cs(cast<CallInst>(i));
0: branch 1 not taken
0: branch 2 not taken
927 0: if (mergeFunction==cs.getCalledFunction())
928 0: return i;
929 : }
930 : }
931 :
932 0: return 0;
933 : }
934 :
935 0: ExecutionState &BumpMergingSearcher::selectState() {
936 0: entry:
937 : // out of base states, pick one to pop
0: branch 1 not taken
0: branch 2 not taken
938 0: if (baseSearcher->empty()) {
939 0: let(it, statesAtMerge.begin());
940 0: ExecutionState *es = it->second;
941 0: statesAtMerge.erase(it);
942 0: ++es->pc;
943 :
944 0: baseSearcher->addState(es);
945 : }
946 :
947 0: ExecutionState &es = baseSearcher->selectState();
948 :
0: branch 1 not taken
0: branch 2 not taken
949 0: if (Instruction *mp = getMergePoint(es)) {
950 0: let(it, statesAtMerge.find(mp));
951 :
952 0: baseSearcher->removeState(&es);
953 :
0: branch 0 not taken
0: branch 1 not taken
954 0: if (it==statesAtMerge.end()) {
955 0: statesAtMerge.insert(std::make_pair(mp, &es));
956 : } else {
957 0: ExecutionState *mergeWith = it->second;
0: branch 1 not taken
0: branch 2 not taken
958 0: if (mergeWith->merge(es)) {
959 : // hack, because we are terminating the state we need to let
960 : // the baseSearcher know about it again
961 0: baseSearcher->addState(&es);
962 0: executor.terminateState(es);
963 : } else {
964 0: it->second = &es; // the bump
965 0: ++mergeWith->pc;
966 :
967 0: baseSearcher->addState(mergeWith);
968 : }
969 : }
970 :
971 : goto entry;
972 : } else {
973 0: return es;
974 : }
975 : }
976 :
977 : void BumpMergingSearcher::update(ExecutionState *current,
978 : const std::set<ExecutionState*> &addedStates,
979 0: const std::set<ExecutionState*> &removedStates) {
980 0: baseSearcher->update(current, addedStates, removedStates);
981 0: }
982 :
983 : ///
984 :
985 5: MergingSearcher::MergingSearcher(Executor &_executor, Searcher *_baseSearcher)
986 : : executor(_executor),
987 : baseSearcher(_baseSearcher),
988 15: mergeFunction(executor.kmodule->kleeMergeFn) {
989 5: }
990 :
991 5: MergingSearcher::~MergingSearcher() {
5: branch 0 taken
0: branch 1 not taken
5: branch 3 taken
5: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
992 5: delete baseSearcher;
5: branch 2 taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 12 not taken
0: branch 13 not taken
993 5: }
994 :
995 : ///
996 :
997 1550: Instruction *MergingSearcher::getMergePoint(ExecutionState &es) {
1550: branch 0 taken
0: branch 1 not taken
998 1550: if (mergeFunction) {
999 3100: Instruction *i = es.pc->inst;
1000 :
180: branch 0 taken
1370: branch 1 taken
1001 3100: if (i->getOpcode()==Instruction::Call) {
1002 180: CallSite cs(cast<CallInst>(i));
160: branch 1 taken
20: branch 2 taken
1003 180: if (mergeFunction==cs.getCalledFunction())
1004 160: return i;
1005 : }
1006 : }
1007 :
1008 1390: return 0;
1009 : }
1010 :
1011 1395: ExecutionState &MergingSearcher::selectState() {
1470: branch 1 taken
5: branch 2 taken
1012 2870: while (!baseSearcher->empty()) {
1013 1470: ExecutionState &es = baseSearcher->selectState();
80: branch 1 taken
1390: branch 2 taken
1014 1470: if (getMergePoint(es)) {
1015 80: baseSearcher->removeState(&es, &es);
1016 80: statesAtMerge.insert(&es);
1017 : } else {
1018 1390: return es;
1019 : }
1020 : }
1021 :
1022 : // build map of merge point -> state list
1023 : std::map<Instruction*, std::vector<ExecutionState*> > merges;
80: branch 1 taken
5: branch 2 taken
1024 180: foreach(it, statesAtMerge.begin(), statesAtMerge.end()) {
1025 80: ExecutionState &state = **it;
1026 80: Instruction *mp = getMergePoint(state);
1027 :
1028 160: merges[mp].push_back(&state);
1029 : }
1030 :
1: branch 0 taken
4: branch 1 taken
1031 5: if (DebugLogMerge)
1032 : llvm::cerr << "-- all at merge --\n";
10: branch 1 taken
5: branch 2 taken
1033 30: foreach(it, merges.begin(), merges.end()) {
2: branch 0 taken
8: branch 1 taken
1034 10: if (DebugLogMerge) {
1035 2: llvm::cerr << "\tmerge: " << it->first << " [";
16: branch 0 taken
2: branch 1 taken
1036 24: foreach(it2, it->second.begin(), it->second.end()) {
1037 16: ExecutionState *state = *it2;
1038 : llvm::cerr << state << ", ";
1039 : }
1040 : llvm::cerr << "]\n";
1041 : }
1042 :
1043 : // merge states
1044 30: std::set<ExecutionState*> toMerge(it->second.begin(), it->second.end());
10: branch 1 taken
10: branch 2 taken
1045 30: while (!toMerge.empty()) {
1046 10: ExecutionState *base = *toMerge.begin();
1047 10: toMerge.erase(toMerge.begin());
1048 :
1049 : std::set<ExecutionState*> toErase;
70: branch 1 taken
10: branch 2 taken
1050 160: foreach(it, toMerge.begin(), toMerge.end()) {
1051 70: ExecutionState *mergeWith = *it;
1052 :
70: branch 1 taken
0: branch 2 not taken
1053 70: if (base->merge(*mergeWith)) {
1054 70: toErase.insert(mergeWith);
1055 : }
1056 : }
2: branch 0 taken
8: branch 1 taken
1: branch 2 taken
1: branch 3 taken
1: branch 4 taken
9: branch 5 taken
1057 12: if (DebugLogMerge && !toErase.empty()) {
1058 : llvm::cerr << "\t\tmerged: " << base << " with [";
14: branch 1 taken
1: branch 2 taken
1059 30: foreach(it, toErase.begin(), toErase.end()) {
13: branch 0 taken
1: branch 1 taken
1060 14: if (it!=toErase.begin()) llvm::cerr << ", ";
1061 : llvm::cerr << *it;
1062 : }
1063 : llvm::cerr << "]\n";
1064 : }
70: branch 1 taken
10: branch 2 taken
1065 160: foreach(it, toErase.begin(), toErase.end()) {
1066 70: let(it2, toMerge.find(*it));
0: branch 0 not taken
70: branch 1 taken
1067 70: assert(it2!=toMerge.end());
1068 70: executor.terminateState(**it);
1069 70: toMerge.erase(it2);
1070 : }
1071 :
1072 : // step past merge and toss base back in pool
1073 10: statesAtMerge.erase(statesAtMerge.find(base));
1074 10: ++base->pc;
1075 10: baseSearcher->addState(base);
1076 : }
1077 : }
1078 :
1: branch 0 taken
4: branch 1 taken
1079 5: if (DebugLogMerge)
1080 : llvm::cerr << "-- merge complete, continuing --\n";
1081 :
1082 5: return selectState();
1083 : }
1084 :
1085 : void MergingSearcher::update(ExecutionState *current,
1086 : const std::set<ExecutionState*> &addedStates,
1087 1395: const std::set<ExecutionState*> &removedStates) {
15: branch 0 taken
1380: branch 1 taken
1088 1395: if (!removedStates.empty()) {
1089 15: std::set<ExecutionState *> alt = removedStates;
80: branch 1 taken
15: branch 2 taken
1090 175: foreach(it, removedStates.begin(), removedStates.end()) {
1091 80: ExecutionState *es = *it;
1092 80: let(it, statesAtMerge.find(es));
70: branch 0 taken
10: branch 1 taken
1093 160: if (it!=statesAtMerge.end()) {
1094 70: statesAtMerge.erase(it);
1095 70: alt.erase(alt.find(es));
1096 : }
1097 : }
1098 15: baseSearcher->update(current, addedStates, alt);
1099 : } else {
1100 1380: baseSearcher->update(current, addedStates, removedStates);
1101 : }
1102 1395: }
1103 :
1104 : ///
1105 :
1106 : BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
1107 : double _timeBudget,
1108 16: unsigned _instructionBudget)
1109 : : baseSearcher(_baseSearcher),
1110 : timeBudget(_timeBudget),
1111 : instructionBudget(_instructionBudget),
1112 32: lastState(0) {
1113 :
1114 16: }
1115 :
1116 16: BatchingSearcher::~BatchingSearcher() {
16: branch 0 taken
0: branch 1 not taken
16: branch 3 taken
16: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
1117 16: delete baseSearcher;
16: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
1118 16: }
1119 :
1120 7056: ExecutionState &BatchingSearcher::selectState() {
6792: branch 0 taken
264: branch 1 taken
6792: branch 3 taken
0: branch 4 not taken
0: branch 5 not taken
6792: branch 6 taken
264: branch 7 taken
6792: branch 8 taken
1121 13848: if (!lastState ||
1122 : (util::getWallTime()-lastStartTime)>timeBudget ||
1123 : (stats::instructions-lastStartInstructions)>instructionBudget) {
0: branch 0 not taken
264: branch 1 taken
1124 264: if (lastState) {
1125 0: double delta = util::getWallTime()-lastStartTime;
0: branch 0 not taken
0: branch 1 not taken
1126 0: if (delta>timeBudget*1.1) {
1127 0: llvm::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n";
1128 0: timeBudget = delta;
1129 : }
1130 : }
1131 264: lastState = &baseSearcher->selectState();
1132 264: lastStartTime = util::getWallTime();
1133 264: lastStartInstructions = stats::instructions;
1134 264: return *lastState;
1135 : } else {
1136 6792: return *lastState;
1137 : }
1138 : }
1139 :
1140 : void BatchingSearcher::update(ExecutionState *current,
1141 : const std::set<ExecutionState*> &addedStates,
1142 7084: const std::set<ExecutionState*> &removedStates) {
264: branch 0 taken
6820: branch 1 taken
1143 14168: if (removedStates.count(lastState))
1144 264: lastState = 0;
1145 7084: baseSearcher->update(current, addedStates, removedStates);
1146 7084: }
1147 :
1148 : ///
1149 :
1150 : OwningSearcher::OwningSearcher(Executor &_executor,
1151 12: Searcher *_baseSearcher)
1152 : : executor(_executor),
1153 36: baseSearcher(_baseSearcher) {
1154 12: }
1155 :
1156 12: OwningSearcher::~OwningSearcher() {
12: branch 0 taken
0: branch 1 not taken
12: branch 3 taken
12: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
1157 12: delete baseSearcher;
12: branch 2 taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 12 not taken
0: branch 13 not taken
1158 24: }
1159 :
1160 200: ExecutionState &OwningSearcher::selectState() {
1161 200: return baseSearcher->selectState();
1162 : }
1163 :
1164 : #include <vector>
1165 :
1166 103: static std::map<BasicBlock*, std::set<Function*> > bbTargets;
1167 103: static std::map<Function*, std::set<BasicBlock*> > functionCallers;
1168 103: static std::map<BasicBlock*, std::map<BasicBlock*, unsigned> > shortestPathTable;
1169 103: static std::set<BasicBlock*> bbsMakingIndirectCalls;
1170 :
1171 : static void getSuccs(BasicBlock *bb, std::vector<BasicBlock*> &results,
1172 384: KModule *km) {
384: branch 0 taken
384: branch 1 taken
1173 1536: foreach(it, succ_begin(bb), succ_end(bb))
1174 384: results.push_back(*it);
168: branch 2 taken
384: branch 3 taken
1175 1320: foreach(it, bbTargets[bb].begin(), bbTargets[bb].end()) {
1176 168: Function *f = *it;
56: branch 1 taken
112: branch 2 taken
1177 168: if (!f->isDeclaration())
1178 56: results.push_back(f->begin());
1179 : }
1180 : #if 1
0: branch 0 not taken
384: branch 1 taken
1181 384: if (bbsMakingIndirectCalls.count(bb)) {
0: branch 0 not taken
0: branch 1 not taken
1182 0: foreach(it, km->escapingFunctions.begin(), km->escapingFunctions.end()) {
1183 0: Function *f = *it;
0: branch 1 not taken
0: branch 2 not taken
1184 0: if (!f->isDeclaration())
1185 0: results.push_back(f->begin());
1186 : }
1187 : }
1188 :
1189 384: Instruction *i = bb->getTerminator();
288: branch 0 taken
96: branch 1 taken
0: branch 2 not taken
288: branch 3 taken
96: branch 4 taken
288: branch 5 taken
1190 672: if (isa<ReturnInst>(i) || isa<UnwindInst>(i)) {
1191 192: Function *f = bb->getParent();
0: branch 0 not taken
96: branch 1 taken
1192 192: if (km->escapingFunctions.count(f)) {
0: branch 0 not taken
0: branch 1 not taken
1193 0: foreach(it, bbsMakingIndirectCalls.begin(), bbsMakingIndirectCalls.end()) {
1194 0: results.push_back(*it);
1195 : }
1196 : }
1197 :
1198 96: std::set<BasicBlock*> &callers = functionCallers[f];
56: branch 0 taken
96: branch 1 taken
1199 152: foreach(it, callers.begin(), callers.end()) {
1200 56: results.push_back(*it);
1201 : }
1202 : }
1203 : #endif
1204 384: }
1205 :
1206 : static std::map<BasicBlock*, unsigned> &getShortestPaths(BasicBlock *start,
1207 560: KModule *km) {
1208 : let(it, shortestPathTable.find(start));
1209 :
40: branch 0 taken
520: branch 1 taken
1210 560: if (it==shortestPathTable.end()) {
1211 : std::vector<BasicBlock*> Q;
1212 40: std::map<BasicBlock*, unsigned> &cost = shortestPathTable[start];
1213 40: cost[start] = 0;
1214 40: Q.push_back(start);
384: branch 0 taken
40: branch 1 taken
1215 464: while (!Q.empty()) {
1216 : // select best
1217 : let(it, Q.begin());
1218 384: let(bestIt, it);
756: branch 0 taken
384: branch 1 taken
1219 1524: for (; it!=Q.end(); ++it)
0: branch 2 not taken
756: branch 3 taken
1220 1512: if (cost[*it]<cost[*bestIt])
1221 0: bestIt = it;
1222 384: BasicBlock *best = *bestIt;
1223 384: unsigned bestCost = cost[best];
1224 384: Q.erase(bestIt);
1225 :
1226 : std::vector<BasicBlock*> succs;
1227 384: getSuccs(best, succs, km);
496: branch 0 taken
384: branch 1 taken
1228 1264: foreach(it, succs.begin(), succs.end()) {
1229 496: BasicBlock *succ = *it;
1230 496: unsigned succCost = bestCost + 1;
1231 : let(it2, cost.find(succ));
152: branch 0 taken
344: branch 1 taken
0: branch 2 not taken
152: branch 3 taken
344: branch 4 taken
152: branch 5 taken
1232 648: if (it2==cost.end() || succCost<it2->second) {
1233 344: Q.push_back(succ);
1234 344: cost[succ] = succCost;
1235 : }
1236 : }
1237 : }
1238 40: return cost;
1239 : } else {
1240 520: return it->second;
1241 : }
1242 : }
1243 :
1244 : void OwningSearcher::splitStates(std::set<llvm::BasicBlock*> &bbs,
1245 180: std::set<ExecutionState*> &states) {
1246 : static bool init = true;
1247 :
12: branch 0 taken
168: branch 1 taken
1248 180: if (init) {
1249 12: init = false;
1250 :
96: branch 1 taken
12: branch 2 taken
1251 228: foreach(fnIt, executor.kmodule->module->begin(), executor.kmodule->module->end()) {
1252 96: Function *f = &*fnIt;
180: branch 1 taken
96: branch 2 taken
1253 456: foreach(bbIt, f->begin(), f->end()) {
1254 180: BasicBlock *bb = &*bbIt;
900: branch 1 taken
180: branch 2 taken
1255 2160: foreach(it, bbIt->begin(), bbIt->end()) {
816: branch 1 taken
84: branch 2 taken
0: branch 4 not taken
816: branch 5 taken
84: branch 6 taken
816: branch 7 taken
1256 2616: if (isa<CallInst>(&*it) || isa<InvokeInst>(&*it)) {
1257 84: Function *target = getDirectCallTarget(&*it);
84: branch 0 taken
0: branch 1 not taken
1258 84: if (target) {
1259 84: functionCallers[target].insert(bb);
1260 84: bbTargets[bb].insert(target);
1261 : } else {
1262 0: bbsMakingIndirectCalls.insert(bb);
1263 : }
1264 : }
1265 : }
1266 : }
1267 : }
1268 : }
1269 :
1270 : std::map<BasicBlock*, std::pair<unsigned,ExecutionState*> > best;
360: branch 1 taken
180: branch 2 taken
1271 1080: foreach(it, states.begin(), states.end()) {
1272 360: ExecutionState *es = *it;
1273 720: Instruction *instr = es->pc->inst;
1274 360: BasicBlock *esbb = instr->getParent();
1275 : std::map<BasicBlock*, unsigned> &shortestPaths = getShortestPaths(esbb,
1276 360: executor.kmodule);
1277 :
1440: branch 0 taken
360: branch 1 taken
1278 2160: foreach(it2, bbs.begin(), bbs.end()) {
1279 1440: BasicBlock *bb = *it2;
1280 : let(it, shortestPaths.find(bb));
1440: branch 0 taken
0: branch 1 not taken
1281 1440: if (it!=shortestPaths.end()) {
1282 1440: unsigned cost = it->second;
1283 : let(it2, best.find(bb));
720: branch 0 taken
720: branch 1 taken
1284 1440: if (it2==best.end()) {
1285 1440: best.insert(std::make_pair(bb, std::make_pair(cost,es)));
1286 : } else {
240: branch 0 taken
480: branch 1 taken
1287 720: if (cost<it2->second.first) {
1288 240: it2->second.first = cost;
1289 240: it2->second.second = es;
1290 : }
1291 : }
1292 : }
1293 : }
1294 : }
1295 :
1296 180: std::set<BasicBlock*> lost = bbs;
1297 :
720: branch 0 taken
180: branch 1 taken
1298 1080: foreach(it, best.begin(), best.end()) {
1299 720: BasicBlock *bb = it->first;
1300 720: ExecutionState *es = it->second.second;
1301 :
1302 : // unsigned cost = it->second.first;
1303 : // llvm::cerr << " assigned: "
1304 : // << bb->getParent()->getName() << ":" << bb->getName()
1305 : // << " to " << es << " (cost: " << cost << ")\n";
1306 720: bbMap[es].insert(bb);
1307 :
1308 : let(it2, lost.find(bb));
0: branch 0 not taken
720: branch 1 taken
1309 720: assert(it2!=lost.end());
1310 720: lost.erase(it2);
1311 : }
1312 :
1313 180: resurrect(lost);
1314 180: }
1315 :
1316 396: void OwningSearcher::resurrect(std::set<BasicBlock*> &bbs) {
180: branch 0 taken
216: branch 1 taken
1317 396: if (bbs.empty())
1318 180: return;
1319 :
1320 : #if 0
1321 : llvm::cerr << "-- resurrecting: [";
1322 : foreach(it, bbs.begin(), bbs.end()) {
1323 : BasicBlock *bb = *it;
1324 : llvm::cerr << bb->getParent()->getName() << ":" << bb->getName() << ",";
1325 : }
1326 : llvm::cerr << "]\n";
1327 : #endif
1328 :
1329 : if (0) {
1330 : std::map<BasicBlock*, std::pair<unsigned,ExecutionState*> > bests;
1331 :
1332 : std::set<ExecutionState*> states;
1333 : foreach(it, bbMap.begin(), bbMap.end())
1334 : states.insert(it->first);
1335 : states.insert(deadStates.begin(), deadStates.end());
1336 :
1337 : foreach(it, states.begin(), states.end()) {
1338 : ExecutionState *es = *it;
1339 : Instruction *instr = es->pc->inst;
1340 : BasicBlock *esbb = instr->getParent();
1341 : std::map<BasicBlock*, unsigned> &shortestPaths = getShortestPaths(esbb,
1342 : executor.kmodule);
1343 :
1344 : foreach(it2, bbs.begin(), bbs.end()) {
1345 : BasicBlock *bb = *it2;
1346 : let(it, shortestPaths.find(bb));
1347 : if (it!=shortestPaths.end()) {
1348 : let(it2, bests.find(bb));
1349 : if (it2==bests.end()) {
1350 : bests.insert(std::make_pair(bb,std::make_pair(it->second,es)));
1351 : } else {
1352 : if (it->second<it2->second.first) {
1353 : it2->second.first = it->second;
1354 : it2->second.second = es;
1355 : }
1356 : }
1357 : }
1358 : }
1359 : }
1360 :
1361 : foreach(it, bests.begin(), bests.end()) {
1362 : BasicBlock *bb = it->first;
1363 : ExecutionState *es = it->second.second;
1364 :
1365 : if (deadStates.count(es)) {
1366 : // llvm::cerr << "-- resurrected: " << es << " for "
1367 : // << bb->getParent()->getName() << ":" << bb->getName() << "\n";
1368 : deadStates.erase(deadStates.find(es));
1369 : baseSearcher->addState(es);
1370 : } else {
1371 : // llvm::cerr << "-- gifted: " << es << " received "
1372 : // << bb->getParent()->getName() << ":" << bb->getName() << "\n";
1373 : }
1374 :
1375 : bbMap[es].insert(bb);
1376 :
1377 : bbs.erase(bbs.find(bb));
1378 : }
1379 : } else {
1380 : // llvm::cerr << "a\n";
0: branch 1 not taken
216: branch 2 taken
1381 648: foreach(it, bbMap.begin(), bbMap.end()) {
1382 0: ExecutionState *es = it->first;
1383 0: Instruction *instr = es->pc->inst;
1384 0: BasicBlock *esbb = instr->getParent();
1385 0: std::set<BasicBlock*> &esBBs = it->second;
1386 : std::set<BasicBlock*> gifted;
1387 : std::map<BasicBlock*, unsigned> &shortestPaths = getShortestPaths(esbb,
1388 0: executor.kmodule);
1389 :
0: branch 0 not taken
0: branch 1 not taken
1390 0: foreach(it2, bbs.begin(), bbs.end()) {
1391 0: BasicBlock *bb = *it2;
0: branch 0 not taken
0: branch 1 not taken
1392 0: if (shortestPaths.find(bb)!=shortestPaths.end()) {
1393 0: esBBs.insert(bb);
1394 0: gifted.insert(bb);
1395 : }
1396 : }
1397 :
0: branch 0 not taken
0: branch 1 not taken
1398 0: if (!gifted.empty()) {
0: branch 0 not taken
0: branch 1 not taken
1399 0: foreach(it, gifted.begin(), gifted.end()) {
1400 : let(it2, bbs.find(*it));
0: branch 0 not taken
0: branch 1 not taken
1401 0: assert(it2!=bbs.end());
1402 0: bbs.erase(it2);
1403 : }
1404 : #if 0
1405 : llvm::cerr << "-- gifted: " << es << " received [";
1406 : foreach(it, gifted.begin(), gifted.end()) {
1407 : BasicBlock *bb = *it;
1408 : llvm::cerr << bb->getParent()->getName() << ":" << bb->getName() << ",";
1409 : }
1410 : llvm::cerr << "]\n";
1411 : #endif
1412 : }
1413 : }
1414 :
1415 : // llvm::cerr << "b\n";
1416 : std::set<ExecutionState*> resurrected;
200: branch 1 taken
216: branch 2 taken
1417 1264: foreach(it, deadStates.begin(), deadStates.end()) {
1418 200: ExecutionState *es = *it;
1419 400: Instruction *instr = es->pc->inst;
1420 200: BasicBlock *esbb = instr->getParent();
1421 : std::map<BasicBlock*, unsigned> &shortestPaths = getShortestPaths(esbb,
1422 200: executor.kmodule);
1423 200: bool resurrect = false;
1424 :
1008: branch 0 taken
200: branch 1 taken
1425 1408: foreach(it2, bbs.begin(), bbs.end()) {
1426 1008: BasicBlock *bb = *it2;
864: branch 0 taken
144: branch 1 taken
1427 1008: if (shortestPaths.find(bb)!=shortestPaths.end()) {
1428 864: resurrect = true;
1429 864: bbMap[es].insert(bb);
1430 : }
1431 : }
1432 :
200: branch 0 taken
0: branch 1 not taken
1433 200: if (resurrect) {
1434 200: std::set<BasicBlock*> &newBBs = bbMap[es];
864: branch 0 taken
200: branch 1 taken
1435 1064: foreach(it, newBBs.begin(), newBBs.end()) {
1436 : let(it2, bbs.find(*it));
0: branch 0 not taken
864: branch 1 taken
1437 864: assert(it2!=bbs.end());
1438 864: bbs.erase(it2);
1439 : }
1440 : #if 0
1441 : llvm::cerr << "-- resurrected: " << es << " for [";
1442 : foreach(it, bbMap[es].begin(), bbMap[es].end()) {
1443 : BasicBlock *bb = *it;
1444 : llvm::cerr << bb->getParent()->getName() << ":" << bb->getName() << ",";
1445 : }
1446 : llvm::cerr << "]\n";
1447 : #endif
1448 200: baseSearcher->addState(es);
1449 200: resurrected.insert(es);
1450 : }
1451 : }
1452 :
1453 : // llvm::cerr << "c\n";
200: branch 1 taken
216: branch 2 taken
1454 832: foreach(it, resurrected.begin(), resurrected.end()) {
1455 200: let(it2, deadStates.find(*it));
0: branch 0 not taken
200: branch 1 taken
1456 400: assert(it2!=deadStates.end());
1457 200: deadStates.erase(it2);
1458 216: }
1459 : }
1460 :
1461 : #if 0
1462 : if (!bbs.empty()) {
1463 : llvm::cerr << "-- permanently lost: [";
1464 : foreach(it, bbs.begin(), bbs.end()) {
1465 : BasicBlock *bb = *it;
1466 : llvm::cerr << bb->getParent()->getName() << ":" << bb->getName() << ",";
1467 : }
1468 : llvm::cerr << "]\n";
1469 : }
1470 : #endif
1471 : }
1472 :
1473 : void OwningSearcher::update(ExecutionState *current,
1474 : const std::set<ExecutionState*> &addedStates,
1475 5120: const std::set<ExecutionState*> &removedStates) {
1476 : // assert(current == 0 || bbMap.find(current)!=bbMap.end());
1477 : // assert(deadStates.size() + bbMap.size() + addedStates.size() - removedStates.size() == executor.states.size());
5096: branch 0 taken
24: branch 1 taken
5096: branch 2 taken
0: branch 3 not taken
4916: branch 4 taken
180: branch 5 taken
4716: branch 6 taken
200: branch 7 taken
4716: branch 8 taken
404: branch 9 taken
1478 25324: if (current && bbMap.find(current)!=bbMap.end() &&
1479 : addedStates.empty() && removedStates.empty()) {
1480 4716: baseSearcher->update(current, addedStates, removedStates);
1481 4716: return;
1482 : }
1483 :
1484 : std::set<ExecutionState*> baseRemoved;
1485 : std::set<BasicBlock*> lostBBs;
200: branch 1 taken
404: branch 2 taken
1486 1208: foreach(it, removedStates.begin(), removedStates.end()) {
1487 200: let(it2, bbMap.find(*it));
0: branch 0 not taken
200: branch 1 taken
1488 400: if (it2==bbMap.end()) {
1489 0: let(it3, deadStates.find(*it));
0: branch 0 not taken
0: branch 1 not taken
1490 0: assert(it3!=deadStates.end());
1491 0: deadStates.erase(it3);
1492 : } else {
1493 600: lostBBs.insert(it2->second.begin(), it2->second.end());
1494 200: bbMap.erase(it2);
1495 200: baseRemoved.insert(*it);
1496 : }
1497 : }
1498 :
1499 404: let (it, bbMap.find(current));
180: branch 0 taken
224: branch 1 taken
1500 808: if (it!=bbMap.end()) {
1501 180: std::set<BasicBlock*> bbs = it->second;
1502 180: bbMap.erase(it);
1503 :
1504 180: std::set<ExecutionState*> baseAdded, divy = addedStates;
1505 180: divy.insert(current);
1506 180: splitStates(bbs, divy);
360: branch 1 taken
180: branch 2 taken
1507 1080: foreach(it, divy.begin(), divy.end()) {
180: branch 0 taken
180: branch 1 taken
1508 360: if (*it==current) {
0: branch 0 not taken
180: branch 1 taken
1509 540: if (bbMap.find(*it) == bbMap.end()) {
1510 0: baseRemoved.insert(current);
1511 0: deadStates.insert(*it);
1512 : }
1513 : } else {
180: branch 0 taken
0: branch 1 not taken
1514 540: if (bbMap.find(*it) == bbMap.end()) {
1515 180: deadStates.insert(*it);
1516 : } else {
1517 0: baseAdded.insert(*it);
1518 : }
1519 : }
1520 : }
1521 :
1522 180: baseSearcher->update(current, baseAdded, baseRemoved);
1523 : } else {
1524 224: deadStates.insert(addedStates.begin(), addedStates.end());
1525 :
200: branch 1 taken
24: branch 2 taken
1526 448: if (baseRemoved.find(current) != baseRemoved.end()) {
1527 : baseSearcher->update(current,
1528 : std::set<ExecutionState*>(),
1529 400: baseRemoved);
1530 : } else {
1531 : baseSearcher->update(0,
1532 : std::set<ExecutionState*>(),
1533 48: baseRemoved);
1534 : }
1535 : }
1536 :
200: branch 0 taken
204: branch 1 taken
1537 404: if (!lostBBs.empty())
1538 200: resurrect(lostBBs);
1539 :
200: branch 0 taken
204: branch 1 taken
16: branch 3 taken
184: branch 4 taken
16: branch 5 taken
388: branch 6 taken
1540 808: if (!deadStates.empty() && baseSearcher->empty()) {
0: branch 0 not taken
16: branch 1 taken
1541 32: if (!bbMap.empty())
1542 : llvm::cerr << "KLEE: redistributing states\n";
1543 : std::set<BasicBlock*> allBBs;
128: branch 1 taken
16: branch 2 taken
1544 320: foreach(fnIt, executor.kmodule->module->begin(), executor.kmodule->module->end()) {
240: branch 1 taken
128: branch 2 taken
1545 736: foreach(bbIt, fnIt->begin(), fnIt->end()) {
1546 240: allBBs.insert(&*bbIt);
1547 : }
1548 : }
1549 16: resurrect(allBBs);
1550 404: }
1551 :
1552 : // assert(current == 0 || bbMap.find(current)!=bbMap.end());
1553 : // assert(deadStates.size() + bbMap.size() == executor.states.size());
1554 : }
1555 :
1556 : /***/
1557 :
1558 4: IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *_baseSearcher)
1559 : : baseSearcher(_baseSearcher),
1560 8: time(1.) {
1561 4: }
1562 :
1563 4: IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() {
4: branch 0 taken
0: branch 1 not taken
4: branch 3 taken
4: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
1564 4: delete baseSearcher;
4: branch 2 taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 12 not taken
0: branch 13 not taken
1565 4: }
1566 :
1567 1960: ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
1568 1960: ExecutionState &res = baseSearcher->selectState();
1569 1960: startTime = util::getWallTime();
1570 1960: return res;
1571 : }
1572 :
1573 : void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
1574 : const std::set<ExecutionState*> &addedStates,
1575 1964: const std::set<ExecutionState*> &removedStates) {
1576 1964: double elapsed = util::getWallTime() - startTime;
1577 :
64: branch 0 taken
1900: branch 1 taken
1578 1964: if (!removedStates.empty()) {
1579 64: std::set<ExecutionState *> alt = removedStates;
64: branch 1 taken
64: branch 2 taken
1580 192: foreach(it, removedStates.begin(), removedStates.end()) {
1581 64: ExecutionState *es = *it;
1582 64: let(it, pausedStates.find(es));
0: branch 0 not taken
64: branch 1 taken
1583 128: if (it!=pausedStates.end()) {
1584 0: pausedStates.erase(it);
1585 0: alt.erase(alt.find(es));
1586 : }
1587 : }
1588 64: baseSearcher->update(current, addedStates, alt);
1589 : } else {
1590 1900: baseSearcher->update(current, addedStates, removedStates);
1591 : }
1592 :
1960: branch 0 taken
4: branch 1 taken
1896: branch 2 taken
64: branch 3 taken
0: branch 4 not taken
1896: branch 5 taken
0: branch 6 not taken
1964: branch 7 taken
1593 3924: if (current && !removedStates.count(current) && elapsed>time) {
1594 0: pausedStates.insert(current);
1595 0: baseSearcher->removeState(current);
1596 : }
1597 :
4: branch 1 taken
1960: branch 2 taken
1598 1964: if (baseSearcher->empty()) {
1599 4: time *= 2;
1600 4: llvm::cerr << "KLEE: increasing time budget to: " << time << "\n";
1601 8: baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
1602 4: pausedStates.clear();
1603 : }
1604 1964: }
1605 :
1606 : /***/
1607 :
1608 0: InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers)
1609 : : searchers(_searchers),
1610 0: index(1) {
1611 0: }
1612 :
1613 0: InterleavedSearcher::~InterleavedSearcher() {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
1614 0: foreach(it, searchers.begin(), searchers.end())
0: branch 0 not taken
0: branch 1 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
0: branch 7 not taken
1615 0: delete *it;
0: branch 2 not taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 12 not taken
0: branch 13 not taken
1616 0: }
1617 :
1618 0: ExecutionState &InterleavedSearcher::selectState() {
1619 0: Searcher *s = searchers[--index];
0: branch 0 not taken
0: branch 1 not taken
1620 0: if (index==0) index = searchers.size();
1621 0: return s->selectState();
1622 : }
1623 :
1624 : void InterleavedSearcher::update(ExecutionState *current,
1625 : const std::set<ExecutionState*> &addedStates,
1626 0: const std::set<ExecutionState*> &removedStates) {
0: branch 0 not taken
0: branch 1 not taken
1627 0: foreach(it, searchers.begin(), searchers.end())
1628 0: (*it)->update(current, addedStates, removedStates);
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
1629 309: }
Generated: 2009-05-17 22:47 by zcov