llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-clang-static-analyzer-1 Author: Balázs Benics (balazs-benics-sonarsource) <details> <summary>Changes</summary> 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 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: } `````````` </details> https://github.com/llvm/llvm-project/pull/133236 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
