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

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

steakhal updated this revision to Diff 274510.
steakhal added a comment.

- adds statistic to undecidable branch


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D82856/new/

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,23 @@
 // Implementation of FalsePositiveRefutationBRVisitor.
 
//===----------------------------------------------------------------------===//
 
+#define DEBUG_TYPE "FalsePositiveRefutationBRVisitor"
+STATISTIC(CrosscheckedBugReports,
+          "The # of bug reports which were checked for infeasible 
constraints");
+STATISTIC(
+    CrosscheckUndecidable,
+    "The # of bug reports not invalidated due to undecidable constraints");
+STATISTIC(CrosscheckInvalidatedBugReports,
+          "The # of bug reports invalidated due to infeasible constraints");
+#undef DEBUG_TYPE
+
 FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
     : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
+  ++CrosscheckedBugReports;
   // Collect new constraints
   addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
 
@@ -2845,11 +2857,15 @@
 
   // And check for satisfiability
   Optional<bool> IsSAT = RefutationSolver->check();
-  if (!IsSAT.hasValue())
+  if (!IsSAT.hasValue()) {
+    ++CrosscheckUndecidable;
     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,23 @@
 // Implementation of FalsePositiveRefutationBRVisitor.
 //===----------------------------------------------------------------------===//
 
+#define DEBUG_TYPE "FalsePositiveRefutationBRVisitor"
+STATISTIC(CrosscheckedBugReports,
+          "The # of bug reports which were checked for infeasible constraints");
+STATISTIC(
+    CrosscheckUndecidable,
+    "The # of bug reports not invalidated due to undecidable constraints");
+STATISTIC(CrosscheckInvalidatedBugReports,
+          "The # of bug reports invalidated due to infeasible constraints");
+#undef DEBUG_TYPE
+
 FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
     : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
+  ++CrosscheckedBugReports;
   // Collect new constraints
   addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
 
@@ -2845,11 +2857,15 @@
 
   // And check for satisfiability
   Optional<bool> IsSAT = RefutationSolver->check();
-  if (!IsSAT.hasValue())
+  if (!IsSAT.hasValue()) {
+    ++CrosscheckUndecidable;
     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