diff options
author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2017-06-24 19:23:32 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-11-30 12:18:15 +0000 |
commit | bc84fb1f642cbd15064c86d3839e278be536b254 (patch) | |
tree | 316c6a71c8eb894ea9d7b05e0ffbf88273cac961 /lib | |
parent | fb01144ad362210e088a27e21c062ecd16b3f097 (diff) | |
download | klee-bc84fb1f642cbd15064c86d3839e278be536b254.tar.gz |
Added pause and continue functionality for states in Executor
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 28 | ||||
-rw-r--r-- | lib/Core/Executor.h | 11 |
2 files changed, 39 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0b7aa1a9..e79d6a2c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2456,6 +2456,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { void Executor::updateStates(ExecutionState *current) { if (searcher) { searcher->update(current, addedStates, removedStates); + searcher->update(0, continuedStates, pausedStates); + pausedStates.clear(); + continuedStates.clear(); } states.insert(addedStates.begin(), addedStates.end()); @@ -2741,6 +2744,31 @@ std::string Executor::getAddressInfo(ExecutionState &state, return info.str(); } +void Executor::pauseState(ExecutionState &state){ + std::vector<ExecutionState *>::iterator it = std::find(continuedStates.begin(), continuedStates.end(), &state); + // If the state was to be continued, but now gets paused again + if (it != continuedStates.end()){ + // ...just don't continue it + std::swap(*it, continuedStates.back()); + continuedStates.pop_back(); + } else { + pausedStates.push_back(&state); + } +} + +void Executor::continueState(ExecutionState &state){ + std::vector<ExecutionState *>::iterator it = std::find(pausedStates.begin(), pausedStates.end(), &state); + // If the state was to be paused, but now gets continued again + if (it != pausedStates.end()){ + // ...don't pause it + std::swap(*it, pausedStates.back()); + pausedStates.pop_back(); + } else { + continuedStates.push_back(&state); + } +} + + void Executor::terminateState(ExecutionState &state) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 27cefcc0..c6f01179 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -144,6 +144,13 @@ private: /// \invariant \ref addedStates and \ref removedStates are disjoint. std::vector<ExecutionState *> removedStates; + /// Used to track states that are not terminated, but should not + /// be scheduled by the searcher. + std::vector<ExecutionState *> pausedStates; + /// States that were 'paused' from scheduling, that now may be + /// scheduled again + std::vector<ExecutionState *> continuedStates; + /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order /// (outside the normal search interface) until they terminate. When @@ -389,6 +396,10 @@ private: bool shouldExitOn(enum TerminateReason termReason); + // remove state from searcher only + void pauseState(ExecutionState& state); + // add state to searcher only + void continueState(ExecutionState& state); // remove state from queue and delete void terminateState(ExecutionState &state); // call exit handler and terminate state |