[analyzer] Add metrics tracking time spent in Z3 solver (llvm#133236)

These metrics would turn out to be useful for verifying an upgrade of Z3.

Author: balazs-benics-sonarsource

clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp

@@ -41,6 +41,11 @@ STAT_COUNTER(NumTimesZ3QueryRejectReport,
 STAT_COUNTER(NumTimesZ3QueryRejectEQClass,
              "Number of times rejecting an report equivalenece class");
 
+STAT_COUNTER(TimeSpentSolvingZ3Queries,
+             "Total time spent solving Z3 queries excluding retries");
+STAT_MAX(MaxTimeSpentSolvingZ3Queries,
+         "Max time spent solving a Z3 query excluding retries");
+
 using namespace clang;
 using namespace ento;
 
@@ -145,6 +150,8 @@ Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
     const Z3CrosscheckVisitor::Z3Result &Query) {
   ++NumZ3QueriesDone;
   AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
+  TimeSpentSolvingZ3Queries += Query.Z3QueryTimeMilliseconds;
+  MaxTimeSpentSolvingZ3Queries.updateMax(Query.Z3QueryTimeMilliseconds);
 
   if (Query.IsSAT && Query.IsSAT.value()) {
     ++NumTimesZ3QueryAcceptsReport;

clang/test/Analysis/analyzer-stats/entry-point-stats.cpp

@@ -31,10 +31,12 @@
 // CHECK-NEXT:     "NumTimesZ3SpendsTooMuchTimeOnASingleEQClass": "{{[0-9]+}}",
 // CHECK-NEXT:     "NumTimesZ3TimedOut": "{{[0-9]+}}",
 // CHECK-NEXT:     "NumZ3QueriesDone": "{{[0-9]+}}",
+// CHECK-NEXT:     "TimeSpentSolvingZ3Queries": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxBugClassSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxCFGSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxQueueSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxReachableSize": "{{[0-9]+}}",
+// CHECK-NEXT:     "MaxTimeSpentSolvingZ3Queries": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxValidBugClassSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "PathRunningTime": "{{[0-9]+}}"
 // CHECK-NEXT:   },
@@ -64,10 +66,12 @@
 // CHECK-NEXT:     "NumTimesZ3SpendsTooMuchTimeOnASingleEQClass": "{{[0-9]+}}",
 // CHECK-NEXT:     "NumTimesZ3TimedOut": "{{[0-9]+}}",
 // CHECK-NEXT:     "NumZ3QueriesDone": "{{[0-9]+}}",
+// CHECK-NEXT:     "TimeSpentSolvingZ3Queries": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxBugClassSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxCFGSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxQueueSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxReachableSize": "{{[0-9]+}}",
+// CHECK-NEXT:     "MaxTimeSpentSolvingZ3Queries": "{{[0-9]+}}",
 // CHECK-NEXT:     "MaxValidBugClassSize": "{{[0-9]+}}",
 // CHECK-NEXT:     "PathRunningTime": "{{[0-9]+}}"
 // CHECK-NEXT:   }