clang/unittests/Analysis/FlowSensitive/SolverTest.h

   1 //===--- SolverTest.h - Type-parameterized test for solvers ---------------===//
   2 //
   3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
   4 // See https://llvm.org/LICENSE.txt for license information.
   5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
   6 //
   7 //===----------------------------------------------------------------------===//
   8
   9 #ifndef LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_SOLVER_TEST_H_
  10 #define LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_SOLVER_TEST_H_
  11
  12 #include "TestingSupport.h"
  13 #include "clang/Analysis/FlowSensitive/Solver.h"
  14 #include "gmock/gmock.h"
  15 #include "gtest/gtest.h"
  16
  17 namespace clang::dataflow::test {
  18
  19 namespace {
  20
  21 constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
  22 constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
  23
  24 using testing::_;
  25 using testing::AnyOf;
  26 using testing::Pair;
  27 using testing::UnorderedElementsAre;
  28
  29 } // namespace
  30
  31 /// Type-parameterized test for implementations of the `Solver` interface.
  32 /// To use:
  33 /// 1.  Implement a specialization of `createSolverWithLowTimeout()` for the
  34 ///     solver you want to test.
  35 /// 2.  Instantiate the test suite for the solver you want to test using
  36 ///     `INSTANTIATE_TYPED_TEST_SUITE_P()`.
  37 /// See WatchedLiteralsSolverTest.cpp for an example.
  38 template <typename SolverT> class SolverTest : public ::testing::Test {
  39 protected:
  40   // Checks if the conjunction of `Vals` is satisfiable and returns the
  41   // corresponding result.
  42   Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
  43     return SolverT().solve(Vals);
  44   }
  45
  46   // Create a specialization for the solver type to test.
  47   SolverT createSolverWithLowTimeout();
  48 };
  49
  50 TYPED_TEST_SUITE_P(SolverTest);
  51
  52 MATCHER(unsat, "") {
  53   return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
  54 }
  55
  56 MATCHER_P(sat, SolutionMatcher,
  57           "is satisfiable, where solution " +
  58               (testing::DescribeMatcher<
  59                   llvm::DenseMap<Atom, Solver::Result::Assignment>>(
  60                   SolutionMatcher))) {
  61   if (arg.getStatus() != Solver::Result::Status::Satisfiable)
  62     return false;
  63   auto Solution = *arg.getSolution();
  64   return testing::ExplainMatchResult(SolutionMatcher, Solution,
  65                                      result_listener);
  66 }
  67
  68 TYPED_TEST_P(SolverTest, Var) {
  69   ConstraintContext Ctx;
  70   auto X = Ctx.atom();
  71
  72   // X
  73   EXPECT_THAT(this->solve({X}),
  74               sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
  75 }
  76
  77 TYPED_TEST_P(SolverTest, NegatedVar) {
  78   ConstraintContext Ctx;
  79   auto X = Ctx.atom();
  80   auto NotX = Ctx.neg(X);
  81
  82   // !X
  83   EXPECT_THAT(this->solve({NotX}),
  84               sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
  85 }
  86
  87 TYPED_TEST_P(SolverTest, UnitConflict) {
  88   ConstraintContext Ctx;
  89   auto X = Ctx.atom();
  90   auto NotX = Ctx.neg(X);
  91
  92   // X ^ !X
  93   EXPECT_THAT(this->solve({X, NotX}), unsat());
  94 }
  95
  96 TYPED_TEST_P(SolverTest, DistinctVars) {
  97   ConstraintContext Ctx;
  98   auto X = Ctx.atom();
  99   auto Y = Ctx.atom();
 100   auto NotY = Ctx.neg(Y);
 101
 102   // X ^ !Y
 103   EXPECT_THAT(this->solve({X, NotY}),
 104               sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
 105                                        Pair(Y->getAtom(), AssignedFalse))));
 106 }
 107
 108 TYPED_TEST_P(SolverTest, DoubleNegation) {
 109   ConstraintContext Ctx;
 110   auto X = Ctx.atom();
 111   auto NotX = Ctx.neg(X);
 112   auto NotNotX = Ctx.neg(NotX);
 113
 114   // !!X ^ !X
 115   EXPECT_THAT(this->solve({NotNotX, NotX}), unsat());
 116 }
 117
 118 TYPED_TEST_P(SolverTest, NegatedDisjunction) {
 119   ConstraintContext Ctx;
 120   auto X = Ctx.atom();
 121   auto Y = Ctx.atom();
 122   auto XOrY = Ctx.disj(X, Y);
 123   auto NotXOrY = Ctx.neg(XOrY);
 124
 125   // !(X v Y) ^ (X v Y)
 126   EXPECT_THAT(this->solve({NotXOrY, XOrY}), unsat());
 127 }
 128
 129 TYPED_TEST_P(SolverTest, NegatedConjunction) {
 130   ConstraintContext Ctx;
 131   auto X = Ctx.atom();
 132   auto Y = Ctx.atom();
 133   auto XAndY = Ctx.conj(X, Y);
 134   auto NotXAndY = Ctx.neg(XAndY);
 135
 136   // !(X ^ Y) ^ (X ^ Y)
 137   EXPECT_THAT(this->solve({NotXAndY, XAndY}), unsat());
 138 }
 139
 140 TYPED_TEST_P(SolverTest, DisjunctionSameVarWithNegation) {
 141   ConstraintContext Ctx;
 142   auto X = Ctx.atom();
 143   auto NotX = Ctx.neg(X);
 144   auto XOrNotX = Ctx.disj(X, NotX);
 145
 146   // X v !X
 147   EXPECT_THAT(this->solve({XOrNotX}), sat(_));
 148 }
 149
 150 TYPED_TEST_P(SolverTest, DisjunctionSameVar) {
 151   ConstraintContext Ctx;
 152   auto X = Ctx.atom();
 153   auto XOrX = Ctx.disj(X, X);
 154
 155   // X v X
 156   EXPECT_THAT(this->solve({XOrX}), sat(_));
 157 }
 158
 159 TYPED_TEST_P(SolverTest, ConjunctionSameVarsConflict) {
 160   ConstraintContext Ctx;
 161   auto X = Ctx.atom();
 162   auto NotX = Ctx.neg(X);
 163   auto XAndNotX = Ctx.conj(X, NotX);
 164
 165   // X ^ !X
 166   EXPECT_THAT(this->solve({XAndNotX}), unsat());
 167 }
 168
 169 TYPED_TEST_P(SolverTest, ConjunctionSameVar) {
 170   ConstraintContext Ctx;
 171   auto X = Ctx.atom();
 172   auto XAndX = Ctx.conj(X, X);
 173
 174   // X ^ X
 175   EXPECT_THAT(this->solve({XAndX}), sat(_));
 176 }
 177
 178 TYPED_TEST_P(SolverTest, PureVar) {
 179   ConstraintContext Ctx;
 180   auto X = Ctx.atom();
 181   auto Y = Ctx.atom();
 182   auto NotX = Ctx.neg(X);
 183   auto NotXOrY = Ctx.disj(NotX, Y);
 184   auto NotY = Ctx.neg(Y);
 185   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 186
 187   // (!X v Y) ^ (!X v !Y)
 188   EXPECT_THAT(this->solve({NotXOrY, NotXOrNotY}),
 189               sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
 190                                        Pair(Y->getAtom(), _))));
 191 }
 192
 193 TYPED_TEST_P(SolverTest, MustAssumeVarIsFalse) {
 194   ConstraintContext Ctx;
 195   auto X = Ctx.atom();
 196   auto Y = Ctx.atom();
 197   auto XOrY = Ctx.disj(X, Y);
 198   auto NotX = Ctx.neg(X);
 199   auto NotXOrY = Ctx.disj(NotX, Y);
 200   auto NotY = Ctx.neg(Y);
 201   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 202
 203   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
 204   EXPECT_THAT(this->solve({XOrY, NotXOrY, NotXOrNotY}),
 205               sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
 206                                        Pair(Y->getAtom(), AssignedTrue))));
 207 }
 208
 209 TYPED_TEST_P(SolverTest, DeepConflict) {
 210   ConstraintContext Ctx;
 211   auto X = Ctx.atom();
 212   auto Y = Ctx.atom();
 213   auto XOrY = Ctx.disj(X, Y);
 214   auto NotX = Ctx.neg(X);
 215   auto NotXOrY = Ctx.disj(NotX, Y);
 216   auto NotY = Ctx.neg(Y);
 217   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 218   auto XOrNotY = Ctx.disj(X, NotY);
 219
 220   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
 221   EXPECT_THAT(this->solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
 222 }
 223
 224 TYPED_TEST_P(SolverTest, IffIsEquivalentToDNF) {
 225   ConstraintContext Ctx;
 226   auto X = Ctx.atom();
 227   auto Y = Ctx.atom();
 228   auto NotX = Ctx.neg(X);
 229   auto NotY = Ctx.neg(Y);
 230   auto XIffY = Ctx.iff(X, Y);
 231   auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY));
 232   auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
 233
 234   // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
 235   EXPECT_THAT(this->solve({NotEquivalent}), unsat());
 236 }
 237
 238 TYPED_TEST_P(SolverTest, IffSameVars) {
 239   ConstraintContext Ctx;
 240   auto X = Ctx.atom();
 241   auto XEqX = Ctx.iff(X, X);
 242
 243   // X <=> X
 244   EXPECT_THAT(this->solve({XEqX}), sat(_));
 245 }
 246
 247 TYPED_TEST_P(SolverTest, IffDistinctVars) {
 248   ConstraintContext Ctx;
 249   auto X = Ctx.atom();
 250   auto Y = Ctx.atom();
 251   auto XEqY = Ctx.iff(X, Y);
 252
 253   // X <=> Y
 254   EXPECT_THAT(
 255       this->solve({XEqY}),
 256       sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
 257                                      Pair(Y->getAtom(), AssignedTrue)),
 258                 UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
 259                                      Pair(Y->getAtom(), AssignedFalse)))));
 260 }
 261
 262 TYPED_TEST_P(SolverTest, IffWithUnits) {
 263   ConstraintContext Ctx;
 264   auto X = Ctx.atom();
 265   auto Y = Ctx.atom();
 266   auto XEqY = Ctx.iff(X, Y);
 267
 268   // (X <=> Y) ^ X ^ Y
 269   EXPECT_THAT(this->solve({XEqY, X, Y}),
 270               sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
 271                                        Pair(Y->getAtom(), AssignedTrue))));
 272 }
 273
 274 TYPED_TEST_P(SolverTest, IffWithUnitsConflict) {
 275   Arena A;
 276   auto Constraints = parseFormulas(A, R"(
 277      (V0 = V1)
 278      V0
 279      !V1
 280   )");
 281   EXPECT_THAT(this->solve(Constraints), unsat());
 282 }
 283
 284 TYPED_TEST_P(SolverTest, IffTransitiveConflict) {
 285   Arena A;
 286   auto Constraints = parseFormulas(A, R"(
 287      (V0 = V1)
 288      (V1 = V2)
 289      V2
 290      !V0
 291   )");
 292   EXPECT_THAT(this->solve(Constraints), unsat());
 293 }
 294
 295 TYPED_TEST_P(SolverTest, DeMorgan) {
 296   Arena A;
 297   auto Constraints = parseFormulas(A, R"(
 298      (!(V0 | V1) = (!V0 & !V1))
 299      (!(V2 & V3) = (!V2 | !V3))
 300   )");
 301   EXPECT_THAT(this->solve(Constraints), sat(_));
 302 }
 303
 304 TYPED_TEST_P(SolverTest, RespectsAdditionalConstraints) {
 305   Arena A;
 306   auto Constraints = parseFormulas(A, R"(
 307      (V0 = V1)
 308      V0
 309      !V1
 310   )");
 311   EXPECT_THAT(this->solve(Constraints), unsat());
 312 }
 313
 314 TYPED_TEST_P(SolverTest, ImplicationIsEquivalentToDNF) {
 315   Arena A;
 316   auto Constraints = parseFormulas(A, R"(
 317      !((V0 => V1) = (!V0 | V1))
 318   )");
 319   EXPECT_THAT(this->solve(Constraints), unsat());
 320 }
 321
 322 TYPED_TEST_P(SolverTest, ImplicationConflict) {
 323   Arena A;
 324   auto Constraints = parseFormulas(A, R"(
 325      (V0 => V1)
 326      (V0 & !V1)
 327   )");
 328   EXPECT_THAT(this->solve(Constraints), unsat());
 329 }
 330
 331 TYPED_TEST_P(SolverTest, ReachedLimitsReflectsTimeouts) {
 332   Arena A;
 333   auto Constraints = parseFormulas(A, R"(
 334      (!(V0 | V1) = (!V0 & !V1))
 335      (!(V2 & V3) = (!V2 & !V3))
 336   )");
 337   TypeParam solver = this->createSolverWithLowTimeout();
 338   ASSERT_EQ(solver.solve(Constraints).getStatus(),
 339             Solver::Result::Status::TimedOut);
 340   EXPECT_TRUE(solver.reachedLimit());
 341 }
 342
 343 TYPED_TEST_P(SolverTest, SimpleButLargeContradiction) {
 344   // This test ensures that the solver takes a short-cut on known
 345   // contradictory inputs, without using max_iterations. At the time
 346   // this test is added, formulas that are easily recognized to be
 347   // contradictory at CNF construction time would lead to timeout.
 348   TypeParam solver = this->createSolverWithLowTimeout();
 349   ConstraintContext Ctx;
 350   auto first = Ctx.atom();
 351   auto last = first;
 352   for (int i = 1; i < 10000; ++i) {
 353     last = Ctx.conj(last, Ctx.atom());
 354   }
 355   last = Ctx.conj(Ctx.neg(first), last);
 356   ASSERT_EQ(solver.solve({last}).getStatus(),
 357             Solver::Result::Status::Unsatisfiable);
 358   EXPECT_FALSE(solver.reachedLimit());
 359
 360   first = Ctx.atom();
 361   last = Ctx.neg(first);
 362   for (int i = 1; i < 10000; ++i) {
 363     last = Ctx.conj(last, Ctx.neg(Ctx.atom()));
 364   }
 365   last = Ctx.conj(first, last);
 366   ASSERT_EQ(solver.solve({last}).getStatus(),
 367             Solver::Result::Status::Unsatisfiable);
 368   EXPECT_FALSE(solver.reachedLimit());
 369 }
 370
 371 REGISTER_TYPED_TEST_SUITE_P(
 372     SolverTest, Var, NegatedVar, UnitConflict, DistinctVars, DoubleNegation,
 373     NegatedDisjunction, NegatedConjunction, DisjunctionSameVarWithNegation,
 374     DisjunctionSameVar, ConjunctionSameVarsConflict, ConjunctionSameVar,
 375     PureVar, MustAssumeVarIsFalse, DeepConflict, IffIsEquivalentToDNF,
 376     IffSameVars, IffDistinctVars, IffWithUnits, IffWithUnitsConflict,
 377     IffTransitiveConflict, DeMorgan, RespectsAdditionalConstraints,
 378     ImplicationIsEquivalentToDNF, ImplicationConflict,
 379     ReachedLimitsReflectsTimeouts, SimpleButLargeContradiction);
 380
 381 } // namespace clang::dataflow::test
 382
 383 #endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_