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/Solver.h"
13 #include "TestingSupport.h"
14 #include "clang/Analysis/FlowSensitive/Value.h"
15 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
16 #include "gmock/gmock.h"
17 #include "gtest/gtest.h"
18 
19 namespace {
20 
21 using namespace clang;
22 using namespace dataflow;
23 
24 using test::ConstraintContext;
25 using testing::_;
26 using testing::AnyOf;
27 using testing::Optional;
28 using testing::Pair;
29 using testing::UnorderedElementsAre;
30 
31 // Checks if the conjunction of `Vals` is satisfiable and returns the
32 // corresponding result.
33 Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
34   return WatchedLiteralsSolver().solve(std::move(Vals));
35 }
36 
37 void expectUnsatisfiable(Solver::Result Result) {
38   EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
39   EXPECT_FALSE(Result.getSolution().has_value());
40 }
41 
42 template <typename Matcher>
43 void expectSatisfiable(Solver::Result Result, Matcher Solution) {
44   EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
45   EXPECT_THAT(Result.getSolution(), Optional(Solution));
46 }
47 
48 TEST(SolverTest, Var) {
49   ConstraintContext Ctx;
50   auto X = Ctx.atom();
51 
52   // X
53   expectSatisfiable(
54       solve({X}),
55       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
56 }
57 
58 TEST(SolverTest, NegatedVar) {
59   ConstraintContext Ctx;
60   auto X = Ctx.atom();
61   auto NotX = Ctx.neg(X);
62 
63   // !X
64   expectSatisfiable(
65       solve({NotX}),
66       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
67 }
68 
69 TEST(SolverTest, UnitConflict) {
70   ConstraintContext Ctx;
71   auto X = Ctx.atom();
72   auto NotX = Ctx.neg(X);
73 
74   // X ^ !X
75   expectUnsatisfiable(solve({X, NotX}));
76 }
77 
78 TEST(SolverTest, DistinctVars) {
79   ConstraintContext Ctx;
80   auto X = Ctx.atom();
81   auto Y = Ctx.atom();
82   auto NotY = Ctx.neg(Y);
83 
84   // X ^ !Y
85   expectSatisfiable(
86       solve({X, NotY}),
87       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
88                            Pair(Y, Solver::Result::Assignment::AssignedFalse)));
89 }
90 
91 TEST(SolverTest, DoubleNegation) {
92   ConstraintContext Ctx;
93   auto X = Ctx.atom();
94   auto NotX = Ctx.neg(X);
95   auto NotNotX = Ctx.neg(NotX);
96 
97   // !!X ^ !X
98   expectUnsatisfiable(solve({NotNotX, NotX}));
99 }
100 
101 TEST(SolverTest, NegatedDisjunction) {
102   ConstraintContext Ctx;
103   auto X = Ctx.atom();
104   auto Y = Ctx.atom();
105   auto XOrY = Ctx.disj(X, Y);
106   auto NotXOrY = Ctx.neg(XOrY);
107 
108   // !(X v Y) ^ (X v Y)
109   expectUnsatisfiable(solve({NotXOrY, XOrY}));
110 }
111 
112 TEST(SolverTest, NegatedConjunction) {
113   ConstraintContext Ctx;
114   auto X = Ctx.atom();
115   auto Y = Ctx.atom();
116   auto XAndY = Ctx.conj(X, Y);
117   auto NotXAndY = Ctx.neg(XAndY);
118 
119   // !(X ^ Y) ^ (X ^ Y)
120   expectUnsatisfiable(solve({NotXAndY, XAndY}));
121 }
122 
123 TEST(SolverTest, DisjunctionSameVarWithNegation) {
124   ConstraintContext Ctx;
125   auto X = Ctx.atom();
126   auto NotX = Ctx.neg(X);
127   auto XOrNotX = Ctx.disj(X, NotX);
128 
129   // X v !X
130   expectSatisfiable(solve({XOrNotX}), _);
131 }
132 
133 TEST(SolverTest, DisjunctionSameVar) {
134   ConstraintContext Ctx;
135   auto X = Ctx.atom();
136   auto XOrX = Ctx.disj(X, X);
137 
138   // X v X
139   expectSatisfiable(solve({XOrX}), _);
140 }
141 
142 TEST(SolverTest, ConjunctionSameVarsConflict) {
143   ConstraintContext Ctx;
144   auto X = Ctx.atom();
145   auto NotX = Ctx.neg(X);
146   auto XAndNotX = Ctx.conj(X, NotX);
147 
148   // X ^ !X
149   expectUnsatisfiable(solve({XAndNotX}));
150 }
151 
152 TEST(SolverTest, ConjunctionSameVar) {
153   ConstraintContext Ctx;
154   auto X = Ctx.atom();
155   auto XAndX = Ctx.conj(X, X);
156 
157   // X ^ X
158   expectSatisfiable(solve({XAndX}), _);
159 }
160 
161 TEST(SolverTest, PureVar) {
162   ConstraintContext Ctx;
163   auto X = Ctx.atom();
164   auto Y = Ctx.atom();
165   auto NotX = Ctx.neg(X);
166   auto NotXOrY = Ctx.disj(NotX, Y);
167   auto NotY = Ctx.neg(Y);
168   auto NotXOrNotY = Ctx.disj(NotX, NotY);
169 
170   // (!X v Y) ^ (!X v !Y)
171   expectSatisfiable(
172       solve({NotXOrY, NotXOrNotY}),
173       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
174                            Pair(Y, _)));
175 }
176 
177 TEST(SolverTest, MustAssumeVarIsFalse) {
178   ConstraintContext Ctx;
179   auto X = Ctx.atom();
180   auto Y = Ctx.atom();
181   auto XOrY = Ctx.disj(X, Y);
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) ^ (!X v !Y)
188   expectSatisfiable(
189       solve({XOrY, NotXOrY, NotXOrNotY}),
190       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
191                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));
192 }
193 
194 TEST(SolverTest, DeepConflict) {
195   ConstraintContext Ctx;
196   auto X = Ctx.atom();
197   auto Y = Ctx.atom();
198   auto XOrY = Ctx.disj(X, Y);
199   auto NotX = Ctx.neg(X);
200   auto NotXOrY = Ctx.disj(NotX, Y);
201   auto NotY = Ctx.neg(Y);
202   auto NotXOrNotY = Ctx.disj(NotX, NotY);
203   auto XOrNotY = Ctx.disj(X, NotY);
204 
205   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
206   expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
207 }
208 
209 TEST(SolverTest, IffSameVars) {
210   ConstraintContext Ctx;
211   auto X = Ctx.atom();
212   auto XEqX = Ctx.iff(X, X);
213 
214   // X <=> X
215   expectSatisfiable(solve({XEqX}), _);
216 }
217 
218 TEST(SolverTest, IffDistinctVars) {
219   ConstraintContext Ctx;
220   auto X = Ctx.atom();
221   auto Y = Ctx.atom();
222   auto XEqY = Ctx.iff(X, Y);
223 
224   // X <=> Y
225   expectSatisfiable(
226       solve({XEqY}),
227       AnyOf(UnorderedElementsAre(
228                 Pair(X, Solver::Result::Assignment::AssignedTrue),
229                 Pair(Y, Solver::Result::Assignment::AssignedTrue)),
230             UnorderedElementsAre(
231                 Pair(X, Solver::Result::Assignment::AssignedFalse),
232                 Pair(Y, Solver::Result::Assignment::AssignedFalse))));
233 }
234 
235 TEST(SolverTest, IffWithUnits) {
236   ConstraintContext Ctx;
237   auto X = Ctx.atom();
238   auto Y = Ctx.atom();
239   auto XEqY = Ctx.iff(X, Y);
240 
241   // (X <=> Y) ^ X ^ Y
242   expectSatisfiable(
243       solve({XEqY, X, Y}),
244       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
245                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));
246 }
247 
248 TEST(SolverTest, IffWithUnitsConflict) {
249   ConstraintContext Ctx;
250   auto X = Ctx.atom();
251   auto Y = Ctx.atom();
252   auto XEqY = Ctx.iff(X, Y);
253   auto NotY = Ctx.neg(Y);
254 
255   // (X <=> Y) ^ X  !Y
256   expectUnsatisfiable(solve({XEqY, X, NotY}));
257 }
258 
259 TEST(SolverTest, IffTransitiveConflict) {
260   ConstraintContext Ctx;
261   auto X = Ctx.atom();
262   auto Y = Ctx.atom();
263   auto Z = Ctx.atom();
264   auto XEqY = Ctx.iff(X, Y);
265   auto YEqZ = Ctx.iff(Y, Z);
266   auto NotX = Ctx.neg(X);
267 
268   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
269   expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
270 }
271 
272 TEST(SolverTest, DeMorgan) {
273   ConstraintContext Ctx;
274   auto X = Ctx.atom();
275   auto Y = Ctx.atom();
276   auto Z = Ctx.atom();
277   auto W = Ctx.atom();
278 
279   // !(X v Y) <=> !X ^ !Y
280   auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
281 
282   // !(Z ^ W) <=> !Z v !W
283   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
284 
285   // A ^ B
286   expectSatisfiable(solve({A, B}), _);
287 }
288 
289 TEST(SolverTest, RespectsAdditionalConstraints) {
290   ConstraintContext Ctx;
291   auto X = Ctx.atom();
292   auto Y = Ctx.atom();
293   auto XEqY = Ctx.iff(X, Y);
294   auto NotY = Ctx.neg(Y);
295 
296   // (X <=> Y) ^ X ^ !Y
297   expectUnsatisfiable(solve({XEqY, X, NotY}));
298 }
299 
300 TEST(SolverTest, ImplicationConflict) {
301   ConstraintContext Ctx;
302   auto X = Ctx.atom();
303   auto Y = Ctx.atom();
304   auto *XImplY = Ctx.impl(X, Y);
305   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
306 
307   // X => Y ^ X ^ !Y
308   expectUnsatisfiable(solve({XImplY, XAndNotY}));
309 }
310 
311 } // namespace
312