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

[Dmitri Gribenko via cfe-commits]

Author: Wei Yi Tee
Date: 2022-06-25T00:05:43+02:00
New Revision: 42a7ddb428c999229491b0effbb1a4059149fba8

URL: https://github.com/llvm/llvm-project/commit/42a7ddb428c999229491b0effbb1a4059149fba8
DIFF: https://github.com/llvm/llvm-project/commit/42a7ddb428c999229491b0effbb1a4059149fba8.diff

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

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

Reviewed By: gribozavr2, xazax.hun

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

Added: 
    

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

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 9f89b2ff5b831..8a1fc9745b215 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -212,6 +212,19 @@ class DataflowAnalysisContext {
       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.

diff  --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 10e7df394f40f..57c8750a67e66 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -108,6 +108,13 @@ DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
   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
@@ -115,28 +122,19 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
   // 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(