1 //===- unittests/Analysis/FlowSensitive/DebugSupportTest.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/DebugSupport.h"
10 #include "TestingSupport.h"
11 #include "clang/Analysis/FlowSensitive/Value.h"
12 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
13 #include "gmock/gmock.h"
14 #include "gtest/gtest.h"
15 
16 namespace {
17 
18 using namespace clang;
19 using namespace dataflow;
20 
21 using test::ConstraintContext;
22 using testing::StrEq;
23 
24 TEST(BoolValueDebugStringTest, AtomicBoolean) {
25   // B0
26   ConstraintContext Ctx;
27   auto B = Ctx.atom();
28 
29   auto Expected = R"(B0)";
30   debugString(*B);
31   EXPECT_THAT(debugString(*B), StrEq(Expected));
32 }
33 
34 TEST(BoolValueDebugStringTest, Negation) {
35   // !B0
36   ConstraintContext Ctx;
37   auto B = Ctx.neg(Ctx.atom());
38 
39   auto Expected = R"((not
40     B0))";
41   EXPECT_THAT(debugString(*B), StrEq(Expected));
42 }
43 
44 TEST(BoolValueDebugStringTest, Conjunction) {
45   // B0 ^ B1
46   ConstraintContext Ctx;
47   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
48 
49   auto Expected = R"((and
50     B0
51     B1))";
52   EXPECT_THAT(debugString(*B), StrEq(Expected));
53 }
54 
55 TEST(BoolValueDebugStringTest, Disjunction) {
56   // B0 v B1
57   ConstraintContext Ctx;
58   auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
59 
60   auto Expected = R"((or
61     B0
62     B1))";
63   EXPECT_THAT(debugString(*B), StrEq(Expected));
64 }
65 
66 TEST(BoolValueDebugStringTest, Implication) {
67   // B0 => B1, implemented as !B0 v B1
68   ConstraintContext Ctx;
69   auto B = Ctx.disj(Ctx.neg(Ctx.atom()), Ctx.atom());
70 
71   auto Expected = R"((or
72     (not
73         B0)
74     B1))";
75   EXPECT_THAT(debugString(*B), StrEq(Expected));
76 }
77 
78 TEST(BoolValueDebugStringTest, Iff) {
79   // B0 <=> B1, implemented as (!B0 v B1) ^ (B0 v !B1)
80   ConstraintContext Ctx;
81   auto B0 = Ctx.atom();
82   auto B1 = Ctx.atom();
83   auto B = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
84 
85   auto Expected = R"((and
86     (or
87         (not
88             B0)
89         B1)
90     (or
91         B0
92         (not
93             B1))))";
94   EXPECT_THAT(debugString(*B), StrEq(Expected));
95 }
96 
97 TEST(BoolValueDebugStringTest, Xor) {
98   // (B0 ^ !B1) V (!B0 ^ B1)
99   ConstraintContext Ctx;
100   auto B0 = Ctx.atom();
101   auto B1 = Ctx.atom();
102   auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
103 
104   auto Expected = R"((or
105     (and
106         B0
107         (not
108             B1))
109     (and
110         (not
111             B0)
112         B1)))";
113   EXPECT_THAT(debugString(*B), StrEq(Expected));
114 }
115 
116 TEST(BoolValueDebugStringTest, NestedBoolean) {
117   // B0 ^ (B1 v (B2 ^ (B3 v B4)))
118   ConstraintContext Ctx;
119   auto B = Ctx.conj(
120       Ctx.atom(),
121       Ctx.disj(Ctx.atom(),
122                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
123 
124   auto Expected = R"((and
125     B0
126     (or
127         B1
128         (and
129             B2
130             (or
131                 B3
132                 B4)))))";
133   EXPECT_THAT(debugString(*B), StrEq(Expected));
134 }
135 
136 TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
137   // True
138   ConstraintContext Ctx;
139   auto True = cast<AtomicBoolValue>(Ctx.atom());
140   auto B = True;
141 
142   auto Expected = R"(True)";
143   EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
144 }
145 
146 TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
147   // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
148   ConstraintContext Ctx;
149   auto Cond = cast<AtomicBoolValue>(Ctx.atom());
150   auto Then = cast<AtomicBoolValue>(Ctx.atom());
151   auto Else = cast<AtomicBoolValue>(Ctx.atom());
152   auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
153                     Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
154 
155   auto Expected = R"((or
156     (and
157         Cond
158         (and
159             Then
160             (not
161                 Else)))
162     (and
163         (not
164             Cond)
165         (and
166             (not
167                 Then)
168             Else))))";
169   EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
170               StrEq(Expected));
171 }
172 
173 TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
174   // (False && B0) v (True v B1)
175   ConstraintContext Ctx;
176   auto True = cast<AtomicBoolValue>(Ctx.atom());
177   auto False = cast<AtomicBoolValue>(Ctx.atom());
178   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
179 
180   auto Expected = R"((or
181     (and
182         False
183         B0)
184     (or
185         True
186         B1)))";
187   EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
188               StrEq(Expected));
189 }
190 
191 Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
192   llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),
193                                              Constraints.end());
194   return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
195 }
196 
197 TEST(SATCheckDebugStringTest, AtomicBoolean) {
198   // B0
199   ConstraintContext Ctx;
200   std::vector<BoolValue *> Constraints({Ctx.atom()});
201   auto Result = CheckSAT(Constraints);
202 
203   auto Expected = R"(
204 Constraints
205 ------------
206 B0
207 ------------
208 Satisfiable.
209 
210 B0 = True
211 )";
212   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
213 }
214 
215 TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
216   // B0, !B0
217   ConstraintContext Ctx;
218   auto B0 = Ctx.atom();
219   std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
220   auto Result = CheckSAT(Constraints);
221 
222   auto Expected = R"(
223 Constraints
224 ------------
225 B0
226 
227 (not
228     B0)
229 ------------
230 Unsatisfiable.
231 
232 )";
233   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
234 }
235 
236 TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
237   // B0, B1
238   ConstraintContext Ctx;
239   std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
240   auto Result = CheckSAT(Constraints);
241 
242   auto Expected = R"(
243 Constraints
244 ------------
245 B0
246 
247 B1
248 ------------
249 Satisfiable.
250 
251 B0 = True
252 B1 = True
253 )";
254   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
255 }
256 
257 TEST(SATCheckDebugStringTest, Implication) {
258   // B0, B0 => B1
259   ConstraintContext Ctx;
260   auto B0 = Ctx.atom();
261   auto B1 = Ctx.atom();
262   auto Impl = Ctx.disj(Ctx.neg(B0), B1);
263   std::vector<BoolValue *> Constraints({B0, Impl});
264   auto Result = CheckSAT(Constraints);
265 
266   auto Expected = R"(
267 Constraints
268 ------------
269 B0
270 
271 (or
272     (not
273         B0)
274     B1)
275 ------------
276 Satisfiable.
277 
278 B0 = True
279 B1 = True
280 )";
281   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
282 }
283 
284 TEST(SATCheckDebugStringTest, Iff) {
285   // B0, B0 <=> B1
286   ConstraintContext Ctx;
287   auto B0 = Ctx.atom();
288   auto B1 = Ctx.atom();
289   auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
290   std::vector<BoolValue *> Constraints({B0, Iff});
291   auto Result = CheckSAT(Constraints);
292 
293   auto Expected = R"(
294 Constraints
295 ------------
296 B0
297 
298 (and
299     (or
300         (not
301             B0)
302         B1)
303     (or
304         B0
305         (not
306             B1)))
307 ------------
308 Satisfiable.
309 
310 B0 = True
311 B1 = True
312 )";
313   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
314 }
315 
316 TEST(SATCheckDebugStringTest, Xor) {
317   // B0, XOR(B0, B1)
318   ConstraintContext Ctx;
319   auto B0 = Ctx.atom();
320   auto B1 = Ctx.atom();
321   auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
322   std::vector<BoolValue *> Constraints({B0, XOR});
323   auto Result = CheckSAT(Constraints);
324 
325   auto Expected = R"(
326 Constraints
327 ------------
328 B0
329 
330 (or
331     (and
332         B0
333         (not
334             B1))
335     (and
336         (not
337             B0)
338         B1))
339 ------------
340 Satisfiable.
341 
342 B0 = True
343 B1 = False
344 )";
345   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
346 }
347 
348 TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
349   // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
350   ConstraintContext Ctx;
351   auto Cond = cast<AtomicBoolValue>(Ctx.atom());
352   auto Then = cast<AtomicBoolValue>(Ctx.atom());
353   auto Else = cast<AtomicBoolValue>(Ctx.atom());
354   auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
355                     Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
356   std::vector<BoolValue *> Constraints({Cond, B});
357   auto Result = CheckSAT(Constraints);
358 
359   auto Expected = R"(
360 Constraints
361 ------------
362 Cond
363 
364 (or
365     (and
366         Cond
367         (and
368             Then
369             (not
370                 Else)))
371     (and
372         (not
373             Cond)
374         (and
375             (not
376                 Then)
377             Else)))
378 ------------
379 Satisfiable.
380 
381 Cond = True
382 Else = False
383 Then = True
384 )";
385   EXPECT_THAT(debugString(Constraints, Result,
386                           {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
387               StrEq(Expected));
388 }
389 
390 TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
391   // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
392   ConstraintContext Ctx;
393   auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
394   auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
395   auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
396   auto BothZeroImpliesEQ =
397       Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
398   std::vector<BoolValue *> Constraints(
399       {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
400   auto Result = CheckSAT(Constraints);
401 
402   auto Expected = R"(
403 Constraints
404 ------------
405 ThisIntEqZero
406 
407 (not
408     IntsAreEq)
409 
410 (or
411     (not
412         (and
413             ThisIntEqZero
414             OtherIntEqZero))
415     IntsAreEq)
416 ------------
417 Satisfiable.
418 
419 IntsAreEq      = False
420 OtherIntEqZero = False
421 ThisIntEqZero  = True
422 )";
423   EXPECT_THAT(debugString(Constraints, Result,
424                           {{IntsAreEq, "IntsAreEq"},
425                            {ThisIntEqZero, "ThisIntEqZero"},
426                            {OtherIntEqZero, "OtherIntEqZero"}}),
427               StrEq(Expected));
428 }
429 } // namespace
430