[clang][dataflow] Add explicit "AST" nodes for implications and iff

Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugaring makes
debug output (Environment::dump()) less readable than it could be.
Therefore, it makes sense to keep the sugared representation of a
boolean formula, and desugar it in the solver.

Reviewed By: sgatev, xazax.hun, wyt

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

diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index abc3183..b3e725a 100644 (file)
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -340,6 +340,10 @@ private:
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
       DisjunctionVals;
   llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
+      ImplicationVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
+      BiconditionalVals;
 
   // Flow conditions are tracked symbolically: each unique flow condition is
   // associated with a fresh symbolic variable (token), bound to the clause that

diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h
index 70348f8..c63799f 100644 (file)
--- a/clang/include/clang/Analysis/FlowSensitive/Value.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Value.h
@@ -37,12 +37,13 @@ public:
     Pointer,
     Struct,
 
-    // Synthetic boolean values are either atomic values or composites that
-    // represent conjunctions, disjunctions, and negations.
+    // Synthetic boolean values are either atomic values or logical connectives.
     AtomicBool,
     Conjunction,
     Disjunction,
-    Negation
+    Negation,
+    Implication,
+    Biconditional,
   };
 
   explicit Value(Kind ValKind) : ValKind(ValKind) {}
@@ -84,7 +85,9 @@ public:
     return Val->getKind() == Kind::AtomicBool ||
            Val->getKind() == Kind::Conjunction ||
            Val->getKind() == Kind::Disjunction ||
-           Val->getKind() == Kind::Negation;
+           Val->getKind() == Kind::Negation ||
+           Val->getKind() == Kind::Implication ||
+           Val->getKind() == Kind::Biconditional;
   }
 };
 
@@ -162,6 +165,54 @@ private:
   BoolValue &SubVal;
 };
 
