https://github.com/steakhal updated https://github.com/llvm/llvm-project/pull/120239
>From f7041f5f6f0127f335bedf081f648e769007a827 Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Tue, 17 Dec 2024 15:35:27 +0100 Subject: [PATCH 1/6] [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. --- Why should this help? In short, retrying queries should bring stability because if a query runs long it's more likely that it did so due to some runtime anomaly than it's on the edge of succeeding. This is because most queries run quick, and the queries that run long, usually run long by a fair amount. Consequently, retries should improve the stability of the outcome of the Z3 query. In general, the retries shouldn't increase the overall analysis time because it's really rare we hit the 0.1% of the cases when we would do retries. But keep in mind that the retry attempts can add up if many retries are allowed, or the individual query timeout is large. 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(); +} >From 7dc6f3162a0ce5c3168766e01dc10638d6b12c7f Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Jan 2025 09:23:43 +0100 Subject: [PATCH 2/6] Use zero-based raw for-loop for counting the Z3 attempts --- clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index 7f4d7a93ee1b11..4ccbffa598b708 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -99,8 +99,7 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, // And check for satisfiability unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max(); - unsigned NumRetries = Opts.Z3CrosscheckRetriesOnTimeout; - for (unsigned Attempt = 1; Attempt <= 1 + NumRetries; ++Attempt) { + for (unsigned I = 0; I <= Opts.Z3CrosscheckRetriesOnTimeout; ++I) { Result = AttemptOnce(RefutationSolver); Result.Z3QueryTimeMilliseconds = std::min(MinQueryTimeAcrossAttempts, Result.Z3QueryTimeMilliseconds); >From 06c41842c81adb0a5790f4e823d6e07fc12340e6 Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Jan 2025 15:34:49 +0100 Subject: [PATCH 3/6] Make the analysis option a Positive value --- .../StaticAnalyzer/Core/AnalyzerOptions.def | 19 +++++++------- .../StaticAnalyzer/Core/AnalyzerOptions.h | 25 +++++++++++++++++++ clang/lib/Frontend/CompilerInvocation.cpp | 19 ++++++++++++++ .../Core/Z3CrosscheckVisitor.cpp | 6 ++--- clang/test/Analysis/analyzer-config.c | 2 +- clang/test/Analysis/z3-crosscheck-retry.cpp | 4 +-- .../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 11 +++++++- 7 files changed, 70 insertions(+), 16 deletions(-) diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index 46ff91f488fb5c..976d56497cf18f 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -10,9 +10,10 @@ // //===----------------------------------------------------------------------===// -#ifndef LLVM_ADT_STRINGREF_H +#if !defined(LLVM_ADT_STRINGREF_H) || !defined(LLVM_CLANG_STATICANALYZER_CORE_ANALYZEROPTIONS_H) #error This .def file is expected to be included in translation units where \ -"llvm/ADT/StringRef.h" is already included! +"llvm/ADT/StringRef.h" and "clang/StaticAnalyzer/Core/AnalyzerOptions.h" are \ +already included! #endif #ifdef ANALYZER_OPTION @@ -216,13 +217,13 @@ ANALYZER_OPTION( "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) + PositiveAnalyzerOption, Z3CrosscheckMaxAttemptsPerQuery, + "crosscheck-with-z3-max-attempts-per-query", + "Set how many times the oracle is allowed to run a Z3 query. " + "This must be a positive value. Set 1 to not allow any retry attempts. " + "Increasing the number of attempts is often more effective at reducing " + "the number of nondeterministic diagnostics than " + "\"crosscheck-with-z3-timeout-threshold\" in practice.", 3) ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile, "report-in-main-source-file", diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h index 2f4cd277cccdc6..3f341ecf8c1e4f 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h @@ -124,6 +124,31 @@ enum UserModeKind { enum class CTUPhase1InliningKind { None, Small, All }; +class PositiveAnalyzerOption { +public: + PositiveAnalyzerOption() = default; + PositiveAnalyzerOption(const PositiveAnalyzerOption &) = default; + PositiveAnalyzerOption &operator=(const PositiveAnalyzerOption &) = default; + + static std::optional<PositiveAnalyzerOption> create(unsigned Val) { + if (Val == 0) + return std::nullopt; + return PositiveAnalyzerOption{Val}; + } + static std::optional<PositiveAnalyzerOption> create(StringRef Str) { + unsigned Parsed = 0; + if (Str.getAsInteger(0, Parsed)) + return std::nullopt; + return PositiveAnalyzerOption::create(Parsed); + } + operator unsigned() const { return Value; } + +private: + explicit constexpr PositiveAnalyzerOption(unsigned Value) : Value(Value) {} + + unsigned Value = 1; +}; + /// Stores options for the analyzer from the command line. /// /// Some options are frontend flags (e.g.: -analyzer-output), but some are diff --git a/clang/lib/Frontend/CompilerInvocation.cpp b/clang/lib/Frontend/CompilerInvocation.cpp index 36dc45bde11abc..6e47b374d4ed86 100644 --- a/clang/lib/Frontend/CompilerInvocation.cpp +++ b/clang/lib/Frontend/CompilerInvocation.cpp @@ -1260,6 +1260,25 @@ static void initOption(AnalyzerOptions::ConfigTable &Config, << Name << "an unsigned"; } +static void initOption(AnalyzerOptions::ConfigTable &Config, + DiagnosticsEngine *Diags, + PositiveAnalyzerOption &OptionField, StringRef Name, + unsigned DefaultVal) { + auto Parsed = PositiveAnalyzerOption::create( + getStringOption(Config, Name, std::to_string(DefaultVal))); + if (Parsed.has_value()) { + OptionField = Parsed.value(); + return; + } + if (Diags && !Parsed.has_value()) + Diags->Report(diag::err_analyzer_config_invalid_input) + << Name << "a positive"; + + auto Default = PositiveAnalyzerOption::create(DefaultVal); + assert(Default.has_value()); + OptionField = Default.value(); +} + static void parseAnalyzerConfigs(AnalyzerOptions &AnOpts, DiagnosticsEngine *Diags) { // TODO: There's no need to store the entire configtable, it'd be plenty diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index 4ccbffa598b708..7c2e5541647972 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -21,8 +21,8 @@ #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 +// Queries retried at most `Z3CrosscheckMaxAttemptsPerQuery` 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"); @@ -99,7 +99,7 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, // And check for satisfiability unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max(); - for (unsigned I = 0; I <= Opts.Z3CrosscheckRetriesOnTimeout; ++I) { + for (unsigned I = 0; I <= Opts.Z3CrosscheckMaxAttemptsPerQuery; ++I) { Result = AttemptOnce(RefutationSolver); Result.Z3QueryTimeMilliseconds = std::min(MinQueryTimeAcrossAttempts, Result.Z3QueryTimeMilliseconds); diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c index af4527c9fb2823..d5eb790b82f238 100644 --- a/clang/test/Analysis/analyzer-config.c +++ b/clang/test/Analysis/analyzer-config.c @@ -41,7 +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-max-attempts-per-query = 3 // 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 index b81d3469b3dd26..ee8ff6df709e14 100644 --- a/clang/test/Analysis/z3-crosscheck-retry.cpp +++ b/clang/test/Analysis/z3-crosscheck-retry.cpp @@ -1,7 +1,7 @@ // 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 +// CHECK: crosscheck-with-z3-max-attempts-per-query = 3 // RUN: rm -rf %t && mkdir %t // RUN: %host_cxx -shared -fPIC \ @@ -14,7 +14,7 @@ // DEFINE: -analyzer-config crosscheck-with-z3=true \ // DEFINE: -analyzer-checker=core -// DEFINE: %{retry} = -analyzer-config crosscheck-with-z3-retries-on-timeout +// DEFINE: %{retry} = -analyzer-config crosscheck-with-z3-max-attempts-per-query // RUN: Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{retry}=0 -verify=refuted // RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{retry}=0 -verify=refuted diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp index 626f5c163d17d0..ed8627c500098a 100644 --- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp +++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp @@ -27,13 +27,22 @@ static constexpr std::optional<bool> UNDEF = std::nullopt; static unsigned operator""_ms(unsigned long long ms) { return ms; } static unsigned operator""_step(unsigned long long rlimit) { return rlimit; } +template <class Ret, class Arg> static Ret makeDefaultOption(Arg Value) { + return Value; +} +template <> PositiveAnalyzerOption makeDefaultOption(int Value) { + auto DefaultVal = PositiveAnalyzerOption::create(Value); + assert(DefaultVal.has_value()); + return DefaultVal.value(); +} + static const AnalyzerOptions DefaultOpts = [] { AnalyzerOptions Config; #define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC, \ SHALLOW_VAL, DEEP_VAL) \ ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL) #define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL) \ - Config.NAME = DEFAULT_VAL; + Config.NAME = makeDefaultOption<TYPE>(DEFAULT_VAL); #include "clang/StaticAnalyzer/Core/AnalyzerOptions.def" // Remember to update the tests in this file when these values change. >From 930b2a8c310d1f3ae0a4671e0dfaecbf80784f83 Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Jan 2025 16:28:35 +0100 Subject: [PATCH 4/6] Fix off-by-one error in loop condition --- clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index 7c2e5541647972..8d5e83ec258107 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -99,7 +99,7 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, // And check for satisfiability unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max(); - for (unsigned I = 0; I <= Opts.Z3CrosscheckMaxAttemptsPerQuery; ++I) { + for (unsigned I = 0; I < Opts.Z3CrosscheckMaxAttemptsPerQuery; ++I) { Result = AttemptOnce(RefutationSolver); Result.Z3QueryTimeMilliseconds = std::min(MinQueryTimeAcrossAttempts, Result.Z3QueryTimeMilliseconds); >From 9a9c112939926cb86fe746b429288bb5448cf15f Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Jan 2025 16:30:00 +0100 Subject: [PATCH 5/6] Uplift test to match the new name of the flag; test added semantics --- ...try.cpp => z3-crosscheck-max-attempts.cpp} | 23 +++++++++++-------- 1 file changed, 13 insertions(+), 10 deletions(-) rename clang/test/Analysis/{z3-crosscheck-retry.cpp => z3-crosscheck-max-attempts.cpp} (71%) diff --git a/clang/test/Analysis/z3-crosscheck-retry.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp similarity index 71% rename from clang/test/Analysis/z3-crosscheck-retry.cpp rename to clang/test/Analysis/z3-crosscheck-max-attempts.cpp index ee8ff6df709e14..7951d265464735 100644 --- a/clang/test/Analysis/z3-crosscheck-retry.cpp +++ b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp @@ -14,19 +14,22 @@ // DEFINE: -analyzer-config crosscheck-with-z3=true \ // DEFINE: -analyzer-checker=core -// DEFINE: %{retry} = -analyzer-config crosscheck-with-z3-max-attempts-per-query +// DEFINE: %{attempts} = -analyzer-config crosscheck-with-z3-max-attempts-per-query -// 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: not %clang_analyze_cc1 %{attempts}=0 2>&1 | FileCheck %s --check-prefix=VERIFY-INVALID +// VERIFY-INVALID: invalid input for analyzer-config option 'crosscheck-with-z3-max-attempts-per-query', that expects a positive value -// 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" %{mocked_clang} %{attempts}=1 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{attempts}=1 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{attempts}=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 +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{attempts}=2 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{attempts}=2 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{attempts}=2 -verify=accepted + +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{attempts}=3 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{attempts}=3 -verify=refuted +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{attempts}=3 -verify=accepted // REQUIRES: z3, asserts, shell, system-linux >From 23a16546cb67331c763ae28017a4d9123f3e2b99 Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Jan 2025 16:41:29 +0100 Subject: [PATCH 6/6] Update stale comment --- clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp index 8d5e83ec258107..c4dd016f70d866 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -21,9 +21,10 @@ #define DEBUG_TYPE "Z3CrosscheckOracle" -// Queries retried at most `Z3CrosscheckMaxAttemptsPerQuery` 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. +// Queries attempted at most `Z3CrosscheckMaxAttemptsPerQuery` number of times. +// Multiple `check()` calls might be called on the same query if previous +// attempts of the same query resulted in UNSAT 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, _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
