Skip to content

Improve stability of confidence rate #87

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
misonijnik merged 1 commit into from
May 18, 2023
Merged

Improve stability of confidence rate #87

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion lib/Core/Executor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3788,7 +3788,6 @@ void Executor::updateStates(ExecutionState *current) {
processForest->remove(es->ptreeNode);
delete es;
}
removedButReachableStates.clear();
removedStates.clear();
}

Expand Down
1 change: 0 additions & 1 deletion lib/Core/Executor.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,6 @@ class Executor : public Interpreter {

SetOfStates states;
SetOfStates pausedStates;
SetOfStates removedButReachableStates;
StatsTracker *statsTracker;
TreeStreamWriter *pathWriter, *symPathWriter;
SpecialFunctionHandler *specialFunctionHandler;
Expand Down
107 changes: 50 additions & 57 deletions lib/Core/Searcher.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -439,24 +439,18 @@ void TargetedSearcher::removeReached() {
GuidedSearcher::GuidedSearcher(
Searcher *baseSearcher, CodeGraphDistance &codeGraphDistance,
TargetCalculator &stateHistory,
std::set<ExecutionState *, ExecutionStateIDCompare>
&removedButReachableStates,
std::set<ExecutionState *, ExecutionStateIDCompare> &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<ExecutionState *, ExecutionStateIDCompare>
&removedButReachableStates,
std::set<ExecutionState *, ExecutionStateIDCompare> &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() {
Expand Down Expand Up @@ -548,13 +542,39 @@ static void updateConfidences(ExecutionState *current,
current->targetForest.divideConfidenceBy(reachableStatesOfTarget);
}

static void updateConfidences(ExecutionState *current,
const std::vector<ExecutionState *> &addedStates,
const GuidedSearcher::TargetToStateUnorderedSetMap
&reachableStatesOfTarget) {
updateConfidences(current, reachableStatesOfTarget);
for (auto state : addedStates) {
updateConfidences(state, reachableStatesOfTarget);
void GuidedSearcher::updateTargetedSearcherForStates(
std::vector<ExecutionState *> &states,
std::vector<ExecutionState *> &tmpAddedStates,
std::vector<ExecutionState *> &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();
}
}
}

Expand All @@ -566,6 +586,7 @@ void GuidedSearcher::innerUpdate(
baseRemovedStates.insert(baseRemovedStates.end(), removedStates.begin(),
removedStates.end());

std::vector<ExecutionState *> addedStuckStates;
if (ErrorGuidance == guidance) {
if (current &&
(std::find(baseRemovedStates.begin(), baseRemovedStates.end(),
Expand All @@ -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());
Expand Down Expand Up @@ -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();
}
Expand Down
12 changes: 6 additions & 6 deletions lib/Core/Searcher.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,8 +220,6 @@ class GuidedSearcher final : public Searcher {
CodeGraphDistance &codeGraphDistance;
TargetCalculator *stateHistory;
TargetHashSet reachedTargets;
std::set<ExecutionState *, ExecutionStateIDCompare>
&removedButReachableStates;
std::set<ExecutionState *, ExecutionStateIDCompare> &pausedStates;
std::size_t bound;
RNG &theRNG;
Expand All @@ -244,6 +242,12 @@ class GuidedSearcher final : public Searcher {
ref<Target> target, ExecutionState *current,
std::vector<ExecutionState *> &addedStates,
std::vector<ExecutionState *> &removedStates);
void updateTargetedSearcherForStates(
std::vector<ExecutionState *> &states,
std::vector<ExecutionState *> &tmpAddedStates,
std::vector<ExecutionState *> &tmpRemovedStates,
TargetToStateUnorderedSetMap &reachableStatesOfTarget,
bool areStatesStuck, bool areStatesRemoved);

void clearReached(const std::vector<ExecutionState *> &removedStates);
void collectReached(TargetToStateSetMap &reachedStates);
Expand All @@ -253,14 +257,10 @@ class GuidedSearcher final : public Searcher {
GuidedSearcher(
Searcher *baseSearcher, CodeGraphDistance &codeGraphDistance,
TargetCalculator &stateHistory,
std::set<ExecutionState *, ExecutionStateIDCompare>
&removedButReachableStates,
std::set<ExecutionState *, ExecutionStateIDCompare> &pausedStates,
std::size_t bound, RNG &rng);
GuidedSearcher(
CodeGraphDistance &codeGraphDistance,
std::set<ExecutionState *, ExecutionStateIDCompare>
&removedButReachableStates,
std::set<ExecutionState *, ExecutionStateIDCompare> &pausedStates,
std::size_t bound, RNG &rng);
~GuidedSearcher() override = default;
Expand Down
9 changes: 4 additions & 5 deletions lib/Core/UserSearcher.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down