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