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(Operand: 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(Operand: 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(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 | |
108 | TYPED_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 | |
118 | TYPED_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 | |
129 | TYPED_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 | |
140 | TYPED_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 | |
150 | TYPED_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 | |
159 | TYPED_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 | |
169 | TYPED_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 | |
178 | TYPED_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 | |
193 | TYPED_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 | |
209 | TYPED_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 | |
224 | TYPED_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 | |
238 | TYPED_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 | |
247 | TYPED_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 | |
262 | TYPED_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 | |
274 | TYPED_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 | |
284 | TYPED_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 | |
295 | TYPED_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 | |
304 | TYPED_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 | |
314 | TYPED_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 | |
322 | TYPED_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 | |
331 | TYPED_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 | |
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(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 | |
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_ |
384 |
Definitions
- AssignedTrue
- AssignedFalse
- SolverTest
- solve
- unsat
- sat
- Var
- NegatedVar
- UnitConflict
- DistinctVars
- DoubleNegation
- NegatedDisjunction
- NegatedConjunction
- DisjunctionSameVarWithNegation
- DisjunctionSameVar
- ConjunctionSameVarsConflict
- ConjunctionSameVar
- PureVar
- MustAssumeVarIsFalse
- DeepConflict
- IffIsEquivalentToDNF
- IffSameVars
- IffDistinctVars
- IffWithUnits
- IffWithUnitsConflict
- IffTransitiveConflict
- DeMorgan
- RespectsAdditionalConstraints
- ImplicationIsEquivalentToDNF
- ImplicationConflict
- ReachedLimitsReflectsTimeouts
Learn to use CMake with our Intro Training
Find out more