Unverified Commit 3eed23d3 authored by martinboehme's avatar martinboehme Committed by GitHub
Browse files

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

It's only used in its own unit tests.
parent 0374bbba

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

+0 −4
Original line number Diff line number Diff line
@@ -133,10 +133,6 @@ public: 
  /// 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.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

+0 −9
Original line number Diff line number Diff line
@@ -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;

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

+0 −27
Original line number Diff line number Diff line
@@ -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());