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 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
280   auto &X = Context.createAtomicBoolValue();
281   auto &True = Context.getBoolLiteralValue(true);
282   auto &False = Context.getBoolLiteralValue(false);
283 
284   // FC = X
285   auto &FC = Context.makeFlowConditionToken();
286   Context.addFlowConditionConstraint(FC, X);
287 
288   // If X is true in FC, FC = X must be true
289   auto &FCWithXTrue =
290       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
291   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
292 
293   // If X is false in FC, FC = X must be false
294   auto &FC1WithXFalse =
295       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
296   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
297 }
298 
299 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
300   auto &X = Context.createAtomicBoolValue();
301   auto &True = Context.getBoolLiteralValue(true);
302   auto &False = Context.getBoolLiteralValue(false);
303 
304   // FC = !X
305   auto &FC = Context.makeFlowConditionToken();
306   Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));
307 
308   // If X is true in FC, FC = !X must be false
309   auto &FCWithXTrue =
310       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
311   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
312 
313   // If X is false in FC, FC = !X must be true
314   auto &FC1WithXFalse =
315       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
316   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
317 }
318 
319 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
320   auto &X = Context.createAtomicBoolValue();
321   auto &Y = Context.createAtomicBoolValue();
322   auto &True = Context.getBoolLiteralValue(true);
323   auto &False = Context.getBoolLiteralValue(false);
324 
325   // FC = X || Y
326   auto &FC = Context.makeFlowConditionToken();
327   Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
328 
329   // If X is true in FC, FC = X || Y must be true
330   auto &FCWithXTrue =
331       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
332   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
333 
334   // If X is false in FC, FC = X || Y is equivalent to evaluating Y
335   auto &FC1WithXFalse =
336       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
337   EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
338 }
339 
340 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
341   auto &X = Context.createAtomicBoolValue();
342   auto &Y = Context.createAtomicBoolValue();
343   auto &True = Context.getBoolLiteralValue(true);
344   auto &False = Context.getBoolLiteralValue(false);
345 
346   // FC = X && Y
347   auto &FC = Context.makeFlowConditionToken();
348   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
349 
350   // If X is true in FC, FC = X && Y is equivalent to evaluating Y
351   auto &FCWithXTrue =
352       Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
353   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
354 
355   // If X is false in FC, FC = X && Y must be false
356   auto &FCWithXFalse =
357       Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
358   EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
359 }
360 
361 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
362   auto &X = Context.createAtomicBoolValue();
363   auto &Y = Context.createAtomicBoolValue();
364   auto &Z = Context.createAtomicBoolValue();
365   auto &True = Context.getBoolLiteralValue(true);
366   auto &False = Context.getBoolLiteralValue(false);
367 
368   // FC = X && Y
369   auto &FC = Context.makeFlowConditionToken();
370   Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
371   // ForkedFC = FC && Z = X && Y && Z
372   auto &ForkedFC = Context.forkFlowCondition(FC);
373   Context.addFlowConditionConstraint(ForkedFC, Z);
374 
375   // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
376   // to evaluating the conjunction of the remaining values
377   auto &ForkedFCWithZTrue =
378       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
379   EXPECT_TRUE(Context.equivalentBoolValues(
380       ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
381   auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
382       ForkedFC, {{&Y, &True}, {&Z, &True}});
383   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
384 
385   // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
386   auto &ForkedFCWithXFalse =
387       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
388   auto &ForkedFCWithYFalse =
389       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
390   auto &ForkedFCWithZFalse =
391       Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
392   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
393   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
394   EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
395 }
396 
397 TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
398   auto &X = Context.createAtomicBoolValue();
399   auto &Y = Context.createAtomicBoolValue();
400   auto &Z = Context.createAtomicBoolValue();
401   auto &True = Context.getBoolLiteralValue(true);
402   auto &False = Context.getBoolLiteralValue(false);
403 
404   // FC1 = X
405   auto &FC1 = Context.makeFlowConditionToken();
406   Context.addFlowConditionConstraint(FC1, X);
407   // FC2 = Y
408   auto &FC2 = Context.makeFlowConditionToken();
409   Context.addFlowConditionConstraint(FC2, Y);
410   // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
411   auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
412   Context.addFlowConditionConstraint(JoinedFC, Z);
413 
414   // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
415   // to evaluating the remaining Z
416   auto &JoinedFCWithXTrue =
417       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
418   auto &JoinedFCWithYTrue =
419       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
420   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
421   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
422 
423   // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
424   // evaluating the remaining disjunction (X || Y)
425   auto &JoinedFCWithZTrue =
426       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
427   EXPECT_TRUE(Context.equivalentBoolValues(
428       JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
429 
430   // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
431   // to evaluating the conjunction of the other value and Z
432   auto &JoinedFCWithXFalse =
433       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
434   auto &JoinedFCWithYFalse =
435       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
436   EXPECT_TRUE(Context.equivalentBoolValues(
437       JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
438   EXPECT_TRUE(Context.equivalentBoolValues(
439       JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
440 
441   // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
442   auto &JoinedFCWithZFalse =
443       Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
444   EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
445 }
446 
447 } // namespace
448