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
TEST(BoolValueDebugStringTest,AtomicBoolean)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
TEST(BoolValueDebugStringTest,Negation)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
TEST(BoolValueDebugStringTest,Conjunction)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
TEST(BoolValueDebugStringTest,Disjunction)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
TEST(BoolValueDebugStringTest,Implication)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
TEST(BoolValueDebugStringTest,Iff)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
TEST(BoolValueDebugStringTest,Xor)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
TEST(BoolValueDebugStringTest,NestedBoolean)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
TEST(BoolValueDebugStringTest,AtomicBooleanWithName)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
TEST(BoolValueDebugStringTest,ComplexBooleanWithNames)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
TEST(BoolValueDebugStringTest,ComplexBooleanWithSomeNames)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
TEST(ConstraintSetDebugStringTest,Empty)182 TEST(ConstraintSetDebugStringTest, Empty) {
183 llvm::DenseSet<BoolValue *> Constraints;
184 EXPECT_THAT(debugString(Constraints), StrEq(""));
185 }
186
TEST(ConstraintSetDebugStringTest,Simple)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
CheckSAT(std::vector<BoolValue * > Constraints)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
TEST(SATCheckDebugStringTest,AtomicBoolean)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
TEST(SATCheckDebugStringTest,AtomicBooleanAndNegation)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
TEST(SATCheckDebugStringTest,MultipleAtomicBooleans)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
TEST(SATCheckDebugStringTest,Implication)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
TEST(SATCheckDebugStringTest,Iff)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
TEST(SATCheckDebugStringTest,Xor)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
TEST(SATCheckDebugStringTest,ComplexBooleanWithNames)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
TEST(SATCheckDebugStringTest,ComplexBooleanWithLongNames)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