Skip to content

Commit bfaabef

Browse files
Columpiomisonijnik
Columpio
authored and
misonijnik
committed
[chore] Optimized IterativeDeepeningSearcher
1 parent cdc1f7f commit bfaabef

3 files changed

Lines changed: 178 additions & 97 deletions

File tree

‎lib/Core/Searcher.cpp‎

Lines changed: 41 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -47,8 +47,8 @@ using namespace llvm;
4747
ExecutionState &DFSSearcher::selectState() { return *states.back(); }
4848

4949
void DFSSearcher::update(ExecutionState *current,
50-
const std::vector<ExecutionState *> &addedStates,
51-
const std::vector<ExecutionState *> &removedStates) {
50+
const StateIterable &addedStates,
51+
const StateIterable &removedStates) {
5252
// insert states
5353
states.insert(states.end(), addedStates.begin(), addedStates.end());
5454

@@ -73,8 +73,8 @@ void DFSSearcher::printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; }
7373
ExecutionState &BFSSearcher::selectState() { return *states.front(); }
7474

7575
void BFSSearcher::update(ExecutionState *current,
76-
const std::vector<ExecutionState *> &addedStates,
77-
const std::vector<ExecutionState *> &removedStates) {
76+
const StateIterable &addedStates,
77+
const StateIterable &removedStates) {
7878
// update current state
7979
// Assumption: If new states were added KLEE forked, therefore states evolved.
8080
// constraints were added to the current state, it evolved.
@@ -114,9 +114,9 @@ ExecutionState &RandomSearcher::selectState() {
114114
return *states[theRNG.getInt32() % states.size()];
115115
}
116116

117-
void RandomSearcher::update(
118-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
119-
const std::vector<ExecutionState *> &removedStates) {
117+
void RandomSearcher::update(ExecutionState *current,
118+
const StateIterable &addedStates,
119+
const StateIterable &removedStates) {
120120
// insert states
121121
states.insert(states.end(), addedStates.begin(), addedStates.end());
122122

@@ -167,9 +167,9 @@ TargetedSearcher::TargetedSearcher(ref<Target> target,
167167

168168
ExecutionState &TargetedSearcher::selectState() { return *states->choose(0); }
169169

170-
void TargetedSearcher::update(
171-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
172-
const std::vector<ExecutionState *> &removedStates) {
170+
void TargetedSearcher::update(ExecutionState *current,
171+
const StateIterable &addedStates,
172+
const StateIterable &removedStates) {
173173

174174
// update current
175175
if (current && std::find(removedStates.begin(), removedStates.end(),
@@ -224,9 +224,9 @@ ExecutionState &GuidedSearcher::selectState() {
224224
return *state;
225225
}
226226

227-
void GuidedSearcher::update(
228-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
229-
const std::vector<ExecutionState *> &removedStates) {
227+
void GuidedSearcher::update(ExecutionState *current,
228+
const StateIterable &addedStates,
229+
const StateIterable &removedStates) {
230230

231231
if (current) {
232232
ref<const TargetsHistory> history = current->history();
@@ -421,9 +421,9 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
421421
}
422422
}
423423

424-
void WeightedRandomSearcher::update(
425-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
426-
const std::vector<ExecutionState *> &removedStates) {
424+
void WeightedRandomSearcher::update(ExecutionState *current,
425+
const StateIterable &addedStates,
426+
const StateIterable &removedStates) {
427427

428428
// update current
429429
if (current && updateWeights &&
@@ -514,11 +514,11 @@ ExecutionState &RandomPathSearcher::selectState() {
514514
return *n->state;
515515
}
516516

517-
void RandomPathSearcher::update(
518-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
519-
const std::vector<ExecutionState *> &removedStates) {
517+
void RandomPathSearcher::update(ExecutionState *current,
518+
const StateIterable &addedStates,
519+
const StateIterable &removedStates) {
520520
// insert states
521-
for (auto &es : addedStates) {
521+
for (auto es : addedStates) {
522522
PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
523523
PTreeNodePtr &root = processForest.getPTrees().at(pnode->getTreeID())->root;
524524
PTreeNodePtr *childPtr;
@@ -618,9 +618,9 @@ ExecutionState &BatchingSearcher::selectState() {
618618
return *lastState;
619619
}
620620

621-
void BatchingSearcher::update(
622-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
623-
const std::vector<ExecutionState *> &removedStates) {
621+
void BatchingSearcher::update(ExecutionState *current,
622+
const StateIterable &addedStates,
623+
const StateIterable &removedStates) {
624624
// drop memoized state if it is marked for deletion
625625
if (std::find(removedStates.begin(), removedStates.end(), lastState) !=
626626
removedStates.end())
@@ -697,46 +697,30 @@ ExecutionState &IterativeDeepeningSearcher::selectState() {
697697
return res;
698698
}
699699

700-
void IterativeDeepeningSearcher::filter(const StatesVector &states,
701-
StatesVector &result) const {
702-
StatesVector states1(states);
703-
std::sort(states1.begin(), states1.end());
704-
std::set_difference(states1.begin(), states1.end(), pausedStates.begin(),
705-
pausedStates.end(), std::back_inserter(result));
706-
}
707-
708700
void IterativeDeepeningSearcher::update(
709701
const TargetHistoryTargetPairToStatesMap &added,
710702
const TargetHistoryTargetPairToStatesMap &removed) {
711703
if (!tms)
712704
return;
713-
TargetHistoryTargetPairToStatesMap removedRefined(removed.size());
714-
for (const auto &pair : removed) {
715-
StatesVector refined;
716-
IterativeDeepeningSearcher::filter(pair.second, refined);
717-
removedRefined.emplace(pair.first, std::move(refined));
718-
}
719-
tms->update(added, removedRefined);
705+
added.setWithout(&pausedStates);
706+
removed.setWithout(&pausedStates);
707+
tms->update(added, removed);
708+
added.clearWithout();
709+
removed.clearWithout();
720710
}
721711

722712
void IterativeDeepeningSearcher::update(ExecutionState *current,
723-
const StatesVector &addedStates,
724-
const StatesVector &removedStates) {
725-
726-
// update underlying searcher (filter paused states unknown to underlying
727-
// searcher)
728-
if (!removedStates.empty()) {
729-
StatesVector alt;
730-
IterativeDeepeningSearcher::filter(removedStates, alt);
731-
baseSearcher->update(current, addedStates, alt);
732-
} else {
733-
baseSearcher->update(current, addedStates, removedStates);
734-
}
713+
const StateIterable &added,
714+
const StateIterable &removed) {
715+
removed.setWithout(&pausedStates);
716+
baseSearcher->update(current, added, removed);
717+
removed.clearWithout();
718+
719+
for (auto state : removed)
720+
pausedStates.erase(state);
735721

736-
// update current: pause if time exceeded
737722
if (current &&
738-
std::find(removedStates.begin(), removedStates.end(), current) ==
739-
removedStates.end() &&
723+
std::find(removed.begin(), removed.end(), current) == removed.end() &&
740724
metric->exceeds(*current)) {
741725
pausedStates.insert(current);
742726
baseSearcher->update(nullptr, {}, {current});
@@ -745,8 +729,7 @@ void IterativeDeepeningSearcher::update(ExecutionState *current,
745729
// no states left in underlying searcher: fill with paused states
746730
if (baseSearcher->empty()) {
747731
metric->increaseLimit();
748-
StatesVector ps(pausedStates.begin(), pausedStates.end());
749-
baseSearcher->update(nullptr, ps, {});
732+
baseSearcher->update(nullptr, pausedStates, {});
750733
pausedStates.clear();
751734
}
752735
}
@@ -775,9 +758,9 @@ ExecutionState &InterleavedSearcher::selectState() {
775758
return s->selectState();
776759
}
777760

778-
void InterleavedSearcher::update(
779-
ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
780-
const std::vector<ExecutionState *> &removedStates) {
761+
void InterleavedSearcher::update(ExecutionState *current,
762+
const StateIterable &addedStates,
763+
const StateIterable &removedStates) {
781764

782765
// update underlying searchers
783766
for (auto &searcher : searchers)

‎lib/Core/Searcher.h‎

Lines changed: 22 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -63,9 +63,8 @@ class Searcher {
6363
/// \param current The currently selected state for exploration.
6464
/// \param addedStates The newly branched states with `current` as common
6565
/// ancestor. \param removedStates The states that will be terminated.
66-
virtual void update(ExecutionState *current,
67-
const std::vector<ExecutionState *> &addedStates,
68-
const std::vector<ExecutionState *> &removedStates) = 0;
66+
virtual void update(ExecutionState *current, const StateIterable &addedStates,
67+
const StateIterable &removedStates) = 0;
6968

7069
/// \return True if no state left for exploration, False otherwise
7170
virtual bool empty() = 0;
@@ -96,9 +95,8 @@ class DFSSearcher final : public Searcher {
9695

9796
public:
9897
ExecutionState &selectState() override;
99-
void update(ExecutionState *current,
100-
const std::vector<ExecutionState *> &addedStates,
101-
const std::vector<ExecutionState *> &removedStates) override;
98+
void update(ExecutionState *current, const StateIterable &addedStates,
99+
const StateIterable &removedStates) override;
102100
bool empty() override;
103101
void printName(llvm::raw_ostream &os) override;
104102
};
@@ -112,9 +110,8 @@ class BFSSearcher final : public Searcher {
112110

113111
public:
114112
ExecutionState &selectState() override;
115-
void update(ExecutionState *current,
116-
const std::vector<ExecutionState *> &addedStates,
117-
const std::vector<ExecutionState *> &removedStates) override;
113+
void update(ExecutionState *current, const StateIterable &addedStates,
114+
const StateIterable &removedStates) override;
118115
bool empty() override;
119116
void printName(llvm::raw_ostream &os) override;
120117
};
@@ -127,9 +124,8 @@ class RandomSearcher final : public Searcher {
127124
public:
128125
explicit RandomSearcher(RNG &rng);
129126
ExecutionState &selectState() override;
130-
void update(ExecutionState *current,
131-
const std::vector<ExecutionState *> &addedStates,
132-
const std::vector<ExecutionState *> &removedStates) override;
127+
void update(ExecutionState *current, const StateIterable &addedStates,
128+
const StateIterable &removedStates) override;
133129
bool empty() override;
134130
void printName(llvm::raw_ostream &os) override;
135131
};
@@ -148,9 +144,8 @@ class TargetedSearcher final : public Searcher {
148144
~TargetedSearcher() override;
149145

150146
ExecutionState &selectState() override;
151-
void update(ExecutionState *current,
152-
const std::vector<ExecutionState *> &addedStates,
153-
const std::vector<ExecutionState *> &removedStates) override;
147+
void update(ExecutionState *current, const StateIterable &addedStates,
148+
const StateIterable &removedStates) override;
154149
bool empty() override;
155150
void printName(llvm::raw_ostream &os) override;
156151
};
@@ -197,9 +192,8 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber {
197192
theRNG(rng) {}
198193
~GuidedSearcher() override = default;
199194
ExecutionState &selectState() override;
200-
void update(ExecutionState *current,
201-
const std::vector<ExecutionState *> &addedStates,
202-
const std::vector<ExecutionState *> &removedStates) override;
195+
void update(ExecutionState *current, const StateIterable &addedStates,
196+
const StateIterable &removedStates) override;
203197
void update(const TargetHistoryTargetPairToStatesMap &added,
204198
const TargetHistoryTargetPairToStatesMap &removed) override;
205199
void updateTargets(ExecutionState *current);
@@ -238,9 +232,8 @@ class WeightedRandomSearcher final : public Searcher {
238232
~WeightedRandomSearcher() override = default;
239233

240234
ExecutionState &selectState() override;
241-
void update(ExecutionState *current,
242-
const std::vector<ExecutionState *> &addedStates,
243-
const std::vector<ExecutionState *> &removedStates) override;
235+
void update(ExecutionState *current, const StateIterable &addedStates,
236+
const StateIterable &removedStates) override;
244237
bool empty() override;
245238
void printName(llvm::raw_ostream &os) override;
246239
};
@@ -275,9 +268,8 @@ class RandomPathSearcher final : public Searcher {
275268
~RandomPathSearcher() override = default;
276269

277270
ExecutionState &selectState() override;
278-
void update(ExecutionState *current,
279-
const std::vector<ExecutionState *> &addedStates,
280-
const std::vector<ExecutionState *> &removedStates) override;
271+
void update(ExecutionState *current, const StateIterable &addedStates,
272+
const StateIterable &removedStates) override;
281273
bool empty() override;
282274
void printName(llvm::raw_ostream &os) override;
283275
};
@@ -309,9 +301,8 @@ class BatchingSearcher final : public Searcher {
309301
~BatchingSearcher() override = default;
310302

311303
ExecutionState &selectState() override;
312-
void update(ExecutionState *current,
313-
const std::vector<ExecutionState *> &addedStates,
314-
const std::vector<ExecutionState *> &removedStates) override;
304+
void update(ExecutionState *current, const StateIterable &addedStates,
305+
const StateIterable &removedStates) override;
315306
bool empty() override;
316307
void printName(llvm::raw_ostream &os) override;
317308
};
@@ -337,9 +328,6 @@ class IterativeDeepeningSearcher final : public Searcher,
337328
std::unique_ptr<Metric> metric;
338329
std::set<ExecutionState *> pausedStates;
339330

340-
void filter(const std::vector<ExecutionState *> &states,
341-
std::vector<ExecutionState *> &result) const;
342-
343331
public:
344332
/// \param baseSearcher The underlying searcher (takes ownership).
345333
explicit IterativeDeepeningSearcher(Searcher *baseSearcher,
@@ -348,9 +336,8 @@ class IterativeDeepeningSearcher final : public Searcher,
348336
~IterativeDeepeningSearcher() override = default;
349337

350338
ExecutionState &selectState() override;
351-
void update(ExecutionState *current,
352-
const std::vector<ExecutionState *> &addedStates,
353-
const std::vector<ExecutionState *> &removedStates) override;
339+
void update(ExecutionState *current, const StateIterable &addedStates,
340+
const StateIterable &removedStates) override;
354341
void update(const TargetHistoryTargetPairToStatesMap &added,
355342
const TargetHistoryTargetPairToStatesMap &removed) override;
356343
bool empty() override;
@@ -370,9 +357,8 @@ class InterleavedSearcher final : public Searcher {
370357
~InterleavedSearcher() override = default;
371358

372359
ExecutionState &selectState() override;
373-
void update(ExecutionState *current,
374-
const std::vector<ExecutionState *> &addedStates,
375-
const std::vector<ExecutionState *> &removedStates) override;
360+
void update(ExecutionState *current, const StateIterable &addedStates,
361+
const StateIterable &removedStates) override;
376362
bool empty() override;
377363
void printName(llvm::raw_ostream &os) override;
378364
};

0 commit comments

Comments
 (0)