Skip to content

[clang-tidy] For bugprone-unchecked-optional-access add simple BoolSolverModel option - #240848

Merged
jvoung merged 6 commits into
llvm:mainfrom
jvoung:simple_bool_model_optional_checker_options
Nov 11, 2026
Merged

jvoung merged 6 commits into
llvm:mainfrom
jvoung:simple_bool_model_optional_checker_options

Conversation

@jvoung

@jvoung jvoung commented Nov 10, 2026 •

Copy link
Copy Markdown
Contributor

Adds a checker option to select the Simple BoolModel (introduced in the framework in #231061) for #224638. This gives users the choice of faster analysis (e.g., one way to address #69369), but requires "has value" checks to be more straightforward (no correlated branch conditions for example).

…del option

Adds a checker option to select the Simple BoolModel (introduced in the
framework in llvm#231061). This
gives users the choice of faster analysis (e.g., one way to address
llvm#69369), but requires has
value checks to be more straightforward (no correlated branch conditions
for example).
@github-actions

github-actions Bot commented Nov 10, 2026 •

Copy link
Copy Markdown

✅ With the latest revision this PR passed the C/C++ code formatter.

@jvoung
jvoung marked this pull request as ready for review November 10, 2026 15:12
@llvmorg-github-actions llvmorg-github-actions Bot added clang-tools-extra clang-tidy clang:dataflow Clang Dataflow Analysis framework - https://clang.llvm.org/docs/DataFlowAnalysisIntro.html clang:analysis labels Nov 10, 2026
@llvmorg-github-actions

llvmorg-github-actions Bot commented Nov 10, 2026 •

Copy link
Copy Markdown

@llvm/pr-subscribers-clang-tidy

@llvm/pr-subscribers-clang-tools-extra

Author: Jan Voung (jvoung)

Changes

Adds a checker option to select the Simple BoolModel (introduced in the framework in #231061). This gives users the choice of faster analysis (e.g., one way to address #69369), but requires "has value" checks to be more straightforward (no correlated branch conditions for example).


Full diff: https://github.com/llvm/llvm-project/pull/240848.diff

6 Files Affected:

  • (modified) clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp (+41-2)
  • (modified) clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h (+6-9)
  • (modified) clang-tools-extra/docs/ReleaseNotes.md (+9-3)
  • (modified) clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md (+14)
  • (modified) clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp (+6-1)
  • (modified) clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h (+6-4)
diff --git a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
index 09c86e7da94f31..351fcbbde85c1d 100644
--- a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
+++ b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
@@ -7,15 +7,33 @@
 //===----------------------------------------------------------------------===//
 
 #include "UncheckedOptionalAccessCheck.h"
+#include "../ClangTidyCheck.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/ASTMatchers/ASTMatchFinder.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h"
 #include "clang/Basic/SourceLocation.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Error.h"
 
+#include <optional>
+#include <utility>
+
+namespace clang::tidy {
+template <> struct OptionEnumMapping<dataflow::BoolModelKind> {
+  static llvm::ArrayRef<std::pair<dataflow::BoolModelKind, llvm::StringRef>>
+  getEnumMapping() {
+    static constexpr std::pair<dataflow::BoolModelKind, llvm::StringRef>
+        Mapping[] = {{dataflow::BoolModelKind::SAT, "SAT"},
+                     {dataflow::BoolModelKind::Simple, "Simple"}};
+    return {Mapping};
+  }
+};
+} // namespace clang::tidy
+
 namespace clang::tidy::bugprone {
 using ast_matchers::MatchFinder;
 using dataflow::UncheckedOptionalAccessDiagnoser;
@@ -24,6 +42,21 @@ using dataflow::UncheckedOptionalAccessModel;
 
 static constexpr StringRef FuncID = "fun";
 
+UncheckedOptionalAccessCheck::UncheckedOptionalAccessCheck(
+    StringRef Name, ClangTidyContext *Context)
+    : ClangTidyCheck(Name, Context),
+      ModelOptions{Options.get("IgnoreSmartPointerDereference", false),
+                   Options.get("IgnoreValueCalls", false)},
+      BoolModel(Options.get("BoolModel", dataflow::BoolModelKind::SAT)) {}
+
+void UncheckedOptionalAccessCheck::storeOptions(
+    ClangTidyOptions::OptionMap &Opts) {
+  Options.store(Opts, "IgnoreSmartPointerDereference",
+                ModelOptions.IgnoreSmartPointerDereference);
+  Options.store(Opts, "IgnoreValueCalls", ModelOptions.IgnoreValueCalls);
+  Options.store(Opts, "BoolModel", BoolModel);
+}
+
 void UncheckedOptionalAccessCheck::registerMatchers(MatchFinder *Finder) {
   using namespace ast_matchers;
 
@@ -57,13 +90,19 @@ void UncheckedOptionalAccessCheck::check(
   if (llvm::Expected<SmallVector<UncheckedOptionalAccessDiagnostic>> Diags =
           dataflow::diagnoseFunction<UncheckedOptionalAccessModel,
                                      UncheckedOptionalAccessDiagnostic>(
-              *FuncDecl, *Result.Context, Diagnoser))
+              *FuncDecl, *Result.Context, Diagnoser,
+              dataflow::kDefaultMaxSATIterations,
+              dataflow::kDefaultMaxBlockVisits,
+              {/*ContextSensitiveOpts=*/std::nullopt,
+               /*Logger=*/nullptr,
+               /*BoolModel=*/BoolModel})) {
     for (const UncheckedOptionalAccessDiagnostic &Diag : *Diags) {
       diag(Diag.Range.getBegin(), "unchecked access to optional value")
           << Diag.Range;
     }
-  else
+  } else {
     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..342c2c542207f8 100644
--- a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
+++ b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
@@ -11,6 +11,7 @@
 
 #include "../ClangTidyCheck.h"
 #include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h"
 
 namespace clang::tidy::bugprone {
@@ -23,23 +24,19 @@ namespace clang::tidy::bugprone {
 /// https://clang.llvm.org/extra/clang-tidy/checks/bugprone/unchecked-optional-access.html
 class UncheckedOptionalAccessCheck : public ClangTidyCheck {
 public:
-  UncheckedOptionalAccessCheck(StringRef Name, ClangTidyContext *Context)
-      : ClangTidyCheck(Name, Context),
-        ModelOptions{Options.get("IgnoreSmartPointerDereference", false),
-                     Options.get("IgnoreValueCalls", false)} {}
+  UncheckedOptionalAccessCheck(StringRef Name, ClangTidyContext *Context);
   void registerMatchers(ast_matchers::MatchFinder *Finder) override;
   void check(const ast_matchers::MatchFinder::MatchResult &Result) override;
   bool isLanguageVersionSupported(const LangOptions &LangOpts) const override {
     return LangOpts.CPlusPlus;
   }
-  void storeOptions(ClangTidyOptions::OptionMap &Opts) override {
-    Options.store(Opts, "IgnoreSmartPointerDereference",
-                  ModelOptions.IgnoreSmartPointerDereference);
-    Options.store(Opts, "IgnoreValueCalls", ModelOptions.IgnoreValueCalls);
-  }
+  void storeOptions(ClangTidyOptions::OptionMap &Opts) override;
 
 private:
   dataflow::UncheckedOptionalAccessModelOptions ModelOptions;
+  // Note: The boolean model is an option for the framework, not the checker
+  // model, so we keep separate from ModelOptions.
+  dataflow::BoolModelKind BoolModel;
 };
 
 } // namespace clang::tidy::bugprone
diff --git a/clang-tools-extra/docs/ReleaseNotes.md b/clang-tools-extra/docs/ReleaseNotes.md
index 4cd6b4b8a82eee..5632cb0b8ec48c 100644
--- a/clang-tools-extra/docs/ReleaseNotes.md
+++ b/clang-tools-extra/docs/ReleaseNotes.md
@@ -239,9 +239,15 @@ infrastructure are described first, followed by tool-specific sections.
   lambda closure types used as template arguments.
 
 - Improved {doc}`bugprone-unchecked-optional-access
-  <clang-tidy/checks/bugprone/unchecked-optional-access>` by fixing false
-  positives on `bsl::optional` and `bdlb::NullableValue` constructed from a
-  value or returned by `bsl::make_optional`.
+  <clang-tidy/checks/bugprone/unchecked-optional-access>` check:
+
+  - Fixed false positives on `bsl::optional` and `bdlb::NullableValue`
+    constructed from a value or returned by `bsl::make_optional`.
+
+  - Added the {option}`BoolModel` option to allow use of a "Simple" boolean
+    model that avoids relying on a SAT solver. Previously, only SAT was
+    available. This leads to faster analysis, but the trade-off is more false
+    positives (when has value checks involve correlated variables or ORs).
 
 - Improved {doc}`cppcoreguidelines-missing-std-forward
   <clang-tidy/checks/cppcoreguidelines/missing-std-forward>` check by diagnosing
diff --git a/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md b/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md
index 5f784f100f2440..fae7ae73831b4d 100644
--- a/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md
+++ b/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md
@@ -157,6 +157,8 @@ void f(std::optional<int> opt) {
 }
 ```
 
+(correlated-branches)=
+
 ### Ensure that a value exists, then access the value in a correlated branch
 
 The check is aware of correlated branches in the code and can figure out
@@ -324,3 +326,15 @@ to `optional::value()`. Diagnostics for `operator*()` and
 intentionally rely on `value()` for defined, guarded access while still
 flagging UB-prone operator dereferences. Default is `false`.
 ```
+
+```{option} BoolModel
+Can be set to `SAT` (default) or `Simple`. The flow-sensitive analysis uses
+boolean formulas to model whether an `optional<T>` object has a value among
+other conditions. The analysis checks that, during accesses, the "has a value"
+state is provably true. The `SAT` model uses a SAT solver for this proof, so
+it can handle {ref}`branches with correlated conditions <correlated-branches>`
+and branches that contain ORs. The `Simple` model does a more limited tracking
+of boolean constants, and evaluates formulas without backtracking given
+assumptions at branch points, and does not introduce ORs for joins. As a result,
+the `Simple` model is faster but may have more false positives.
+```
diff --git a/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp b/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp
index 8bff66670f0da1..a0ea40f648880f 100644
--- a/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp
+++ b/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp
@@ -1,4 +1,9 @@
-// RUN: %check_clang_tidy %s bugprone-unchecked-optional-access %t -- -- -I %S/Inputs/unchecked-optional-access
+// RUN: %check_clang_tidy %s bugprone-unchecked-optional-access %t -- -- \
+// RUN:   -I %S/Inputs/unchecked-optional-access
+// RUN: %check_clang_tidy %s bugprone-unchecked-optional-access %t -- \
+// RUN:   -config="{CheckOptions: \
+// RUN:            {bugprone-unchecked-optional-access.BoolModel: Simple}}" -- \
+// RUN:   -I %S/Inputs/unchecked-optional-access
 
 #include "absl/types/optional.h"
 #include "bde/types/bdlb_nullablevalue.h"
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
index e6efde091871fc..af499aa9e8e0a8 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
@@ -322,13 +322,14 @@ llvm::Expected<llvm::SmallVector<Diagnostic>>
 diagnoseFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx,
                  DiagnosisCallbacks<AnalysisT, Diagnostic> Diagnoser,
                  std::int64_t MaxSATIterations = kDefaultMaxSATIterations,
-                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits) {
+                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits,
+                 DataflowAnalysisContext::Options ContextOptions = {}) {
   llvm::Expected<AdornedCFG> Context = AdornedCFG::build(FuncDecl);
   if (!Context)
     return Context.takeError();
 
   auto Solver = std::make_unique<WatchedLiteralsSolver>(MaxSATIterations);
-  DataflowAnalysisContext AnalysisContext(*Solver);
+  DataflowAnalysisContext AnalysisContext(*Solver, ContextOptions);
   Environment Env(AnalysisContext, FuncDecl);
   AnalysisT Analysis = createAnalysis<AnalysisT>(ASTCtx, Env);
   llvm::SmallVector<Diagnostic> Diagnostics;
@@ -383,10 +384,11 @@ llvm::Expected<llvm::SmallVector<Diagnostic>>
 diagnoseFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx,
                  DiagnosisCallback<AnalysisT, Diagnostic> Diagnoser,
                  std::int64_t MaxSATIterations = kDefaultMaxSATIterations,
-                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits) {
+                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits,
+                 DataflowAnalysisContext::Options ContextOptions = {}) {
   DiagnosisCallbacks<AnalysisT, Diagnostic> Callbacks = {nullptr, Diagnoser};
   return diagnoseFunction(FuncDecl, ASTCtx, Callbacks, MaxSATIterations,
-                          MaxBlockVisits);
+                          MaxBlockVisits, ContextOptions);
 }
 
 /// Abstract base class for dataflow "models": reusable analysis components that

@llvmorg-github-actions

Copy link
Copy Markdown

@llvm/pr-subscribers-clang-analysis

Author: Jan Voung (jvoung)

Changes

Adds a checker option to select the Simple BoolModel (introduced in the framework in #231061). This gives users the choice of faster analysis (e.g., one way to address #69369), but requires "has value" checks to be more straightforward (no correlated branch conditions for example).


Full diff: https://github.com/llvm/llvm-project/pull/240848.diff

6 Files Affected:

  • (modified) clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp (+41-2)
  • (modified) clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h (+6-9)
  • (modified) clang-tools-extra/docs/ReleaseNotes.md (+9-3)
  • (modified) clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md (+14)
  • (modified) clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp (+6-1)
  • (modified) clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h (+6-4)
diff --git a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
index 09c86e7da94f31..351fcbbde85c1d 100644
--- a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
+++ b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp
@@ -7,15 +7,33 @@
 //===----------------------------------------------------------------------===//
 
 #include "UncheckedOptionalAccessCheck.h"
+#include "../ClangTidyCheck.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/ASTMatchers/ASTMatchFinder.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h"
 #include "clang/Basic/SourceLocation.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Error.h"
 
+#include <optional>
+#include <utility>
+
+namespace clang::tidy {
+template <> struct OptionEnumMapping<dataflow::BoolModelKind> {
+  static llvm::ArrayRef<std::pair<dataflow::BoolModelKind, llvm::StringRef>>
+  getEnumMapping() {
+    static constexpr std::pair<dataflow::BoolModelKind, llvm::StringRef>
+        Mapping[] = {{dataflow::BoolModelKind::SAT, "SAT"},
+                     {dataflow::BoolModelKind::Simple, "Simple"}};
+    return {Mapping};
+  }
+};
+} // namespace clang::tidy
+
 namespace clang::tidy::bugprone {
 using ast_matchers::MatchFinder;
 using dataflow::UncheckedOptionalAccessDiagnoser;
@@ -24,6 +42,21 @@ using dataflow::UncheckedOptionalAccessModel;
 
 static constexpr StringRef FuncID = "fun";
 
+UncheckedOptionalAccessCheck::UncheckedOptionalAccessCheck(
+    StringRef Name, ClangTidyContext *Context)
+    : ClangTidyCheck(Name, Context),
+      ModelOptions{Options.get("IgnoreSmartPointerDereference", false),
+                   Options.get("IgnoreValueCalls", false)},
+      BoolModel(Options.get("BoolModel", dataflow::BoolModelKind::SAT)) {}
+
+void UncheckedOptionalAccessCheck::storeOptions(
+    ClangTidyOptions::OptionMap &Opts) {
+  Options.store(Opts, "IgnoreSmartPointerDereference",
+                ModelOptions.IgnoreSmartPointerDereference);
+  Options.store(Opts, "IgnoreValueCalls", ModelOptions.IgnoreValueCalls);
+  Options.store(Opts, "BoolModel", BoolModel);
+}
+
 void UncheckedOptionalAccessCheck::registerMatchers(MatchFinder *Finder) {
   using namespace ast_matchers;
 
@@ -57,13 +90,19 @@ void UncheckedOptionalAccessCheck::check(
   if (llvm::Expected<SmallVector<UncheckedOptionalAccessDiagnostic>> Diags =
           dataflow::diagnoseFunction<UncheckedOptionalAccessModel,
                                      UncheckedOptionalAccessDiagnostic>(
-              *FuncDecl, *Result.Context, Diagnoser))
+              *FuncDecl, *Result.Context, Diagnoser,
+              dataflow::kDefaultMaxSATIterations,
+              dataflow::kDefaultMaxBlockVisits,
+              {/*ContextSensitiveOpts=*/std::nullopt,
+               /*Logger=*/nullptr,
+               /*BoolModel=*/BoolModel})) {
     for (const UncheckedOptionalAccessDiagnostic &Diag : *Diags) {
       diag(Diag.Range.getBegin(), "unchecked access to optional value")
           << Diag.Range;
     }
-  else
+  } else {
     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..342c2c542207f8 100644
--- a/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
+++ b/clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h
@@ -11,6 +11,7 @@
 
 #include "../ClangTidyCheck.h"
 #include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h"
 
 namespace clang::tidy::bugprone {
@@ -23,23 +24,19 @@ namespace clang::tidy::bugprone {
 /// https://clang.llvm.org/extra/clang-tidy/checks/bugprone/unchecked-optional-access.html
 class UncheckedOptionalAccessCheck : public ClangTidyCheck {
 public:
-  UncheckedOptionalAccessCheck(StringRef Name, ClangTidyContext *Context)
-      : ClangTidyCheck(Name, Context),
-        ModelOptions{Options.get("IgnoreSmartPointerDereference", false),
-                     Options.get("IgnoreValueCalls", false)} {}
+  UncheckedOptionalAccessCheck(StringRef Name, ClangTidyContext *Context);
   void registerMatchers(ast_matchers::MatchFinder *Finder) override;
   void check(const ast_matchers::MatchFinder::MatchResult &Result) override;
   bool isLanguageVersionSupported(const LangOptions &LangOpts) const override {
     return LangOpts.CPlusPlus;
   }
-  void storeOptions(ClangTidyOptions::OptionMap &Opts) override {
-    Options.store(Opts, "IgnoreSmartPointerDereference",
-                  ModelOptions.IgnoreSmartPointerDereference);
-    Options.store(Opts, "IgnoreValueCalls", ModelOptions.IgnoreValueCalls);
-  }
+  void storeOptions(ClangTidyOptions::OptionMap &Opts) override;
 
 private:
   dataflow::UncheckedOptionalAccessModelOptions ModelOptions;
+  // Note: The boolean model is an option for the framework, not the checker
+  // model, so we keep separate from ModelOptions.
+  dataflow::BoolModelKind BoolModel;
 };
 
 } // namespace clang::tidy::bugprone
diff --git a/clang-tools-extra/docs/ReleaseNotes.md b/clang-tools-extra/docs/ReleaseNotes.md
index 4cd6b4b8a82eee..5632cb0b8ec48c 100644
--- a/clang-tools-extra/docs/ReleaseNotes.md
+++ b/clang-tools-extra/docs/ReleaseNotes.md
@@ -239,9 +239,15 @@ infrastructure are described first, followed by tool-specific sections.
   lambda closure types used as template arguments.
 
 - Improved {doc}`bugprone-unchecked-optional-access
-  <clang-tidy/checks/bugprone/unchecked-optional-access>` by fixing false
-  positives on `bsl::optional` and `bdlb::NullableValue` constructed from a
-  value or returned by `bsl::make_optional`.
+  <clang-tidy/checks/bugprone/unchecked-optional-access>` check:
+
+  - Fixed false positives on `bsl::optional` and `bdlb::NullableValue`
+    constructed from a value or returned by `bsl::make_optional`.
+
+  - Added the {option}`BoolModel` option to allow use of a "Simple" boolean
+    model that avoids relying on a SAT solver. Previously, only SAT was
+    available. This leads to faster analysis, but the trade-off is more false
+    positives (when has value checks involve correlated variables or ORs).
 
 - Improved {doc}`cppcoreguidelines-missing-std-forward
   <clang-tidy/checks/cppcoreguidelines/missing-std-forward>` check by diagnosing
diff --git a/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md b/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md
index 5f784f100f2440..fae7ae73831b4d 100644
--- a/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md
+++ b/clang-tools-extra/docs/clang-tidy/checks/bugprone/unchecked-optional-access.md
@@ -157,6 +157,8 @@ void f(std::optional<int> opt) {
 }
 ```
 
+(correlated-branches)=
+
 ### Ensure that a value exists, then access the value in a correlated branch
 
 The check is aware of correlated branches in the code and can figure out
@@ -324,3 +326,15 @@ to `optional::value()`. Diagnostics for `operator*()` and
 intentionally rely on `value()` for defined, guarded access while still
 flagging UB-prone operator dereferences. Default is `false`.
 ```
+
+```{option} BoolModel
+Can be set to `SAT` (default) or `Simple`. The flow-sensitive analysis uses
+boolean formulas to model whether an `optional<T>` object has a value among
+other conditions. The analysis checks that, during accesses, the "has a value"
+state is provably true. The `SAT` model uses a SAT solver for this proof, so
+it can handle {ref}`branches with correlated conditions <correlated-branches>`
+and branches that contain ORs. The `Simple` model does a more limited tracking
+of boolean constants, and evaluates formulas without backtracking given
+assumptions at branch points, and does not introduce ORs for joins. As a result,
+the `Simple` model is faster but may have more false positives.
+```
diff --git a/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp b/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp
index 8bff66670f0da1..a0ea40f648880f 100644
--- a/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp
+++ b/clang-tools-extra/test/clang-tidy/checkers/bugprone/unchecked-optional-access.cpp
@@ -1,4 +1,9 @@
-// RUN: %check_clang_tidy %s bugprone-unchecked-optional-access %t -- -- -I %S/Inputs/unchecked-optional-access
+// RUN: %check_clang_tidy %s bugprone-unchecked-optional-access %t -- -- \
+// RUN:   -I %S/Inputs/unchecked-optional-access
+// RUN: %check_clang_tidy %s bugprone-unchecked-optional-access %t -- \
+// RUN:   -config="{CheckOptions: \
+// RUN:            {bugprone-unchecked-optional-access.BoolModel: Simple}}" -- \
+// RUN:   -I %S/Inputs/unchecked-optional-access
 
 #include "absl/types/optional.h"
 #include "bde/types/bdlb_nullablevalue.h"
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
index e6efde091871fc..af499aa9e8e0a8 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h
@@ -322,13 +322,14 @@ llvm::Expected<llvm::SmallVector<Diagnostic>>
 diagnoseFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx,
                  DiagnosisCallbacks<AnalysisT, Diagnostic> Diagnoser,
                  std::int64_t MaxSATIterations = kDefaultMaxSATIterations,
-                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits) {
+                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits,
+                 DataflowAnalysisContext::Options ContextOptions = {}) {
   llvm::Expected<AdornedCFG> Context = AdornedCFG::build(FuncDecl);
   if (!Context)
     return Context.takeError();
 
   auto Solver = std::make_unique<WatchedLiteralsSolver>(MaxSATIterations);
-  DataflowAnalysisContext AnalysisContext(*Solver);
+  DataflowAnalysisContext AnalysisContext(*Solver, ContextOptions);
   Environment Env(AnalysisContext, FuncDecl);
   AnalysisT Analysis = createAnalysis<AnalysisT>(ASTCtx, Env);
   llvm::SmallVector<Diagnostic> Diagnostics;
@@ -383,10 +384,11 @@ llvm::Expected<llvm::SmallVector<Diagnostic>>
 diagnoseFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx,
                  DiagnosisCallback<AnalysisT, Diagnostic> Diagnoser,
                  std::int64_t MaxSATIterations = kDefaultMaxSATIterations,
-                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits) {
+                 std::int32_t MaxBlockVisits = kDefaultMaxBlockVisits,
+                 DataflowAnalysisContext::Options ContextOptions = {}) {
   DiagnosisCallbacks<AnalysisT, Diagnostic> Callbacks = {nullptr, Diagnoser};
   return diagnoseFunction(FuncDecl, ASTCtx, Callbacks, MaxSATIterations,
-                          MaxBlockVisits);
+                          MaxBlockVisits, ContextOptions);
 }
 
 /// Abstract base class for dataflow "models": reusable analysis components that

and branches that contain ORs. The `Simple` model does a more limited tracking
of boolean constants, and evaluates formulas without backtracking given
assumptions at branch points, and does not introduce ORs for joins. As a result,
the `Simple` model is faster but may have more false positives.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add default value.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you clarify? The first sentence describes the default "Can be set to SAT (default) or Simple." so I think that is already there?

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi, in clang-tidy documentations we typically put default value at the end.

An example in other checks:

IgnoreCatchWithKeywords

This option can be used to ignore specific catch statements containing certain keywords. If a catch
statement body contains (case-insensitive) any of the keywords listed in this semicolon-separated
option, then the catch will be ignored, and no warning will be raised. Default value: [at]TODO;[at]FIXME.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah I see, missed that. Thanks!

Comment thread clang-tools-extra/docs/ReleaseNotes.md Resolved
flagging UB-prone operator dereferences. Default is `false`.
```

```{option} BoolModel

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe name this more verbose like BooleanSolverModel or BoolSolverModel or BooleanSolver. I'm thinking from a not-experienced user POV who will see BoolModel: Simple and this won't say much from config only.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point! Went with BoolSolverModel (it does affect the "solver" but also changes the join modeling)

Suggestions from EugeneZelenko

Co-authored-by: EugeneZelenko <eugene.zelenko@gmail.com>

private:
dataflow::UncheckedOptionalAccessModelOptions ModelOptions;
// Note: The boolean model is an option for the framework, not the checker

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// Note: The boolean model is an option for the framework, not the checker
// Note: The Boolean model is an option for the framework, not the checker

flagging UB-prone operator dereferences. Default is `false`.
```

```{option} BoolModel

@zeyi2 zeyi2 Nov 11, 2026 •

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems that the Option name in documentation was not updated in the lastest commit :)

Just a small reminder in case you forgot to update it.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oops yes, fixed.

jvoung and others added 2 commits November 11, 2026 02:24
Co-authored-by: Zeyi Xu <zeyi2@nekoarch.cc>

@vbvictor vbvictor left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

@zeyi2 zeyi2 changed the title [clang-tidy] For bugprone-unchecked-optional-access add simple BoolModel option [clang-tidy] For bugprone-unchecked-optional-access add simple BoolSolverModel option Nov 11, 2026
@jvoung
jvoung merged commit 85a7e59 into llvm:main Nov 11, 2026
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

clang:analysis clang:dataflow Clang Dataflow Analysis framework - https://clang.llvm.org/docs/DataFlowAnalysisIntro.html clang-tidy clang-tools-extra

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants