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, IffIsEquivalentToDNF) {
210   ConstraintContext Ctx;
211   auto X = Ctx.atom();
212   auto Y = Ctx.atom();
213   auto NotX = Ctx.neg(X);
214   auto NotY = Ctx.neg(Y);
215   auto XIffY = Ctx.iff(X, Y);
216   auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY));
217   auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
218 
219   // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
220   expectUnsatisfiable(solve({NotEquivalent}));
221 }
222 
223 TEST(SolverTest, IffSameVars) {
224   ConstraintContext Ctx;
225   auto X = Ctx.atom();
226   auto XEqX = Ctx.iff(X, X);
227 
228   // X <=> X
229   expectSatisfiable(solve({XEqX}), _);
230 }
231 
232 TEST(SolverTest, IffDistinctVars) {
233   ConstraintContext Ctx;
234   auto X = Ctx.atom();
235   auto Y = Ctx.atom();
236   auto XEqY = Ctx.iff(X, Y);
237 
238   // X <=> Y
239   expectSatisfiable(
240       solve({XEqY}),
241       AnyOf(UnorderedElementsAre(
242                 Pair(X, Solver::Result::Assignment::AssignedTrue),
243                 Pair(Y, Solver::Result::Assignment::AssignedTrue)),
244             UnorderedElementsAre(
245                 Pair(X, Solver::Result::Assignment::AssignedFalse),
246                 Pair(Y, Solver::Result::Assignment::AssignedFalse))));
247 }
248 
249 TEST(SolverTest, IffWithUnits) {
250   ConstraintContext Ctx;
251   auto X = Ctx.atom();
252   auto Y = Ctx.atom();
253   auto XEqY = Ctx.iff(X, Y);
254 
255   // (X <=> Y) ^ X ^ Y
256   expectSatisfiable(
257       solve({XEqY, X, Y}),
258       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
259                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));
260 }
261 
262 TEST(SolverTest, IffWithUnitsConflict) {
263   ConstraintContext Ctx;
264   auto X = Ctx.atom();
265   auto Y = Ctx.atom();
266   auto XEqY = Ctx.iff(X, Y);
267   auto NotY = Ctx.neg(Y);
268 
269   // (X <=> Y) ^ X  !Y
270   expectUnsatisfiable(solve({XEqY, X, NotY}));
271 }
272 
273 TEST(SolverTest, IffTransitiveConflict) {
274   ConstraintContext Ctx;
275   auto X = Ctx.atom();
276   auto Y = Ctx.atom();
277   auto Z = Ctx.atom();
278   auto XEqY = Ctx.iff(X, Y);
279   auto YEqZ = Ctx.iff(Y, Z);
280   auto NotX = Ctx.neg(X);
281 
282   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
283   expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
284 }
285 
286 TEST(SolverTest, DeMorgan) {
287   ConstraintContext Ctx;
288   auto X = Ctx.atom();
289   auto Y = Ctx.atom();
290   auto Z = Ctx.atom();
291   auto W = Ctx.atom();
292 
293   // !(X v Y) <=> !X ^ !Y
294   auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
295 
296   // !(Z ^ W) <=> !Z v !W
297   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
298 
299   // A ^ B
300   expectSatisfiable(solve({A, B}), _);
301 }
302 
303 TEST(SolverTest, RespectsAdditionalConstraints) {
304   ConstraintContext Ctx;
305   auto X = Ctx.atom();
306   auto Y = Ctx.atom();
307   auto XEqY = Ctx.iff(X, Y);
308   auto NotY = Ctx.neg(Y);
309 
310   // (X <=> Y) ^ X ^ !Y
311   expectUnsatisfiable(solve({XEqY, X, NotY}));
312 }
313 
314 TEST(SolverTest, ImplicationIsEquivalentToDNF) {
315   ConstraintContext Ctx;
316   auto X = Ctx.atom();
317   auto Y = Ctx.atom();
318   auto XImpliesY = Ctx.impl(X, Y);
319   auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y);
320   auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
321 
322   // !((X => Y) <=> (!X v Y))
323   expectUnsatisfiable(solve({NotEquivalent}));
324 }
325 
326 TEST(SolverTest, ImplicationConflict) {
327   ConstraintContext Ctx;
328   auto X = Ctx.atom();
329   auto Y = Ctx.atom();
330   auto *XImplY = Ctx.impl(X, Y);
331   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
332 
333   // X => Y ^ X ^ !Y
334   expectUnsatisfiable(solve({XImplY, XAndNotY}));
335 }
336 
337 } // namespace
338