[clang] [analyzer] Retry UNDEF Z3 queries at most "crosscheck-with-z3-retries-on-timeout" times (PR #120239)
Balazs Benics via cfe-commits
cfe-commits at lists.llvm.org
Tue Dec 17 06:51:48 PST 2024
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 <benicsbalazs at 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();
+}
More information about the cfe-commits
mailing list