1 //===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.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/DataflowAnalysisContext.h"
10 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
11 #include "gmock/gmock.h"
12 #include "gtest/gtest.h"
13 #include <memory>
14
15 namespace {
16
17 using namespace clang;
18 using namespace dataflow;
19
20 class DataflowAnalysisContextTest : public ::testing::Test {
21 protected:
DataflowAnalysisContextTest()22 DataflowAnalysisContextTest()
23 : Context(std::make_unique<WatchedLiteralsSolver>()) {}
24
25 DataflowAnalysisContext Context;
26 };
27
TEST_F(DataflowAnalysisContextTest,CreateAtomicBoolValueReturnsDistinctValues)28 TEST_F(DataflowAnalysisContextTest,
29 CreateAtomicBoolValueReturnsDistinctValues) {
30 auto &X = Context.createAtomicBoolValue();
31 auto &Y = Context.createAtomicBoolValue();
32 EXPECT_NE(&X, &Y);
33 }
34
TEST_F(DataflowAnalysisContextTest,GetOrCreateConjunctionReturnsSameExprGivenSameArgs)35 TEST_F(DataflowAnalysisContextTest,
36 GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
37 auto &X = Context.createAtomicBoolValue();
38 auto &XAndX = Context.getOrCreateConjunction(X, X);
39 EXPECT_EQ(&XAndX, &X);
40 }
41
TEST_F(DataflowAnalysisContextTest,GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls)42 TEST_F(DataflowAnalysisContextTest,
43 GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
44 auto &X = Context.createAtomicBoolValue();
45 auto &Y = Context.createAtomicBoolValue();
46 auto &XAndY1 = Context.getOrCreateConjunction(X, Y);
47 auto &XAndY2 = Context.getOrCreateConjunction(X, Y);
48 EXPECT_EQ(&XAndY1, &XAndY2);
49
50 auto &YAndX = Context.getOrCreateConjunction(Y, X);
51 EXPECT_EQ(&XAndY1, &YAndX);
52
53 auto &Z = Context.createAtomicBoolValue();
54 auto &XAndZ = Context.getOrCreateConjunction(X, Z);
55 EXPECT_NE(&XAndY1, &XAndZ);
56 }
57
TEST_F(DataflowAnalysisContextTest,GetOrCreateDisjunctionReturnsSameExprGivenSameArgs)58 TEST_F(DataflowAnalysisContextTest,
59 GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
60 auto &X = Context.createAtomicBoolValue();
61 auto &XOrX = Context.getOrCreateDisjunction(X, X);
62 EXPECT_EQ(&XOrX, &X);
63 }
64
TEST_F(DataflowAnalysisContextTest,GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls)65 TEST_F(DataflowAnalysisContextTest,
66 GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
67 auto &X = Context.createAtomicBoolValue();
68 auto &Y = Context.createAtomicBoolValue();
69 auto &XOrY1 = Context.getOrCreateDisjunction(X, Y);
70 auto &XOrY2 = Context.getOrCreateDisjunction(X, Y);
71 EXPECT_EQ(&XOrY1, &XOrY2);
72
73 auto &YOrX = Context.getOrCreateDisjunction(Y, X);
74 EXPECT_EQ(&XOrY1, &YOrX);
75
76 auto &Z = Context.createAtomicBoolValue();
77 auto &XOrZ = Context.getOrCreateDisjunction(X, Z);
78 EXPECT_NE(&XOrY1, &XOrZ);
79 }
80
TEST_F(DataflowAnalysisContextTest,GetOrCreateNegationReturnsSameExprOnSubsequentCalls)81 TEST_F(DataflowAnalysisContextTest,
82 GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
83 auto &X = Context.createAtomicBoolValue();
84 auto &NotX1 = Context.getOrCreateNegation(X);
85 auto &NotX2 = Context.getOrCreateNegation(X);
86 EXPECT_EQ(&NotX1, &NotX2);
87
88 auto &Y = Context.createAtomicBoolValue();
89 auto &NotY = Context.getOrCreateNegation(Y);
90 EXPECT_NE(&NotX1, &NotY);
91 }
92
TEST_F(DataflowAnalysisContextTest,GetOrCreateImplicationReturnsTrueGivenSameArgs)93 TEST_F(DataflowAnalysisContextTest,
94 GetOrCreateImplicationReturnsTrueGivenSameArgs) {
95 auto &X = Context.createAtomicBoolValue();
96 auto &XImpliesX = Context.getOrCreateImplication(X, X);
97 EXPECT_EQ(&XImpliesX, &Context.getBoolLiteralValue(true));
98 }
99
TEST_F(DataflowAnalysisContextTest,GetOrCreateImplicationReturnsSameExprOnSubsequentCalls)100 TEST_F(DataflowAnalysisContextTest,
101 GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
102 auto &X = Context.createAtomicBoolValue();
103 auto &Y = Context.createAtomicBoolValue();
104 auto &XImpliesY1 = Context.getOrCreateImplication(X, Y);
105 auto &XImpliesY2 = Context.getOrCreateImplication(X, Y);
106 EXPECT_EQ(&XImpliesY1, &XImpliesY2);
107
108 auto &YImpliesX = Context.getOrCreateImplication(Y, X);
109 EXPECT_NE(&XImpliesY1, &YImpliesX);
110
111 auto &Z = Context.createAtomicBoolValue();
112 auto &XImpliesZ = Context.getOrCreateImplication(X, Z);
113 EXPECT_NE(&XImpliesY1, &XImpliesZ);
114 }
115
TEST_F(DataflowAnalysisContextTest,GetOrCreateIffReturnsTrueGivenSameArgs)116 TEST_F(DataflowAnalysisContextTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
117 auto &X = Context.createAtomicBoolValue();
118 auto &XIffX = Context.getOrCreateIff(X, X);
119 EXPECT_EQ(&XIffX, &Context.getBoolLiteralValue(true));
120 }
121
TEST_F(DataflowAnalysisContextTest,GetOrCreateIffReturnsSameExprOnSubsequentCalls)122 TEST_F(DataflowAnalysisContextTest,
123 GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
124 auto &X = Context.createAtomicBoolValue();
125 auto &Y = Context.createAtomicBoolValue();
126 auto &XIffY1 = Context.getOrCreateIff(X, Y);
127 auto &XIffY2 = Context.getOrCreateIff(X, Y);
128 EXPECT_EQ(&XIffY1, &XIffY2);
129
130 auto &YIffX = Context.getOrCreateIff(Y, X);
131 EXPECT_EQ(&XIffY1, &YIffX);
132
133 auto &Z = Context.createAtomicBoolValue();
134 auto &XIffZ = Context.getOrCreateIff(X, Z);
135 EXPECT_NE(&XIffY1, &XIffZ);
136 }
137
TEST_F(DataflowAnalysisContextTest,EmptyFlowCondition)138 TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
139 auto &FC = Context.makeFlowConditionToken();
140 auto &C = Context.createAtomicBoolValue();
141 EXPECT_FALSE(Context.flowConditionImplies(FC, C));
142 }
143
TEST_F(DataflowAnalysisContextTest,AddFlowConditionConstraint)144 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
145 auto &FC = Context.makeFlowConditionToken();
146 auto &C = Context.createAtomicBoolValue();
147 Context.addFlowConditionConstraint(FC, C);
148 EXPECT_TRUE(Context.flowConditionImplies(FC, C));
149 }
150
TEST_F(DataflowAnalysisContextTest,ForkFlowCondition)151 TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
152 auto &FC1 = Context.makeFlowConditionToken();
153 auto &C1 = Context.createAtomicBoolValue();
154 Context.addFlowConditionConstraint(FC1, C1);
155
156 // Forked flow condition inherits the constraints of its parent flow
157 // condition.
158 auto &FC2 = Context.forkFlowCondition(FC1);
159 EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
160
161 // Adding a new constraint to the forked flow condition does not affect its
162 // parent flow condition.
163 auto &C2 = Context.createAtomicBoolValue();
164 Context.addFlowConditionConstraint(FC2, C2);
165 EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
166 EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
167 }
168
TEST_F(DataflowAnalysisContextTest,JoinFlowConditions)169 TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
170 auto &C1 = Context.createAtomicBoolValue();
171 auto &C2 = Context.createAtomicBoolValue();
172 auto &C3 = Context.createAtomicBoolValue();
173
174 auto &FC1 = Context.makeFlowConditionToken();
175 Context.addFlowConditionConstraint(FC1, C1);
176 Context.addFlowConditionConstraint(FC1, C3);
177
178 auto &FC2 = Context.makeFlowConditionToken();
179 Context.addFlowConditionConstraint(FC2, C2);
180 Context.addFlowConditionConstraint(FC2, C3);
181
182 auto &FC3 = Context.joinFlowConditions(FC1, FC2);
183 EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
184 EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
185 EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
186 }
187
TEST_F(DataflowAnalysisContextTest,FlowConditionTautologies)188 TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
189 // Fresh flow condition with empty/no constraints is always true.
190 auto &FC1 = Context.makeFlowConditionToken();
191 EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
192
193 // Literal `true` is always true.
194 auto &FC2 = Context.makeFlowConditionToken();
195 Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true));
196 EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
197
198 // Literal `false` is never true.
199 auto &FC3 = Context.makeFlowConditionToken();
200 Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false));
201 EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
202
203 // We can't prove that an arbitrary bool A is always true...
204 auto &C1 = Context.createAtomicBoolValue();
205 auto &FC4 = Context.makeFlowConditionToken();
206 Context.addFlowConditionConstraint(FC4, C1);
207 EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
208
209 // ... but we can prove A || !A is true.
210 auto &FC5 = Context.makeFlowConditionToken();
211 Context.addFlowConditionConstraint(
212 FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1)));
213 EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
214 }
215
TEST_F(DataflowAnalysisContextTest,EquivBoolVals)216 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
217 auto &X = Context.createAtomicBoolValue();
218 auto &Y = Context.createAtomicBoolValue();
219 auto &Z = Context.createAtomicBoolValue();
220 auto &True = Context.getBoolLiteralValue(true);
221 auto &False = Context.getBoolLiteralValue(false);
222
223 // X == X
224 EXPECT_TRUE(Context.equivalentBoolValues(X, X));
225 // X != Y
226 EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
227
228 // !X != X
229 EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));
230 // !(!X) = X
231 EXPECT_TRUE(Context.equivalentBoolValues(
232 Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));
233
234 // (X || X) == X
235 EXPECT_TRUE(
236 Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));
237 // (X || Y) != X
238 EXPECT_FALSE(
239 Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));
240 // (X || True) == True
241 EXPECT_TRUE(Context.equivalentBoolValues(
242 Context.getOrCreateDisjunction(X, True), True));
243 // (X || False) == X
244 EXPECT_TRUE(Context.equivalentBoolValues(
245 Context.getOrCreateDisjunction(X, False), X));
246
247 // (X && X) == X
248 EXPECT_TRUE(
249 Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X));
250 // (X && Y) != X
251 EXPECT_FALSE(
252 Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X));
253 // (X && True) == X
254 EXPECT_TRUE(
255 Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X));
256 // (X && False) == False
257 EXPECT_TRUE(Context.equivalentBoolValues(
258 Context.getOrCreateConjunction(X, False), False));
259
260 // (X || Y) == (Y || X)
261 EXPECT_TRUE(
262 Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y),
263 Context.getOrCreateDisjunction(Y, X)));
264 // (X && Y) == (Y && X)
265 EXPECT_TRUE(
266 Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y),
267 Context.getOrCreateConjunction(Y, X)));
268
269 // ((X || Y) || Z) == (X || (Y || Z))
270 EXPECT_TRUE(Context.equivalentBoolValues(
271 Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),
272 Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));
273 // ((X && Y) && Z) == (X && (Y && Z))
274 EXPECT_TRUE(Context.equivalentBoolValues(
275 Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),
276 Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
277 }
278
279 #if !defined(NDEBUG) && GTEST_HAS_DEATH_TEST
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionsTrueUnchanged)280 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsTrueUnchanged) {
281 auto &True = Context.getBoolLiteralValue(true);
282 auto &Other = Context.createAtomicBoolValue();
283
284 // FC = True
285 auto &FC = Context.makeFlowConditionToken();
286 Context.addFlowConditionConstraint(FC, True);
287
288 // `True` should never be substituted
289 EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&True, &Other}}),
290 "Do not substitute true/false boolean literals");
291 }
292
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionsFalseUnchanged)293 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsFalseUnchanged) {
294 auto &False = Context.getBoolLiteralValue(false);
295 auto &Other = Context.createAtomicBoolValue();
296
297 // FC = False
298 auto &FC = Context.makeFlowConditionToken();
299 Context.addFlowConditionConstraint(FC, False);
300
301 // `False` should never be substituted
302 EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&False, &Other}}),
303 "Do not substitute true/false boolean literals");
304 }
305 #endif
306
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionContainingAtomic)307 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) {
308 auto &X = Context.createAtomicBoolValue();
309 auto &True = Context.getBoolLiteralValue(true);
310 auto &False = Context.getBoolLiteralValue(false);
311
312 // FC = X
313 auto &FC = Context.makeFlowConditionToken();
314 Context.addFlowConditionConstraint(FC, X);
315
316 // If X is true, FC is true
317 auto &FCWithXTrue =
318 Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
319 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
320
321 // If X is false, FC is false
322 auto &FC1WithXFalse =
323 Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
324 EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
325 }
326
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionContainingNegation)327 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingNegation) {
328 auto &X = Context.createAtomicBoolValue();
329 auto &True = Context.getBoolLiteralValue(true);
330 auto &False = Context.getBoolLiteralValue(false);
331
332 // FC = !X
333 auto &FC = Context.makeFlowConditionToken();
334 Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));
335
336 // If X is true, FC is false
337 auto &FCWithXTrue =
338 Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
339 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
340
341 // If X is false, FC is true
342 auto &FC1WithXFalse =
343 Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
344 EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
345 }
346
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionContainingDisjunction)347 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingDisjunction) {
348 auto &X = Context.createAtomicBoolValue();
349 auto &Y = Context.createAtomicBoolValue();
350 auto &True = Context.getBoolLiteralValue(true);
351 auto &False = Context.getBoolLiteralValue(false);
352
353 // FC = X || Y
354 auto &FC = Context.makeFlowConditionToken();
355 Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
356
357 // If X is true, FC is true
358 auto &FCWithXTrue =
359 Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
360 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
361
362 // If X is false, FC is equivalent to Y
363 auto &FC1WithXFalse =
364 Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
365 EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
366 }
367
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionContainingConjunction)368 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingConjunction) {
369 auto &X = Context.createAtomicBoolValue();
370 auto &Y = Context.createAtomicBoolValue();
371 auto &True = Context.getBoolLiteralValue(true);
372 auto &False = Context.getBoolLiteralValue(false);
373
374 // FC = X && Y
375 auto &FC = Context.makeFlowConditionToken();
376 Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
377
378 // If X is true, FC is equivalent to Y
379 auto &FCWithXTrue =
380 Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
381 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
382
383 // If X is false, FC is false
384 auto &FCWithXFalse =
385 Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
386 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
387 }
388
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionContainingImplication)389 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingImplication) {
390 auto &X = Context.createAtomicBoolValue();
391 auto &Y = Context.createAtomicBoolValue();
392 auto &True = Context.getBoolLiteralValue(true);
393 auto &False = Context.getBoolLiteralValue(false);
394
395 // FC = (X => Y)
396 auto &FC = Context.makeFlowConditionToken();
397 Context.addFlowConditionConstraint(FC, Context.getOrCreateImplication(X, Y));
398
399 // If X is true, FC is equivalent to Y
400 auto &FCWithXTrue =
401 Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
402 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
403
404 // If X is false, FC is true
405 auto &FC1WithXFalse =
406 Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
407 EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
408
409 // If Y is true, FC is true
410 auto &FCWithYTrue =
411 Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});
412 EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, True));
413
414 // If Y is false, FC is equivalent to !X
415 auto &FCWithYFalse =
416 Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});
417 EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,
418 Context.getOrCreateNegation(X)));
419 }
420
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionContainingBiconditional)421 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingBiconditional) {
422 auto &X = Context.createAtomicBoolValue();
423 auto &Y = Context.createAtomicBoolValue();
424 auto &True = Context.getBoolLiteralValue(true);
425 auto &False = Context.getBoolLiteralValue(false);
426
427 // FC = (X <=> Y)
428 auto &FC = Context.makeFlowConditionToken();
429 Context.addFlowConditionConstraint(FC, Context.getOrCreateIff(X, Y));
430
431 // If X is true, FC is equivalent to Y
432 auto &FCWithXTrue =
433 Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
434 EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
435
436 // If X is false, FC is equivalent to !Y
437 auto &FC1WithXFalse =
438 Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
439 EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse,
440 Context.getOrCreateNegation(Y)));
441
442 // If Y is true, FC is equivalent to X
443 auto &FCWithYTrue =
444 Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});
445 EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, X));
446
447 // If Y is false, FC is equivalent to !X
448 auto &FCWithYFalse =
449 Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});
450 EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,
451 Context.getOrCreateNegation(X)));
452 }
453
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionsForkedFC)454 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
455 auto &X = Context.createAtomicBoolValue();
456 auto &Y = Context.createAtomicBoolValue();
457 auto &Z = Context.createAtomicBoolValue();
458 auto &True = Context.getBoolLiteralValue(true);
459 auto &False = Context.getBoolLiteralValue(false);
460
461 // FC = X && Y
462 auto &FC = Context.makeFlowConditionToken();
463 Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
464 // ForkedFC = FC && Z = X && Y && Z
465 auto &ForkedFC = Context.forkFlowCondition(FC);
466 Context.addFlowConditionConstraint(ForkedFC, Z);
467
468 // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
469 // to evaluating the conjunction of the remaining values
470 auto &ForkedFCWithZTrue =
471 Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
472 EXPECT_TRUE(Context.equivalentBoolValues(
473 ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
474 auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
475 ForkedFC, {{&Y, &True}, {&Z, &True}});
476 EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
477
478 // If any of X,Y,Z is false, ForkedFC is false
479 auto &ForkedFCWithXFalse =
480 Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
481 auto &ForkedFCWithYFalse =
482 Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
483 auto &ForkedFCWithZFalse =
484 Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
485 EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
486 EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
487 EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
488 }
489
TEST_F(DataflowAnalysisContextTest,SubstituteFlowConditionsJoinedFC)490 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
491 auto &X = Context.createAtomicBoolValue();
492 auto &Y = Context.createAtomicBoolValue();
493 auto &Z = Context.createAtomicBoolValue();
494 auto &True = Context.getBoolLiteralValue(true);
495 auto &False = Context.getBoolLiteralValue(false);
496
497 // FC1 = X
498 auto &FC1 = Context.makeFlowConditionToken();
499 Context.addFlowConditionConstraint(FC1, X);
500 // FC2 = Y
501 auto &FC2 = Context.makeFlowConditionToken();
502 Context.addFlowConditionConstraint(FC2, Y);
503 // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
504 auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
505 Context.addFlowConditionConstraint(JoinedFC, Z);
506
507 // If any of X, Y is true, JoinedFC is equivalent to Z
508 auto &JoinedFCWithXTrue =
509 Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
510 auto &JoinedFCWithYTrue =
511 Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
512 EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
513 EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
514
515 // If Z is true, JoinedFC is equivalent to (X || Y)
516 auto &JoinedFCWithZTrue =
517 Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
518 EXPECT_TRUE(Context.equivalentBoolValues(
519 JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
520
521 // If any of X, Y is false, JoinedFC is equivalent to the conjunction of the
522 // other value and Z
523 auto &JoinedFCWithXFalse =
524 Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
525 auto &JoinedFCWithYFalse =
526 Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
527 EXPECT_TRUE(Context.equivalentBoolValues(
528 JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
529 EXPECT_TRUE(Context.equivalentBoolValues(
530 JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
531
532 // If Z is false, JoinedFC is false
533 auto &JoinedFCWithZFalse =
534 Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
535 EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
536 }
537
538 } // namespace
539