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

[gribozavr]

Summary

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.

[gribozavr]

Normalized more comments

[xazax.hun]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

332

I wonder why this simplification is done here only for BiconditionalValue. Other operations seem to not do these sorts of simplifications. Also, when would we take this branch? getOrCreateIff has a special case when both operands are the same.

[xazax.hun]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

332

Oh, looking at the other patch I see it mentioning desugaring. So can desugaring also introduce Biconditionals?

[gribozavr2]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

332

It is also necessary in the other cases due to the precondition of addClause(), I'm adding that special handling in a separate patch: https://reviews.llvm.org/D130522

We would take this branch when someone avoids using the DataflowContext API. So not extremely likely at the moment, but it is a latent bug that can be exposed by some future refactoring.

[xazax.hun]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

332

I see, thanks!

[sgatev]

clang/include/clang/Analysis/FlowSensitive/Value.h

40–41

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

110

I think <=> would be more natural.

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

201

Let's add a label: !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))

303

Let's add a label: !((X => Y) <=> (!X v Y))

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/Value.h

40–41

Applied.

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

110

Yeah, but = is what smtlib uses.

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

332

Marking done.

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

201

Added!

303

Added!

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

private:
 
   // Indices that are used to avoid recreating the same composite boolean
   // values.
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
       ConjunctionVals;
   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
   // defines the flow condition. Conceptually, each binding corresponds to an
   // "iff" of the form `FC <=> (C1 ^ C2 ^ ...)` where `FC` is a flow condition
   // token (an atomic boolean) and `Ci`s are the set of constraints in the flow
   // flow condition clause. The set of constraints (C1 ^ C2 ^ ...) are stored in
   // the `FlowConditionConstraints` map, keyed by the token of the flow

clang/include/clang/Analysis/FlowSensitive/Value.h

 class Value {
 public:
   enum class Kind {
     Integer,
     Reference,
     Pointer,
     Struct,
 
     // Synthetic boolean values are either atomic values or composites that
     // represent conjunctions, disjunctions, and negations.
     AtomicBool,
     Conjunction,
     Disjunction,
-    Negation
+    Negation,
+    Implication,
+    Biconditional,
   };
 
   explicit Value(Kind ValKind) : ValKind(ValKind) {}
 
   // Non-copyable because addresses of values are used as their identities
   // throughout framework and user code. The framework is responsible for
   // construction and destruction of values.
   Value(const Value &) = delete;

 class BoolValue : public Value {
 public:
   explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
 
   static bool classof(const Value *Val) {
     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;
   }
 };
 
 /// Models an atomic boolean.
 class AtomicBoolValue : public BoolValue {
 public:
   explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {}
 
public:
 
   /// Returns the sub-value of the negation.
   BoolValue &getSubVal() const { return SubVal; }
 
 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:
   explicit IntegerValue() : Value(Kind::Integer) {}
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::Integer;
   }

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) {
   auto Res = NegationVals.try_emplace(&Val, nullptr);
   if (Res.second)
     Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
   return *Res.first->second;
 }
 
 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() {
   return createAtomicBoolValue();
 }
 
 void DataflowAnalysisContext::addFlowConditionConstraint(
     AtomicBoolValue &Token, BoolValue &Constraint) {
case Value::Kind::Conjunction: {
     auto &Conjunct = *cast<ConjunctionValue>(&Val);
     auto &LeftSub =
         substituteBoolValue(Conjunct.getLeftSubValue(), SubstitutionsCache);
     auto &RightSub =
         substituteBoolValue(Conjunct.getRightSubValue(), SubstitutionsCache);
     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");
   }
   SubstitutionsCache[&Val] = Result;
   return *Result;
 }
 
 BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowCondition(

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

case Value::Kind::Disjunction: {
       S = formatv("(or\n{0}\n{1})", L, R);
       break;
     }
     case Value::Kind::Negation: {
       auto &N = cast<NegationValue>(B);
       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");
     }
     auto Indent = Depth * 4;
     return formatv("{0}", fmt_pad(S, Indent, 0));
   }
 
   std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) {

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

while (!UnprocessedSubVals.empty()) {
         UnprocessedSubVals.push(&D->getRightSubValue());
         break;
       }
       case Value::Kind::Negation: {
         auto *N = cast<NegationValue>(Val);
         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;
       }
       default:
         llvm_unreachable("buildBooleanFormula: unhandled value kind");
       }
     }
