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 } // namespace
217