[clang][dataflow] Refactor function that queries the solver for satisfiability checking.

[wyt]

Summary

Given a set of Constraints, querySolver adds common background information across queries (TrueVal is always true and FalseVal is always false) and passes the query to the solver.

checkUnsatisfiable is a simple wrapper around querySolver for checking that the solver returns an unsatisfiable result.

Depends On D128519

[gribozavr2]

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

224

[wyt]

Rename checkUnsatisfiable to isUnsatisfiable

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

private:
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
       AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
+  /// Returns the result of satisfiability checking on `Constraints`.
+  /// Possible return values are:
+  /// - `Satisfiable`: There exists a satisfying assignment for `Constraints`.
+  /// - `Unsatisfiable`: There is no satisfying assignment for `Constraints`.
+  /// - `TimedOut`: The solver gives up on finding a satisfying assignment.
+  Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+
+  /// Returns true if the solver is able to prove that there is no satisfying
+  /// assignment for `Constraints`
+  bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
+    return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+  }
+
   std::unique_ptr<Solver> S;
 
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
 
   // Maps from program declarations and statements to storage locations that are
   // assigned to them. These assignments are global (aggregated across all basic

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
   auto &Token = makeFlowConditionToken();
   FlowConditionDeps[&Token].insert(&FirstToken);
   FlowConditionDeps[&Token].insert(&SecondToken);
   addFlowConditionConstraint(Token,
                              getOrCreateDisjunction(FirstToken, SecondToken));
   return Token;
 }
 
+Solver::Result
+DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
+  Constraints.insert(&getBoolLiteralValue(true));
+  Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false)));
+  return S->solve(std::move(Constraints));
+}
+
 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
                                                    BoolValue &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
-  llvm::DenseSet<BoolValue *> Constraints = {
-      &Token,
-      &getBoolLiteralValue(true),
-      &getOrCreateNegation(getBoolLiteralValue(false)),
-      &getOrCreateNegation(Val),
-  };
+  llvm::DenseSet<BoolValue *> Constraints = {&Token, &getOrCreateNegation(Val)};
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
-  return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+  return isUnsatisfiable(std::move(Constraints));
 }
 
 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
-  llvm::DenseSet<BoolValue *> Constraints = {
-      &getBoolLiteralValue(true),
-      &getOrCreateNegation(getBoolLiteralValue(false)),
-      &getOrCreateNegation(Token),
-  };
+  llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
-  return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+  return isUnsatisfiable(std::move(Constraints));
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;