diff options
author | Dmitri Gribenko <gribozavr@gmail.com> | 2022-07-26 10:16:13 +0200 |
---|---|---|
committer | Dmitri Gribenko <gribozavr@gmail.com> | 2022-07-26 10:26:44 +0200 |
commit | 3281138aad80fcefc7f266c7e3b2e359d5dbc8da (patch) | |
tree | f80e2d4cc66c001c5e6a74809b4c69d45824b41c /clang/unittests | |
parent | a618d5e0dd5d6fee5d73e823dbf8301663be0b4f (diff) | |
download | llvm-3281138aad80fcefc7f266c7e3b2e359d5dbc8da.zip llvm-3281138aad80fcefc7f266c7e3b2e359d5dbc8da.tar.gz llvm-3281138aad80fcefc7f266c7e3b2e359d5dbc8da.tar.bz2 |
[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
Diffstat (limited to 'clang/unittests')
-rw-r--r-- | clang/unittests/Analysis/FlowSensitive/SolverTest.cpp | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index 3bb7ace..0c50c19 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(); |