+/// Models a boolean implication.
+///
+/// Equivalent to `!LHS v RHS`.
+class ImplicationValue : public BoolValue {
+public:
+  explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
+      : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal),
+        RightSubVal(RightSubVal) {}
+
+  static bool classof(const Value *Val) {
+    return Val->getKind() == Kind::Implication;
+  }
+
+  /// Returns the left sub-value of the implication.
+  BoolValue &getLeftSubValue() const { return LeftSubVal; }
+
+  /// Returns the right sub-value of the implication.
+  BoolValue &getRightSubValue() const { return RightSubVal; }
+
+private:
+  BoolValue &LeftSubVal;
+  BoolValue &RightSubVal;
+};
+
+/// Models a boolean biconditional.
+///
+/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`.
+class BiconditionalValue : public BoolValue {
+public:
+  explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
+      : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal),
+        RightSubVal(RightSubVal) {}
+
+  static bool classof(const Value *Val) {
+    return Val->getKind() == Kind::Biconditional;
+  }
+
+  /// Returns the left sub-value of the biconditional.
+  BoolValue &getLeftSubValue() const { return LeftSubVal; }
+
+  /// Returns the right sub-value of the biconditional.
+  BoolValue &getRightSubValue() const { return RightSubVal; }
+
+private:
+  BoolValue &LeftSubVal;
+  BoolValue &RightSubVal;
+};
+
 /// Models an integer.
 class IntegerValue : public Value {
 public:

diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 8f2296d..216f41b 100644 (file)
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -113,16 +113,27 @@ BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) {
 
 BoolValue &DataflowAnalysisContext::getOrCreateImplication(BoolValue &LHS,
                                                            BoolValue &RHS) {
-  return &LHS == &RHS ? getBoolLiteralValue(true)
-                      : getOrCreateDisjunction(getOrCreateNegation(LHS), RHS);
+  if (&LHS == &RHS)
+    return getBoolLiteralValue(true);
+
+  auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<ImplicationValue>(LHS, RHS));
+  return *Res.first->second;
 }
 
 BoolValue &DataflowAnalysisContext::getOrCreateIff(BoolValue &LHS,
                                                    BoolValue &RHS) {
-  return &LHS == &RHS
-             ? getBoolLiteralValue(true)
-             : getOrCreateConjunction(getOrCreateImplication(LHS, RHS),
-                                      getOrCreateImplication(RHS, LHS));
+  if (&LHS == &RHS)
+    return getBoolLiteralValue(true);
+
+  auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                           nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<BiconditionalValue>(LHS, RHS));
+  return *Res.first->second;
 }
 
 AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
@@ -258,6 +269,24 @@ BoolValue &DataflowAnalysisContext::substituteBoolValue(
     Result = &getOrCreateConjunction(LeftSub, RightSub);
     break;
   }
+  case Value::Kind::Implication: {
+    auto &IV = *cast<ImplicationValue>(&Val);
+    auto &LeftSub =
+        substituteBoolValue(IV.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolValue(IV.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateImplication(LeftSub, RightSub);
+    break;
+  }
+  case Value::Kind::Biconditional: {
+    auto &BV = *cast<BiconditionalValue>(&Val);
+    auto &LeftSub =
+        substituteBoolValue(BV.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolValue(BV.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateIff(LeftSub, RightSub);
+    break;
+  }
   default:
     llvm_unreachable("Unhandled Value Kind");
   }

diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index 309ff06..714ad08 100644 (file)
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -96,6 +96,20 @@ public:
       S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
       break;
     }
+    case Value::Kind::Implication: {
+      auto &IV = cast<ImplicationValue>(B);
+      auto L = debugString(IV.getLeftSubValue(), Depth + 1);
+      auto R = debugString(IV.getRightSubValue(), Depth + 1);
+      S = formatv("(=>\n{0}\n{1})", L, R);
+      break;
+    }
+    case Value::Kind::Biconditional: {
+      auto &BV = cast<BiconditionalValue>(B);
+      auto L = debugString(BV.getLeftSubValue(), Depth + 1);
+      auto R = debugString(BV.getRightSubValue(), Depth + 1);
+      S = formatv("(=\n{0}\n{1})", L, R);
+      break;
+    }
     default:
       llvm_unreachable("Unhandled value kind");
     }

diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index b081543..cd1fd70 100644 (file)
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -221,6 +221,18 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
         UnprocessedSubVals.push(&N->getSubVal());
         break;
       }
+      case Value::Kind::Implication: {
+        auto *I = cast<ImplicationValue>(Val);
+        UnprocessedSubVals.push(&I->getLeftSubValue());
+        UnprocessedSubVals.push(&I->getRightSubValue());
+        break;
+      }
+      case Value::Kind::Biconditional: {
+        auto *B = cast<BiconditionalValue>(Val);
+        UnprocessedSubVals.push(&B->getLeftSubValue());
+        UnprocessedSubVals.push(&B->getRightSubValue());
+        break;
+      }
       case Value::Kind::AtomicBool: {
         Atomics[Var] = cast<AtomicBoolValue>(Val);
         break;
@@ -320,6 +332,46 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
 
       // Visit the sub-values of `Val`.
       UnprocessedSubVals.push(&N->getSubVal());
+    } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&I->getRightSubValue());
+
+      // `X <=> (A => B)` is equivalent to
+      // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
+      // conjunctive normal form. Below we add each of the conjuncts of the
+      // latter expression to the result.
+      Formula.addClause(posLit(Var), posLit(LeftSubVar));
+      Formula.addClause(posLit(Var), negLit(RightSubVar));
+      Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
+
+      // Visit the sub-values of `Val`.
+      UnprocessedSubVals.push(&I->getLeftSubValue());
+      UnprocessedSubVals.push(&I->getRightSubValue());
+    } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&B->getRightSubValue());
+
+      if (LeftSubVar == RightSubVar) {
+        // `X <=> (A <=> A)` is equvalent to `X` which is already in
+        // conjunctive normal form. Below we add each of the conjuncts of the
+        // latter expression to the result.
+        Formula.addClause(posLit(Var));
+
+        // No need to visit the sub-values of `Val`.
+      } else {
+        // `X <=> (A <=> B)` is equivalent to
+        // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
+        // already in conjunctive normal form. Below we add each of the conjuncts
+        // of the latter expression to the result.
+        Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+        Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
+        Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&B->getLeftSubValue());
+        UnprocessedSubVals.push(&B->getRightSubValue());
+      }
     }
   }
 

diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 758b1a8..926e871 100644 (file)
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -304,7 +304,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsFalseUnchanged) {
 }
 #endif
 
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) {
   auto &X = Context.createAtomicBoolValue();
   auto &True = Context.getBoolLiteralValue(true);
   auto &False = Context.getBoolLiteralValue(false);
@@ -313,18 +313,18 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
   auto &FC = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC, X);
 
-  // If X is true in FC, FC = X must be true
+  // If X is true, FC is true
   auto &FCWithXTrue =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
 
-  // If X is false in FC, FC = X must be false
+  // If X is false, FC is false
   auto &FC1WithXFalse =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
 }
 
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingNegation) {
   auto &X = Context.createAtomicBoolValue();
   auto &True = Context.getBoolLiteralValue(true);
   auto &False = Context.getBoolLiteralValue(false);
@@ -333,18 +333,18 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
   auto &FC = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));
 
-  // If X is true in FC, FC = !X must be false
+  // If X is true, FC is false
   auto &FCWithXTrue =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
 
-  // If X is false in FC, FC = !X must be true
+  // If X is false, FC is true
   auto &FC1WithXFalse =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
 }
 
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingDisjunction) {
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
   auto &True = Context.getBoolLiteralValue(true);
@@ -354,18 +354,18 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
   auto &FC = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
 
-  // If X is true in FC, FC = X || Y must be true
+  // If X is true, FC is true
   auto &FCWithXTrue =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
 
-  // If X is false in FC, FC = X || Y is equivalent to evaluating Y
+  // If X is false, FC is equivalent to Y
   auto &FC1WithXFalse =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
 }
 
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingConjunction) {
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
   auto &True = Context.getBoolLiteralValue(true);
@@ -375,17 +375,82 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
   auto &FC = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
 
-  // If X is true in FC, FC = X && Y is equivalent to evaluating Y
+  // If X is true, FC is equivalent to Y
   auto &FCWithXTrue =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
 
-  // If X is false in FC, FC = X && Y must be false
+  // If X is false, FC is false
   auto &FCWithXFalse =
       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
 }
 
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingImplication) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = (X => Y)
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateImplication(X, Y));
+
+  // If X is true, FC is equivalent to Y
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
+
+  // If X is false, FC is true
+  auto &FC1WithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
+
+  // If Y is true, FC is true
+  auto &FCWithYTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, True));
+
+  // If Y is false, FC is equivalent to !X
+  auto &FCWithYFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,
+                                           Context.getOrCreateNegation(X)));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingBiconditional) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = (X <=> Y)
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateIff(X, Y));
+
+  // If X is true, FC is equivalent to Y
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
+
+  // If X is false, FC is equivalent to !Y
+  auto &FC1WithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse,
+                                           Context.getOrCreateNegation(Y)));
+
+  // If Y is true, FC is equivalent to X
+  auto &FCWithYTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, X));
+
+  // If Y is false, FC is equivalent to !X
+  auto &FCWithYFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,
+                                           Context.getOrCreateNegation(X)));
+}
+
 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
@@ -410,7 +475,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
       ForkedFC, {{&Y, &True}, {&Z, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
 
-  // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
+  // If any of X,Y,Z is false, ForkedFC is false
   auto &ForkedFCWithXFalse =
       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
   auto &ForkedFCWithYFalse =
@@ -439,8 +504,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
   auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
   Context.addFlowConditionConstraint(JoinedFC, Z);
 
-  // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
-  // to evaluating the remaining Z
+  // If any of X, Y is true, JoinedFC is equivalent to Z
   auto &JoinedFCWithXTrue =
       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
   auto &JoinedFCWithYTrue =
@@ -448,15 +512,14 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
 
-  // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
-  // evaluating the remaining disjunction (X || Y)
+  // If Z is true, JoinedFC is equivalent to (X || Y)
   auto &JoinedFCWithZTrue =
       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(
       JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
 
-  // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
-  // to evaluating the conjunction of the other value and Z
+  // If any of X, Y is false, JoinedFC is equivalent to the conjunction of the
+  // other value and Z
   auto &JoinedFCWithXFalse =
       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
   auto &JoinedFCWithYFalse =
@@ -466,7 +529,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
   EXPECT_TRUE(Context.equivalentBoolValues(
       JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
 
-  // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
+  // If Z is false, JoinedFC is false
   auto &JoinedFCWithZFalse =
       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));

diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index 6b9321b..6dded4b 100644 (file)
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -64,33 +64,24 @@ TEST(BoolValueDebugStringTest, Disjunction) {
 }
 
 TEST(BoolValueDebugStringTest, Implication) {
-  // B0 => B1, implemented as !B0 v B1
+  // B0 => B1
   ConstraintContext Ctx;
-  auto B = Ctx.disj(Ctx.neg(Ctx.atom()), Ctx.atom());
+  auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((or
-    (not
-        B0)
+  auto Expected = R"((=>
+    B0
     B1))";
   EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Iff) {
-  // B0 <=> B1, implemented as (!B0 v B1) ^ (B0 v !B1)
+  // B0 <=> B1
   ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto B = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
+  auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((and
-    (or
-        (not
-            B0)
-        B1)
-    (or
-        B0
-        (not
-            B1))))";
+  auto Expected = R"((=
+    B0
+    B1))";
   EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 

diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index 0c50c19..1de1c3a 100644 (file)
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -206,6 +206,20 @@ TEST(SolverTest, DeepConflict) {
   expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
 }
 
+TEST(SolverTest, IffIsEquivalentToDNF) {
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto Y = Ctx.atom();
+  auto NotX = Ctx.neg(X);
+  auto NotY = Ctx.neg(Y);
+  auto XIffY = Ctx.iff(X, Y);
+  auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY));
+  auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
+
+  // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
+  expectUnsatisfiable(solve({NotEquivalent}));
+}
+
 TEST(SolverTest, IffSameVars) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
@@ -297,6 +311,18 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
   expectUnsatisfiable(solve({XEqY, X, NotY}));
 }
 
+TEST(SolverTest, ImplicationIsEquivalentToDNF) {
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto Y = Ctx.atom();
+  auto XImpliesY = Ctx.impl(X, Y);
+  auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y);
+  auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
+
+  // !((X => Y) <=> (!X v Y))
+  expectUnsatisfiable(solve({NotEquivalent}));
+}
+
 TEST(SolverTest, ImplicationConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();

diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index debff04..8cb5008 100644 (file)
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -251,12 +251,16 @@ public:
 
   // Creates a boolean implication value.
   BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    return disj(neg(LeftSubVal), RightSubVal);
+    Vals.push_back(
+        std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
+    return Vals.back().get();
   }
 
   // Creates a boolean biconditional value.
   BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal));
+    Vals.push_back(
+        std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
+    return Vals.back().get();
   }
 
 private: