Make the analysis option a Positive value

Author: steakhal

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

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,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);

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

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

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.