[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

Author: steakhal

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 "

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(

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 = ""

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}}
+}

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) {
   }

clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c

@@ -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();
+}