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

`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

Reviewed By: gribozavr2, xazax.hun

Differential Revision: https://reviews.llvm.org/D128521

3 files changed, 75 insertions, 0 deletions

diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 8a1fc97..6011584 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -203,6 +203,11 @@ public:
   /// 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
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 57c8750..475eeef 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -137,6 +137,13 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
   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) {
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 1ff7cf1..1f0116c 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -213,4 +213,67 @@ TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
   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