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

[Dmitri Gribenko via cfe-commits]

Author: Dmitri Gribenko
Date: 2022-07-26T10:26:44+02:00
New Revision: 3281138aad80fcefc7f266c7e3b2e359d5dbc8da

URL: https://github.com/llvm/llvm-project/commit/3281138aad80fcefc7f266c7e3b2e359d5dbc8da
DIFF: https://github.com/llvm/llvm-project/commit/3281138aad80fcefc7f266c7e3b2e359d5dbc8da.diff

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

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.

Reviewed By: sgatev, ymandel, xazax.hun

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

Added: 
    

Modified: 
    clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
    clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

Removed: 
    


################################################################################
diff  --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index 6a3948bd1fea0..b081543ac1333 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -263,30 +263,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));
-
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&C->getLeftSubValue());
-      UnprocessedSubVals.push(&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).
+        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());
 

diff  --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index 3bb7acef383c1..0c50c19a1559a 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -120,7 +120,7 @@ TEST(SolverTest, NegatedConjunction) {
   expectUnsatisfiable(solve({NotXAndY, XAndY}));
 }
 
-TEST(SolverTest, DisjunctionSameVars) {
+TEST(SolverTest, DisjunctionSameVarWithNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
@@ -130,6 +130,15 @@ TEST(SolverTest, DisjunctionSameVars) {
   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();
@@ -140,6 +149,15 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
   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();