[PATCH] D82900: [analyzer][Z3-refutation] Add statistics tracking invalidated bug report classes

[Balázs Benics via Phabricator via cfe-commits]

steakhal created this revision.
steakhal added reviewers: NoQ, xazax.hun, Szelethus, martong.
Herald added subscribers: cfe-commits, ASDenysPetrov, Charusso, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, whisperity.
Herald added a project: clang.

Counts how many bug report equivalence classes were created and
how many of them were completely invalidated.

In other words how many times avoided emitting diagnostic to the user due to
Z3 refutation.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D82900

Files:
  clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporter.h
  clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  clang/lib/StaticAnalyzer/Core/BugReporter.cpp
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp


Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2849,7 +2849,7 @@
     return;
 
   if (!IsSAT.getValue())
-    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+    BR.markInvalid(Tag, EndPathNode->getLocationContext());
 }
 
 void FalsePositiveRefutationBRVisitor::addConstraints(
Index: clang/lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -82,6 +82,11 @@
 STATISTIC(MaxValidBugClassSize,
           "The maximum number of bug reports in the same equivalence class "
           "where at least one report is valid (not suppressed)");
+STATISTIC(TotalBugReportEquivClasses,
+          "The # of bug report equivalence classes");
+STATISTIC(InvalidatedBugReportEquivClasses,
+          "The # of bug report equivalence classes invalidated due to "
+          "infeasible constraints");
 
 BugReporterVisitor::~BugReporterVisitor() = default;
 
@@ -2403,6 +2408,9 @@
 }
 
 void BugReporter::FlushReports() {
+  // Increment the total bug report equivalence classes processed statistic.
+  TotalBugReportEquivClasses += EQClassesVector.size();
+
   // We need to flush reports in deterministic order to ensure the order
   // of the reports is consistent between runs.
   for (const auto EQ : EQClassesVector)
@@ -2998,6 +3006,16 @@
   std::unique_ptr<DiagnosticForConsumerMapTy> Diagnostics =
       generateDiagnosticForConsumerMap(report, Consumers, bugReports);
 
+  // Increment the statistic if necessary.
+  const bool IsEQClassInvalidatedByCrosscheck = llvm::all_of(
+      EQ.getReports(), [](const std::unique_ptr<BugReport> &RawReport) {
+        const auto *Report = dyn_cast<PathSensitiveBugReport>(RawReport.get());
+        return Report && Report->isInvalidatedByTag(
+                             FalsePositiveRefutationBRVisitor::Tag);
+      });
+  if (IsEQClassInvalidatedByCrosscheck)
+    ++InvalidatedBugReportEquivClasses;
+
   for (auto &P : *Diagnostics) {
     PathDiagnosticConsumer *Consumer = P.first;
     std::unique_ptr<PathDiagnostic> &PD = P.second;
Index: clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -378,6 +378,8 @@
 public:
   FalsePositiveRefutationBRVisitor();
 
+  static constexpr char *Tag = "Infeasible constraints";
+
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
   PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
Index: clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporter.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporter.h
+++ clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporter.h
@@ -480,6 +480,14 @@
     Invalidations.insert(std::make_pair(Tag, Data));
   }
 
+  /// Returns whether or not this report was marked invalid by a given Tag.
+  bool isInvalidatedByTag(const void *Tag) const {
+    const auto EqByTag = [Tag](const auto &TagAndData) {
+      return TagAndData.first == Tag;
+    };
+    return llvm::any_of(Invalidations, EqByTag);
+  }
+
   /// Profile to identify equivalent bug reports for error report coalescing.
   /// Reports are uniqued to ensure that we do not emit multiple diagnostics
   /// for each bug.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D82900.274557.patch
Type: text/x-patch
Size: 3765 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200630/c1093430/attachment-0001.bin>