[clang][dataflow] Implement functionality to compare if two boolean values are equivalent.

[wyt]

Summary

equivalentBoolValues compares equivalence between two booleans. The current implementation does not consider constraints imposed by flow conditions on the booleans and its subvalues.

Depends On D128520

[sgatev]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

140

This seems unrelated to flow conditions (is this intentional?) and a bit too specific for DataflowAnalysisContext. Perhaps we should expose the solver and let user code use it the way it needs to.

[wyt]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

140

This seems unrelated to flow conditions (is this intentional?) and a bit too specific for DataflowAnalysisContext. Perhaps we should expose the solver and let user code use it the way it needs to.

Yes, we noticed this. Unfortunately, creation and using of values is tightly tied to DataflowAnalysisContext currently, since the context is responsible for owning the values. @gribozavr2 and I were discussing about refactoring this logic out, some ideas we considered include

1. A class responsible for communicating with the solver, responsible for building input and processing output from the solver. The context and this class would have a circular dependency. The context relies on this class to interface with the solver, the class relies on the context to create and use values.
2. A further refactoring could be moving the ownership of Values into another object, e.g. a DataflowArena maybe. Objects which need Values would have this object as a field.

I chose to stick with this implementation for now and to consider the refactoring in a future patch so that pointer nullability analysis relying on buildAndSubstituteFlowCondition will not be blocked by this.

@gribozavr2: Please add if I missed something.
@all: Let me know your thoughts on this, and if you have any ideas as well.
Thanks!!

[wyt]

Rename createIff to getOrCreateIff based on change in parent patch.

[wyt]

Propagate change from parent patch.

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

public:
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` imply that `Val` is true.
   bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
 
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` are always true.
   bool flowConditionIsTautology(AtomicBoolValue &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.
+  bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
+
 private:
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
       AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

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 = {&getOrCreateNegation(Token)};
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
+bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
+                                                   BoolValue &Val2) {
+  llvm::DenseSet<BoolValue *> Constraints = {
+      &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
+  return isUnsatisfiable(Constraints);
+}
+
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
   auto ConstraintsIT = FlowConditionConstraints.find(&Token);

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
 
   // ... but we can prove A || !A is true.
   auto &FC5 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(
       FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1)));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
 }
 
+TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &Z = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // X == X
+  EXPECT_TRUE(Context.equivalentBoolValues(X, X));
+  // X != Y
+  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+
+  // !X != X
+  EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));
+  // !(!X) = X
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));
+
+  // (X || X) == X
+  EXPECT_TRUE(
+      Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));
+  // (X || Y) != X
+  EXPECT_FALSE(
+      Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));
+  // (X || True) == True
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      Context.getOrCreateDisjunction(X, True), True));
+  // (X || False) == X
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      Context.getOrCreateDisjunction(X, False), X));
+
+  // (X && X) == X
+  EXPECT_TRUE(
+      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X));
+  // (X && Y) != X
+  EXPECT_FALSE(
+      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X));
+  // (X && True) == X
+  EXPECT_TRUE(
+      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X));
+  // (X && False) == False
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      Context.getOrCreateConjunction(X, False), False));
+
+  // (X || Y) == (Y || X)
+  EXPECT_TRUE(
+      Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y),
+                                   Context.getOrCreateDisjunction(Y, X)));
+  // (X && Y) == (Y && X)
+  EXPECT_TRUE(
+      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y),
+                                   Context.getOrCreateConjunction(Y, X)));
+
+  // ((X || Y) || Z) == (X || (Y || Z))
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),
+      Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));
+  // ((X && Y) && Z) == (X && (Y && Z))
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),
+      Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
+}
+
 } // namespace