1 //===- ArenaTest.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/Arena.h"
10 #include "llvm/Support/ScopedPrinter.h"
11 #include "llvm/Testing/Support/Error.h"
12 #include "gmock/gmock.h"
13 #include "gtest/gtest.h"
14
15 namespace clang::dataflow {
16 namespace {
17 using llvm::HasValue;
18 using testing::Ref;
19
20 class ArenaTest : public ::testing::Test {
21 protected:
22 Arena A;
23 };
24
TEST_F(ArenaTest,CreateAtomicBoolValueReturnsDistinctValues)25 TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
26 auto &X = A.makeAtomValue();
27 auto &Y = A.makeAtomValue();
28 EXPECT_NE(&X, &Y);
29 }
30
TEST_F(ArenaTest,CreateTopBoolValueReturnsDistinctValues)31 TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
32 auto &X = A.makeTopValue();
33 auto &Y = A.makeTopValue();
34 EXPECT_NE(&X, &Y);
35 }
36
TEST_F(ArenaTest,GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls)37 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
38 auto &X = A.makeAtomRef(A.makeAtom());
39 auto &Y = A.makeAtomRef(A.makeAtom());
40 auto &XAndY1 = A.makeAnd(X, Y);
41 auto &XAndY2 = A.makeAnd(X, Y);
42 EXPECT_EQ(&XAndY1, &XAndY2);
43
44 auto &YAndX = A.makeAnd(Y, X);
45 EXPECT_EQ(&XAndY1, &YAndX);
46
47 auto &Z = A.makeAtomRef(A.makeAtom());
48 auto &XAndZ = A.makeAnd(X, Z);
49 EXPECT_NE(&XAndY1, &XAndZ);
50 }
51
TEST_F(ArenaTest,GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls)52 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
53 auto &X = A.makeAtomRef(A.makeAtom());
54 auto &Y = A.makeAtomRef(A.makeAtom());
55 auto &XOrY1 = A.makeOr(X, Y);
56 auto &XOrY2 = A.makeOr(X, Y);
57 EXPECT_EQ(&XOrY1, &XOrY2);
58
59 auto &YOrX = A.makeOr(Y, X);
60 EXPECT_EQ(&XOrY1, &YOrX);
61
62 auto &Z = A.makeAtomRef(A.makeAtom());
63 auto &XOrZ = A.makeOr(X, Z);
64 EXPECT_NE(&XOrY1, &XOrZ);
65 }
66
TEST_F(ArenaTest,GetOrCreateNegationReturnsSameExprOnSubsequentCalls)67 TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
68 auto &X = A.makeAtomRef(A.makeAtom());
69 auto &NotX1 = A.makeNot(X);
70 auto &NotX2 = A.makeNot(X);
71 EXPECT_EQ(&NotX1, &NotX2);
72 auto &Y = A.makeAtomRef(A.makeAtom());
73 auto &NotY = A.makeNot(Y);
74 EXPECT_NE(&NotX1, &NotY);
75 }
76
TEST_F(ArenaTest,GetOrCreateImplicationReturnsSameExprOnSubsequentCalls)77 TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
78 auto &X = A.makeAtomRef(A.makeAtom());
79 auto &Y = A.makeAtomRef(A.makeAtom());
80 auto &XImpliesY1 = A.makeImplies(X, Y);
81 auto &XImpliesY2 = A.makeImplies(X, Y);
82 EXPECT_EQ(&XImpliesY1, &XImpliesY2);
83
84 auto &YImpliesX = A.makeImplies(Y, X);
85 EXPECT_NE(&XImpliesY1, &YImpliesX);
86
87 auto &Z = A.makeAtomRef(A.makeAtom());
88 auto &XImpliesZ = A.makeImplies(X, Z);
89 EXPECT_NE(&XImpliesY1, &XImpliesZ);
90 }
91
TEST_F(ArenaTest,GetOrCreateIffReturnsSameExprOnSubsequentCalls)92 TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
93 auto &X = A.makeAtomRef(A.makeAtom());
94 auto &Y = A.makeAtomRef(A.makeAtom());
95 auto &XIffY1 = A.makeEquals(X, Y);
96 auto &XIffY2 = A.makeEquals(X, Y);
97 EXPECT_EQ(&XIffY1, &XIffY2);
98
99 auto &YIffX = A.makeEquals(Y, X);
100 EXPECT_EQ(&XIffY1, &YIffX);
101
102 auto &Z = A.makeAtomRef(A.makeAtom());
103 auto &XIffZ = A.makeEquals(X, Z);
104 EXPECT_NE(&XIffY1, &XIffZ);
105 }
106
TEST_F(ArenaTest,Interning)107 TEST_F(ArenaTest, Interning) {
108 Atom X = A.makeAtom();
109 Atom Y = A.makeAtom();
110 const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));
111 const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
112 EXPECT_EQ(&F1, &F2);
113 BoolValue &B1 = A.makeBoolValue(F1);
114 BoolValue &B2 = A.makeBoolValue(F2);
115 EXPECT_EQ(&B1, &B2);
116 EXPECT_EQ(&B1.formula(), &F1);
117 }
118
TEST_F(ArenaTest,ParseFormula)119 TEST_F(ArenaTest, ParseFormula) {
120 Atom V5{5};
121 Atom V6{6};
122 EXPECT_THAT_EXPECTED(A.parseFormula("V5"), HasValue(Ref(A.makeAtomRef(V5))));
123 EXPECT_THAT_EXPECTED(A.parseFormula("true"),
124 HasValue(Ref(A.makeLiteral(true))));
125 EXPECT_THAT_EXPECTED(A.parseFormula("!V5"),
126 HasValue(Ref(A.makeNot(A.makeAtomRef(V5)))));
127
128 EXPECT_THAT_EXPECTED(
129 A.parseFormula("(V5 = V6)"),
130 HasValue(Ref(A.makeEquals(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
131 EXPECT_THAT_EXPECTED(
132 A.parseFormula("(V5 => V6)"),
133 HasValue(Ref(A.makeImplies(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
134 EXPECT_THAT_EXPECTED(
135 A.parseFormula("(V5 & V6)"),
136 HasValue(Ref(A.makeAnd(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
137 EXPECT_THAT_EXPECTED(
138 A.parseFormula("(V5 | V6)"),
139 HasValue(Ref(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
140
141 EXPECT_THAT_EXPECTED(
142 A.parseFormula("((V5 & (V6 & !false)) => ((V5 | V6) | false))"),
143 HasValue(Ref(
144 A.makeImplies(A.makeAnd(A.makeAtomRef(V5),
145 A.makeAnd(A.makeAtomRef(V6),
146 A.makeNot(A.makeLiteral(false)))),
147 A.makeOr(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)),
148 A.makeLiteral(false))))));
149
150 EXPECT_THAT_EXPECTED(
151 A.parseFormula("(V0 => error)"), llvm::FailedWithMessage(R"(bad formula at offset 7
152 (V0 => error)
153 ^)"));
154 EXPECT_THAT_EXPECTED(
155 A.parseFormula("V1 V2"), llvm::FailedWithMessage(R"(bad formula at offset 3
156 V1 V2
157 ^)"));
158 }
159
TEST_F(ArenaTest,IdentitySimplification)160 TEST_F(ArenaTest, IdentitySimplification) {
161 auto &X = A.makeAtomRef(A.makeAtom());
162
163 EXPECT_EQ(&X, &A.makeAnd(X, X));
164 EXPECT_EQ(&X, &A.makeOr(X, X));
165 EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
166 EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
167 EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
168 }
169
TEST_F(ArenaTest,LiteralSimplification)170 TEST_F(ArenaTest, LiteralSimplification) {
171 auto &X = A.makeAtomRef(A.makeAtom());
172
173 EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
174 EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
175
176 EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
177 EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
178
179 EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
180 EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
181 EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
182 EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
183
184 EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
185 EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
186
187 EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
188 EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
189 }
190
191 } // namespace
192 } // namespace clang::dataflow
193