aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def15
-rw-r--r--clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h25
-rw-r--r--clang/lib/Frontend/CompilerInvocation.cpp19
-rw-r--r--clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp38
-rw-r--r--clang/test/Analysis/analyzer-config.c1
-rw-r--r--clang/test/Analysis/z3-crosscheck-max-attempts.cpp42
-rw-r--r--clang/test/Analysis/z3/D83660.c17
-rw-r--r--clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c28
-rw-r--r--clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp62
-rw-r--r--clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp11
10 files changed, 208 insertions, 50 deletions
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
index d8a7c75..34bb7a8 100644
--- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
+++ b/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 "
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
index 2f4cd27..3f341ec 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 36dc45b..6e47b37 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 739db95..c4dd016 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/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(
diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c
index 8ce6184..d5eb790 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-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-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
new file mode 100644
index 0000000..7951d26
--- /dev/null
+++ b/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}}
+}
diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index fd46333..b42d934 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 9c63a64..0000000
--- 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 0000000..54cd86d
--- /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();
+}
diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
index 626f5c1..ed8627c 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.
generated by cgit v1.1 at 2025-08-04 05:11:55 +0000