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
15namespace clang::dataflow {
16namespace {
17using llvm::HasValue;
18using testing::Ref;
19
20class ArenaTest : public ::testing::Test {
21protected:
22 Arena A;
23};
24
25TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
26 auto &X = A.makeAtomValue();
27 auto &Y = A.makeAtomValue();
28 EXPECT_NE(&X, &Y);
29}
30
31TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
32 auto &X = A.makeTopValue();
33 auto &Y = A.makeTopValue();
34 EXPECT_NE(&X, &Y);
35}
36
37TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
38 auto &X = A.makeAtomRef(A: A.makeAtom());
39 auto &Y = A.makeAtomRef(A: A.makeAtom());
40 auto &XAndY1 = A.makeAnd(LHS: X, RHS: Y);
41 auto &XAndY2 = A.makeAnd(LHS: X, RHS: Y);
42 EXPECT_EQ(&XAndY1, &XAndY2);
43
44 auto &YAndX = A.makeAnd(LHS: Y, RHS: X);
45 EXPECT_EQ(&XAndY1, &YAndX);
46
47 auto &Z = A.makeAtomRef(A: A.makeAtom());
48 auto &XAndZ = A.makeAnd(LHS: X, RHS: Z);
49 EXPECT_NE(&XAndY1, &XAndZ);
50}
51
52TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
53 auto &X = A.makeAtomRef(A: A.makeAtom());
54 auto &Y = A.makeAtomRef(A: A.makeAtom());
55 auto &XOrY1 = A.makeOr(LHS: X, RHS: Y);
56 auto &XOrY2 = A.makeOr(LHS: X, RHS: Y);
57 EXPECT_EQ(&XOrY1, &XOrY2);
58
59 auto &YOrX = A.makeOr(LHS: Y, RHS: X);
60 EXPECT_EQ(&XOrY1, &YOrX);
61
62 auto &Z = A.makeAtomRef(A: A.makeAtom());
63 auto &XOrZ = A.makeOr(LHS: X, RHS: Z);
64 EXPECT_NE(&XOrY1, &XOrZ);
65}
66
67TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
68 auto &X = A.makeAtomRef(A: A.makeAtom());
69 auto &NotX1 = A.makeNot(Val: X);
70 auto &NotX2 = A.makeNot(Val: X);
71 EXPECT_EQ(&NotX1, &NotX2);
72 auto &Y = A.makeAtomRef(A: A.makeAtom());
73 auto &NotY = A.makeNot(Val: Y);
74 EXPECT_NE(&NotX1, &NotY);
75}
76
77TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
78 auto &X = A.makeAtomRef(A: A.makeAtom());
79 auto &Y = A.makeAtomRef(A: A.makeAtom());
80 auto &XImpliesY1 = A.makeImplies(LHS: X, RHS: Y);
81 auto &XImpliesY2 = A.makeImplies(LHS: X, RHS: Y);
82 EXPECT_EQ(&XImpliesY1, &XImpliesY2);
83
84 auto &YImpliesX = A.makeImplies(LHS: Y, RHS: X);
85 EXPECT_NE(&XImpliesY1, &YImpliesX);
86
87 auto &Z = A.makeAtomRef(A: A.makeAtom());
88 auto &XImpliesZ = A.makeImplies(LHS: X, RHS: Z);
89 EXPECT_NE(&XImpliesY1, &XImpliesZ);
90}
91
92TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
93 auto &X = A.makeAtomRef(A: A.makeAtom());
94 auto &Y = A.makeAtomRef(A: A.makeAtom());
95 auto &XIffY1 = A.makeEquals(LHS: X, RHS: Y);
96 auto &XIffY2 = A.makeEquals(LHS: X, RHS: Y);
97 EXPECT_EQ(&XIffY1, &XIffY2);
98
99 auto &YIffX = A.makeEquals(LHS: Y, RHS: X);
100 EXPECT_EQ(&XIffY1, &YIffX);
101
102 auto &Z = A.makeAtomRef(A: A.makeAtom());
103 auto &XIffZ = A.makeEquals(LHS: X, RHS: Z);
104 EXPECT_NE(&XIffY1, &XIffZ);
105}
106
107TEST_F(ArenaTest, Interning) {
108 Atom X = A.makeAtom();
109 Atom Y = A.makeAtom();
110 const Formula &F1 = A.makeAnd(LHS: A.makeAtomRef(A: X), RHS: A.makeAtomRef(A: Y));
111 const Formula &F2 = A.makeAnd(LHS: A.makeAtomRef(A: Y), RHS: A.makeAtomRef(A: 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
119TEST_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
156V1 V2
157 ^)"));
158}
159
160TEST_F(ArenaTest, IdentitySimplification) {
161 auto &X = A.makeAtomRef(A: 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
170TEST_F(ArenaTest, LiteralSimplification) {
171 auto &X = A.makeAtomRef(A: 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

source code of clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp