diff options
| author | Balázs Benics <108414871+balazs-benics-sonarsource@users.noreply.github.com> | 2025-03-28 11:26:28 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-03-28 11:26:28 +0100 |
| commit | 319045d8c42dc855eacdb4bd1d71b6ac3fca3257 (patch) | |
| tree | 30065f23d5211799e941409200df481130619bef | |
| parent | f7a034d400860501a26e3429e1c6a9f310f07f76 (diff) | |
| download | llvm-319045d8c42dc855eacdb4bd1d71b6ac3fca3257.zip llvm-319045d8c42dc855eacdb4bd1d71b6ac3fca3257.tar.gz llvm-319045d8c42dc855eacdb4bd1d71b6ac3fca3257.tar.bz2 | |
[analyzer] Add metrics tracking time spent in Z3 solver (#133236)
These metrics would turn out to be useful for verifying an upgrade of Z3.
| -rw-r--r-- | clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp | 7 | ||||
| -rw-r--r-- | clang/test/Analysis/analyzer-stats/entry-point-stats.cpp | 4 |
2 files changed, 11 insertions, 0 deletions
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index fca792c..836fc37 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 bddba08..1ff31d1 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: } |