[clang] [clang-tools-extra] Use Z3 (when available) for more complex cases in the clang dataflow framework (PR #222378)
Jan Voung via cfe-commits
cfe-commits at lists.llvm.org
Sat Oct 24 20:49:02 PDT 2026
https://github.com/jvoung updated https://github.com/llvm/llvm-project/pull/222378
>From da6e01cc670f9f9c8a95b48f4e511dd16e951269 Mon Sep 17 00:00:00 2001
From: Jan Voung <jvoung at gmail.com>
Date: Wed, 9 Sep 2026 16:04:38 +0000
Subject: [PATCH 1/2] Use Z3 (when available) for more complex cases in the
clang dataflow framework
Adds a Solver factory that users can override at the entry point
of the clang dataflow framework.
Current approach implicitly/automatically uses Z3 if available in
the build. If it is not available in the build, will just use
the current basic WatchedLiteralsSolver (no functionality change).
Alternatively, we could gate this on a checker option similar to how CSA
has `-crosscheck-with-z3=true`, which a user must request explicitly.
Then, there is a runtime error if z3 was not actually available.
Benchmark with ccache (issue #69369):
- before: 78.4121 seconds overall (24.9s for the sloweset TU
argprocessing.cpp -- including parsing, etc.)
- after: 4.9644 seconds overall (8.7s for the slowest TU
argprocessing.cpp -- including parsing, etc.)
"Overall" time is from run-clang-tidy.py -enable-check-profile sum
over the ccache project.
---
.../Analysis/FlowSensitive/DataflowAnalysis.h | 23 ++-
.../Analysis/FlowSensitive/TieredSolver.h | 64 +++++++++
.../clang/Analysis/FlowSensitive/Z3Solver.h | 58 ++++++++
.../lib/Analysis/FlowSensitive/CMakeLists.txt | 4 +-
.../FlowSensitive/DataflowAnalysis.cpp | 50 +++++++
clang/lib/Analysis/FlowSensitive/Z3Solver.cpp | 135 ++++++++++++++++++
.../Analysis/FlowSensitive/CMakeLists.txt | 1 +
.../FlowSensitive/TieredSolverTest.cpp | 84 +++++++++++
.../Analysis/FlowSensitive/Z3SolverTest.cpp | 27 ++++
9 files changed, 433 insertions(+), 13 deletions(-)
create mode 100644 clang/include/clang/Analysis/FlowSensitive/TieredSolver.h
create mode 100644 clang/include/clang/Analysis/FlowSensitive/Z3Solver.h
create mode 100644 clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp
create mode 100644 clang/lib/Analysis/FlowSensitive/Z3Solver.cpp
create mode 100644 clang/unittests/Analysis/FlowSensitive/TieredSolverTest.cpp
create mode 100644 clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
index e6efde091871fc..5bceda5f26dc94 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
@@ -209,8 +209,11 @@ template <typename AnalysisT, typename Diagnostic> struct DiagnosisCallbacks {
DiagnosisCallback<AnalysisT, Diagnostic> After;
};
-/// Default for the maximum number of SAT solver iterations during analysis.
-inline constexpr std::int64_t kDefaultMaxSATIterations = 1'000'000'000;
+/// A factory for creating a Solver.
+using SolverFactory = std::function<std::unique_ptr<Solver>()>;
+
+/// Default SolverFactory.
+std::unique_ptr<Solver> createDefaultSolver();
/// Default for the maximum number of block visits during analysis.
inline constexpr std::int32_t kDefaultMaxBlockVisits = 20'000;
@@ -307,12 +310,8 @@ auto createAnalysis(ASTContext &ASTCtx, Environment &Env)
/// error. Currently, errors can occur (at least) because the analysis requires
/// too many iterations over the CFG or the SAT solver times out.
///
-/// The default value of `MaxSATIterations` was chosen based on the following
-/// observations:
-/// - Non-pathological calls to the solver typically require only a few hundred
-/// iterations.
-/// - This limit is still low enough to keep runtimes acceptable (on typical
-/// machines) in cases where we hit the limit.
+/// `MakeSolver` allows the caller to inject a custom SAT solver (e.g.,
+/// it may have custom timeout settings, or use different algorithms).
///
/// `MaxBlockVisits` caps the number of block visits during analysis. See
/// `runDataflowAnalysis` for a full description and explanation of the default
@@ -321,13 +320,13 @@ template <typename AnalysisT, typename Diagnostic>
llvm::Expected<llvm::SmallVector<Diagnostic>>
diagnoseFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx,
DiagnosisCallbacks<AnalysisT, Diagnostic> Diagnoser,
- std::int64_t MaxSATIterations = kDefaultMaxSATIterations,
+ const SolverFactory &MakeSolver = createDefaultSolver,
std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits) {
llvm::Expected<AdornedCFG> Context = AdornedCFG::build(FuncDecl);
if (!Context)
return Context.takeError();
- auto Solver = std::make_unique<WatchedLiteralsSolver>(MaxSATIterations);
+ auto Solver = MakeSolver();
DataflowAnalysisContext AnalysisContext(*Solver);
Environment Env(AnalysisContext, FuncDecl);
AnalysisT Analysis = createAnalysis<AnalysisT>(ASTCtx, Env);
@@ -382,10 +381,10 @@ template <typename AnalysisT, typename Diagnostic>
llvm::Expected<llvm::SmallVector<Diagnostic>>
diagnoseFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx,
DiagnosisCallback<AnalysisT, Diagnostic> Diagnoser,
- std::int64_t MaxSATIterations = kDefaultMaxSATIterations,
+ const SolverFactory &MakeSolver = createDefaultSolver,
std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits) {
DiagnosisCallbacks<AnalysisT, Diagnostic> Callbacks = {nullptr, Diagnoser};
- return diagnoseFunction(FuncDecl, ASTCtx, Callbacks, MaxSATIterations,
+ return diagnoseFunction(FuncDecl, ASTCtx, Callbacks, MakeSolver,
MaxBlockVisits);
}
diff --git a/clang/include/clang/Analysis/FlowSensitive/TieredSolver.h b/clang/include/clang/Analysis/FlowSensitive/TieredSolver.h
new file mode 100644
index 00000000000000..b3ffc90a5822f1
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/TieredSolver.h
@@ -0,0 +1,64 @@
+//===- TieredSolver.h -------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a SAT solver implementation that can be used by dataflow
+// analyses.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_TIEREDSOLVER_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_TIEREDSOLVER_H
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "llvm/ADT/ArrayRef.h"
+
+namespace clang {
+namespace dataflow {
+
+/// A `Solver` implementation that delegates to a sequence of other solvers.
+///
+/// The first solver that does not time out is used to produce the result.
+///
+/// The intent is that we can combine a solver that solves simple problems
+/// quickly but times out on harder problems (e.g. `WatchedLiteralsSolver`) with
+/// a solver that solves simple problems more slowly but can solve harder
+/// problems without timing out.
+class TieredSolver : public Solver {
+public:
+ explicit TieredSolver(llvm::SmallVector<std::unique_ptr<Solver>> Tiers)
+ : Tiers_(std::move(Tiers)) {
+ assert(!Tiers_.empty());
+ }
+
+ Result solve(llvm::ArrayRef<const Formula *> Constraints) override {
+ for (const auto &Tier : Tiers_) {
+ Result Res = Tier->solve(Constraints);
+ if (Res.getStatus() != Result::Status::TimedOut)
+ return Res;
+ }
+
+ return Result::TimedOut();
+ }
+
+ bool reachedLimit() const override {
+ for (const auto &Tier : Tiers_)
+ if (!Tier->reachedLimit())
+ return false;
+
+ return true;
+ }
+
+private:
+ llvm::SmallVector<std::unique_ptr<Solver>> Tiers_;
+};
+
+} // namespace dataflow
+} // namespace clang
+
+#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_TIEREDSOLVER_H
diff --git a/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h b/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h
new file mode 100644
index 00000000000000..62444778bbeb6f
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h
@@ -0,0 +1,58 @@
+//===- Z3Solver.h -----------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a Z3-based SAT solver implementation that can be used by
+// dataflow analyses.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_Z3SOLVER_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_Z3SOLVER_H
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/Support/SMTAPI.h"
+
+namespace clang {
+namespace dataflow {
+
+/// Wrapper around Z3 to use it as a SAT solver (not full SMT).
+class Z3Solver : public Solver {
+
+public:
+ Z3Solver() : Solver(llvm::CreateZ3Solver()) {
+ Solver->setBoolParam("model", true);
+ }
+
+ // Creates a Z3-based solver with the given "rlimit" (0 is unlimited).
+ // Rlimit is a count of operations, which may be more deterministic
+ // than time. However, it could change across Z3 versions:
+ // https://stackoverflow.com/questions/45457131/what-is-the-relation-between-options-rlimit-and-timeout/45458651#45458651
+ explicit Z3Solver(std::uint32_t Rlimit)
+ : Rlimit(Rlimit), Solver(llvm::CreateZ3Solver()) {
+ Solver->setBoolParam("model", true);
+ }
+
+ Result solve(llvm::ArrayRef<const Formula *> Vals) override;
+
+ bool reachedLimit() const override { return EverTimedOut; }
+
+private:
+ std::uint32_t Rlimit = 0; // 0 is unlimited
+ std::uint32_t RlimitUsed = 0; // track rlimit used (if Rlimit is non-zero)
+ bool EverTimedOut = false;
+ llvm::SMTSolverRef Solver;
+
+ void updateRlimitUsed(const llvm::SMTSolverRef &Solver);
+};
+
+} // namespace dataflow
+} // namespace clang
+
+#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_Z3SOLVER_H
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 97e09c9bce95f8..4f94720400463e 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,8 +3,10 @@ add_clang_library(clangAnalysisFlowSensitive
Arena.cpp
ASTOps.cpp
CNFFormula.cpp
+ DataflowAnalysis.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
+ DebugSupport.cpp
Formula.cpp
FormulaSerialization.cpp
HTMLLogger.cpp
@@ -16,7 +18,7 @@ add_clang_library(clangAnalysisFlowSensitive
TypeErasedDataflowAnalysis.cpp
Value.cpp
WatchedLiteralsSolver.cpp
- DebugSupport.cpp
+ Z3Solver.cpp
DEPENDS
clangAnalysisFlowSensitiveResources
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp
new file mode 100644
index 00000000000000..a35510e870be6b
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp
@@ -0,0 +1,50 @@
+//===-- DataflowAnalysis.cpp ------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines functions for the DataflowAnalysis entry points.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/TieredSolver.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Analysis/FlowSensitive/Z3Solver.h"
+#include "llvm/ADT/SmallVector.h"
+
+namespace clang {
+namespace dataflow {
+
+std::unique_ptr<Solver> createDefaultSolver() {
+#ifdef LLVM_WITH_Z3
+ // When Z3 is available, do a tiering strategy:
+ // - a simple solver for simple functions
+ // - fall back to a production-grade solver for more complex functions.
+ llvm::SmallVector<std::unique_ptr<dataflow::Solver>> Tiers;
+ constexpr std::int64_t MaxSATIterations = 5'000'000;
+ Tiers.push_back(
+ std::make_unique<dataflow::WatchedLiteralsSolver>(MaxSATIterations));
+
+ constexpr std::uint32_t Z3Rlimit = 1'000'000'000;
+ Tiers.push_back(std::make_unique<dataflow::Z3Solver>(Z3Rlimit));
+ return std::make_unique<TieredSolver>(std::move(Tiers));
+#else
+ /// Default for the maximum number of SAT solver iterations during analysis.
+ /// The value was chosen based on the following observations:
+ /// - Non-pathological calls to the solver typically require only a few
+ /// hundred
+ /// iterations.
+ /// - This limit is still low enough to keep runtimes acceptable (on typical
+ /// machines) in cases where we hit the limit.
+ constexpr std::int64_t kDefaultMaxSATIterations = 1'000'000'000;
+ return std::make_unique<WatchedLiteralsSolver>(kDefaultMaxSATIterations);
+#endif
+}
+
+} // namespace dataflow
+} // namespace clang
diff --git a/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp b/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp
new file mode 100644
index 00000000000000..1462d7b22d4367
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp
@@ -0,0 +1,135 @@
+//===- Z3Solver.cpp ---------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a Z3-based SAT solver implementation that can be used by
+// dataflow analyses.
+//
+//===----------------------------------------------------------------------===//
+
+#include <cassert>
+#include <vector>
+
+#include "clang/Analysis/FlowSensitive/CNFFormula.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Z3Solver.h"
+#include "llvm/ADT/APInt.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/SmallString.h"
+#include "llvm/Support/SMTAPI.h"
+
+namespace clang {
+namespace dataflow {
+
+static llvm::DenseMap<Atom, Solver::Result::Assignment>
+buildSolution(const llvm::SMTSolverRef &Solver,
+ const llvm::DenseMap<Variable, Atom> &Atomics,
+ llvm::ArrayRef<llvm::SMTExprRef> BoolVars) {
+ llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
+
+ for (auto &Atomic : Atomics) {
+ llvm::SMTExprRef Var = BoolVars[Atomic.first];
+ llvm::APSInt Result = llvm::APSInt(1);
+ if (!Solver->getInterpretation(Var, Result)) {
+ // Model doesn't assign a value -- just pick one.
+ Solution[Atomic.second] = Solver::Result::Assignment::AssignedTrue;
+ } else {
+ Solution[Atomic.second] = Result.getBoolValue()
+ ? Solver::Result::Assignment::AssignedTrue
+ : Solver::Result::Assignment::AssignedFalse;
+ }
+ }
+
+ return Solution;
+}
+
+void Z3Solver::updateRlimitUsed(const llvm::SMTSolverRef &Solver) {
+ if (Rlimit > 0) {
+ std::uint32_t NextRlimitUsed =
+ Solver->getStatistics()->getUnsigned("rlimit count");
+ std::uint32_t Next = RlimitUsed + NextRlimitUsed;
+ // If overflow, clamp
+ if (Next < RlimitUsed)
+ RlimitUsed = Rlimit;
+ // If going past Rlimit, clamp
+ else if (Next > Rlimit)
+ RlimitUsed = Rlimit;
+ else
+ RlimitUsed = Next;
+ }
+}
+
+Solver::Result Z3Solver::solve(llvm::ArrayRef<const Formula *> Constraints) {
+ if (Constraints.empty()) {
+ return Result::Satisfiable(llvm::DenseMap<Atom, Result::Assignment>());
+ }
+ if (Rlimit > 0 && RlimitUsed == Rlimit) {
+ return Result::TimedOut();
+ }
+
+ llvm::DenseMap<Variable, Atom> Atomics;
+ CNFFormula CNF = buildCNF(Constraints, Atomics);
+
+ if (CNF.knownContradictory())
+ return Result::Unsatisfiable();
+
+ Solver->reset();
+ Solver->setBoolParam("model", true);
+ if (Rlimit != 0) {
+ std::uint32_t Remaining = Rlimit - RlimitUsed;
+ Solver->setUnsignedParam("rlimit", Remaining);
+ }
+
+ std::vector<llvm::SMTExprRef> BoolVars;
+ BoolVars.resize(CNF.largestVar() + 1);
+ llvm::SmallString<16> Str;
+ llvm::raw_svector_ostream OS(Str);
+ llvm::SMTSortRef BoolSort = Solver->getBoolSort();
+ for (Variable V = 1; V <= CNF.largestVar(); ++V) {
+ OS << "v" << V;
+ BoolVars[V] = Solver->mkSymbol(Str.c_str(), BoolSort);
+ Str.clear();
+ }
+
+ for (size_t ClauseId = 1; ClauseId <= CNF.numClauses(); ++ClauseId) {
+ llvm::SMTExprRef Clause = nullptr;
+ for (Literal Lit : CNF.clauseLiterals(ClauseId)) {
+ llvm::SMTExprRef Var = BoolVars[var(Lit)];
+ if (isNegLit(Lit))
+ Var = Solver->mkNot(Var);
+ if (Clause == nullptr) {
+ Clause = Var;
+ } else {
+ Clause = Solver->mkOr(Clause, Var);
+ }
+ }
+ if (Clause == nullptr) {
+ Solver->addConstraint(Solver->mkBoolean(false));
+ } else {
+ Solver->addConstraint(Clause);
+ }
+ }
+
+ std::optional<bool> IsSat = Solver->check();
+
+ // Update rlimit
+ updateRlimitUsed(Solver);
+
+ if (IsSat.has_value()) {
+ if (IsSat.value()) {
+ return Result::Satisfiable(buildSolution(Solver, Atomics, BoolVars));
+ }
+ return Result::Unsatisfiable();
+ }
+ EverTimedOut = true;
+ return Result::TimedOut();
+}
+
+} // namespace dataflow
+} // namespace clang
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index 1d932ec6e8a963..6e6b1c535af565 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -29,6 +29,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
UncheckedStatusOrAccessModelTestFixture.cpp
ValueTest.cpp
WatchedLiteralsSolverTest.cpp
+ Z3SolverTest.cpp
CLANG_LIBS
clangAST
clangASTMatchers
diff --git a/clang/unittests/Analysis/FlowSensitive/TieredSolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/TieredSolverTest.cpp
new file mode 100644
index 00000000000000..0809615525902b
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/TieredSolverTest.cpp
@@ -0,0 +1,84 @@
+#include "clang/Analysis/FlowSensitive/TieredSolver.h"
+
+#include <memory>
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/SmallVector.h"
+#include "gtest/gtest.h"
+
+namespace clang::dataflow::test {
+
+namespace {
+
+using Result = Solver::Result;
+
+class MockSolver : public Solver {
+public:
+ explicit MockSolver(Result Res) : Res(Res) {}
+
+ Result solve(llvm::ArrayRef<const dataflow::Formula *>) override {
+ return Res;
+ }
+
+ bool reachedLimit() const override {
+ return Res.getStatus() == Result::Status::TimedOut;
+ }
+
+private:
+ Result Res;
+};
+
+static llvm::SmallVector<std::unique_ptr<Solver>>
+makeMockSolvers(llvm::ArrayRef<Result> Results) {
+ llvm::SmallVector<std::unique_ptr<dataflow::Solver>> Solvers;
+
+ for (const auto &Res : Results)
+ Solvers.push_back(std::make_unique<MockSolver>(Res));
+
+ return Solvers;
+}
+
+TEST(TieredSolverTest, SingleSatisfiableStage) {
+ TieredSolver Solver(makeMockSolvers({Result::Satisfiable({{}})}));
+ EXPECT_EQ(Solver.solve({}).getStatus(), Result::Status::Satisfiable);
+ EXPECT_FALSE(Solver.reachedLimit());
+}
+
+TEST(TieredSolverTest, SingleUnsatisfiableStage) {
+ TieredSolver Solver(makeMockSolvers({Result::Unsatisfiable()}));
+ EXPECT_EQ(Solver.solve({}).getStatus(), Result::Status::Unsatisfiable);
+ EXPECT_FALSE(Solver.reachedLimit());
+}
+
+TEST(TieredSolverTest, SingleTimedOutStage) {
+ TieredSolver Solver(makeMockSolvers({Result::TimedOut()}));
+ EXPECT_EQ(Solver.solve({}).getStatus(), Result::Status::TimedOut);
+ EXPECT_TRUE(Solver.reachedLimit());
+}
+
+TEST(TieredSolverTest, UnsatisfiableThenTimedOut) {
+ TieredSolver Solver(
+ makeMockSolvers({Result::Unsatisfiable(), Result::TimedOut()}));
+ EXPECT_EQ(Solver.solve({}).getStatus(), Result::Status::Unsatisfiable);
+ EXPECT_FALSE(Solver.reachedLimit());
+}
+
+TEST(TieredSolverTest, TimedOutThenUnsatisfiable) {
+ TieredSolver Solver(
+ makeMockSolvers({Result::TimedOut(), Result::Unsatisfiable()}));
+ EXPECT_EQ(Solver.solve({}).getStatus(), Result::Status::Unsatisfiable);
+ EXPECT_FALSE(Solver.reachedLimit());
+}
+
+TEST(TieredSolverTest, TwoTimedOutStages) {
+ TieredSolver Solver(
+ makeMockSolvers({Result::TimedOut(), Result::TimedOut()}));
+ EXPECT_EQ(Solver.solve({}).getStatus(), Result::Status::TimedOut);
+ EXPECT_TRUE(Solver.reachedLimit());
+}
+
+} // namespace
+
+} // namespace clang::dataflow::test
diff --git a/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp
new file mode 100644
index 00000000000000..d53be2b23feee1
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp
@@ -0,0 +1,27 @@
+//===- unittests/Analysis/FlowSensitive/Z3SolverTest.cpp -----===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Z3Solver.h"
+#include "SolverTest.h"
+
+namespace clang::dataflow::test {
+
+#ifdef LLVM_WITH_Z3
+template <> Z3Solver SolverTest<Z3Solver>::createSolverWithLowTimeout() {
+ return Z3Solver(1);
+}
+
+namespace {
+
+INSTANTIATE_TYPED_TEST_SUITE_P(Z3SolverTest, SolverTest, Z3Solver, );
+
+} // namespace
+
+#endif // LLVM_WITH_Z3
+
+} // namespace clang::dataflow::test
>From 1e717da7b1c1a2ab65b1d7a23a30415b06cca40b Mon Sep 17 00:00:00 2001
From: Jan Voung <jvoung at gmail.com>
Date: Fri, 9 Oct 2026 13:47:27 +0000
Subject: [PATCH 2/2] Fix accounting of rlimit used in Z3, now that we reuse
the Z3 instance
... and just call reset between queries. Reset doesn't reset the
cumulative rlimit count, so our separate accounting of the rlimit count
assuming it reset each time is wrong.
---
.../bugprone/UncheckedOptionalAccessCheck.cpp | 7 ++-
.../bugprone/UncheckedOptionalAccessCheck.h | 25 ++++++++--
.../Analysis/FlowSensitive/DataflowAnalysis.h | 10 ++++
.../clang/Analysis/FlowSensitive/Z3Solver.h | 5 +-
.../FlowSensitive/DataflowAnalysis.cpp | 39 ++++++++++-----
clang/lib/Analysis/FlowSensitive/Z3Solver.cpp | 31 +++++-------
.../Analysis/FlowSensitive/Z3SolverTest.cpp | 47 ++++++++++++++++++-
7 files changed, 120 insertions(+), 44 deletions(-)
diff --git a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
index 09c86e7da94f31..81cd962e9c4edc 100644
--- a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
+++ b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
@@ -57,13 +57,16 @@ void UncheckedOptionalAccessCheck::check(
if (llvm::Expected<SmallVector<UncheckedOptionalAccessDiagnostic>> Diags =
dataflow::diagnoseFunction<UncheckedOptionalAccessModel,
UncheckedOptionalAccessDiagnostic>(
- *FuncDecl, *Result.Context, Diagnoser))
+ *FuncDecl, *Result.Context, Diagnoser,
+ [this] { return dataflow::createSolver(SolverMode); }))
for (const UncheckedOptionalAccessDiagnostic &Diag : *Diags) {
diag(Diag.Range.getBegin(), "unchecked access to optional value")
<< Diag.Range;
}
- else
+ else {
+ diag(FuncDecl->getBeginLoc(), "timeout in SAT analysis");
llvm::consumeError(Diags.takeError());
+ }
}
} // namespace clang::tidy::bugprone
diff --git a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
index 62bf42da4f9f97..a44ecae4695b24 100644
--- a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
+++ b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
@@ -11,9 +11,24 @@
#include "../ClangTidyCheck.h"
#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
#include "clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h"
-namespace clang::tidy::bugprone {
+namespace clang::tidy {
+
+template <> struct OptionEnumMapping<dataflow::SolverMode> {
+ static llvm::ArrayRef<std::pair<dataflow::SolverMode, StringRef>>
+ getEnumMapping() {
+ static constexpr std::pair<dataflow::SolverMode, StringRef> Mapping[] = {
+ {dataflow::SolverMode::WatchedLiterals, "watched"},
+ {dataflow::SolverMode::Z3, "z3"},
+ {dataflow::SolverMode::Tiered, "tiered"},
+ };
+ return {Mapping};
+ }
+};
+
+namespace bugprone {
/// Warns when the code is unwrapping a `std::optional<T>`, `absl::optional<T>`,
/// or `base::std::optional<T>` object without assuring that it contains a
@@ -26,7 +41,8 @@ class UncheckedOptionalAccessCheck : public ClangTidyCheck {
UncheckedOptionalAccessCheck(StringRef Name, ClangTidyContext *Context)
: ClangTidyCheck(Name, Context),
ModelOptions{Options.get("IgnoreSmartPointerDereference", false),
- Options.get("IgnoreValueCalls", false)} {}
+ Options.get("IgnoreValueCalls", false)},
+ SolverMode(Options.get("SolverMode", dataflow::SolverMode::Tiered)) {}
void registerMatchers(ast_matchers::MatchFinder *Finder) override;
void check(const ast_matchers::MatchFinder::MatchResult &Result) override;
bool isLanguageVersionSupported(const LangOptions &LangOpts) const override {
@@ -36,12 +52,15 @@ class UncheckedOptionalAccessCheck : public ClangTidyCheck {
Options.store(Opts, "IgnoreSmartPointerDereference",
ModelOptions.IgnoreSmartPointerDereference);
Options.store(Opts, "IgnoreValueCalls", ModelOptions.IgnoreValueCalls);
+ Options.store(Opts, "SolverMode", SolverMode);
}
private:
dataflow::UncheckedOptionalAccessModelOptions ModelOptions;
+ dataflow::SolverMode SolverMode;
};
-} // namespace clang::tidy::bugprone
+} // namespace bugprone
+} // namespace clang::tidy
#endif // LLVM_CLANG_TOOLS_EXTRA_CLANG_TIDY_BUGPRONE_UNCHECKEDOPTIONALACCESSCHECK_H
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
index 5bceda5f26dc94..95b05fcc4c1ab3 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
@@ -212,6 +212,16 @@ template <typename AnalysisT, typename Diagnostic> struct DiagnosisCallbacks {
/// A factory for creating a Solver.
using SolverFactory = std::function<std::unique_ptr<Solver>()>;
+enum class SolverMode {
+ WatchedLiterals,
+ Z3,
+ Tiered,
+};
+
+/// Creates a Solver for the given `Mode` (falling back to
+/// `WatchedLiteralsSolver` if Z3 is not available).
+std::unique_ptr<Solver> createSolver(SolverMode Mode);
+
/// Default SolverFactory.
std::unique_ptr<Solver> createDefaultSolver();
diff --git a/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h b/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h
index 62444778bbeb6f..c26ccc40f22b84 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Z3Solver.h
@@ -44,12 +44,9 @@ class Z3Solver : public Solver {
bool reachedLimit() const override { return EverTimedOut; }
private:
- std::uint32_t Rlimit = 0; // 0 is unlimited
- std::uint32_t RlimitUsed = 0; // track rlimit used (if Rlimit is non-zero)
+ std::uint32_t Rlimit = 0; // 0 is unlimited
bool EverTimedOut = false;
llvm::SMTSolverRef Solver;
-
- void updateRlimitUsed(const llvm::SMTSolverRef &Solver);
};
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp
index a35510e870be6b..4ec1ac2a64ebf4 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysis.cpp
@@ -16,23 +16,33 @@
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "clang/Analysis/FlowSensitive/Z3Solver.h"
#include "llvm/ADT/SmallVector.h"
+#include "llvm/Support/ErrorHandling.h"
namespace clang {
namespace dataflow {
-std::unique_ptr<Solver> createDefaultSolver() {
+std::unique_ptr<Solver> createSolver(SolverMode Mode) {
+ constexpr std::int64_t kDefaultMaxSATIterations = 1'000'000'000;
#ifdef LLVM_WITH_Z3
- // When Z3 is available, do a tiering strategy:
- // - a simple solver for simple functions
- // - fall back to a production-grade solver for more complex functions.
- llvm::SmallVector<std::unique_ptr<dataflow::Solver>> Tiers;
- constexpr std::int64_t MaxSATIterations = 5'000'000;
- Tiers.push_back(
- std::make_unique<dataflow::WatchedLiteralsSolver>(MaxSATIterations));
-
- constexpr std::uint32_t Z3Rlimit = 1'000'000'000;
- Tiers.push_back(std::make_unique<dataflow::Z3Solver>(Z3Rlimit));
- return std::make_unique<TieredSolver>(std::move(Tiers));
+ constexpr std::uint32_t kDefaultZ3Rlimit = 1'000'000'000;
+ switch (Mode) {
+ case SolverMode::WatchedLiterals:
+ return std::make_unique<WatchedLiteralsSolver>(kDefaultMaxSATIterations);
+ case SolverMode::Z3:
+ return std::make_unique<Z3Solver>(kDefaultZ3Rlimit);
+ case SolverMode::Tiered: {
+ // When Z3 is available, do a tiering strategy:
+ // - a simple solver for simple functions
+ // - fall back to a production-grade solver for more complex functions.
+ llvm::SmallVector<std::unique_ptr<dataflow::Solver>> Tiers;
+ constexpr std::int64_t MaxSATIterations = 5'000'000;
+ Tiers.push_back(
+ std::make_unique<dataflow::WatchedLiteralsSolver>(MaxSATIterations));
+ Tiers.push_back(std::make_unique<dataflow::Z3Solver>(kDefaultZ3Rlimit));
+ return std::make_unique<TieredSolver>(std::move(Tiers));
+ }
+ }
+ llvm_unreachable("Unhandled SolverMode");
#else
/// Default for the maximum number of SAT solver iterations during analysis.
/// The value was chosen based on the following observations:
@@ -41,10 +51,13 @@ std::unique_ptr<Solver> createDefaultSolver() {
/// iterations.
/// - This limit is still low enough to keep runtimes acceptable (on typical
/// machines) in cases where we hit the limit.
- constexpr std::int64_t kDefaultMaxSATIterations = 1'000'000'000;
return std::make_unique<WatchedLiteralsSolver>(kDefaultMaxSATIterations);
#endif
}
+std::unique_ptr<Solver> createDefaultSolver() {
+ return createSolver(SolverMode::Tiered);
+}
+
} // namespace dataflow
} // namespace clang
diff --git a/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp b/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp
index 1462d7b22d4367..546b748e0ac298 100644
--- a/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Z3Solver.cpp
@@ -49,29 +49,23 @@ buildSolution(const llvm::SMTSolverRef &Solver,
return Solution;
}
-void Z3Solver::updateRlimitUsed(const llvm::SMTSolverRef &Solver) {
- if (Rlimit > 0) {
- std::uint32_t NextRlimitUsed =
- Solver->getStatistics()->getUnsigned("rlimit count");
- std::uint32_t Next = RlimitUsed + NextRlimitUsed;
- // If overflow, clamp
- if (Next < RlimitUsed)
- RlimitUsed = Rlimit;
- // If going past Rlimit, clamp
- else if (Next > Rlimit)
- RlimitUsed = Rlimit;
- else
- RlimitUsed = Next;
- }
-}
-
Solver::Result Z3Solver::solve(llvm::ArrayRef<const Formula *> Constraints) {
if (Constraints.empty()) {
return Result::Satisfiable(llvm::DenseMap<Atom, Result::Assignment>());
}
- if (Rlimit > 0 && RlimitUsed == Rlimit) {
+ if (EverTimedOut) {
return Result::TimedOut();
}
+ std::uint32_t RlimitUsed = 0;
+ if (Rlimit > 0) {
+ // Z3's "rlimit count" statistic is cumulative across `Solver->reset()`
+ // calls on the same Z3 context.
+ RlimitUsed = Solver->getStatistics()->getUnsigned("rlimit count");
+ if (RlimitUsed >= Rlimit) {
+ EverTimedOut = true;
+ return Result::TimedOut();
+ }
+ }
llvm::DenseMap<Variable, Atom> Atomics;
CNFFormula CNF = buildCNF(Constraints, Atomics);
@@ -118,9 +112,6 @@ Solver::Result Z3Solver::solve(llvm::ArrayRef<const Formula *> Constraints) {
std::optional<bool> IsSat = Solver->check();
- // Update rlimit
- updateRlimitUsed(Solver);
-
if (IsSat.has_value()) {
if (IsSat.value()) {
return Result::Satisfiable(buildSolution(Solver, Atomics, BoolVars));
diff --git a/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp
index d53be2b23feee1..7ed90847362346 100644
--- a/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/Z3SolverTest.cpp
@@ -11,15 +11,58 @@
namespace clang::dataflow::test {
-#ifdef LLVM_WITH_Z3
+#if LLVM_WITH_Z3
template <> Z3Solver SolverTest<Z3Solver>::createSolverWithLowTimeout() {
- return Z3Solver(1);
+ return Z3Solver(10);
}
namespace {
INSTANTIATE_TYPED_TEST_SUITE_P(Z3SolverTest, SolverTest, Z3Solver, );
+TEST(Z3SolverSpecificTest, ReuseSolverDoesNotOvercountCumulativeRlimit) {
+ Arena A;
+ auto Constraints = parseFormulas(A, R"(
+ (!(V0 | V1) = (!V0 & !V1))
+ (!(V2 & V3) = (!V2 | !V3))
+ )");
+ // Each solve uses ~800-1000 rlimit units. 10 solves use < 20000 rlimit units
+ // in total (linear in N), whereas mistakenly summing cumulative
+ // "rlimit count" stats across calls grows quadratically (~45x single-solve
+ // cost) and would exceed 20000.
+ Z3Solver Solver(20000);
+ for (int I = 0; I < 10; ++I) {
+ EXPECT_EQ(Solver.solve(Constraints).getStatus(),
+ Solver::Result::Status::Satisfiable);
+ EXPECT_FALSE(Solver.reachedLimit());
+ }
+}
+
+TEST(Z3SolverSpecificTest, ExhaustingRlimitAcrossMultipleCallsSetsReachedLimit) {
+ Arena A;
+ auto Constraints = parseFormulas(A, R"(
+ (!(V0 | V1) = (!V0 & !V1))
+ (!(V2 & V3) = (!V2 | !V3))
+ )");
+ Z3Solver Solver(3000);
+ bool SawSatisfiable = false;
+ bool SawTimeout = false;
+ for (int I = 0; I < 10; ++I) {
+ Solver::Result Res = Solver.solve(Constraints);
+ if (Res.getStatus() == Solver::Result::Status::Satisfiable) {
+ SawSatisfiable = true;
+ EXPECT_FALSE(SawTimeout);
+ EXPECT_FALSE(Solver.reachedLimit());
+ } else {
+ EXPECT_EQ(Res.getStatus(), Solver::Result::Status::TimedOut);
+ SawTimeout = true;
+ EXPECT_TRUE(Solver.reachedLimit());
+ }
+ }
+ EXPECT_TRUE(SawSatisfiable);
+ EXPECT_TRUE(SawTimeout);
+}
+
} // namespace
#endif // LLVM_WITH_Z3
More information about the cfe-commits
mailing list