aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp18
-rw-r--r--lib/Core/Executor.h4
-rw-r--r--lib/Core/ExecutorTimers.cpp4
-rw-r--r--lib/Core/Searcher.cpp122
-rw-r--r--lib/Core/Searcher.h56
5 files changed, 114 insertions, 90 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2c4e5202..49cba67f 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -665,7 +665,7 @@ void Executor::branch(ExecutionState &state,
for (unsigned i=1; i<N; ++i) {
ExecutionState *es = result[theRNG.getInt32() % i];
ExecutionState *ns = es->branch();
- addedStates.insert(ns);
+ addedStates.push_back(ns);
result.push_back(ns);
es->ptreeNode->data = 0;
std::pair<PTree::Node*,PTree::Node*> res =
@@ -883,7 +883,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
++stats::forks;
falseState = trueState->branch();
- addedStates.insert(falseState);
+ addedStates.push_back(falseState);
if (RandomizeFork && theRNG.getBool())
std::swap(trueState, falseState);
@@ -2467,9 +2467,9 @@ void Executor::updateStates(ExecutionState *current) {
states.insert(addedStates.begin(), addedStates.end());
addedStates.clear();
-
- for (std::set<ExecutionState*>::iterator
- it = removedStates.begin(), ie = removedStates.end();
+
+ for (std::vector<ExecutionState *>::iterator it = removedStates.begin(),
+ ie = removedStates.end();
it != ie; ++it) {
ExecutionState *es = *it;
std::set<ExecutionState*>::iterator it2 = states.find(es);
@@ -2674,7 +2674,8 @@ void Executor::run(ExecutionState &initialState) {
searcher = constructUserSearcher(*this);
- searcher->update(0, states, std::set<ExecutionState*>());
+ std::vector<ExecutionState *> newStates(states.begin(), states.end());
+ searcher->update(0, newStates, std::vector<ExecutionState *>());
while (!states.empty() && !haltExecution) {
ExecutionState &state = searcher->selectState();
@@ -2753,11 +2754,12 @@ void Executor::terminateState(ExecutionState &state) {
interpreterHandler->incPathsExplored();
- std::set<ExecutionState*>::iterator it = addedStates.find(&state);
+ std::vector<ExecutionState *>::iterator it =
+ std::find(addedStates.begin(), addedStates.end(), &state);
if (it==addedStates.end()) {
state.pc = state.prevPC;
- removedStates.insert(&state);
+ removedStates.push_back(&state);
} else {
// never reached searcher, just delete immediately
std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 =
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 99f5921b..92edc364 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -122,12 +122,12 @@ private:
/// instructions step.
/// \invariant \ref addedStates is a subset of \ref states.
/// \invariant \ref addedStates and \ref removedStates are disjoint.
- std::set<ExecutionState*> addedStates;
+ std::vector<ExecutionState *> addedStates;
/// Used to track states that have been removed during the current
/// instructions step.
/// \invariant \ref removedStates is a subset of \ref states.
/// \invariant \ref addedStates and \ref removedStates are disjoint.
- std::set<ExecutionState*> removedStates;
+ std::vector<ExecutionState *> removedStates;
/// When non-empty the Executor is running in "seed" mode. The
/// states in this map will be executed in an arbitrary order
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 480f1cde..f1c45105 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -179,7 +179,9 @@ void Executor::processTimers(ExecutionState *current,
dumpStates = 0;
}
- if (maxInstTime>0 && current && !removedStates.count(current)) {
+ if (maxInstTime > 0 && current &&
+ std::find(removedStates.begin(), removedStates.end(), current) ==
+ removedStates.end()) {
if (timerTicks*kSecondsPerTick > maxInstTime) {
klee_warning("max-instruction-time exceeded: %.2fs",
timerTicks*kSecondsPerTick);
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 299bb89d..973057c3 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -67,13 +67,14 @@ ExecutionState &DFSSearcher::selectState() {
}
void DFSSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
states.insert(states.end(),
addedStates.begin(),
addedStates.end());
- for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
- ie = removedStates.end(); it != ie; ++it) {
+ for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+ ie = removedStates.end();
+ it != ie; ++it) {
ExecutionState *es = *it;
if (es == states.back()) {
states.pop_back();
@@ -101,13 +102,14 @@ ExecutionState &BFSSearcher::selectState() {
}
void BFSSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
states.insert(states.end(),
addedStates.begin(),
addedStates.end());
- for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
- ie = removedStates.end(); it != ie; ++it) {
+ for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+ ie = removedStates.end();
+ it != ie; ++it) {
ExecutionState *es = *it;
if (es == states.front()) {
states.pop_front();
@@ -134,14 +136,16 @@ ExecutionState &RandomSearcher::selectState() {
return *states[theRNG.getInt32()%states.size()];
}
-void RandomSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+void
+RandomSearcher::update(ExecutionState *current,
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
states.insert(states.end(),
addedStates.begin(),
addedStates.end());
- for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
- ie = removedStates.end(); it != ie; ++it) {
+ for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+ ie = removedStates.end();
+ it != ie; ++it) {
ExecutionState *es = *it;
bool ok = false;
@@ -224,20 +228,24 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
}
}
-void WeightedRandomSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
- if (current && updateWeights && !removedStates.count(current))
+void WeightedRandomSearcher::update(
+ ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
+ if (current && updateWeights &&
+ std::find(removedStates.begin(), removedStates.end(), current) ==
+ removedStates.end())
states->update(current, getWeight(current));
-
- for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(),
- ie = addedStates.end(); it != ie; ++it) {
+
+ for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(),
+ ie = addedStates.end();
+ it != ie; ++it) {
ExecutionState *es = *it;
states->insert(es, getWeight(es));
}
- for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
- ie = removedStates.end(); it != ie; ++it) {
+ for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+ ie = removedStates.end();
+ it != ie; ++it) {
states->remove(*it);
}
}
@@ -277,9 +285,10 @@ ExecutionState &RandomPathSearcher::selectState() {
return *n->data;
}
-void RandomPathSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+void
+RandomPathSearcher::update(ExecutionState *current,
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
}
bool RandomPathSearcher::empty() {
@@ -358,9 +367,9 @@ entry:
}
}
-void BumpMergingSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+void BumpMergingSearcher::update(
+ ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
baseSearcher->update(current, addedStates, removedStates);
}
@@ -472,18 +481,21 @@ ExecutionState &MergingSearcher::selectState() {
return selectState();
}
-void MergingSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+void
+MergingSearcher::update(ExecutionState *current,
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
if (!removedStates.empty()) {
- std::set<ExecutionState *> alt = removedStates;
- for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
- ie = removedStates.end(); it != ie; ++it) {
+ std::vector<ExecutionState *> alt = removedStates;
+ for (std::vector<ExecutionState *>::const_iterator
+ it = removedStates.begin(),
+ ie = removedStates.end();
+ it != ie; ++it) {
ExecutionState *es = *it;
std::set<ExecutionState*>::const_iterator it2 = statesAtMerge.find(es);
if (it2 != statesAtMerge.end()) {
statesAtMerge.erase(it2);
- alt.erase(alt.find(es));
+ alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end());
}
}
baseSearcher->update(current, addedStates, alt);
@@ -529,10 +541,12 @@ ExecutionState &BatchingSearcher::selectState() {
}
}
-void BatchingSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
- if (removedStates.count(lastState))
+void
+BatchingSearcher::update(ExecutionState *current,
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
+ if (std::find(removedStates.begin(), removedStates.end(), lastState) !=
+ removedStates.end())
lastState = 0;
baseSearcher->update(current, addedStates, removedStates);
}
@@ -554,20 +568,22 @@ ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
return res;
}
-void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+void IterativeDeepeningTimeSearcher::update(
+ ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
double elapsed = util::getWallTime() - startTime;
if (!removedStates.empty()) {
- std::set<ExecutionState *> alt = removedStates;
- for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
- ie = removedStates.end(); it != ie; ++it) {
+ std::vector<ExecutionState *> alt = removedStates;
+ for (std::vector<ExecutionState *>::const_iterator
+ it = removedStates.begin(),
+ ie = removedStates.end();
+ it != ie; ++it) {
ExecutionState *es = *it;
std::set<ExecutionState*>::const_iterator it2 = pausedStates.find(es);
if (it2 != pausedStates.end()) {
pausedStates.erase(it2);
- alt.erase(alt.find(es));
+ alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end());
}
}
baseSearcher->update(current, addedStates, alt);
@@ -575,7 +591,10 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
baseSearcher->update(current, addedStates, removedStates);
}
- if (current && !removedStates.count(current) && elapsed>time) {
+ if (current &&
+ std::find(removedStates.begin(), removedStates.end(), current) ==
+ removedStates.end() &&
+ elapsed > time) {
pausedStates.insert(current);
baseSearcher->removeState(current);
}
@@ -583,7 +602,8 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
if (baseSearcher->empty()) {
time *= 2;
llvm::errs() << "KLEE: increasing time budget to: " << time << "\n";
- baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
+ std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
+ baseSearcher->update(0, ps, std::vector<ExecutionState *>());
pausedStates.clear();
}
}
@@ -607,9 +627,9 @@ ExecutionState &InterleavedSearcher::selectState() {
return s->selectState();
}
-void InterleavedSearcher::update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) {
+void InterleavedSearcher::update(
+ ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) {
for (std::vector<Searcher*>::const_iterator it = searchers.begin(),
ie = searchers.end(); it != ie; ++it)
(*it)->update(current, addedStates, removedStates);
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index d866f521..4ede3640 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -35,8 +35,8 @@ namespace klee {
virtual ExecutionState &selectState() = 0;
virtual void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates) = 0;
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates) = 0;
virtual bool empty() = 0;
@@ -55,15 +55,15 @@ namespace klee {
// utility functions
void addState(ExecutionState *es, ExecutionState *current = 0) {
- std::set<ExecutionState*> tmp;
- tmp.insert(es);
- update(current, tmp, std::set<ExecutionState*>());
+ std::vector<ExecutionState *> tmp;
+ tmp.push_back(es);
+ update(current, tmp, std::vector<ExecutionState *>());
}
void removeState(ExecutionState *es, ExecutionState *current = 0) {
- std::set<ExecutionState*> tmp;
- tmp.insert(es);
- update(current, std::set<ExecutionState*>(), tmp);
+ std::vector<ExecutionState *> tmp;
+ tmp.push_back(es);
+ update(current, std::vector<ExecutionState *>(), tmp);
}
enum CoreSearchType {
@@ -86,8 +86,8 @@ namespace klee {
public:
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return states.empty(); }
void printName(llvm::raw_ostream &os) {
os << "DFSSearcher\n";
@@ -100,8 +100,8 @@ namespace klee {
public:
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return states.empty(); }
void printName(llvm::raw_ostream &os) {
os << "BFSSearcher\n";
@@ -114,8 +114,8 @@ namespace klee {
public:
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return states.empty(); }
void printName(llvm::raw_ostream &os) {
os << "RandomSearcher\n";
@@ -146,8 +146,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty();
void printName(llvm::raw_ostream &os) {
os << "WeightedRandomSearcher::";
@@ -172,8 +172,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty();
void printName(llvm::raw_ostream &os) {
os << "RandomPathSearcher\n";
@@ -195,8 +195,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
void printName(llvm::raw_ostream &os) {
os << "MergingSearcher\n";
@@ -218,8 +218,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
void printName(llvm::raw_ostream &os) {
os << "BumpMergingSearcher\n";
@@ -243,8 +243,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return baseSearcher->empty(); }
void printName(llvm::raw_ostream &os) {
os << "<BatchingSearcher> timeBudget: " << timeBudget
@@ -266,8 +266,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return baseSearcher->empty() && pausedStates.empty(); }
void printName(llvm::raw_ostream &os) {
os << "IterativeDeepeningTimeSearcher\n";
@@ -286,8 +286,8 @@ namespace klee {
ExecutionState &selectState();
void update(ExecutionState *current,
- const std::set<ExecutionState*> &addedStates,
- const std::set<ExecutionState*> &removedStates);
+ const std::vector<ExecutionState *> &addedStates,
+ const std::vector<ExecutionState *> &removedStates);
bool empty() { return searchers[0]->empty(); }
void printName(llvm::raw_ostream &os) {
os << "<InterleavedSearcher> containing "
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-23 12:47:38 +0000