384 lines · c
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-exception6//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 17namespace clang::dataflow::test {18 19namespace {20 21constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;22constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;23 24using testing::_;25using testing::AnyOf;26using testing::Pair;27using testing::UnorderedElementsAre;28 29} // namespace30 31/// Type-parameterized test for implementations of the `Solver` interface.32/// To use:33/// 1. Implement a specialization of `createSolverWithLowTimeout()` for the34/// solver you want to test.35/// 2. Instantiate the test suite for the solver you want to test using36/// `INSTANTIATE_TYPED_TEST_SUITE_P()`.37/// See WatchedLiteralsSolverTest.cpp for an example.38template <typename SolverT> class SolverTest : public ::testing::Test {39protected:40 // Checks if the conjunction of `Vals` is satisfiable and returns the41 // 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 50TYPED_TEST_SUITE_P(SolverTest);51 52MATCHER(unsat, "") {53 return arg.getStatus() == Solver::Result::Status::Unsatisfiable;54}55 56MATCHER_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 68TYPED_TEST_P(SolverTest, Var) {69 ConstraintContext Ctx;70 auto X = Ctx.atom();71 72 // X73 EXPECT_THAT(this->solve({X}),74 sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));75}76 77TYPED_TEST_P(SolverTest, NegatedVar) {78 ConstraintContext Ctx;79 auto X = Ctx.atom();80 auto NotX = Ctx.neg(X);81 82 // !X83 EXPECT_THAT(this->solve({NotX}),84 sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));85}86 87TYPED_TEST_P(SolverTest, UnitConflict) {88 ConstraintContext Ctx;89 auto X = Ctx.atom();90 auto NotX = Ctx.neg(X);91 92 // X ^ !X93 EXPECT_THAT(this->solve({X, NotX}), unsat());94}95 96TYPED_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 ^ !Y103 EXPECT_THAT(this->solve({X, NotY}),104 sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),105 Pair(Y->getAtom(), AssignedFalse))));106}107 108TYPED_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 ^ !X115 EXPECT_THAT(this->solve({NotNotX, NotX}), unsat());116}117 118TYPED_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 129TYPED_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 140TYPED_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 !X147 EXPECT_THAT(this->solve({XOrNotX}), sat(_));148}149 150TYPED_TEST_P(SolverTest, DisjunctionSameVar) {151 ConstraintContext Ctx;152 auto X = Ctx.atom();153 auto XOrX = Ctx.disj(X, X);154 155 // X v X156 EXPECT_THAT(this->solve({XOrX}), sat(_));157}158 159TYPED_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 ^ !X166 EXPECT_THAT(this->solve({XAndNotX}), unsat());167}168 169TYPED_TEST_P(SolverTest, ConjunctionSameVar) {170 ConstraintContext Ctx;171 auto X = Ctx.atom();172 auto XAndX = Ctx.conj(X, X);173 174 // X ^ X175 EXPECT_THAT(this->solve({XAndX}), sat(_));176}177 178TYPED_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 193TYPED_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 209TYPED_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 224TYPED_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 238TYPED_TEST_P(SolverTest, IffSameVars) {239 ConstraintContext Ctx;240 auto X = Ctx.atom();241 auto XEqX = Ctx.iff(X, X);242 243 // X <=> X244 EXPECT_THAT(this->solve({XEqX}), sat(_));245}246 247TYPED_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 <=> Y254 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 262TYPED_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 ^ Y269 EXPECT_THAT(this->solve({XEqY, X, Y}),270 sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),271 Pair(Y->getAtom(), AssignedTrue))));272}273 274TYPED_TEST_P(SolverTest, IffWithUnitsConflict) {275 Arena A;276 auto Constraints = parseFormulas(A, R"(277 (V0 = V1)278 V0279 !V1280 )");281 EXPECT_THAT(this->solve(Constraints), unsat());282}283 284TYPED_TEST_P(SolverTest, IffTransitiveConflict) {285 Arena A;286 auto Constraints = parseFormulas(A, R"(287 (V0 = V1)288 (V1 = V2)289 V2290 !V0291 )");292 EXPECT_THAT(this->solve(Constraints), unsat());293}294 295TYPED_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 304TYPED_TEST_P(SolverTest, RespectsAdditionalConstraints) {305 Arena A;306 auto Constraints = parseFormulas(A, R"(307 (V0 = V1)308 V0309 !V1310 )");311 EXPECT_THAT(this->solve(Constraints), unsat());312}313 314TYPED_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 322TYPED_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 331TYPED_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 343TYPED_TEST_P(SolverTest, SimpleButLargeContradiction) {344 // This test ensures that the solver takes a short-cut on known345 // contradictory inputs, without using max_iterations. At the time346 // this test is added, formulas that are easily recognized to be347 // 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 371REGISTER_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::test382 383#endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_384