1 files changed, 92 insertions, 18 deletions

diff --git a/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index 6a3948bd1fea..cd1fd708a43a 100644
--- a/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/contrib/llvm-project/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;
@@ -263,30 +275,52 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
       const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
       const Variable RightSubVar = GetVar(&C->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(negLit(Var), posLit(LeftSubVar));
-      Formula.addClause(negLit(Var), posLit(RightSubVar));
-      Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+      if (LeftSubVar == RightSubVar) {
+        // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` 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), posLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
 
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&C->getLeftSubValue());
-      UnprocessedSubVals.push(&C->getRightSubValue());
+        // Visit a sub-value of `Val` (pick any, they are identical).
+        UnprocessedSubVals.push(&C->getLeftSubValue());
+      } else {
+        // `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(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(negLit(Var), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&C->getLeftSubValue());
+        UnprocessedSubVals.push(&C->getRightSubValue());
+      }
     } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
       const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
       const Variable RightSubVar = GetVar(&D->getRightSubValue());
 
-      // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X 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(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
-      Formula.addClause(posLit(Var), negLit(LeftSubVar));
-      Formula.addClause(posLit(Var), negLit(RightSubVar));
+      if (LeftSubVar == RightSubVar) {
+        // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` 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), posLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
 
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&D->getLeftSubValue());
-      UnprocessedSubVals.push(&D->getRightSubValue());
+        // Visit a sub-value of `Val` (pick any, they are identical).
+        UnprocessedSubVals.push(&D->getLeftSubValue());
+      } else {
+        // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X 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(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&D->getLeftSubValue());
+        UnprocessedSubVals.push(&D->getRightSubValue());
+      }
     } else if (auto *N = dyn_cast<NegationValue>(Val)) {
       const Variable SubVar = GetVar(&N->getSubVal());
 
@@ -298,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());
+      }
     }
   }