[analyzer][Z3-refutation] Add statistics for refutation visitor

[steakhal]

Summary

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

[xazax.hun]

Yay! This looks good to me and I love statistics, so a huge +1.
I have one question though. Isn't this counting all the reports in an equivalence class? I.e. if the analyzer finds something multiple times it will only be displayed once but here it will be counted multiple times. I think it might be worth to have two statistics, one for all bug reports and one for equivalence classes. What do you think?

[steakhal]

In D82856#2122330, @xazax.hun wrote:

Yay! This looks good to me and I love statistics, so a huge +1.
I have one question though. Isn't this counting all the reports in an equivalence class? I.e. if the analyzer finds something multiple times it will only be displayed once but here it will be counted multiple times. I think it might be worth to have two statistics, one for all bug reports and one for equivalence classes. What do you think?

You might be right.

[NoQ]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2860–2863

I strongly recommend a statistic for this branch as well. I.e., how many reports were too difficult for the refutation solver to solve.

[NoQ]

I have one question though. Isn't this counting all the reports in an equivalence class?

Yes it is. You have no choice but to run refutation before deduplication; otherwise the otherwise-best report in the class may be false when other reports are true.

[steakhal]

• adds statistic to undecidable branch

[steakhal]

It might be useful in the future, but right now, I'm not interested in upstreaming this.

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/ADT/STLExtras.h"
 #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"
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <deque>
 #include <memory>
UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
   }
   return nullptr;
 }
 
 //===----------------------------------------------------------------------===//
 // 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);
 
   // Create a refutation manager
   llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
   ASTContext &Ctx = BRC.getASTContext();
 
   // Add constraints to the solver
while ((++RangeIt) != I.second.end()) {
                                                 /*InRange=*/true));
     }
 
     RefutationSolver->addConstraint(SMTConstraints);
   }
 
   // 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(
     const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
   // Collect new constraints
   const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
   ConstraintRangeTy::Factory &CF =
       N->getState()->get_context<ConstraintRange>();