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
22namespace {
23
24using namespace clang;
25using namespace dataflow;
26
27using test::ConstraintContext;
28using test::parseFormulas;
29using testing::_;
30using testing::AnyOf;
31using testing::Pair;
32using testing::UnorderedElementsAre;
33
34constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
35constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
36
37// Checks if the conjunction of `Vals` is satisfiable and returns the
38// corresponding result.
39Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
40 return WatchedLiteralsSolver().solve(Vals);
41}
42
43MATCHER(unsat, "") {
44 return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
45}
46MATCHER_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
58TEST(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
67TEST(SolverTest, NegatedVar) {
68 ConstraintContext Ctx;
69 auto X = Ctx.atom();
70 auto NotX = Ctx.neg(Operand: X);
71
72 // !X
73 EXPECT_THAT(solve({NotX}),
74 sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
75}
76
77TEST(SolverTest, UnitConflict) {
78 ConstraintContext Ctx;
79 auto X = Ctx.atom();
80 auto NotX = Ctx.neg(Operand: X);
81
82 // X ^ !X
83 EXPECT_THAT(solve({X, NotX}), unsat());
84}
85
86TEST(SolverTest, DistinctVars) {
87 ConstraintContext Ctx;
88 auto X = Ctx.atom();
89 auto Y = Ctx.atom();
90 auto NotY = Ctx.neg(Operand: 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
98TEST(SolverTest, DoubleNegation) {
99 ConstraintContext Ctx;
100 auto X = Ctx.atom();
101 auto NotX = Ctx.neg(Operand: X);
102 auto NotNotX = Ctx.neg(Operand: NotX);
103
104 // !!X ^ !X
105 EXPECT_THAT(solve({NotNotX, NotX}), unsat());
106}
107
108TEST(SolverTest, NegatedDisjunction) {
109 ConstraintContext Ctx;
110 auto X = Ctx.atom();
111 auto Y = Ctx.atom();
112 auto XOrY = Ctx.disj(LHS: X, RHS: Y);
113 auto NotXOrY = Ctx.neg(Operand: XOrY);
114
115 // !(X v Y) ^ (X v Y)
116 EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
117}
118
119TEST(SolverTest, NegatedConjunction) {
120 ConstraintContext Ctx;
121 auto X = Ctx.atom();
122 auto Y = Ctx.atom();
123 auto XAndY = Ctx.conj(LHS: X, RHS: Y);
124 auto NotXAndY = Ctx.neg(Operand: XAndY);
125
126 // !(X ^ Y) ^ (X ^ Y)
127 EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
128}
129
130TEST(SolverTest, DisjunctionSameVarWithNegation) {
131 ConstraintContext Ctx;
132 auto X = Ctx.atom();
133 auto NotX = Ctx.neg(Operand: X);
134 auto XOrNotX = Ctx.disj(LHS: X, RHS: NotX);
135
136 // X v !X
137 EXPECT_THAT(solve({XOrNotX}), sat(_));
138}
139
140TEST(SolverTest, DisjunctionSameVar) {
141 ConstraintContext Ctx;
142 auto X = Ctx.atom();
143 auto XOrX = Ctx.disj(LHS: X, RHS: X);
144
145 // X v X
146 EXPECT_THAT(solve({XOrX}), sat(_));
147}
148
149TEST(SolverTest, ConjunctionSameVarsConflict) {
150 ConstraintContext Ctx;
151 auto X = Ctx.atom();
152 auto NotX = Ctx.neg(Operand: X);
153 auto XAndNotX = Ctx.conj(LHS: X, RHS: NotX);
154
155 // X ^ !X
156 EXPECT_THAT(solve({XAndNotX}), unsat());
157}
158
159TEST(SolverTest, ConjunctionSameVar) {
160 ConstraintContext Ctx;
161 auto X = Ctx.atom();
162 auto XAndX = Ctx.conj(LHS: X, RHS: X);
163
164 // X ^ X
165 EXPECT_THAT(solve({XAndX}), sat(_));
166}
167
168TEST(SolverTest, PureVar) {
169 ConstraintContext Ctx;
170 auto X = Ctx.atom();
171 auto Y = Ctx.atom();
172 auto NotX = Ctx.neg(Operand: X);
173 auto NotXOrY = Ctx.disj(LHS: NotX, RHS: Y);
174 auto NotY = Ctx.neg(Operand: Y);
175 auto NotXOrNotY = Ctx.disj(LHS: NotX, RHS: 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
183TEST(SolverTest, MustAssumeVarIsFalse) {
184 ConstraintContext Ctx;
185 auto X = Ctx.atom();
186 auto Y = Ctx.atom();
187 auto XOrY = Ctx.disj(LHS: X, RHS: Y);
188 auto NotX = Ctx.neg(Operand: X);
189 auto NotXOrY = Ctx.disj(LHS: NotX, RHS: Y);
190 auto NotY = Ctx.neg(Operand: Y);
191 auto NotXOrNotY = Ctx.disj(LHS: NotX, RHS: 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
199TEST(SolverTest, DeepConflict) {
200 ConstraintContext Ctx;
201 auto X = Ctx.atom();
202 auto Y = Ctx.atom();
203 auto XOrY = Ctx.disj(LHS: X, RHS: Y);
204 auto NotX = Ctx.neg(Operand: X);
205 auto NotXOrY = Ctx.disj(LHS: NotX, RHS: Y);
206 auto NotY = Ctx.neg(Operand: Y);
207 auto NotXOrNotY = Ctx.disj(LHS: NotX, RHS: NotY);
208 auto XOrNotY = Ctx.disj(LHS: X, RHS: 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
214TEST(SolverTest, IffIsEquivalentToDNF) {
215 ConstraintContext Ctx;
216 auto X = Ctx.atom();
217 auto Y = Ctx.atom();
218 auto NotX = Ctx.neg(Operand: X);
219 auto NotY = Ctx.neg(Operand: Y);
220 auto XIffY = Ctx.iff(LHS: X, RHS: Y);
221 auto XIffYDNF = Ctx.disj(LHS: Ctx.conj(LHS: X, RHS: Y), RHS: Ctx.conj(LHS: NotX, RHS: NotY));
222 auto NotEquivalent = Ctx.neg(Operand: Ctx.iff(LHS: XIffY, RHS: XIffYDNF));
223
224 // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
225 EXPECT_THAT(solve({NotEquivalent}), unsat());
226}
227
228TEST(SolverTest, IffSameVars) {
229 ConstraintContext Ctx;
230 auto X = Ctx.atom();
231 auto XEqX = Ctx.iff(LHS: X, RHS: X);
232
233 // X <=> X
234 EXPECT_THAT(solve({XEqX}), sat(_));
235}
236
237TEST(SolverTest, IffDistinctVars) {
238 ConstraintContext Ctx;
239 auto X = Ctx.atom();
240 auto Y = Ctx.atom();
241 auto XEqY = Ctx.iff(LHS: X, RHS: 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
252TEST(SolverTest, IffWithUnits) {
253 ConstraintContext Ctx;
254 auto X = Ctx.atom();
255 auto Y = Ctx.atom();
256 auto XEqY = Ctx.iff(LHS: X, RHS: 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
264TEST(SolverTest, IffWithUnitsConflict) {
265 Arena A;
266 auto Constraints = parseFormulas(A, Lines: R"(
267 (V0 = V1)
268 V0
269 !V1
270 )");
271 EXPECT_THAT(solve(Constraints), unsat());
272}
273
274TEST(SolverTest, IffTransitiveConflict) {
275 Arena A;
276 auto Constraints = parseFormulas(A, Lines: R"(
277 (V0 = V1)
278 (V1 = V2)
279 V2
280 !V0
281 )");
282 EXPECT_THAT(solve(Constraints), unsat());
283}
284
285TEST(SolverTest, DeMorgan) {
286 Arena A;
287 auto Constraints = parseFormulas(A, Lines: R"(
288 (!(V0 | V1) = (!V0 & !V1))
289 (!(V2 & V3) = (!V2 | !V3))
290 )");
291 EXPECT_THAT(solve(Constraints), sat(_));
292}
293
294TEST(SolverTest, RespectsAdditionalConstraints) {
295 Arena A;
296 auto Constraints = parseFormulas(A, Lines: R"(
297 (V0 = V1)
298 V0
299 !V1
300 )");
301 EXPECT_THAT(solve(Constraints), unsat());
302}
303
304TEST(SolverTest, ImplicationIsEquivalentToDNF) {
305 Arena A;
306 auto Constraints = parseFormulas(A, Lines: R"(
307 !((V0 => V1) = (!V0 | V1))
308 )");
309 EXPECT_THAT(solve(Constraints), unsat());
310}
311
312TEST(SolverTest, ImplicationConflict) {
313 Arena A;
314 auto Constraints = parseFormulas(A, Lines: R"(
315 (V0 => V1)
316 (V0 & !V1)
317 )");
318 EXPECT_THAT(solve(Constraints), unsat());
319}
320
321TEST(SolverTest, ReachedLimitsReflectsTimeouts) {
322 Arena A;
323 auto Constraints = parseFormulas(A, Lines: 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
333TEST(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(LHS: last, RHS: Ctx.atom());
344 }
345 last = Ctx.conj(LHS: Ctx.neg(Operand: first), RHS: 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(Operand: first);
352 for (int i = 1; i < 10000; ++i) {
353 last = Ctx.conj(LHS: last, RHS: Ctx.neg(Operand: Ctx.atom()));
354 }
355 last = Ctx.conj(LHS: first, RHS: last);
356 ASSERT_EQ(solver.solve({last}).getStatus(),
357 Solver::Result::Status::Unsatisfiable);
358 EXPECT_FALSE(solver.reachedLimit());
359}
360
361} // namespace
362

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