clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

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