if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
       // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
       // conjunctive normal form. Below we add each of the conjuncts of the
       // latter expression to the result.
       Formula.addClause(negLit(Var), negLit(SubVar));
       Formula.addClause(posLit(Var), posLit(SubVar));
 
       // 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());
+      }
     }
   }
 
   return Formula;
 }
 
 class WatchedLiteralsSolverImpl {
   /// A boolean formula in conjunctive normal form that the solver will attempt

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsFalseUnchanged) {
   Context.addFlowConditionConstraint(FC, False);
 
   // `False` should never be substituted
   EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&False, &Other}}),
                "Do not substitute true/false boolean literals");
 }
 #endif
 
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) {
   auto &X = Context.createAtomicBoolValue();
   auto &True = Context.getBoolLiteralValue(true);
   auto &False = Context.getBoolLiteralValue(false);
 
   // FC = X
   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);
 
   // FC = !X
   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);
   auto &False = Context.getBoolLiteralValue(false);
 
   // FC = X || Y
   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);
   auto &False = Context.getBoolLiteralValue(false);
 
   // FC = X && Y
   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();
   auto &Z = Context.createAtomicBoolValue();
   auto &True = Context.getBoolLiteralValue(true);
   auto &False = Context.getBoolLiteralValue(false);
 
   // FC = X && Y
   auto &FC = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
   // ForkedFC = FC && Z = X && Y && Z
   auto &ForkedFC = Context.forkFlowCondition(FC);
   Context.addFlowConditionConstraint(ForkedFC, Z);
 
   // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
   // to evaluating the conjunction of the remaining values
   auto &ForkedFCWithZTrue =
       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
   EXPECT_TRUE(Context.equivalentBoolValues(
       ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
   auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
       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 =
       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
   auto &ForkedFCWithZFalse =
       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
   Context.addFlowConditionConstraint(FC1, X);
   // FC2 = Y
   auto &FC2 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, Y);
   // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
   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 =
       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
   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 =
       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
   EXPECT_TRUE(Context.equivalentBoolValues(
       JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
   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));
 }
 
 } // namespace

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

TEST(BoolValueDebugStringTest, Disjunction) {
 
   auto Expected = R"((or
     B0
     B1))";
   EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 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"((=
+    B1))";
   EXPECT_THAT(debugString(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Xor) {
   // (B0 ^ !B1) V (!B0 ^ B1)
   ConstraintContext Ctx;
   auto B0 = Ctx.atom();
   auto B1 = Ctx.atom();

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

TEST(SolverTest, DeepConflict) {
   auto NotY = Ctx.neg(Y);
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
   auto XOrNotY = Ctx.disj(X, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
   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));
+
+  expectUnsatisfiable(solve({NotEquivalent}));
+}
+
 TEST(SolverTest, IffSameVars) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto XEqX = Ctx.iff(X, X);
 
   // X <=> X
   expectSatisfiable(solve({XEqX}), _);
 }
TEST(SolverTest, RespectsAdditionalConstraints) {
   auto Y = Ctx.atom();
   auto XEqY = Ctx.iff(X, Y);
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X ^ !Y
   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));
+
+  expectUnsatisfiable(solve({NotEquivalent}));
+}
+
 TEST(SolverTest, ImplicationConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto *XImplY = Ctx.impl(X, Y);
   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
 
   // X => Y ^ X ^ !Y
   expectUnsatisfiable(solve({XImplY, XAndNotY}));
 }
 
 } // namespace

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

public:
   // Creates a boolean negation value.
   BoolValue *neg(BoolValue *SubVal) {
     Vals.push_back(std::make_unique<NegationValue>(*SubVal));
     return Vals.back().get();
   }
 
   // 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:
   std::vector<std::unique_ptr<BoolValue>> Vals;
 };
 
 } // namespace test
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_