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 class SolverTest : public ::testing::Test {
24 protected:
25   // Checks if the conjunction of `Vals` is satisfiable and returns the
26   // corresponding result.
27   Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
28     return WatchedLiteralsSolver().solve(std::move(Vals));
29   }
30 
31   // Creates an atomic boolean value.
32   BoolValue *atom() {
33     Vals.push_back(std::make_unique<AtomicBoolValue>());
34     return Vals.back().get();
35   }
36 
37   // Creates a boolean conjunction value.
38   BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
39     Vals.push_back(
40         std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
41     return Vals.back().get();
42   }
43 
44   // Creates a boolean disjunction value.
45   BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
46     Vals.push_back(
47         std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
48     return Vals.back().get();
49   }
50 
51   // Creates a boolean negation value.
52   BoolValue *neg(BoolValue *SubVal) {
53     Vals.push_back(std::make_unique<NegationValue>(*SubVal));
54     return Vals.back().get();
55   }
56 
57   // Creates a boolean implication value.
58   BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
59     return disj(neg(LeftSubVal), RightSubVal);
60   }
61 
62   // Creates a boolean biconditional value.
63   BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
64     return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal));
65   }
66 
67 private:
68   std::vector<std::unique_ptr<BoolValue>> Vals;
69 };
70 
71 TEST_F(SolverTest, Var) {
72   auto X = atom();
73 
74   // X
75   EXPECT_EQ(solve({X}), Solver::Result::Satisfiable);
76 }
77 
78 TEST_F(SolverTest, NegatedVar) {
79   auto X = atom();
80   auto NotX = neg(X);
81 
82   // !X
83   EXPECT_EQ(solve({NotX}), Solver::Result::Satisfiable);
84 }
85 
86 TEST_F(SolverTest, UnitConflict) {
87   auto X = atom();
88   auto NotX = neg(X);
89 
90   // X ^ !X
91   EXPECT_EQ(solve({X, NotX}), Solver::Result::Unsatisfiable);
92 }
93 
94 TEST_F(SolverTest, DistinctVars) {
95   auto X = atom();
96   auto Y = atom();
97   auto NotY = neg(Y);
98 
99   // X ^ !Y
100   EXPECT_EQ(solve({X, NotY}), Solver::Result::Satisfiable);
101 }
102 
103 TEST_F(SolverTest, DoubleNegation) {
104   auto X = atom();
105   auto NotX = neg(X);
106   auto NotNotX = neg(NotX);
107 
108   // !!X ^ !X
109   EXPECT_EQ(solve({NotNotX, NotX}), Solver::Result::Unsatisfiable);
110 }
111 
112 TEST_F(SolverTest, NegatedDisjunction) {
113   auto X = atom();
114   auto Y = atom();
115   auto XOrY = disj(X, Y);
116   auto NotXOrY = neg(XOrY);
117 
118   // !(X v Y) ^ (X v Y)
119   EXPECT_EQ(solve({NotXOrY, XOrY}), Solver::Result::Unsatisfiable);
120 }
121 
122 TEST_F(SolverTest, NegatedConjunction) {
123   auto X = atom();
124   auto Y = atom();
125   auto XAndY = conj(X, Y);
126   auto NotXAndY = neg(XAndY);
127 
128   // !(X ^ Y) ^ (X ^ Y)
129   EXPECT_EQ(solve({NotXAndY, XAndY}), Solver::Result::Unsatisfiable);
130 }
131 
132 TEST_F(SolverTest, DisjunctionSameVars) {
133   auto X = atom();
134   auto NotX = neg(X);
135   auto XOrNotX = disj(X, NotX);
136 
137   // X v !X
138   EXPECT_EQ(solve({XOrNotX}), Solver::Result::Satisfiable);
139 }
140 
141 TEST_F(SolverTest, ConjunctionSameVarsConflict) {
142   auto X = atom();
143   auto NotX = neg(X);
144   auto XAndNotX = conj(X, NotX);
145 
146   // X ^ !X
147   EXPECT_EQ(solve({XAndNotX}), Solver::Result::Unsatisfiable);
148 }
149 
150 TEST_F(SolverTest, PureVar) {
151   auto X = atom();
152   auto Y = atom();
153   auto NotX = neg(X);
154   auto NotXOrY = disj(NotX, Y);
155   auto NotY = neg(Y);
156   auto NotXOrNotY = disj(NotX, NotY);
157 
158   // (!X v Y) ^ (!X v !Y)
159   EXPECT_EQ(solve({NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable);
160 }
161 
162 TEST_F(SolverTest, MustAssumeVarIsFalse) {
163   auto X = atom();
164   auto Y = atom();
165   auto XOrY = disj(X, Y);
166   auto NotX = neg(X);
167   auto NotXOrY = disj(NotX, Y);
168   auto NotY = neg(Y);
169   auto NotXOrNotY = disj(NotX, NotY);
170 
171   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
172   EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable);
173 }
174 
175 TEST_F(SolverTest, DeepConflict) {
176   auto X = atom();
177   auto Y = atom();
178   auto XOrY = disj(X, Y);
179   auto NotX = neg(X);
180   auto NotXOrY = disj(NotX, Y);
181   auto NotY = neg(Y);
182   auto NotXOrNotY = disj(NotX, NotY);
183   auto XOrNotY = disj(X, NotY);
184 
185   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
186   EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}),
187             Solver::Result::Unsatisfiable);
188 }
189 
190 TEST_F(SolverTest, IffSameVars) {
191   auto X = atom();
192   auto XEqX = iff(X, X);
193 
194   // X <=> X
195   EXPECT_EQ(solve({XEqX}), Solver::Result::Satisfiable);
196 }
197 
198 TEST_F(SolverTest, IffDistinctVars) {
199   auto X = atom();
200   auto Y = atom();
201   auto XEqY = iff(X, Y);
202 
203   // X <=> Y
204   EXPECT_EQ(solve({XEqY}), Solver::Result::Satisfiable);
205 }
206 
207 TEST_F(SolverTest, IffWithUnits) {
208   auto X = atom();
209   auto Y = atom();
210   auto XEqY = iff(X, Y);
211 
212   // (X <=> Y) ^ X ^ Y
213   EXPECT_EQ(solve({XEqY, X, Y}), Solver::Result::Satisfiable);
214 }
215 
216 TEST_F(SolverTest, IffWithUnitsConflict) {
217   auto X = atom();
218   auto Y = atom();
219   auto XEqY = iff(X, Y);
220   auto NotY = neg(Y);
221 
222   // (X <=> Y) ^ X  !Y
223   EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable);
224 }
225 
226 TEST_F(SolverTest, IffTransitiveConflict) {
227   auto X = atom();
228   auto Y = atom();
229   auto Z = atom();
230   auto XEqY = iff(X, Y);
231   auto YEqZ = iff(Y, Z);
232   auto NotX = neg(X);
233 
234   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
235   EXPECT_EQ(solve({XEqY, YEqZ, Z, NotX}), Solver::Result::Unsatisfiable);
236 }
237 
238 TEST_F(SolverTest, DeMorgan) {
239   auto X = atom();
240   auto Y = atom();
241   auto Z = atom();
242   auto W = atom();
243 
244   // !(X v Y) <=> !X ^ !Y
245   auto A = iff(neg(disj(X, Y)), conj(neg(X), neg(Y)));
246 
247   // !(Z ^ W) <=> !Z v !W
248   auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W)));
249 
250   // A ^ B
251   EXPECT_EQ(solve({A, B}), Solver::Result::Satisfiable);
252 }
253 
254 TEST_F(SolverTest, RespectsAdditionalConstraints) {
255   auto X = atom();
256   auto Y = atom();
257   auto XEqY = iff(X, Y);
258   auto NotY = neg(Y);
259 
260   // (X <=> Y) ^ X ^ !Y
261   EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable);
262 }
263 
264 TEST_F(SolverTest, ImplicationConflict) {
265   auto X = atom();
266   auto Y = atom();
267   auto *XImplY = impl(X, Y);
268   auto *XAndNotY = conj(X, neg(Y));
269 
270   // X => Y ^ X ^ !Y
271   EXPECT_EQ(solve({XImplY, XAndNotY}), Solver::Result::Unsatisfiable);
272 }
273 
274 } // namespace
275