[PATCH] D124943: [clang][dataflow] Add flowConditionIsTautology function

[Eric Li via Phabricator via cfe-commits]

li.zhe.hua created this revision.
li.zhe.hua added reviewers: ymandel, sgatev, xazax.hun.
Herald added subscribers: tschuett, steakhal, rnkovacs.
Herald added a project: All.
li.zhe.hua requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Provide a way for users to check if a flow condition is
unconditionally true.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D124943

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


Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -140,4 +140,43 @@
   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
 }
 
+TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
+  // Default flow condition with empty/no constraints is always true.
+  auto &FC1 = Context.makeFlowConditionToken();
+  EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
+
+  // Negation of empty constraints is never true.
+  auto &FC2 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC2,
+                                     Context.getOrCreateNegationValue(FC1));
+  EXPECT_FALSE(Context.flowConditionIsTautology(FC2));
+
+  // FC1 || !FC1 is always true.
+  EXPECT_TRUE(
+      Context.flowConditionIsTautology(Context.joinFlowConditions(FC1, FC2)));
+
+  // Literal `true` is always true.
+  auto &FC3 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(true));
+  EXPECT_TRUE(Context.flowConditionIsTautology(FC3));
+
+  // Literal `false` is never true.
+  auto &FC4 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC4, Context.getBoolLiteralValue(false));
+  EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
+
+  // We can't prove that an arbitrary bool A is always true...
+  auto &C1 = Context.createAtomicBoolValue();
+  auto &FC5 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC5, C1);
+  EXPECT_FALSE(Context.flowConditionIsTautology(FC5));
+
+  // ... but we can prove A || !A is true.
+  auto &FC6 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(
+      FC6, Context.getOrCreateDisjunctionValue(
+               C1, Context.getOrCreateNegationValue(C1)));
+  EXPECT_TRUE(Context.flowConditionIsTautology(FC6));
+}
+
 } // namespace
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -117,6 +117,19 @@
   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
 }
 
+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),
+      &getOrCreateNegationValue(getBoolLiteralValue(false)),
+      &getOrCreateNegationValue(Token),
+  };
+  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
+  return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+}
+
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -173,6 +173,10 @@
   /// identified by `Token` imply that `Val` is true.
   bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
 
+  /// Returns true if the constraints of the flow condition identified by
+  /// `Token` is always true.
+  bool flowConditionIsTautology(AtomicBoolValue &Token);
+
 private:
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D124943.427057.patch
Type: text/x-patch
Size: 3989 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220504/8e8af0af/attachment-0001.bin>