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>()), A(Context.arena()) {
24 }
25
26 DataflowAnalysisContext Context;
27 Arena &A;
28 };
29
TEST_F(DataflowAnalysisContextTest,DistinctTopsNotEquivalent)30 TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
31 auto &X = A.makeTopValue();
32 auto &Y = A.makeTopValue();
33 EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
34 }
35
TEST_F(DataflowAnalysisContextTest,TautologicalFlowConditionImplies)36 TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionImplies) {
37 Atom FC = A.makeFlowConditionToken();
38 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));
39 EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeLiteral(false)));
40 EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));
41 }
42
TEST_F(DataflowAnalysisContextTest,TautologicalFlowConditionAllows)43 TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionAllows) {
44 Atom FC = A.makeFlowConditionToken();
45 EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeLiteral(true)));
46 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));
47 EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));
48 }
49
TEST_F(DataflowAnalysisContextTest,ContradictoryFlowConditionImpliesAnything)50 TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionImpliesAnything) {
51 Atom FC = A.makeFlowConditionToken();
52 Context.addFlowConditionConstraint(FC, A.makeLiteral(false));
53 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));
54 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(false)));
55 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));
56 }
57
TEST_F(DataflowAnalysisContextTest,ContradictoryFlowConditionAllowsNothing)58 TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionAllowsNothing) {
59 Atom FC = A.makeFlowConditionToken();
60 Context.addFlowConditionConstraint(FC, A.makeLiteral(false));
61 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(true)));
62 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));
63 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));
64 }
65
TEST_F(DataflowAnalysisContextTest,AddFlowConditionConstraint)66 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
67 Atom FC = A.makeFlowConditionToken();
68 auto &C = A.makeAtomRef(A.makeAtom());
69 Context.addFlowConditionConstraint(FC, C);
70 EXPECT_TRUE(Context.flowConditionImplies(FC, C));
71 }
72
TEST_F(DataflowAnalysisContextTest,AddInvariant)73 TEST_F(DataflowAnalysisContextTest, AddInvariant) {
74 Atom FC = A.makeFlowConditionToken();
75 auto &C = A.makeAtomRef(A.makeAtom());
76 Context.addInvariant(C);
77 EXPECT_TRUE(Context.flowConditionImplies(FC, C));
78 }
79
TEST_F(DataflowAnalysisContextTest,InvariantAndFCConstraintInteract)80 TEST_F(DataflowAnalysisContextTest, InvariantAndFCConstraintInteract) {
81 Atom FC = A.makeFlowConditionToken();
82 auto &C = A.makeAtomRef(A.makeAtom());
83 auto &D = A.makeAtomRef(A.makeAtom());
84 Context.addInvariant(A.makeImplies(C, D));
85 Context.addFlowConditionConstraint(FC, C);
86 EXPECT_TRUE(Context.flowConditionImplies(FC, D));
87 }
88
TEST_F(DataflowAnalysisContextTest,ForkFlowCondition)89 TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
90 Atom FC1 = A.makeFlowConditionToken();
91 auto &C1 = A.makeAtomRef(A.makeAtom());
92 Context.addFlowConditionConstraint(FC1, C1);
93
94 // Forked flow condition inherits the constraints of its parent flow
95 // condition.
96 Atom FC2 = Context.forkFlowCondition(FC1);
97 EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
98
99 // Adding a new constraint to the forked flow condition does not affect its
100 // parent flow condition.
101 auto &C2 = A.makeAtomRef(A.makeAtom());
102 Context.addFlowConditionConstraint(FC2, C2);
103 EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
104 EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
105 }
106
TEST_F(DataflowAnalysisContextTest,JoinFlowConditions)107 TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
108 auto &C1 = A.makeAtomRef(A.makeAtom());
109 auto &C2 = A.makeAtomRef(A.makeAtom());
110 auto &C3 = A.makeAtomRef(A.makeAtom());
111
112 Atom FC1 = A.makeFlowConditionToken();
113 Context.addFlowConditionConstraint(FC1, C1);
114 Context.addFlowConditionConstraint(FC1, C3);
115
116 Atom FC2 = A.makeFlowConditionToken();
117 Context.addFlowConditionConstraint(FC2, C2);
118 Context.addFlowConditionConstraint(FC2, C3);
119
120 Atom FC3 = Context.joinFlowConditions(FC1, FC2);
121 EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
122 EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
123 EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
124 }
125
TEST_F(DataflowAnalysisContextTest,EquivBoolVals)126 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
127 auto &X = A.makeAtomRef(A.makeAtom());
128 auto &Y = A.makeAtomRef(A.makeAtom());
129 auto &Z = A.makeAtomRef(A.makeAtom());
130 auto &True = A.makeLiteral(true);
131 auto &False = A.makeLiteral(false);
132
133 // X == X
134 EXPECT_TRUE(Context.equivalentFormulas(X, X));
135 // X != Y
136 EXPECT_FALSE(Context.equivalentFormulas(X, Y));
137
138 // !X != X
139 EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
140 // !(!X) = X
141 EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
142
143 // (X || X) == X
144 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
145 // (X || Y) != X
146 EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
147 // (X || True) == True
148 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
149 // (X || False) == X
150 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
151
152 // (X && X) == X
153 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
154 // (X && Y) != X
155 EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
156 // (X && True) == X
157 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
158 // (X && False) == False
159 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
160
161 // (X || Y) == (Y || X)
162 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
163 // (X && Y) == (Y && X)
164 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
165
166 // ((X || Y) || Z) == (X || (Y || Z))
167 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
168 A.makeOr(X, A.makeOr(Y, Z))));
169 // ((X && Y) && Z) == (X && (Y && Z))
170 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),
171 A.makeAnd(X, A.makeAnd(Y, Z))));
172 }
173
174 } // namespace
175