[analyzer] Add metrics tracking time spent in Z3 solver

[balazs-benics-sonarsource]

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

[llvmbot]

@llvm/pr-subscribers-clang

@llvm/pr-subscribers-clang-static-analyzer-1

Author: Balázs Benics (balazs-benics-sonarsource)

Changes

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

---

Full diff: https://github.com/llvm/llvm-project/pull/133236.diff

2 Files Affected:

• (modified) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (+7)
• (modified) clang/test/Analysis/analyzer-stats/entry-point-stats.cpp (+4)

diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
index fca792cdf86f7..836fc375809ad 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/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;
diff --git a/clang/test/Analysis/analyzer-stats/entry-point-stats.cpp b/clang/test/Analysis/analyzer-stats/entry-point-stats.cpp
index bddba084ee4bf..1ff31d114ee99 100644
--- a/clang/test/Analysis/analyzer-stats/entry-point-stats.cpp
+++ b/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:   }

[NagyDonat]

LGTM.

I'm a bit surprised to see that you're excluding the retries from this measurement (I feel that measuring the total time would be a more "natural" statistic), but if you're interested in this information, then there is no reason to oppose measuring it.

[balazs-benics-sonarsource]

LGTM.

I'm a bit surprised to see that you're excluding the retries from this measurement (I feel that measuring the total time would be a more "natural" statistic), but if you're interested in this information, then there is no reason to oppose measuring it.

Thanks for the review! I see. I'd probably not refactor this now. I think it proves some value in the current format in https://discourse.llvm.org/t/z3-upgrade-experience-report/85531