[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

[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.

This patch adds two statics.
The diff speaks for itself.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D82856

Files:
  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
@@ -52,6 +52,7 @@
 #include "llvm/ADT/SmallPtrSet.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/Statistic.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Casting.h"
@@ -2812,12 +2813,19 @@
 // Implementation of FalsePositiveRefutationBRVisitor.
 
//===----------------------------------------------------------------------===//
 
+#define DEBUG_TYPE "FalsePositiveRefutationBRVisitor"
+STATISTIC(CrosscheckedBugReports,
+          "The # of bug reports which were checked for infeasible 
constraints");
+STATISTIC(CrosscheckInvalidatedBugReports,
+          "The # of bug reports invalidated due to infeasible constraints");
+
 FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
     : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
+  ++CrosscheckedBugReports;
   // Collect new constraints
   addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
 
@@ -2848,8 +2856,10 @@
   if (!IsSAT.hasValue())
     return;
 
-  if (!IsSAT.getValue())
+  if (!IsSAT.getValue()) {
+    ++CrosscheckInvalidatedBugReports;
     BR.markInvalid("Infeasible constraints", 
EndPathNode->getLocationContext());
+  }
 }
 
 void FalsePositiveRefutationBRVisitor::addConstraints(



Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -52,6 +52,7 @@
 #include "llvm/ADT/SmallPtrSet.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/Statistic.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Casting.h"
@@ -2812,12 +2813,19 @@
 // Implementation of FalsePositiveRefutationBRVisitor.
 //===----------------------------------------------------------------------===//
 
+#define DEBUG_TYPE "FalsePositiveRefutationBRVisitor"
+STATISTIC(CrosscheckedBugReports,
+          "The # of bug reports which were checked for infeasible constraints");
+STATISTIC(CrosscheckInvalidatedBugReports,
+          "The # of bug reports invalidated due to infeasible constraints");
+
 FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
     : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
+  ++CrosscheckedBugReports;
   // Collect new constraints
   addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
 
@@ -2848,8 +2856,10 @@
   if (!IsSAT.hasValue())
     return;
 
-  if (!IsSAT.getValue())
+  if (!IsSAT.getValue()) {
+    ++CrosscheckInvalidatedBugReports;
     BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+  }
 }
 
 void FalsePositiveRefutationBRVisitor::addConstraints(

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits