From be61cfa4311c00b8cbfb910f8b77e51517c4d340 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Thu, 8 Dec 2022 15:00:09 +0300 Subject: [PATCH] [feat] Output number of reached events instead of confidence rate --- lib/Core/TargetForest.cpp | 17 +++++++++++++++++ lib/Core/TargetForest.h | 11 +++++++++++ lib/Core/TargetedExecutionManager.cpp | 21 ++++++++++++++------- lib/Runner/run_klee.cpp | 3 +-- 4 files changed, 43 insertions(+), 9 deletions(-) diff --git a/lib/Core/TargetForest.cpp b/lib/Core/TargetForest.cpp index 7ff63920f4..55d2c6ca0c 100644 --- a/lib/Core/TargetForest.cpp +++ b/lib/Core/TargetForest.cpp @@ -280,6 +280,7 @@ void TargetForest::stepTo(ref loc) { } else { history = history->add(loc); forest = forest->replaceChildWith(loc, res->second.get()); + loc->isReported = true; } if (forest->empty() && !loc->shouldFailOnThisTarget()) { history = History::create(); @@ -407,3 +408,19 @@ TargetForest::Layer *TargetForest::Layer::divideConfidenceBy(std::multiset> &trace2eventCount, + unsigned reached, + unsigned total) const { + total++; + for (const auto &p : forest) { + auto target = p.first; + auto child = p.second; + auto reachedCurrent = target->isReported ? reached + 1 : reached; + if (target->shouldFailOnThisTarget()) { + trace2eventCount[target->getId()] = std::make_pair(reachedCurrent, total); + } + child->collectHowManyEventsInTracesWereReached(trace2eventCount, reachedCurrent, total); + } +} diff --git a/lib/Core/TargetForest.h b/lib/Core/TargetForest.h index 2d063a19f6..8dc9154584 100644 --- a/lib/Core/TargetForest.h +++ b/lib/Core/TargetForest.h @@ -56,6 +56,11 @@ class TargetForest { std::unordered_map &loc2Targets, std::unordered_set &broken_traces); + void collectHowManyEventsInTracesWereReached( + std::unordered_map> &trace2eventCount, + unsigned reached, + unsigned total) const; + public: using iterator = InternalLayer::const_iterator; @@ -90,6 +95,9 @@ class TargetForest { void divideConfidenceBy(unsigned factor); Layer *divideConfidenceBy(std::multiset > &reachableStatesOfTarget); confidence_ty getConfidence() const { return getConfidence(MAX_CONFIDENCE); } + void collectHowManyEventsInTracesWereReached(std::unordered_map> &trace2eventCount) const { + collectHowManyEventsInTracesWereReached(trace2eventCount, 0, 0); + } }; ref forest; @@ -187,6 +195,9 @@ class TargetForest { void divideConfidenceBy(std::multiset > &reachableStatesOfTarget) { forest = forest->divideConfidenceBy(reachableStatesOfTarget); } + void collectHowManyEventsInTracesWereReached(std::unordered_map> &trace2eventCount) const { + forest->collectHowManyEventsInTracesWereReached(trace2eventCount); + } }; struct TargetsHistoryHash { diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index b1662861d4..8bd8d412d7 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -255,6 +255,8 @@ TargetedExecutionManager::prepareTargets(KModule *origModule, KModule *kmodule, void TargetedExecutionManager::reportFalsePositives(ref &targets, bool canReachSomeTarget) { if (targets.isNull()) return; + std::unordered_map> trace2eventCount; + targets->collectHowManyEventsInTracesWereReached(trace2eventCount); auto leafs = targets->leafs(); for (const auto &targetWithConfidence : *leafs) { auto target = targetWithConfidence.first; @@ -263,10 +265,15 @@ void TargetedExecutionManager::reportFalsePositives(ref &targets, continue; if (target->isReported) continue; - if (canReachSomeTarget && confidence > 99.0) // We should not be so sure if there are states that can reach some targets - confidence = 99.00; - klee_warning("%.2f%% %s False Positive at trace %u", confidence, - ReachWithErrorNames[target->getError()], target->getId()); + if (canReachSomeTarget) { + if (confidence > 99.0) // We should not be so sure if there are states that can reach some targets + confidence = 99.00; + auto eventCount = trace2eventCount[target->getId()]; + klee_warning("Time limit; reached only %u out of %u events at trace %u", eventCount.first, eventCount.second, target->getId()); + } else { + klee_warning("%s False Positive at trace %u", + ReachWithErrorNames[target->getError()], target->getId()); + } target->isReported = true; } delete leafs; @@ -274,7 +281,7 @@ void TargetedExecutionManager::reportFalsePositives(ref &targets, void TargetedExecutionManager::reportFalseNegative(ExecutionState &state, ReachWithError error) { - klee_warning("100.00%% %s False Negative at: %s", ReachWithErrorNames[error], + klee_warning("%s False Negative at: %s", ReachWithErrorNames[error], state.prevPC->getSourceLocation().c_str()); } @@ -306,9 +313,9 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, ReachWi atLeastOneReported = true; assert(!target->isReported); if (target->getError() == ReachWithError::Reachable) { - klee_warning("100.00%% %s Reachable at trace %u", ReachWithErrorNames[target->getError()], target->getId()); + klee_warning("%s Reachable at trace %u", ReachWithErrorNames[target->getError()], target->getId()); } else { - klee_warning("100.00%% %s True Positive at trace %u", ReachWithErrorNames[target->getError()], target->getId()); + klee_warning("%s True Positive at trace %u", ReachWithErrorNames[target->getError()], target->getId()); } target->isReported = true; } diff --git a/lib/Runner/run_klee.cpp b/lib/Runner/run_klee.cpp index 96b256ec7e..191a1dae6a 100644 --- a/lib/Runner/run_klee.cpp +++ b/lib/Runner/run_klee.cpp @@ -1328,7 +1328,6 @@ static Interpreter *theInterpreter = 0; static PathForest *pathTree = 0; static std::atomic_bool interrupted{false}; -static std::atomic_bool reported{false}; // Pulled out so it can be easily called from a debugger. extern "C" @@ -1358,7 +1357,7 @@ static void interrupt_handle() { auto nextTree = p.second; if (nextTree->empty()) { if (event->error != ReachWithError::None) { - klee_warning("0.00%% False Positive at trace %u", event->id); + klee_warning("Time limit; not started investigating at trace %u", event->id); } } else { q.push_back(nextTree);