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:
22   DataflowAnalysisContextTest()
23       : Context(std::make_unique<WatchedLiteralsSolver>()) {}
24 
25   DataflowAnalysisContext Context;
26 };
27 
28 TEST_F(DataflowAnalysisContextTest,
29        CreateAtomicBoolValueReturnsDistinctValues) {
30   auto &X = Context.createAtomicBoolValue();
31   auto &Y = Context.createAtomicBoolValue();
32   EXPECT_NE(&X, &Y);
33 }
34 
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 
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 
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 
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 
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 
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 
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 
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 
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 
138 TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
139   auto &FC = Context.makeFlowConditionToken();
140   auto &C = Context.createAtomicBoolValue();
141   EXPECT_FALSE(Context.flowConditionImplies(FC, C));
142 }
143 
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 
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 
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 
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 
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
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 
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 
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 
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 
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 
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 
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 
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 
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 
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