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

[Dmitri Gribenko via cfe-commits]

Author: Wei Yi Tee
Date: 2022-06-25T00:10:35+02:00
New Revision: 0f65a3e610051fc319372eea647fb50f60b2b21c

URL: https://github.com/llvm/llvm-project/commit/0f65a3e610051fc319372eea647fb50f60b2b21c
DIFF: https://github.com/llvm/llvm-project/commit/0f65a3e610051fc319372eea647fb50f60b2b21c.diff

LOG: [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

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 8a1fc9745b21..6011584f2006 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -203,6 +203,11 @@ class DataflowAnalysisContext {
   /// 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 57c8750a67e6..475eeef53737 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 1ff7cf1dce9e..1f0116cdbf2e 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