caio/clang-p2996
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

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

Browse Source 
These metrics would turn out to be useful for verifying an upgrade of Z3.
This commit is contained in:
Balázs Benics
2025-03-28 11:26:28 +01:00
committed by GitHub
parent f7a034d400
commit 319045d8c4
2 changed files with 11 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
View File

@@ -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;

4
clang/test/Analysis/analyzer-stats/entry-point-stats.cpp
View File

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