From 75197d4d8734050892272b8c290bc72e50f8fbe7 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 19 Dec 2023 01:00:52 +0400 Subject: [PATCH 1/4] [feat] Improve `and/or` expressions simplification --- lib/Expr/Expr.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 27cc2bcfff..6f707132b0 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -2018,6 +2018,9 @@ static ref AndExpr_createPartialR(const ref &cl, Expr *r) { return AndExpr_createPartial(r, cl); } static ref AndExpr_create(Expr *l, Expr *r) { + if (*l == *r) { + return l; + } return AndExpr::alloc(l, r); } @@ -2033,7 +2036,12 @@ static ref OrExpr_createPartial(Expr *l, const ref &cr) { static ref OrExpr_createPartialR(const ref &cl, Expr *r) { return OrExpr_createPartial(r, cl); } -static ref OrExpr_create(Expr *l, Expr *r) { return OrExpr::alloc(l, r); } +static ref OrExpr_create(Expr *l, Expr *r) { + if (*l == *r) { + return l; + } + return OrExpr::alloc(l, r); +} static ref XorExpr_createPartialR(const ref &cl, Expr *r) { if (cl->isZero()) { From 7d24f52e7773e8e53f7d95903830e1edae911f32 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 3 Feb 2024 22:37:11 +0100 Subject: [PATCH 2/4] [chore] Enable output of compile commands during generation --- CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 72ef2d30fb..6f6dedd689 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -70,6 +70,8 @@ endif() SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE) # use, i.e. don't skip the full RPATH for the build tree set(CMAKE_SKIP_BUILD_RPATH FALSE) +# Enable/Disable output of compile commands during generation +set(CMAKE_EXPORT_COMPILE_COMMANDS TRUE) ################################################################################ # Add our CMake module directory to the list of module search directories From 035f6923e0d98bdb2aa0a355fdc79403b3526c62 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 19 Feb 2024 10:27:55 +0100 Subject: [PATCH 3/4] [chore] Update `.gitignore` --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index e27fc5e755..77c409f5ec 100644 --- a/.gitignore +++ b/.gitignore @@ -33,3 +33,4 @@ autom4te.cache/ .vscode/ .cache/ +.helix/ From 2d8c9d5904fcb99cc1fdf44766ba823e5fa3e57d Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 28 Feb 2024 14:00:34 +0100 Subject: [PATCH 4/4] [feat] Rework `TargetManager`, get rid of `TargetManagerSubscriber` --- include/klee/ADT/PersistentSet.h | 3 + include/klee/Module/TargetForest.h | 6 +- lib/Core/ExecutionState.cpp | 2 + lib/Core/Executor.cpp | 7 +- lib/Core/Searcher.cpp | 130 +++++++++++++---------- lib/Core/Searcher.h | 78 ++++++++------ lib/Core/TargetCalculator.cpp | 23 +++- lib/Core/TargetCalculator.h | 3 +- lib/Core/TargetManager.cpp | 90 ++++++++++------ lib/Core/TargetManager.h | 145 ++------------------------ lib/Core/TargetedExecutionManager.cpp | 8 +- lib/Core/UserSearcher.cpp | 12 +-- lib/Module/CodeGraphInfo.cpp | 12 ++- lib/Module/TargetForest.cpp | 41 ++++++-- 14 files changed, 272 insertions(+), 288 deletions(-) diff --git a/include/klee/ADT/PersistentSet.h b/include/klee/ADT/PersistentSet.h index 186f556b38..a01f94c1e6 100644 --- a/include/klee/ADT/PersistentSet.h +++ b/include/klee/ADT/PersistentSet.h @@ -72,6 +72,9 @@ template > class PersistentSet { } return true; } + bool operator!=(const PersistentSet &other) const { + return !(*this == other); + } iterator find(const key_type &key) const { return elts.find(key); } iterator lower_bound(const key_type &key) const { diff --git a/include/klee/Module/TargetForest.h b/include/klee/Module/TargetForest.h index e664821e9f..a729df7115 100644 --- a/include/klee/Module/TargetForest.h +++ b/include/klee/Module/TargetForest.h @@ -293,9 +293,10 @@ class TargetForest { } void dump(unsigned n) const; - void addLeafs( + void pullConfidences( std::vector, confidence::ty>> &leafs, confidence::ty parentConfidence) const; + void pullLeafs(std::vector> &leafs) const; void propagateConfidenceToChildren(); ref deepCopy(); Layer *copy(); @@ -357,7 +358,8 @@ class TargetForest { const TargetHashSet getTargets() const { return forest->getTargets(); } void dump() const; std::vector, confidence::ty>> - leafs() const; + confidences() const; + std::set> leafs() const; ref deepCopy(); void divideConfidenceBy(unsigned factor) { forest->divideConfidenceBy(factor); diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index fa14493607..78d2f6a546 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -189,6 +189,8 @@ ExecutionState *ExecutionState::branch() { auto *falseState = new ExecutionState(*this); falseState->setID(); falseState->coveredLines.clear(); + falseState->prevTargets_ = falseState->targets_; + falseState->prevHistory_ = falseState->history_; return falseState; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index eca2e57d1e..0539d46757 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4642,7 +4642,12 @@ void Executor::executeStep(ExecutionState &state) { .c_str()); } - if (targetManager->isTargeted(state) && state.targets().empty()) { + if (targetManager) { + targetManager->pullGlobal(state); + } + + if (targetManager && targetManager->isTargeted(state) && + state.targets().empty()) { terminateStateEarlyAlgorithm(state, "State missed all it's targets.", StateTerminationType::MissedAllTargets); } else if (state.isCycled(MaxCycles)) { diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index f42f798141..c26df5ec21 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -48,8 +48,8 @@ using namespace llvm; ExecutionState &DFSSearcher::selectState() { return *states.back(); } void DFSSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { + const std::vector &addedStates, + const std::vector &removedStates) { // insert states states.insert(states.end(), addedStates.begin(), addedStates.end()); @@ -74,8 +74,8 @@ void DFSSearcher::printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; } ExecutionState &BFSSearcher::selectState() { return *states.front(); } void BFSSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { + const std::vector &addedStates, + const std::vector &removedStates) { // update current state // Assumption: If new states were added KLEE forked, therefore states evolved. // constraints were added to the current state, it evolved. @@ -115,9 +115,9 @@ ExecutionState &RandomSearcher::selectState() { return *states[theRNG.getInt32() % states.size()]; } -void RandomSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void RandomSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { // insert states states.insert(states.end(), addedStates.begin(), addedStates.end()); @@ -153,9 +153,9 @@ TargetedSearcher::TargetedSearcher(ref target, ExecutionState &TargetedSearcher::selectState() { return *states->choose(0); } -void TargetedSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void TargetedSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { // update current if (current && std::find(removedStates.begin(), removedStates.end(), @@ -211,9 +211,14 @@ ExecutionState &GuidedSearcher::selectState() { return *state; } -void GuidedSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void GuidedSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { + if (current) { + localStates.insert(current); + } + update(localStates); + localStates.clear(); if (current) { ref history = current->history(); @@ -270,13 +275,14 @@ void GuidedSearcher::update(ExecutionState *current, } } -void GuidedSearcher::update(const TargetHistoryTargetPairToStatesMap &added, - const TargetHistoryTargetPairToStatesMap &removed) { - for (const auto &pair : added) { +void GuidedSearcher::update(const states_ty &states) { + targetManager.collectFiltered(states, addedTStates, removedTStates); + + for (const auto &pair : addedTStates) { if (!pair.second.empty()) localHistoryTargets.insert(pair.first); } - for (const auto &pair : removed) { + for (const auto &pair : removedTStates) { if (!pair.second.empty()) localHistoryTargets.insert(pair.first); } @@ -290,13 +296,20 @@ void GuidedSearcher::update(const TargetHistoryTargetPairToStatesMap &added, } targetedSearchers.at({history, target}) - ->update(nullptr, added.at({history, target}), - removed.at({history, target})); + ->update(nullptr, addedTStates.at({history, target}), + removedTStates.at({history, target})); if (targetedSearchers.at({history, target})->empty()) { removeTarget(history, target); } } localHistoryTargets.clear(); + + for (auto &pair : addedTStates) { + pair.second.clear(); + } + for (auto &pair : removedTStates) { + pair.second.clear(); + } } bool GuidedSearcher::isThereTarget(ref history, @@ -408,9 +421,9 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { } } -void WeightedRandomSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void WeightedRandomSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { // update current if (current && updateWeights && @@ -501,11 +514,11 @@ ExecutionState &RandomPathSearcher::selectState() { return *n->state; } -void RandomPathSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void RandomPathSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { // insert states - for (auto es : addedStates) { + for (auto &es : addedStates) { PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; PTreeNodePtr &root = processForest.getPTrees().at(pnode->getTreeID())->root; PTreeNodePtr *childPtr; @@ -605,9 +618,9 @@ ExecutionState &BatchingSearcher::selectState() { return *lastState; } -void BatchingSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void BatchingSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { // drop memoized state if it is marked for deletion if (std::find(removedStates.begin(), removedStates.end(), lastState) != removedStates.end()) @@ -662,10 +675,9 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric { } }; -IterativeDeepeningSearcher::IterativeDeepeningSearcher( - Searcher *baseSearcher, TargetManagerSubscriber *tms, - HaltExecution::Reason m) - : baseSearcher{baseSearcher}, tms{tms} { +IterativeDeepeningSearcher::IterativeDeepeningSearcher(Searcher *baseSearcher, + HaltExecution::Reason m) + : baseSearcher{baseSearcher} { switch (m) { case HaltExecution::Reason::MaxTime: metric = std::make_unique(); @@ -684,30 +696,35 @@ ExecutionState &IterativeDeepeningSearcher::selectState() { return res; } -void IterativeDeepeningSearcher::update( - const TargetHistoryTargetPairToStatesMap &added, - const TargetHistoryTargetPairToStatesMap &removed) { - if (!tms) - return; - added.setWithout(&pausedStates); - removed.setWithout(&pausedStates); - tms->update(added, removed); - added.clearWithout(); - removed.clearWithout(); +void IterativeDeepeningSearcher::updateAndFilter( + const StatesVector &removedStates, StatesVector &result) { + for (auto &state : removedStates) { + if (pausedStates.count(state)) { + pausedStates.erase(state); + } else { + result.push_back(state); + } + } } void IterativeDeepeningSearcher::update(ExecutionState *current, - const StateIterable &added, - const StateIterable &removed) { - removed.setWithout(&pausedStates); - baseSearcher->update(current, added, removed); - removed.clearWithout(); - - for (auto state : removed) - pausedStates.erase(state); + const StatesVector &addedStates, + const StatesVector &removedStates) { + activeRemovedStates.clear(); + // update underlying searcher (filter paused states unknown to underlying + // searcher) + if (!removedStates.empty() && !pausedStates.empty()) { + IterativeDeepeningSearcher::updateAndFilter(removedStates, + activeRemovedStates); + baseSearcher->update(current, addedStates, activeRemovedStates); + } else { + baseSearcher->update(current, addedStates, removedStates); + } + // update current: pause if time exceeded if (current && - std::find(removed.begin(), removed.end(), current) == removed.end() && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end() && metric->exceeds(*current)) { pausedStates.insert(current); baseSearcher->update(nullptr, {}, {current}); @@ -716,7 +733,8 @@ void IterativeDeepeningSearcher::update(ExecutionState *current, // no states left in underlying searcher: fill with paused states if (baseSearcher->empty() && !pausedStates.empty()) { metric->increaseLimit(); - baseSearcher->update(nullptr, pausedStates, {}); + StatesVector ps(pausedStates.begin(), pausedStates.end()); + baseSearcher->update(nullptr, ps, {}); pausedStates.clear(); } } @@ -745,9 +763,9 @@ ExecutionState &InterleavedSearcher::selectState() { return s->selectState(); } -void InterleavedSearcher::update(ExecutionState *current, - const StateIterable &addedStates, - const StateIterable &removedStates) { +void InterleavedSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { // update underlying searchers for (auto &searcher : searchers) diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index f0b7e8d2b5..b2247cf10f 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -63,8 +63,9 @@ class Searcher { /// \param current The currently selected state for exploration. /// \param addedStates The newly branched states with `current` as common /// ancestor. \param removedStates The states that will be terminated. - virtual void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) = 0; + virtual void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) = 0; /// \return True if no state left for exploration, False otherwise virtual bool empty() = 0; @@ -95,8 +96,9 @@ class DFSSearcher final : public Searcher { public: ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -110,8 +112,9 @@ class BFSSearcher final : public Searcher { public: ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -124,8 +127,9 @@ class RandomSearcher final : public Searcher { public: explicit RandomSearcher(RNG &rng); ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -144,13 +148,14 @@ class TargetedSearcher final : public Searcher { ~TargetedSearcher() override; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; -class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { +class GuidedSearcher final : public Searcher { template using TargetHistoryTargetPairHashMap = std::unordered_map baseSearcher; TargetHistoryTargetPairToSearcherMap targetedSearchers; DistanceCalculator &distanceCalculator; + TargetManager &targetManager; RNG &theRNG; unsigned index{1}; bool interleave = true; @@ -176,6 +182,7 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { std::vector baseRemovedStates; TargetHistoryTargetPairToStatesMap addedTStates; TargetHistoryTargetPairToStatesMap removedTStates; + states_ty localStates; TargetHashSet removedTargets; TargetHashSet addedTargets; @@ -188,15 +195,15 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { public: GuidedSearcher(Searcher *baseSearcher, DistanceCalculator &distanceCalculator, - RNG &rng) + TargetManager &targetManager, RNG &rng) : baseSearcher(baseSearcher), distanceCalculator(distanceCalculator), - theRNG(rng) {} + targetManager(targetManager), theRNG(rng) {} ~GuidedSearcher() override = default; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; - void update(const TargetHistoryTargetPairToStatesMap &added, - const TargetHistoryTargetPairToStatesMap &removed) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; + void update(const states_ty &states); void updateTargets(ExecutionState *current); bool empty() override; @@ -233,8 +240,9 @@ class WeightedRandomSearcher final : public Searcher { ~WeightedRandomSearcher() override = default; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -269,8 +277,9 @@ class RandomPathSearcher final : public Searcher { ~RandomPathSearcher() override = default; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -302,8 +311,9 @@ class BatchingSearcher final : public Searcher { ~BatchingSearcher() override = default; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -313,8 +323,7 @@ class BatchingSearcher final : public Searcher { /// limit, it is paused (removed from underlying searcher). When the underlying /// searcher runs out of states, the metric limit is increased and all paused /// states are revived (added to underlying searcher). -class IterativeDeepeningSearcher final : public Searcher, - public TargetManagerSubscriber { +class IterativeDeepeningSearcher final : public Searcher { public: struct Metric { virtual ~Metric() = default; @@ -325,22 +334,22 @@ class IterativeDeepeningSearcher final : public Searcher, private: std::unique_ptr baseSearcher; - TargetManagerSubscriber *tms; std::unique_ptr metric; - std::set pausedStates; + states_ty pausedStates; + StatesVector activeRemovedStates; + + void updateAndFilter(const StatesVector &states, StatesVector &result); public: /// \param baseSearcher The underlying searcher (takes ownership). explicit IterativeDeepeningSearcher(Searcher *baseSearcher, - TargetManagerSubscriber *tms, HaltExecution::Reason metric); ~IterativeDeepeningSearcher() override = default; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; - void update(const TargetHistoryTargetPairToStatesMap &added, - const TargetHistoryTargetPairToStatesMap &removed) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; @@ -358,8 +367,9 @@ class InterleavedSearcher final : public Searcher { ~InterleavedSearcher() override = default; ExecutionState &selectState() override; - void update(ExecutionState *current, const StateIterable &addedStates, - const StateIterable &removedStates) override; + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; bool empty() override; void printName(llvm::raw_ostream &os) override; }; diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index 1b19982b34..fab4393013 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -35,6 +35,23 @@ llvm::cl::opt TrackCoverage( void TargetCalculator::update(const ExecutionState &state) { Function *initialFunction = state.getInitPCBlock()->getParent(); + if (state.prevPC == state.prevPC->parent->getLastInstruction() && + !fullyCoveredFunctions.count(state.pc->parent->parent)) { + auto &fBranches = getCoverageTargets(state.pc->parent->parent); + if (!coveredFunctionsInBranches.count(state.pc->parent->parent)) { + if (fBranches.count(state.pc->parent) != 0) { + if (!coveredBranches[state.pc->parent->parent].count( + state.pc->parent)) { + coveredBranches[state.pc->parent->parent][state.pc->parent]; + } + } + } + if (getCoverageTargets(state.pc->parent->parent) == + coveredBranches[state.pc->parent->parent]) { + coveredFunctionsInBranches.insert(state.pc->parent->parent); + } + } + if (state.prevPC == state.prevPC->parent->getLastInstruction() && !fullyCoveredFunctions.count(state.prevPC->parent->parent)) { auto &fBranches = getCoverageTargets(state.prevPC->parent->parent); @@ -147,9 +164,7 @@ TargetCalculator::getCoverageTargets(KFunction *kf) { } } -bool TargetCalculator::uncoveredBlockPredicate(ExecutionState *state, - KBlock *kblock) { - Function *initialFunction = state->getInitPCBlock()->getParent(); +bool TargetCalculator::uncoveredBlockPredicate(KBlock *kblock) { bool result = false; auto &fBranches = getCoverageTargets(kblock->parent); @@ -196,7 +211,7 @@ TargetHashSet TargetCalculator::calculate(ExecutionState &state) { std::set blocks; using std::placeholders::_1; KBlockPredicate func = - std::bind(&TargetCalculator::uncoveredBlockPredicate, this, &state, _1); + std::bind(&TargetCalculator::uncoveredBlockPredicate, this, _1); codeGraphInfo.getNearestPredicateSatisfying(kb, func, blocks); if (!blocks.empty()) { diff --git a/lib/Core/TargetCalculator.h b/lib/Core/TargetCalculator.h index f337b879fd..3df8bdd28a 100644 --- a/lib/Core/TargetCalculator.h +++ b/lib/Core/TargetCalculator.h @@ -66,6 +66,7 @@ class TargetCalculator { TargetHashSet calculate(ExecutionState &state); bool isCovered(KFunction *kf) const; + bool uncoveredBlockPredicate(KBlock *kblock); private: CodeGraphInfo &codeGraphInfo; @@ -76,8 +77,6 @@ class TargetCalculator { const std::map> & getCoverageTargets(KFunction *kf); - - bool uncoveredBlockPredicate(ExecutionState *state, KBlock *kblock); }; } // namespace klee diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index f72e329135..15f5d0484d 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -20,6 +20,26 @@ using namespace klee; namespace klee {} // namespace klee +void TargetManager::pullGlobal(ExecutionState &state) { + if (!isTargeted(state) || targets(state).size() == 0) { + return; + } + + auto &stateTargetForest = targetForest(state); + + for (auto &target : stateTargetForest.leafs()) { + if (reachedTargets.count(target)) { + stateTargetForest.block(target); + } + } + setTargets(state, stateTargetForest.getTargets()); + if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { + if (targets(state).size() == 0) { + state.setTargeted(false); + } + } +} + void TargetManager::updateMiss(ExecutionState &state, ref target) { auto &stateTargetForest = targetForest(state); stateTargetForest.remove(target); @@ -43,20 +63,7 @@ void TargetManager::updateDone(ExecutionState &state, ref target) { target->shouldFailOnThisTarget()) { if (target->shouldFailOnThisTarget() || !isa(target->getBlock())) { - reachedTargets.insert(target); - } - - for (auto es : states) { - if (isTargeted(*es)) { - auto &esTargetForest = targetForest(*es); - esTargetForest.block(target); - setTargets(*es, esTargetForest.getTargets()); - if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { - if (targets(*es).size() == 0) { - es->setTargeted(false); - } - } - } + setReached(target); } } if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { @@ -106,6 +113,27 @@ void TargetManager::collect(ExecutionState &state) { } } +void TargetManager::collectFiltered( + const StatesSet &filter, TargetHistoryTargetPairToStatesMap &added, + TargetHistoryTargetPairToStatesMap &removed) { + for (auto htStatesPair : addedTStates) { + for (auto &state : htStatesPair.second) { + if (filter.count(state)) { + added[htStatesPair.first].push_back(state); + removed[htStatesPair.first]; + } + } + } + for (auto htStatesPair : removedTStates) { + for (auto &state : htStatesPair.second) { + if (filter.count(state)) { + removed[htStatesPair.first].push_back(state); + added[htStatesPair.first]; + } + } + } +} + void TargetManager::updateReached(ExecutionState &state) { auto prevKI = state.prevPC; auto kf = prevKI->parent->parent; @@ -117,6 +145,10 @@ void TargetManager::updateReached(ExecutionState &state) { if (state.getPrevPCBlock()->getTerminator()->getNumSuccessors() == 0) { target = ReachBlockTarget::create(state.prevPC->parent, true); + } else if (isa(state.prevPC->parent) && + !targetCalculator.uncoveredBlockPredicate( + state.prevPC->parent)) { + target = ReachBlockTarget::create(state.prevPC->parent, true); } else if (!isa(state.prevPC->parent)) { unsigned index = 0; for (auto succ : successors(state.getPrevPCBlock())) { @@ -130,6 +162,8 @@ void TargetManager::updateReached(ExecutionState &state) { if (target && guidance == Interpreter::GuidanceKind::CoverageGuidance) { setReached(target); + target = ReachBlockTarget::create(state.pc->parent, false); + setReached(target); } } } @@ -203,11 +237,15 @@ void TargetManager::update(ExecutionState *current, } } + for (auto &pair : addedTStates) { + pair.second.clear(); + } + for (auto &pair : removedTStates) { + pair.second.clear(); + } + for (auto state : changedStates) { - if (std::find(addedStates.begin(), addedStates.end(), state) == - addedStates.end()) { - collect(*state); - } + collect(*state); state->stepTargetsAndHistory(); } @@ -216,17 +254,6 @@ void TargetManager::update(ExecutionState *current, distances.erase(state); } - for (auto subscriber : subscribers) { - subscriber->update(addedTStates, removedTStates); - } - - for (auto &pair : addedTStates) { - pair.second.clear(); - } - for (auto &pair : removedTStates) { - pair.second.clear(); - } - changedStates.clear(); localStates.clear(); } @@ -257,6 +284,11 @@ bool TargetManager::isReachedTarget(const ExecutionState &state, } return true; } + } else { + if (state.pc->parent == target->getBlock()) { + result = Done; + return true; + } } } diff --git a/lib/Core/TargetManager.h b/lib/Core/TargetManager.h index ba2dea9ab3..dae52abab4 100644 --- a/lib/Core/TargetManager.h +++ b/lib/Core/TargetManager.h @@ -28,139 +28,13 @@ class TargetCalculator; using TargetHistoryTargetPair = std::pair, ref>; using StatesVector = std::vector; -using StateSet = std::set; - -class StateIterable final { -private: - using v = ExecutionState *; - const StatesVector *self; - mutable const StateSet *without = nullptr; - using vec_it = StatesVector::const_iterator; - bool shouldDestruct; - - class it : public std::iterator { - vec_it self; - const vec_it ie; - const StateSet *without = nullptr; - void goUntilRealNode() { - if (!without) - return; - for (; self != ie; self++) { - if (!without->count(*self)) - return; - } - } - - public: - it(vec_it i, vec_it ie, const StateSet *without) - : self(i), ie(ie), without(without) { - goUntilRealNode(); - } - bool operator==(const it &other) const noexcept { - return self == other.self; - }; - bool operator!=(const it &other) const noexcept { - return self != other.self; - }; - it &operator++() noexcept { - if (self != ie) { - self++; - goUntilRealNode(); - } - return *this; - } - v operator*() const noexcept { return *self; } - }; - -public: - StateIterable() : self(new StatesVector()), shouldDestruct(true) {} - StateIterable(v s) : self(new StatesVector({s})), shouldDestruct(true) {} - StateIterable(const StatesVector &v, const StateSet *without) - : self(&v), without(without), shouldDestruct(false) {} - StateIterable(const StatesVector &v) : StateIterable(v, nullptr) {} - StateIterable(const StateSet &s) - : self(new StatesVector(s.begin(), s.end())), shouldDestruct(true) {} - ~StateIterable() { - if (shouldDestruct) - delete self; - } - bool empty() const noexcept { - return without ? begin() == end() : self->empty(); - } - it begin() const noexcept { return it(self->begin(), self->end(), without); } - it end() const noexcept { return it(self->end(), self->end(), without); } - - void setWithout(const StateSet *w) const { without = w; } - void clearWithout() const { without = nullptr; } -}; - -class TargetHistoryTargetPairToStatesMap final { -private: - using k = TargetHistoryTargetPair; - using cv = StateIterable; - using p = std::pair; - using v = StatesVector; - using t = - std::unordered_map; - using map_it = t::iterator; - using map_cit = t::const_iterator; - t self; - mutable const StateSet *without = nullptr; - - class it : public std::iterator { - protected: - map_cit self; - const StateSet *without = nullptr; - - public: - it(map_cit i, const StateSet *without) : self(i), without(without) {} - bool operator==(const it &other) const noexcept { - return self == other.self; - }; - bool operator!=(const it &other) const noexcept { - return self != other.self; - }; - it &operator++() noexcept { - self++; - return *this; - } - p operator*() const noexcept { - return std::make_pair(self->first, StateIterable(self->second, without)); - } - }; - -public: - inline v &operator[](const k &__k) { return self[__k]; } - inline v &operator[](k &&__k) { return self[std::move(__k)]; } - inline v &at(const k &__k) { return self.at(__k); } - inline map_it begin() noexcept { return self.begin(); } - inline map_it end() noexcept { return self.end(); } - - inline const cv at(const k &__k) const { - cv result = self.at(__k); - result.setWithout(without); - return result; - } - inline it begin() const noexcept { return it(self.begin(), without); }; - inline it end() const noexcept { return it(self.end(), without); }; - - void setWithout(const StateSet *w) const { without = w; } - void clearWithout() const { without = nullptr; } -}; - -class TargetManagerSubscriber { -public: - virtual ~TargetManagerSubscriber() = default; - - /// Selects a state for further exploration. - /// \return The selected state. - virtual void update(const TargetHistoryTargetPairToStatesMap &added, - const TargetHistoryTargetPairToStatesMap &removed) = 0; -}; +using TargetHistoryTargetPairToStatesMap = + std::unordered_map; class TargetManager { private: - using StatesSet = std::unordered_set; + using StatesSet = states_ty; using StateToDistanceMap = std::unordered_map>; using TargetForestHistoryTargetSet = @@ -175,7 +49,6 @@ class TargetManager { StateToDistanceMap distances; StatesSet localStates; StatesSet changedStates; - std::vector subscribers; TargetHistoryTargetPairToStatesMap addedTStates; TargetHistoryTargetPairToStatesMap removedTStates; TargetHashSet removedTargets; @@ -261,15 +134,17 @@ class TargetManager { return state.targetForest; } - void subscribe(TargetManagerSubscriber &subscriber) { - subscribers.push_back(&subscriber); - } - bool isTargeted(const ExecutionState &state) { return state.isTargeted(); } bool isReachedTarget(const ExecutionState &state, ref target); void setReached(ref target) { reachedTargets.insert(target); } + + void pullGlobal(ExecutionState &state); + + void collectFiltered(const StatesSet &filter, + TargetHistoryTargetPairToStatesMap &added, + TargetHistoryTargetPairToStatesMap &removed); }; } // namespace klee diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index 37961c20f3..755c261ae2 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -186,8 +186,8 @@ cl::opt } // namespace klee TargetedHaltsOnTraces::TargetedHaltsOnTraces(ref &forest) { - auto leafs = forest->leafs(); - for (auto finalTargetSetPair : leafs) { + auto confidences = forest->confidences(); + for (auto finalTargetSetPair : confidences) { traceToHaltTypeToConfidence.emplace(finalTargetSetPair.first, HaltTypeToConfidence()); } @@ -195,8 +195,8 @@ TargetedHaltsOnTraces::TargetedHaltsOnTraces(ref &forest) { void TargetedHaltsOnTraces::subtractConfidencesFrom( TargetForest &forest, HaltExecution::Reason reason) { - auto leafs = forest.leafs(); - for (auto finalTargetSetPair : leafs) { + auto confidences = forest.confidences(); + for (auto finalTargetSetPair : confidences) { auto &haltTypeToConfidence = traceToHaltTypeToConfidence.at(finalTargetSetPair.first); auto confidence = finalTargetSetPair.second; diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 59674a84f7..47ba08d07f 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -178,22 +178,16 @@ Searcher *klee::constructUserSearcher(Executor &executor, BatchInstructions); } - TargetManagerSubscriber *tms = nullptr; if (executor.guidanceKind != Interpreter::GuidanceKind::NoGuidance) { searcher = new GuidedSearcher(searcher, *executor.distanceCalculator, - executor.theRNG); - tms = static_cast(searcher); + *executor.targetManager, executor.theRNG); } if (UseIterativeDeepeningSearch != HaltExecution::Reason::Unspecified) { - searcher = new IterativeDeepeningSearcher(searcher, tms, - UseIterativeDeepeningSearch); - tms = static_cast(searcher); + searcher = + new IterativeDeepeningSearcher(searcher, UseIterativeDeepeningSearch); } - if (tms) - executor.targetManager->subscribe(*tms); - llvm::raw_ostream &os = executor.getHandler().getInfoStream(); os << "BEGIN searcher description\n"; diff --git a/lib/Module/CodeGraphInfo.cpp b/lib/Module/CodeGraphInfo.cpp index 4823460b87..b57fde6c95 100644 --- a/lib/Module/CodeGraphInfo.cpp +++ b/lib/Module/CodeGraphInfo.cpp @@ -9,6 +9,8 @@ #include "klee/Module/CodeGraphInfo.h" +#include "klee/Module/KModule.h" + #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH DISABLE_WARNING_DEPRECATED_DECLARATIONS @@ -123,10 +125,12 @@ void CodeGraphInfo::calculateFunctionBranches(KFunction *kf) { std::map> &fbranches = functionBranches[kf]; for (auto &kb : kf->blocks) { fbranches[kb.get()]; - for (unsigned branch = 0; - branch < kb->basicBlock()->getTerminator()->getNumSuccessors(); - ++branch) { - fbranches[kb.get()].insert(branch); + if (!isa(kb.get())) { + for (unsigned branch = 0; + branch < kb->basicBlock()->getTerminator()->getNumSuccessors(); + ++branch) { + fbranches[kb.get()].insert(branch); + } } } } diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp index cb2f8a907e..8f4a551e31 100644 --- a/lib/Module/TargetForest.cpp +++ b/lib/Module/TargetForest.cpp @@ -550,26 +550,51 @@ void TargetForest::dump() const { forest->dump(1); } -void TargetForest::Layer::addLeafs( - std::vector, confidence::ty>> &leafs, +void TargetForest::Layer::pullConfidences( + std::vector, confidence::ty>> + &confidences, confidence::ty parentConfidence) const { for (const auto &targetAndForest : forest) { auto targetsVec = targetAndForest.first; auto layer = targetAndForest.second; auto confidence = layer->getConfidence(parentConfidence); if (layer->empty()) { - leafs.push_back(std::make_pair(targetsVec, confidence)); + confidences.push_back(std::make_pair(targetsVec, confidence)); } else { - layer->addLeafs(leafs, confidence); + layer->pullConfidences(confidences, confidence); + } + } +} + +void TargetForest::Layer::pullLeafs(std::vector> &leafs) const { + for (const auto &targetAndForest : forest) { + auto layer = targetAndForest.second; + if (layer->empty()) { + for (auto &targetVect : targetsToVector) { + leafs.push_back(targetVect.first); + } + } else { + layer->pullLeafs(leafs); } } } std::vector, confidence::ty>> -TargetForest::leafs() const { - std::vector, confidence::ty>> leafs; - forest->addLeafs(leafs, forest->getConfidence()); - return leafs; +TargetForest::confidences() const { + std::vector, confidence::ty>> confidences; + forest->pullConfidences(confidences, forest->getConfidence()); + return confidences; +} + +std::set> TargetForest::leafs() const { + std::vector> leafs; + forest->pullLeafs(leafs); + + std::set> targets; + for (auto &leaf : leafs) { + targets.insert(leaf); + } + return targets; } ref TargetForest::deepCopy() {