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.
solve(llvm::DenseSet<BoolValue * > Vals)33 Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
34 return WatchedLiteralsSolver().solve(std::move(Vals));
35 }
36
expectUnsatisfiable(Solver::Result Result)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>
expectSatisfiable(Solver::Result Result,Matcher Solution)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
TEST(SolverTest,Var)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
TEST(SolverTest,NegatedVar)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
TEST(SolverTest,UnitConflict)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
TEST(SolverTest,DistinctVars)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
TEST(SolverTest,DoubleNegation)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
TEST(SolverTest,NegatedDisjunction)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
TEST(SolverTest,NegatedConjunction)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
TEST(SolverTest,DisjunctionSameVarWithNegation)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
TEST(SolverTest,DisjunctionSameVar)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
TEST(SolverTest,ConjunctionSameVarsConflict)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
TEST(SolverTest,ConjunctionSameVar)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
TEST(SolverTest,PureVar)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
TEST(SolverTest,MustAssumeVarIsFalse)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
TEST(SolverTest,DeepConflict)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
TEST(SolverTest,IffIsEquivalentToDNF)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
TEST(SolverTest,IffSameVars)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
TEST(SolverTest,IffDistinctVars)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
TEST(SolverTest,IffWithUnits)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
TEST(SolverTest,IffWithUnitsConflict)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
TEST(SolverTest,IffTransitiveConflict)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
TEST(SolverTest,DeMorgan)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
TEST(SolverTest,RespectsAdditionalConstraints)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
TEST(SolverTest,ImplicationIsEquivalentToDNF)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
TEST(SolverTest,ImplicationConflict)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