[clang] 3eed23d - [clang][dataflow] Remove `DataflowAnalysisContext::flowConditionIsTautology()`. (#69601)

[via cfe-commits]

Author: martinboehme
Date: 2023-10-23T08:18:12+02:00
New Revision: 3eed23d31caab9f19a8fa142aa26ee970a2c60ea

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

LOG: [clang][dataflow] Remove `DataflowAnalysisContext::flowConditionIsTautology()`. (#69601)

It's only used in its own unit tests.

Added: 
    

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

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index c46109a02921e7f..a792c3f911b1dd0 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -133,10 +133,6 @@ class DataflowAnalysisContext {
   /// identified by `Token` imply that `Val` is true.
   bool flowConditionImplies(Atom Token, const Formula &);
 
-  /// Returns true if and only if the constraints of the flow condition
-  /// identified by `Token` are always true.
-  bool flowConditionIsTautology(Atom Token);
-
   /// Returns true if `Val1` is equivalent to `Val2`.
   /// Note: This function doesn't take into account constraints on `Val1` and
   /// `Val2` imposed by the flow condition.

diff  --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 9f6984e1cf8f233..6a1feb229d47b61 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -158,15 +158,6 @@ bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
-  // Returns true if and only if we cannot prove that the flow condition can
-  // ever be false.
-  llvm::SetVector<const Formula *> Constraints;
-  Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token)));
-  addTransitiveFlowConditionConstraints(Token, Constraints);
-  return isUnsatisfiable(std::move(Constraints));
-}
-
 bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
                                                  const Formula &Val2) {
   llvm::SetVector<const Formula *> Constraints;

diff  --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index fb7642c131e3190..88eb11045b9e9f9 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -99,33 +99,6 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
 }
 
-TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
-  // Fresh flow condition with empty/no constraints is always true.
-  Atom FC1 = A.makeFlowConditionToken();
-  EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
-
-  // Literal `true` is always true.
-  Atom FC2 = A.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
-  EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
-
-  // Literal `false` is never true.
-  Atom FC3 = A.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC3, A.makeLiteral(false));
-  EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
-
-  // We can't prove that an arbitrary bool A is always true...
-  auto &C1 = A.makeAtomRef(A.makeAtom());
-  Atom FC4 = A.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC4, C1);
-  EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
-
-  // ... but we can prove A || !A is true.
-  Atom FC5 = A.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
-  EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
-}
-
 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());