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, SubstituteFlowConditionsAtomicFC) {
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 in FC, FC = X must be true
317   auto &FCWithXTrue =
318       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
319   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
320 
321   // If X is false in FC, FC = X must be false
322   auto &FC1WithXFalse =
323       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
324   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
325 }
326 
327 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
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 in FC, FC = !X must be false
337   auto &FCWithXTrue =
338       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
339   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
340 
341   // If X is false in FC, FC = !X must be true
342   auto &FC1WithXFalse =
343       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
344   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
345 }
346 
347 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
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 in FC, FC = X || Y must be true
358   auto &FCWithXTrue =
359       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
360   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
361 
362   // If X is false in FC, FC = X || Y is equivalent to evaluating Y
363   auto &FC1WithXFalse =
364       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
365   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
366 }
367 
368 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
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 in FC, FC = X && Y is equivalent to evaluating Y
379   auto &FCWithXTrue =
380       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
381   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
382 
383   // If X is false in FC, FC = X && Y must be false
384   auto &FCWithXFalse =
385       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
386   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
387 }
388 
389 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
390   auto &X = Context.createAtomicBoolValue();
391   auto &Y = Context.createAtomicBoolValue();
392   auto &Z = Context.createAtomicBoolValue();
393   auto &True = Context.getBoolLiteralValue(true);
394   auto &False = Context.getBoolLiteralValue(false);
395 
396   // FC = X && Y
397   auto &FC = Context.makeFlowConditionToken();
398   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
399   // ForkedFC = FC && Z = X && Y && Z
400   auto &ForkedFC = Context.forkFlowCondition(FC);
401   Context.addFlowConditionConstraint(ForkedFC, Z);
402 
403   // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
404   // to evaluating the conjunction of the remaining values
405   auto &ForkedFCWithZTrue =
406       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
407   EXPECT_TRUE(Context.equivalentBoolValues(
408       ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
409   auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
410       ForkedFC, {{&Y, &True}, {&Z, &True}});
411   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
412 
413   // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
414   auto &ForkedFCWithXFalse =
415       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
416   auto &ForkedFCWithYFalse =
417       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
418   auto &ForkedFCWithZFalse =
419       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
420   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
421   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
422   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
423 }
424 
425 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
426   auto &X = Context.createAtomicBoolValue();
427   auto &Y = Context.createAtomicBoolValue();
428   auto &Z = Context.createAtomicBoolValue();
429   auto &True = Context.getBoolLiteralValue(true);
430   auto &False = Context.getBoolLiteralValue(false);
431 
432   // FC1 = X
433   auto &FC1 = Context.makeFlowConditionToken();
434   Context.addFlowConditionConstraint(FC1, X);
435   // FC2 = Y
436   auto &FC2 = Context.makeFlowConditionToken();
437   Context.addFlowConditionConstraint(FC2, Y);
438   // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
439   auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
440   Context.addFlowConditionConstraint(JoinedFC, Z);
441 
442   // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
443   // to evaluating the remaining Z
444   auto &JoinedFCWithXTrue =
445       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
446   auto &JoinedFCWithYTrue =
447       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
448   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
449   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
450 
451   // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
452   // evaluating the remaining disjunction (X || Y)
453   auto &JoinedFCWithZTrue =
454       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
455   EXPECT_TRUE(Context.equivalentBoolValues(
456       JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
457 
458   // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
459   // to evaluating the conjunction of the other value and Z
460   auto &JoinedFCWithXFalse =
461       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
462   auto &JoinedFCWithYFalse =
463       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
464   EXPECT_TRUE(Context.equivalentBoolValues(
465       JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
466   EXPECT_TRUE(Context.equivalentBoolValues(
467       JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
468 
469   // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
470   auto &JoinedFCWithZFalse =
471       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
472   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
473 }
474 
475 } // namespace
476