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

[weiyi via Phabricator via cfe-commits]

wyt created this revision.
Herald added subscribers: martong, tschuett, xazax.hun.
Herald added a project: All.
wyt requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

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 <https://reviews.llvm.org/D128519>


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D128520

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


Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -106,6 +106,13 @@
   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
@@ -113,28 +120,19 @@
   // 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 checkUnsatisfiable(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 checkUnsatisfiable(std::move(Constraints));
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -212,6 +212,19 @@
       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 checkUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
+    return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+  }
+
   std::unique_ptr<Solver> S;
 
   // Storage for the state of a program.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D128520.439716.patch
Type: text/x-patch
Size: 3548 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220624/874d754b/attachment.bin>