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 TEST(ConstraintSetDebugStringTest, Empty) {
192   llvm::DenseSet<BoolValue *> Constraints;
193   EXPECT_THAT(debugString(Constraints), StrEq(""));
194 }
195 
196 TEST(ConstraintSetDebugStringTest, Simple) {
197   ConstraintContext Ctx;
198   llvm::DenseSet<BoolValue *> Constraints;
199   auto X = cast<AtomicBoolValue>(Ctx.atom());
200   auto Y = cast<AtomicBoolValue>(Ctx.atom());
201   Constraints.insert(Ctx.disj(X, Y));
202   Constraints.insert(Ctx.disj(X, Ctx.neg(Y)));
203 
204   auto Expected = R"((or
205     X
206     (not
207         Y))
208 (or
209     X
210     Y)
211 )";
212   EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
213               StrEq(Expected));
214 }
215 
216 Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
217   llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),
218                                              Constraints.end());
219   return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
220 }
221 
222 TEST(SATCheckDebugStringTest, AtomicBoolean) {
223   // B0
224   ConstraintContext Ctx;
225   std::vector<BoolValue *> Constraints({Ctx.atom()});
226   auto Result = CheckSAT(Constraints);
227 
228   auto Expected = R"(
229 Constraints
230 ------------
231 B0
232 ------------
233 Satisfiable.
234 
235 B0 = True
236 )";
237   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
238 }
239 
240 TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
241   // B0, !B0
242   ConstraintContext Ctx;
243   auto B0 = Ctx.atom();
244   std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
245   auto Result = CheckSAT(Constraints);
246 
247   auto Expected = R"(
248 Constraints
249 ------------
250 B0
251 
252 (not
253     B0)
254 ------------
255 Unsatisfiable.
256 
257 )";
258   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
259 }
260 
261 TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
262   // B0, B1
263   ConstraintContext Ctx;
264   std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
265   auto Result = CheckSAT(Constraints);
266 
267   auto Expected = R"(
268 Constraints
269 ------------
270 B0
271 
272 B1
273 ------------
274 Satisfiable.
275 
276 B0 = True
277 B1 = True
278 )";
279   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
280 }
281 
282 TEST(SATCheckDebugStringTest, Implication) {
283   // B0, B0 => B1
284   ConstraintContext Ctx;
285   auto B0 = Ctx.atom();
286   auto B1 = Ctx.atom();
287   auto Impl = Ctx.disj(Ctx.neg(B0), B1);
288   std::vector<BoolValue *> Constraints({B0, Impl});
289   auto Result = CheckSAT(Constraints);
290 
291   auto Expected = R"(
292 Constraints
293 ------------
294 B0
295 
296 (or
297     (not
298         B0)
299     B1)
300 ------------
301 Satisfiable.
302 
303 B0 = True
304 B1 = True
305 )";
306   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
307 }
308 
309 TEST(SATCheckDebugStringTest, Iff) {
310   // B0, B0 <=> B1
311   ConstraintContext Ctx;
312   auto B0 = Ctx.atom();
313   auto B1 = Ctx.atom();
314   auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
315   std::vector<BoolValue *> Constraints({B0, Iff});
316   auto Result = CheckSAT(Constraints);
317 
318   auto Expected = R"(
319 Constraints
320 ------------
321 B0
322 
323 (and
324     (or
325         (not
326             B0)
327         B1)
328     (or
329         B0
330         (not
331             B1)))
332 ------------
333 Satisfiable.
334 
335 B0 = True
336 B1 = True
337 )";
338   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
339 }
340 
341 TEST(SATCheckDebugStringTest, Xor) {
342   // B0, XOR(B0, B1)
343   ConstraintContext Ctx;
344   auto B0 = Ctx.atom();
345   auto B1 = Ctx.atom();
346   auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
347   std::vector<BoolValue *> Constraints({B0, XOR});
348   auto Result = CheckSAT(Constraints);
349 
350   auto Expected = R"(
351 Constraints
352 ------------
353 B0
354 
355 (or
356     (and
357         B0
358         (not
359             B1))
360     (and
361         (not
362             B0)
363         B1))
364 ------------
365 Satisfiable.
366 
367 B0 = True
368 B1 = False
369 )";
370   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
371 }
372 
373 TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
374   // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
375   ConstraintContext Ctx;
376   auto Cond = cast<AtomicBoolValue>(Ctx.atom());
377   auto Then = cast<AtomicBoolValue>(Ctx.atom());
378   auto Else = cast<AtomicBoolValue>(Ctx.atom());
379   auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
380                     Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
381   std::vector<BoolValue *> Constraints({Cond, B});
382   auto Result = CheckSAT(Constraints);
383 
384   auto Expected = R"(
385 Constraints
386 ------------
387 Cond
388 
389 (or
390     (and
391         Cond
392         (and
393             Then
394             (not
395                 Else)))
396     (and
397         (not
398             Cond)
399         (and
400             (not
401                 Then)
402             Else)))
403 ------------
404 Satisfiable.
405 
406 Cond = True
407 Else = False
408 Then = True
409 )";
410   EXPECT_THAT(debugString(Constraints, Result,
411                           {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
412               StrEq(Expected));
413 }
414 
415 TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
416   // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
417   ConstraintContext Ctx;
418   auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
419   auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
420   auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
421   auto BothZeroImpliesEQ =
422       Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
423   std::vector<BoolValue *> Constraints(
424       {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
425   auto Result = CheckSAT(Constraints);
426 
427   auto Expected = R"(
428 Constraints
429 ------------
430 ThisIntEqZero
431 
432 (not
433     IntsAreEq)
434 
435 (or
436     (not
437         (and
438             ThisIntEqZero
439             OtherIntEqZero))
440     IntsAreEq)
441 ------------
442 Satisfiable.
443 
444 IntsAreEq      = False
445 OtherIntEqZero = False
446 ThisIntEqZero  = True
447 )";
448   EXPECT_THAT(debugString(Constraints, Result,
449                           {{IntsAreEq, "IntsAreEq"},
450                            {ThisIntEqZero, "ThisIntEqZero"},
451                            {OtherIntEqZero, "OtherIntEqZero"}}),
452               StrEq(Expected));
453 }
454 } // namespace
455