diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 88cc18b2fd..d558549c0b 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3788,7 +3788,6 @@ void Executor::updateStates(ExecutionState *current) { processForest->remove(es->ptreeNode); delete es; } - removedButReachableStates.clear(); removedStates.clear(); } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 17501df28a..cc85227a91 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -134,7 +134,6 @@ class Executor : public Interpreter { SetOfStates states; SetOfStates pausedStates; - SetOfStates removedButReachableStates; StatsTracker *statsTracker; TreeStreamWriter *pathWriter, *symPathWriter; SpecialFunctionHandler *specialFunctionHandler; diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 5222e5b138..521216ea26 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -439,24 +439,18 @@ void TargetedSearcher::removeReached() { GuidedSearcher::GuidedSearcher( Searcher *baseSearcher, CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory, - std::set - &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng) : guidance(CoverageGuidance), baseSearcher(baseSearcher), codeGraphDistance(codeGraphDistance), stateHistory(&stateHistory), - removedButReachableStates(removedButReachableStates), pausedStates(pausedStates), bound(bound), theRNG(rng) {} GuidedSearcher::GuidedSearcher( CodeGraphDistance &codeGraphDistance, - std::set - &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng) : guidance(ErrorGuidance), baseSearcher(nullptr), codeGraphDistance(codeGraphDistance), stateHistory(nullptr), - removedButReachableStates(removedButReachableStates), pausedStates(pausedStates), bound(bound), theRNG(rng) {} ExecutionState &GuidedSearcher::selectState() { @@ -548,13 +542,39 @@ static void updateConfidences(ExecutionState *current, current->targetForest.divideConfidenceBy(reachableStatesOfTarget); } -static void updateConfidences(ExecutionState *current, - const std::vector &addedStates, - const GuidedSearcher::TargetToStateUnorderedSetMap - &reachableStatesOfTarget) { - updateConfidences(current, reachableStatesOfTarget); - for (auto state : addedStates) { - updateConfidences(state, reachableStatesOfTarget); +void GuidedSearcher::updateTargetedSearcherForStates( + std::vector &states, + std::vector &tmpAddedStates, + std::vector &tmpRemovedStates, + TargetToStateUnorderedSetMap &reachableStatesOfTarget, bool areStatesStuck, + bool areStatesRemoved) { + for (const auto state : states) { + auto history = state->targetForest.getHistory(); + auto targets = state->targetForest.getTargets(); + TargetForest::TargetsSet stateTargets; + for (auto &targetF : *targets) { + stateTargets.insert(targetF.first); + } + + for (auto &target : stateTargets) { + if (areStatesRemoved || state->targetForest.contains(target)) { + if (areStatesRemoved) + tmpRemovedStates.push_back(state); + else + tmpAddedStates.push_back(state); + assert(!state->targetForest.empty()); + + bool canReach = areStatesStuck; // overapproximation: assume that stuck + // state can reach any target + if (!areStatesStuck) + canReach = updateTargetedSearcher(history, target, nullptr, + tmpAddedStates, tmpRemovedStates); + if (canReach) + reachableStatesOfTarget[target].insert(state); + } + tmpAddedStates.clear(); + tmpRemovedStates.clear(); + } } } @@ -566,6 +586,7 @@ void GuidedSearcher::innerUpdate( baseRemovedStates.insert(baseRemovedStates.end(), removedStates.begin(), removedStates.end()); + std::vector addedStuckStates; if (ErrorGuidance == guidance) { if (current && (std::find(baseRemovedStates.begin(), baseRemovedStates.end(), @@ -577,6 +598,7 @@ void GuidedSearcher::innerUpdate( for (const auto state : addedStates) { if (isStuck(*state)) { pausedStates.insert(state); + addedStuckStates.push_back(state); auto is = std::find(baseAddedStates.begin(), baseAddedStates.end(), state); assert(is != baseAddedStates.end()); @@ -680,56 +702,27 @@ void GuidedSearcher::innerUpdate( } } - for (const auto state : targetedAddedStates) { - auto history = state->targetForest.getHistory(); - auto targets = state->targetForest.getTargets(); - TargetForest::TargetsSet stateTargets; - for (auto &targetF : *targets) { - stateTargets.insert(targetF.first); - } - - for (auto &target : stateTargets) { - if (state->targetForest.contains(target)) { - tmpAddedStates.push_back(state); - assert(!state->targetForest.empty()); - - bool canReach = updateTargetedSearcher( - history, target, nullptr, tmpAddedStates, tmpRemovedStates); - if (canReach) - reachableStatesOfTarget[target].insert(state); - } - tmpAddedStates.clear(); - tmpRemovedStates.clear(); - } - } + updateTargetedSearcherForStates(targetedAddedStates, tmpAddedStates, + tmpRemovedStates, reachableStatesOfTarget, + false, false); targetedAddedStates.clear(); - - for (const auto state : baseRemovedStates) { - auto history = state->targetForest.getHistory(); - auto targets = state->targetForest.getTargets(); - TargetForest::TargetsSet stateTargets; - for (auto &targetF : *targets) { - stateTargets.insert(targetF.first); - } - - for (auto &target : stateTargets) { - tmpRemovedStates.push_back(state); - bool canReach = updateTargetedSearcher(history, target, nullptr, - tmpAddedStates, tmpRemovedStates); - if (canReach) { - reachableStatesOfTarget[target].insert(state); - removedButReachableStates.insert(state); - } - tmpAddedStates.clear(); - tmpRemovedStates.clear(); - } - } + updateTargetedSearcherForStates(addedStuckStates, tmpAddedStates, + tmpRemovedStates, reachableStatesOfTarget, + true, false); + updateTargetedSearcherForStates(baseRemovedStates, tmpAddedStates, + tmpRemovedStates, reachableStatesOfTarget, + false, true); if (CoverageGuidance == guidance) { assert(baseSearcher); baseSearcher->update(current, baseAddedStates, baseRemovedStates); } - updateConfidences(current, baseAddedStates, reachableStatesOfTarget); + + updateConfidences(current, reachableStatesOfTarget); + for (auto state : baseAddedStates) + updateConfidences(state, reachableStatesOfTarget); + for (auto state : addedStuckStates) + updateConfidences(state, reachableStatesOfTarget); baseAddedStates.clear(); baseRemovedStates.clear(); } diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 064e190fa2..9a4cfceaa0 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -220,8 +220,6 @@ class GuidedSearcher final : public Searcher { CodeGraphDistance &codeGraphDistance; TargetCalculator *stateHistory; TargetHashSet reachedTargets; - std::set - &removedButReachableStates; std::set &pausedStates; std::size_t bound; RNG &theRNG; @@ -244,6 +242,12 @@ class GuidedSearcher final : public Searcher { ref target, ExecutionState *current, std::vector &addedStates, std::vector &removedStates); + void updateTargetedSearcherForStates( + std::vector &states, + std::vector &tmpAddedStates, + std::vector &tmpRemovedStates, + TargetToStateUnorderedSetMap &reachableStatesOfTarget, + bool areStatesStuck, bool areStatesRemoved); void clearReached(const std::vector &removedStates); void collectReached(TargetToStateSetMap &reachedStates); @@ -253,14 +257,10 @@ class GuidedSearcher final : public Searcher { GuidedSearcher( Searcher *baseSearcher, CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory, - std::set - &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng); GuidedSearcher( CodeGraphDistance &codeGraphDistance, - std::set - &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng); ~GuidedSearcher() override = default; diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 0c9e450245..562c9d2182 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -193,15 +193,14 @@ Searcher *klee::constructUserSearcher(Executor &executor) { if (executor.guidanceKind == Interpreter::GuidanceKind::CoverageGuidance) { searcher = new GuidedSearcher( searcher, *executor.codeGraphDistance.get(), *executor.targetCalculator, - executor.removedButReachableStates, executor.pausedStates, - MaxCycles - 1, executor.theRNG); + executor.pausedStates, MaxCycles - 1, executor.theRNG); } if (executor.guidanceKind == Interpreter::GuidanceKind::ErrorGuidance) { delete searcher; - searcher = new GuidedSearcher( - *executor.codeGraphDistance.get(), executor.removedButReachableStates, - executor.pausedStates, MaxCycles - 1, executor.theRNG); + searcher = new GuidedSearcher(*executor.codeGraphDistance.get(), + executor.pausedStates, MaxCycles - 1, + executor.theRNG); } llvm::raw_ostream &os = executor.getHandler().getInfoStream();