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