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
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} // 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.
38template <typename SolverT> class SolverTest : public ::testing::Test {
39protected:
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
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 // X
73 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(Operand: X);
81
82 // !X
83 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(Operand: X);
91
92 // X ^ !X
93 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(Operand: 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
108TYPED_TEST_P(SolverTest, DoubleNegation) {
109 ConstraintContext Ctx;
110 auto X = Ctx.atom();
111 auto NotX = Ctx.neg(Operand: X);
112 auto NotNotX = Ctx.neg(Operand: NotX);
113
114 // !!X ^ !X
115 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(LHS: X, RHS: Y);
123 auto NotXOrY = Ctx.neg(Operand: 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(LHS: X, RHS: Y);
134 auto NotXAndY = Ctx.neg(Operand: 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(Operand: X);
144 auto XOrNotX = Ctx.disj(LHS: X, RHS: NotX);
145
146 // X v !X
147 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(LHS: X, RHS: X);
154
155 // X v X
156 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(Operand: X);
163 auto XAndNotX = Ctx.conj(LHS: X, RHS: NotX);
164
165 // X ^ !X
166 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(LHS: X, RHS: X);
173
174 // X ^ X
175 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(Operand: X);
183 auto NotXOrY = Ctx.disj(LHS: NotX, RHS: Y);
184 auto NotY = Ctx.neg(Operand: Y);
185 auto NotXOrNotY = Ctx.disj(LHS: NotX, RHS: 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(LHS: X, RHS: Y);
198 auto NotX = Ctx.neg(Operand: X);
199 auto NotXOrY = Ctx.disj(LHS: NotX, RHS: Y);
200 auto NotY = Ctx.neg(Operand: Y);
201 auto NotXOrNotY = Ctx.disj(LHS: NotX, RHS: 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(LHS: X, RHS: Y);
214 auto NotX = Ctx.neg(Operand: X);
215 auto NotXOrY = Ctx.disj(LHS: NotX, RHS: Y);
216 auto NotY = Ctx.neg(Operand: Y);
217 auto NotXOrNotY = Ctx.disj(LHS: NotX, RHS: NotY);
218 auto XOrNotY = Ctx.disj(LHS: X, RHS: 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(Operand: X);
229 auto NotY = Ctx.neg(Operand: Y);
230 auto XIffY = Ctx.iff(LHS: X, RHS: Y);
231 auto XIffYDNF = Ctx.disj(LHS: Ctx.conj(LHS: X, RHS: Y), RHS: Ctx.conj(LHS: NotX, RHS: NotY));
232 auto NotEquivalent = Ctx.neg(Operand: Ctx.iff(LHS: XIffY, RHS: 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(LHS: X, RHS: X);
242
243 // X <=> X
244 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(LHS: X, RHS: 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
262TYPED_TEST_P(SolverTest, IffWithUnits) {
263 ConstraintContext Ctx;
264 auto X = Ctx.atom();
265 auto Y = Ctx.atom();
266 auto XEqY = Ctx.iff(LHS: X, RHS: 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
274TYPED_TEST_P(SolverTest, IffWithUnitsConflict) {
275 Arena A;
276 auto Constraints = parseFormulas(A, Lines: R"(
277 (V0 = V1)
278 V0
279 !V1
280 )");
281 EXPECT_THAT(this->solve(Constraints), unsat());
282}
283
284TYPED_TEST_P(SolverTest, IffTransitiveConflict) {
285 Arena A;
286 auto Constraints = parseFormulas(A, Lines: R"(
287 (V0 = V1)
288 (V1 = V2)
289 V2
290 !V0
291 )");
292 EXPECT_THAT(this->solve(Constraints), unsat());
293}
294
295TYPED_TEST_P(SolverTest, DeMorgan) {
296 Arena A;
297 auto Constraints = parseFormulas(A, Lines: 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, Lines: R"(
307 (V0 = V1)
308 V0
309 !V1
310 )");
311 EXPECT_THAT(this->solve(Constraints), unsat());
312}
313
314TYPED_TEST_P(SolverTest, ImplicationIsEquivalentToDNF) {
315 Arena A;
316 auto Constraints = parseFormulas(A, Lines: 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, Lines: 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, Lines: 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 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(LHS: last, RHS: Ctx.atom());
354 }
355 last = Ctx.conj(LHS: Ctx.neg(Operand: first), RHS: 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(Operand: first);
362 for (int i = 1; i < 10000; ++i) {
363 last = Ctx.conj(LHS: last, RHS: Ctx.neg(Operand: Ctx.atom()));
364 }
365 last = Ctx.conj(LHS: first, RHS: 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::test
382
383#endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_
384

source code of clang/unittests/Analysis/FlowSensitive/SolverTest.h