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

[Balázs Benics via cfe-commits]

https://github.com/balazs-benics-sonarsource created 
https://github.com/llvm/llvm-project/pull/133236

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

From 5fe04bcbb3eaf5682037ada6ab64fd7e021f787e Mon Sep 17 00:00:00 2001
From: Balazs Benics <balazs.ben...@sonarsource.com>
Date: Thu, 27 Mar 2025 12:13:59 +0100
Subject: [PATCH] [analyzer] Add metrics tracking time spent in Z3 solver

---
 clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp    | 7 +++++++
 clang/test/Analysis/analyzer-stats/entry-point-stats.cpp | 4 ++++
 2 files changed, 11 insertions(+)

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:   }

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