From 64282c60f62bcff74c9f8cc22398aa373145d066 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Thu, 22 Jun 2023 16:04:39 +0300 Subject: [PATCH 1/3] [feat] Target progress report --- include/klee/Module/TargetHash.h | 8 ++++++++ lib/Core/DistanceCalculator.cpp | 17 ++++++++++++++++ lib/Core/DistanceCalculator.h | 15 ++++++++++----- lib/Core/Executor.cpp | 33 ++++++++++++++++++++++++++++++++ lib/Core/Executor.h | 4 ++++ lib/Core/Searcher.h | 8 -------- lib/Module/KModule.cpp | 2 ++ 7 files changed, 74 insertions(+), 13 deletions(-) diff --git a/include/klee/Module/TargetHash.h b/include/klee/Module/TargetHash.h index eccac7db77..a484b521a7 100644 --- a/include/klee/Module/TargetHash.h +++ b/include/klee/Module/TargetHash.h @@ -14,6 +14,7 @@ #include #include +#include namespace llvm { class BasicBlock; @@ -54,5 +55,12 @@ struct RefTargetLess { } }; +template +class TargetHashMap + : public std::unordered_map, T, RefTargetHash, RefTargetCmp> {}; + +class TargetHashSet + : public std::unordered_set, RefTargetHash, RefTargetCmp> {}; + } // namespace klee #endif /* KLEE_TARGETHASH_H */ diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index b87fbcf18a..a1e384ee67 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -13,9 +13,26 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/Target.h" +#include + using namespace llvm; using namespace klee; +bool DistanceResult::operator<(const DistanceResult &b) const { + if (isInsideFunction != b.isInsideFunction) + return isInsideFunction; + if (result == WeightResult::Continue && b.result == WeightResult::Continue) + return weight < b.weight; + return result < b.result; +} + +std::string DistanceResult::toString() const { + std::ostringstream out; + out << "(" << (int)!isInsideFunction << ", " << (int)result << ", " << weight + << ")"; + return out.str(); +} + DistanceResult DistanceCalculator::getDistance(ExecutionState &es, ref target) { return getDistance(es.pc, es.prevPC, es.initPC, es.stack, es.error, target); diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h index 8f46a3696c..eec14f8881 100644 --- a/lib/Core/DistanceCalculator.h +++ b/lib/Core/DistanceCalculator.h @@ -21,9 +21,9 @@ class CodeGraphDistance; struct Target; enum WeightResult : std::uint8_t { - Continue, - Done, - Miss, + Done = 0U, + Continue = 1U, + Miss = 2U, }; using weight_type = unsigned; @@ -33,9 +33,14 @@ struct DistanceResult { weight_type weight; bool isInsideFunction; - explicit DistanceResult(WeightResult result_, weight_type weight_ = 0, + explicit DistanceResult(WeightResult result_ = WeightResult::Miss, + weight_type weight_ = 0, bool isInsideFunction_ = true) - : result(result_), weight(weight_), isInsideFunction(isInsideFunction_) {} + : result(result_), weight(weight_), isInsideFunction(isInsideFunction_){}; + + bool operator<(const DistanceResult &b) const; + + std::string toString() const; }; class DistanceCalculator { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 610d853911..2e8d475edf 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4060,6 +4060,38 @@ void Executor::seed(ExecutionState &initialState) { } } +void Executor::reportProgressTowardsTargets(std::string prefix, + const SetOfStates &states) const { + klee_message("%zu %sstates remaining", states.size(), prefix.c_str()); + TargetHashMap distancesTowardsTargets; + for (auto &state : states) { + for (auto &p : *state->targetForest.getTargets()) { + auto target = p.first; + auto distance = distanceCalculator->getDistance(*state, target); + auto it = distancesTowardsTargets.find(target); + if (it == distancesTowardsTargets.end()) + distancesTowardsTargets.insert(it, std::make_pair(target, distance)); + else { + distance = std::min(distance, it->second); + distancesTowardsTargets[target] = distance; + } + } + } + klee_message("Distances from nearest %sstates to remaining targets:", + prefix.c_str()); + for (auto &p : distancesTowardsTargets) { + auto target = p.first; + auto distance = p.second; + klee_message("%s for %s", distance.toString().c_str(), + target->toString().c_str()); + } +} + +void Executor::reportProgressTowardsTargets() const { + reportProgressTowardsTargets("paused ", pausedStates); + reportProgressTowardsTargets("", states); +} + void Executor::run(std::vector initialStates) { // Delay init till now so that ticks don't accrue during optimization and // such. @@ -4098,6 +4130,7 @@ void Executor::run(std::vector initialStates) { } if (guidanceKind == GuidanceKind::ErrorGuidance) { + reportProgressTowardsTargets(); bool canReachNew1 = decreaseConfidenceFromStoppedStates(pausedStates); bool canReachNew2 = decreaseConfidenceFromStoppedStates(states, haltExecution); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 8aa39b241a..b12e5e7f62 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -593,6 +593,10 @@ class Executor : public Interpreter { void terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message); + void reportProgressTowardsTargets(std::string prefix, + const SetOfStates &states) const; + void reportProgressTowardsTargets() const; + /// bindModuleConstants - Initialize the module constant table. void bindModuleConstants(const llvm::APFloat::roundingMode &rm); diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 436e8dcdd4..ee85de1d58 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -158,14 +158,6 @@ class TargetedSearcher final : public Searcher { }; class GuidedSearcher final : public Searcher { -private: - template - class TargetHashMap - : public std::unordered_map, T, RefTargetHash, RefTargetCmp> { - }; - class TargetHashSet - : public std::unordered_set, RefTargetHash, RefTargetCmp> {}; - public: using TargetToStateUnorderedSetMap = TargetHashMap>; diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 03549daea7..b87e3e0ec2 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -728,6 +728,8 @@ std::string KBlock::getLabel() const { std::string _label; llvm::raw_string_ostream label_stream(_label); basicBlock->printAsOperand(label_stream, false); + label_stream << " (lines " << getFirstInstruction()->info->line << " to " + << getLastInstruction()->info->line << ")"; std::string label = label_stream.str(); return label; } From c32957dbaf4514937b4d5fd40203f1880c66eb4b Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Tue, 27 Jun 2023 17:19:09 +0300 Subject: [PATCH 2/3] [fix] Fixed 0 weight for targets on the same frame --- lib/Core/DistanceCalculator.cpp | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index a1e384ee67..44c2f26e72 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -72,14 +72,7 @@ DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, if (distanceInCallGraph(sfi->kf, kb, callWeight, distanceToTargetFunction, target)) { callWeight *= 2; - if (callWeight == 0 && target->shouldFailOnThisTarget()) { - return target->isTheSameAsIn(kb->getFirstInstruction()) && - target->isThatError(error) - ? DistanceResult(Done) - : DistanceResult(Continue); - } else { - callWeight += sfNum; - } + callWeight += sfNum; if (callWeight < minCallWeight) { minCallWeight = callWeight; From ac939dda5bc5e5d1671fda2953ff70c2647e9082 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Tue, 27 Jun 2023 17:19:33 +0300 Subject: [PATCH 3/3] [test] Added report tests --- test/Industry/if2.c | 4 +++- test/Industry/while_true.c | 7 ++++++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/test/Industry/if2.c b/test/Industry/if2.c index 6936bea6ab..6ab4ec7ae0 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -13,4 +13,6 @@ int main(int x) { // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=19 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE -// CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 \ No newline at end of file +// CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 +// RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE +// CHECK-DISTANCE: KLEE: (0, 1, 1) for Target 1: error in %13 (lines 8 to 8) in function main diff --git a/test/Industry/while_true.c b/test/Industry/while_true.c index 7fa0c973d0..11ef6bba59 100644 --- a/test/Industry/while_true.c +++ b/test/Industry/while_true.c @@ -14,7 +14,12 @@ int main() { // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=10 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 0.00% NullPointerException False Positive at trace 1 +// RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-REACH-1 +// CHECK-REACH-1: (0, 1, 4) for Target 1: error in %17 (lines 8 to 8) in function main + // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=5000 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-ALL -// CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1 \ No newline at end of file +// CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1 +// RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-REACH-2 +// CHECK-REACH-2: (0, 1, 1) for Target 1: error in %17 (lines 8 to 8) in function main