[clang][dataflow] Fix SAT solver crashes on `X ^ X` and `X v X`

[gribozavr]

Summary

BooleanFormula::addClause has an invariant that a clause has no duplicated
literals. When the solver was desugaring a formula into CNF clauses, it
could construct a clause with such duplicated literals in two cases.

[sgatev]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

273

Let's visit C->getLeftSubValue() here.

[gribozavr]

Actually visit a subexpression

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

while (!UnprocessedSubVals.empty()) {
     if (ProcessedSubVals[Var])
       continue;
     ProcessedSubVals[Var] = true;
 
     if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
       const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
       const Variable RightSubVar = GetVar(&C->getRightSubValue());
 
+      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 a sub-value of `Val` (pick any, they are identical).
+      } 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());
 
+      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 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());
 
       // `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));

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

TEST(SolverTest, NegatedConjunction) {
   auto Y = Ctx.atom();
   auto XAndY = Ctx.conj(X, Y);
   auto NotXAndY = Ctx.neg(XAndY);
 
   // !(X ^ Y) ^ (X ^ Y)
   expectUnsatisfiable(solve({NotXAndY, XAndY}));
 }
 
-TEST(SolverTest, DisjunctionSameVars) {
+TEST(SolverTest, DisjunctionSameVarWithNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto XOrNotX = Ctx.disj(X, NotX);
 
   // X v !X
   expectSatisfiable(solve({XOrNotX}), _);
 }
 
+TEST(SolverTest, DisjunctionSameVar) {
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto XOrX = Ctx.disj(X, X);
+
+  // X v X
+  expectSatisfiable(solve({XOrX}), _);
+}
+
 TEST(SolverTest, ConjunctionSameVarsConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto XAndNotX = Ctx.conj(X, NotX);
 
   // X ^ !X
   expectUnsatisfiable(solve({XAndNotX}));
 }
 
+TEST(SolverTest, ConjunctionSameVar) {
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto XAndX = Ctx.conj(X, X);
+
+  // X ^ X
+  expectSatisfiable(solve({XAndX}), _);
+}
+
 TEST(SolverTest, PureVar) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto NotXOrY = Ctx.disj(NotX, Y);
   auto NotY = Ctx.neg(Y);
   auto NotXOrNotY = Ctx.disj(NotX, NotY);