[clang] 3b29b8a - Expose DataflowAnalysisContext.querySolver().

[Dmitri Gribenko via cfe-commits]

Author: Samira Bazuzi
Date: 2023-07-01T00:15:45+02:00
New Revision: 3b29b8a2aba205b59163ba11c537fbfe25133181

URL: https://github.com/llvm/llvm-project/commit/3b29b8a2aba205b59163ba11c537fbfe25133181
DIFF: https://github.com/llvm/llvm-project/commit/3b29b8a2aba205b59163ba11c537fbfe25133181.diff

LOG: Expose DataflowAnalysisContext.querySolver().

This allows for use of the same solver used by the DAC for additional solving post-analysis and thus shared use of MaxIterations in WatchedLiteralsSolver.

Reviewed By: ymandel, gribozavr2, sammccall

Differential Revision: https://reviews.llvm.org/D153805

Added: 
    

Modified: 
    clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index eba42fc3418f68..735f2b2d85021c 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -175,6 +175,14 @@ class DataflowAnalysisContext {
 
   Arena &arena() { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
+
 private:
   friend class Environment;
 
@@ -204,13 +212,6 @@ class DataflowAnalysisContext {
       AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {