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, DisjunctionSameVars) {
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, ConjunctionSameVarsConflict) {
134   ConstraintContext Ctx;
135   auto X = Ctx.atom();
136   auto NotX = Ctx.neg(X);
137   auto XAndNotX = Ctx.conj(X, NotX);
138 
139   // X ^ !X
140   expectUnsatisfiable(solve({XAndNotX}));
141 }
142 
143 TEST(SolverTest, PureVar) {
144   ConstraintContext Ctx;
145   auto X = Ctx.atom();
146   auto Y = Ctx.atom();
147   auto NotX = Ctx.neg(X);
148   auto NotXOrY = Ctx.disj(NotX, Y);
149   auto NotY = Ctx.neg(Y);
150   auto NotXOrNotY = Ctx.disj(NotX, NotY);
151 
152   // (!X v Y) ^ (!X v !Y)
153   expectSatisfiable(
154       solve({NotXOrY, NotXOrNotY}),
155       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
156                            Pair(Y, _)));
157 }
158 
159 TEST(SolverTest, MustAssumeVarIsFalse) {
160   ConstraintContext Ctx;
161   auto X = Ctx.atom();
162   auto Y = Ctx.atom();
163   auto XOrY = Ctx.disj(X, Y);
164   auto NotX = Ctx.neg(X);
165   auto NotXOrY = Ctx.disj(NotX, Y);
166   auto NotY = Ctx.neg(Y);
167   auto NotXOrNotY = Ctx.disj(NotX, NotY);
168 
169   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
170   expectSatisfiable(
171       solve({XOrY, NotXOrY, NotXOrNotY}),
172       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
173                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));
174 }
175 
176 TEST(SolverTest, DeepConflict) {
177   ConstraintContext Ctx;
178   auto X = Ctx.atom();
179   auto Y = Ctx.atom();
180   auto XOrY = Ctx.disj(X, Y);
181   auto NotX = Ctx.neg(X);
182   auto NotXOrY = Ctx.disj(NotX, Y);
183   auto NotY = Ctx.neg(Y);
184   auto NotXOrNotY = Ctx.disj(NotX, NotY);
185   auto XOrNotY = Ctx.disj(X, NotY);
186 
187   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
188   expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
189 }
190 
191 TEST(SolverTest, IffSameVars) {
192   ConstraintContext Ctx;
193   auto X = Ctx.atom();
194   auto XEqX = Ctx.iff(X, X);
195 
196   // X <=> X
197   expectSatisfiable(solve({XEqX}), _);
198 }
199 
200 TEST(SolverTest, IffDistinctVars) {
201   ConstraintContext Ctx;
202   auto X = Ctx.atom();
203   auto Y = Ctx.atom();
204   auto XEqY = Ctx.iff(X, Y);
205 
206   // X <=> Y
207   expectSatisfiable(
208       solve({XEqY}),
209       AnyOf(UnorderedElementsAre(
210                 Pair(X, Solver::Result::Assignment::AssignedTrue),
211                 Pair(Y, Solver::Result::Assignment::AssignedTrue)),
212             UnorderedElementsAre(
213                 Pair(X, Solver::Result::Assignment::AssignedFalse),
214                 Pair(Y, Solver::Result::Assignment::AssignedFalse))));
215 }
216 
217 TEST(SolverTest, IffWithUnits) {
218   ConstraintContext Ctx;
219   auto X = Ctx.atom();
220   auto Y = Ctx.atom();
221   auto XEqY = Ctx.iff(X, Y);
222 
223   // (X <=> Y) ^ X ^ Y
224   expectSatisfiable(
225       solve({XEqY, X, Y}),
226       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
227                            Pair(Y, Solver::Result::Assignment::AssignedTrue)));
228 }
229 
230 TEST(SolverTest, IffWithUnitsConflict) {
231   ConstraintContext Ctx;
232   auto X = Ctx.atom();
233   auto Y = Ctx.atom();
234   auto XEqY = Ctx.iff(X, Y);
235   auto NotY = Ctx.neg(Y);
236 
237   // (X <=> Y) ^ X  !Y
238   expectUnsatisfiable(solve({XEqY, X, NotY}));
239 }
240 
241 TEST(SolverTest, IffTransitiveConflict) {
242   ConstraintContext Ctx;
243   auto X = Ctx.atom();
244   auto Y = Ctx.atom();
245   auto Z = Ctx.atom();
246   auto XEqY = Ctx.iff(X, Y);
247   auto YEqZ = Ctx.iff(Y, Z);
248   auto NotX = Ctx.neg(X);
249 
250   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
251   expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
252 }
253 
254 TEST(SolverTest, DeMorgan) {
255   ConstraintContext Ctx;
256   auto X = Ctx.atom();
257   auto Y = Ctx.atom();
258   auto Z = Ctx.atom();
259   auto W = Ctx.atom();
260 
261   // !(X v Y) <=> !X ^ !Y
262   auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
263 
264   // !(Z ^ W) <=> !Z v !W
265   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
266 
267   // A ^ B
268   expectSatisfiable(solve({A, B}), _);
269 }
270 
271 TEST(SolverTest, RespectsAdditionalConstraints) {
272   ConstraintContext Ctx;
273   auto X = Ctx.atom();
274   auto Y = Ctx.atom();
275   auto XEqY = Ctx.iff(X, Y);
276   auto NotY = Ctx.neg(Y);
277 
278   // (X <=> Y) ^ X ^ !Y
279   expectUnsatisfiable(solve({XEqY, X, NotY}));
280 }
281 
282 TEST(SolverTest, ImplicationConflict) {
283   ConstraintContext Ctx;
284   auto X = Ctx.atom();
285   auto Y = Ctx.atom();
286   auto *XImplY = Ctx.impl(X, Y);
287   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
288 
289   // X => Y ^ X ^ !Y
290   expectUnsatisfiable(solve({XImplY, XAndNotY}));
291 }
292 
293 } // namespace
294