https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/120239
If we have a refutation Z3 query timed out (UNDEF), allow a couple of retries to improve stability of the query. By default allow 2 retries. Retries should help mitigating flaky Z3 queries. See the details in the following RFC: https://discourse.llvm.org/t/analyzer-rfc-retry-z3-crosscheck-queries-on-timeout/83711 Note that with each retry, we spend more time per query. Currently, we have a 15 seconds timeout per query - which are also in effect for the retry attempts. CPP-5920 >From 71e454ef87d733d8f4b7659487696c2b79a3a3bd Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Tue, 17 Dec 2024 15:35:27 +0100 Subject: [PATCH] [analyzer] Retry UNDEF Z3 queries at most "crosscheck-with-z3-retries-on-timeout" times If we have a refutation Z3 query timed out (UNDEF), allow a couple of retries to improve stability of the query. By default allow 2 retries. Retries should help mitigating flaky Z3 queries. See the details in the following RFC: https://discourse.llvm.org/t/analyzer-rfc-retry-z3-crosscheck-queries-on-timeout/83711 Note that with each retry, we spend more time per query. Currently, we have a 15 seconds timeout per query - which are also in effect for the retry attempts. CPP-5920 --- .../StaticAnalyzer/Core/AnalyzerOptions.def | 11 ++++ .../Core/Z3CrosscheckVisitor.cpp | 38 +++++++++--- clang/test/Analysis/analyzer-config.c | 1 + clang/test/Analysis/z3-crosscheck-retry.cpp | 39 ++++++++++++ clang/test/Analysis/z3/D83660.c | 17 +++-- .../Analysis/z3/Inputs/MockZ3_solver_check.c | 28 --------- .../z3/Inputs/MockZ3_solver_check.cpp | 62 +++++++++++++++++++ 7 files changed, 149 insertions(+), 47 deletions(-) create mode 100644 clang/test/Analysis/z3-crosscheck-retry.cpp delete mode 100644 clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c create mode 100644 clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index d8a7c755c95968..46ff91f488fb5c 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -193,6 +193,8 @@ ANALYZER_OPTION( "with \"crosscheck-with-z3-timeout-threshold\" of 300 ms, would nicely " "guarantee that no bug report equivalence class can take longer than " "1 second, effectively mitigating Z3 hangs during refutation. " + "If there were Z3 retries, only the minimum query time is considered " + "when accumulating query times within a report equivalence class. " "Set 0 for no timeout.", 0) ANALYZER_OPTION( @@ -213,6 +215,15 @@ ANALYZER_OPTION( "400'000 should on average make Z3 queries run for up to 100ms on modern " "hardware. Set 0 for unlimited.", 0) +ANALYZER_OPTION( + unsigned, Z3CrosscheckRetriesOnTimeout, + "crosscheck-with-z3-retries-on-timeout", + "Set how many times the oracle is allowed to retry a Z3 query. " + "Set 0 for not allowing retries, in which case each Z3 query would be " + "attempted only once. Increasing the number of retries is often more " + "effective at reducing the number of nondeterministic diagnostics than " + "\"crosscheck-with-z3-timeout-threshold\" in practice.", 2) + ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile, "report-in-main-source-file", "Whether or not the diagnostic report should be always " diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index 739db951b3e185..7f4d7a93ee1b11 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -21,6 +21,9 @@ #define DEBUG_TYPE "Z3CrosscheckOracle" +// Queries retried at most `Z3CrosscheckRetriesOnTimeout` number of times if the +// `check()` call returns `UNDEF` for any reason. Each query is only counted +// once for these statistics, the retries are not accounted for. STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done"); STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out"); STATISTIC(NumTimesZ3ExhaustedRLimit, @@ -77,16 +80,33 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, RefutationSolver->addConstraint(SMTConstraints); } - // And check for satisfiability - llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true); - std::optional<bool> IsSAT = RefutationSolver->check(); - llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false); - Diff -= Start; - Result = Z3Result{ - IsSAT, - static_cast<unsigned>(Diff.getWallTime() * 1000), - RefutationSolver->getStatistics()->getUnsigned("rlimit count"), + auto GetUsedRLimit = [](const llvm::SMTSolverRef &Solver) { + return Solver->getStatistics()->getUnsigned("rlimit count"); + }; + + auto AttemptOnce = [&](const llvm::SMTSolverRef &Solver) -> Z3Result { + constexpr auto getCurrentTime = llvm::TimeRecord::getCurrentTime; + unsigned InitialRLimit = GetUsedRLimit(Solver); + double Start = getCurrentTime(/*Start=*/true).getWallTime(); + std::optional<bool> IsSAT = Solver->check(); + double End = getCurrentTime(/*Start=*/false).getWallTime(); + return { + IsSAT, + static_cast<unsigned>((End - Start) * 1000), + GetUsedRLimit(Solver) - InitialRLimit, + }; }; + + // And check for satisfiability + unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max(); + unsigned NumRetries = Opts.Z3CrosscheckRetriesOnTimeout; + for (unsigned Attempt = 1; Attempt <= 1 + NumRetries; ++Attempt) { + Result = AttemptOnce(RefutationSolver); + Result.Z3QueryTimeMilliseconds = + std::min(MinQueryTimeAcrossAttempts, Result.Z3QueryTimeMilliseconds); + if (Result.IsSAT.has_value()) + return; + } } void Z3CrosscheckVisitor::addConstraints( diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c index 8ce6184144d4b8..af4527c9fb2823 100644 --- a/clang/test/Analysis/analyzer-config.c +++ b/clang/test/Analysis/analyzer-config.c @@ -41,6 +41,7 @@ // CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false // CHECK-NEXT: crosscheck-with-z3 = false // CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 0 +// CHECK-NEXT: crosscheck-with-z3-retries-on-timeout = 2 // CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 0 // CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 15000 // CHECK-NEXT: ctu-dir = "" diff --git a/clang/test/Analysis/z3-crosscheck-retry.cpp b/clang/test/Analysis/z3-crosscheck-retry.cpp new file mode 100644 index 00000000000000..b81d3469b3dd26 --- /dev/null +++ b/clang/test/Analysis/z3-crosscheck-retry.cpp @@ -0,0 +1,39 @@ +// Check the default config. +// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ConfigDumper 2>&1 \ +// RUN: | FileCheck %s --match-full-lines +// CHECK: crosscheck-with-z3-retries-on-timeout = 2 + +// RUN: rm -rf %t && mkdir %t +// RUN: %host_cxx -shared -fPIC \ +// RUN: %S/z3/Inputs/MockZ3_solver_check.cpp \ +// RUN: -o %t/MockZ3_solver_check.so + +// DEFINE: %{mocked_clang} = \ +// DEFINE: LD_PRELOAD="%t/MockZ3_solver_check.so" \ +// DEFINE: %clang_cc1 %s -analyze -setup-static-analyzer \ +// DEFINE: -analyzer-config crosscheck-with-z3=true \ +// DEFINE: -analyzer-checker=core + +// DEFINE: %{retry} = -analyzer-config crosscheck-with-z3-retries-on-timeout + +// RUN: Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{retry}=0 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{retry}=0 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{retry}=0 -verify=accepted + +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{retry}=1 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{retry}=1 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{retry}=1 -verify=accepted + +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{retry}=2 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{retry}=2 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{retry}=2 -verify=accepted + + +// REQUIRES: z3, asserts, shell, system-linux + +// refuted-no-diagnostics + +int div_by_zero_test(int b) { + if (b) {} + return 100 / b; // accepted-warning {{Division by zero}} +} diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c index fd463333a51e38..b42d934bcc9e7b 100644 --- a/clang/test/Analysis/z3/D83660.c +++ b/clang/test/Analysis/z3/D83660.c @@ -1,21 +1,18 @@ // RUN: rm -rf %t && mkdir %t -// RUN: %host_cxx -shared -fPIC %S/Inputs/MockZ3_solver_check.c -o %t/MockZ3_solver_check.so +// RUN: %host_cxx -shared -fPIC \ +// RUN: %S/Inputs/MockZ3_solver_check.cpp \ +// RUN: -o %t/MockZ3_solver_check.so // -// RUN: LD_PRELOAD="%t/MockZ3_solver_check.so" \ -// RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \ -// RUN: -analyzer-checker=core,debug.ExprInspection %s -verify 2>&1 | FileCheck %s +// RUN: Z3_SOLVER_RESULTS="SAT,SAT,SAT,SAT,UNDEF" \ +// RUN: LD_PRELOAD="%t/MockZ3_solver_check.so" \ +// RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \ +// RUN: -analyzer-checker=core %s -verify // // REQUIRES: z3, asserts, shell, system-linux // // Works only with the z3 constraint manager. // expected-no-diagnostics -// CHECK: Z3_solver_check returns the real value: TRUE -// CHECK-NEXT: Z3_solver_check returns the real value: TRUE -// CHECK-NEXT: Z3_solver_check returns the real value: TRUE -// CHECK-NEXT: Z3_solver_check returns the real value: TRUE -// CHECK-NEXT: Z3_solver_check returns a mocked value: UNDEF - void D83660(int b) { if (b) { } diff --git a/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c b/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c deleted file mode 100644 index 9c63a64ada2201..00000000000000 --- a/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c +++ /dev/null @@ -1,28 +0,0 @@ -#include <dlfcn.h> -#include <stdio.h> - -#include <z3.h> - -// Mock implementation: return UNDEF for the 5th invocation, otherwise it just -// returns the result of the real invocation. -Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s) { - static Z3_lbool (*OriginalFN)(Z3_context, Z3_solver); - if (!OriginalFN) { - OriginalFN = (Z3_lbool(*)(Z3_context, Z3_solver))dlsym(RTLD_NEXT, - "Z3_solver_check"); - } - - // Invoke the actual solver. - Z3_lbool Result = OriginalFN(c, s); - - // Mock the 5th invocation to return UNDEF. - static unsigned int Counter = 0; - if (++Counter == 5) { - fprintf(stderr, "Z3_solver_check returns a mocked value: UNDEF\n"); - return Z3_L_UNDEF; - } - fprintf(stderr, "Z3_solver_check returns the real value: %s\n", - (Result == Z3_L_UNDEF ? "UNDEF" - : ((Result == Z3_L_TRUE ? "TRUE" : "FALSE")))); - return Result; -} diff --git a/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp b/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp new file mode 100644 index 00000000000000..54cd86d0ac32c0 --- /dev/null +++ b/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp @@ -0,0 +1,62 @@ +#include <cassert> +#include <dlfcn.h> +#include <cstdio> +#include <cstdlib> +#include <cstring> + +#include <z3.h> + +static char *Z3ResultsBegin; +static char *Z3ResultsCursor; + +static __attribute__((constructor)) void init() { + const char *Env = getenv("Z3_SOLVER_RESULTS"); + if (!Env) { + fprintf(stderr, "Z3_SOLVER_RESULTS envvar must be defined; abort\n"); + abort(); + } + Z3ResultsBegin = strdup(Env); + Z3ResultsCursor = Z3ResultsBegin; + if (!Z3ResultsBegin) { + fprintf(stderr, "strdup failed; abort\n"); + abort(); + } +} + +static __attribute__((destructor)) void finit() { + if (strlen(Z3ResultsCursor) > 0) { + fprintf(stderr, "Z3_SOLVER_RESULTS should have been completely consumed " + "by the end of the test; abort\n"); + abort(); + } + free(Z3ResultsBegin); +} + +static bool consume_token(char **pointer_to_cursor, const char *token) { + assert(pointer_to_cursor); + int len = strlen(token); + if (*pointer_to_cursor && strncmp(*pointer_to_cursor, token, len) == 0) { + *pointer_to_cursor += len; + return true; + } + return false; +} + +Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s) { + consume_token(&Z3ResultsCursor, ","); + + if (consume_token(&Z3ResultsCursor, "UNDEF")) { + printf("Z3_solver_check returns UNDEF\n"); + return Z3_L_UNDEF; + } + if (consume_token(&Z3ResultsCursor, "SAT")) { + printf("Z3_solver_check returns SAT\n"); + return Z3_L_TRUE; + } + if (consume_token(&Z3ResultsCursor, "UNSAT")) { + printf("Z3_solver_check returns UNSAT\n"); + return Z3_L_FALSE; + } + fprintf(stderr, "Z3_SOLVER_RESULTS was exhausted; abort\n"); + abort(); +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
