[analyzer] Retry UNDEF Z3 queries 2 times by default

clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def

@@ -10,9 +10,9 @@
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef LLVM_ADT_STRINGREF_H
+#ifndef 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!
+"clang/StaticAnalyzer/Core/AnalyzerOptions.h" is already included!
 #endif
 
 #ifdef ANALYZER_OPTION
@@ -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(
+    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",
                 "Whether or not the diagnostic report should be always "

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

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

clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp

@@ -21,6 +21,10 @@
 
 #define DEBUG_TYPE "Z3CrosscheckOracle"
 
+// 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,
@@ -77,16 +81,32 @@ 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();
+  for (unsigned I = 0; I < Opts.Z3CrosscheckMaxAttemptsPerQuery; ++I) {
+    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-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 = ""

clang/test/Analysis/z3-crosscheck-max-attempts.cpp

@@ -0,0 +1,42 @@
+// Check the default config.
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ConfigDumper 2>&1 \
+// RUN: | FileCheck %s --match-full-lines
+// CHECK: crosscheck-with-z3-max-attempts-per-query = 3
+
+// 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: %{attempts} = -analyzer-config crosscheck-with-z3-max-attempts-per-query
+
+// 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"             %{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"       %{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
+
+// 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.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();
+}

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.