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(); _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits