1 //===- unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.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/SimplifyConstraints.h"
10 #include "TestingSupport.h"
11 #include "clang/Analysis/FlowSensitive/Arena.h"
12 #include "gmock/gmock.h"
13 #include "gtest/gtest.h"
14
15 namespace {
16
17 using namespace clang;
18 using namespace dataflow;
19
20 using ::testing::ElementsAre;
21 using ::testing::IsEmpty;
22
23 class SimplifyConstraintsTest : public ::testing::Test {
24 protected:
parse(StringRef Lines)25 llvm::SetVector<const Formula *> parse(StringRef Lines) {
26 std::vector<const Formula *> formulas = test::parseFormulas(A, Lines);
27 llvm::SetVector<const Formula *> Constraints(formulas.begin(),
28 formulas.end());
29 return Constraints;
30 }
31
simplify(StringRef Lines,SimplifyConstraintsInfo & Info)32 llvm::SetVector<const Formula *> simplify(StringRef Lines,
33 SimplifyConstraintsInfo &Info) {
34 llvm::SetVector<const Formula *> Constraints = parse(Lines);
35 simplifyConstraints(Constraints, A, &Info);
36 return Constraints;
37 }
38
39 Arena A;
40 };
41
printConstraints(const llvm::SetVector<const Formula * > & Constraints,raw_ostream & OS)42 void printConstraints(const llvm::SetVector<const Formula *> &Constraints,
43 raw_ostream &OS) {
44 if (Constraints.empty()) {
45 OS << "empty";
46 return;
47 }
48 for (const auto *Constraint : Constraints) {
49 Constraint->print(OS);
50 OS << "\n";
51 }
52 }
53
54 std::string
constraintsToString(const llvm::SetVector<const Formula * > & Constraints)55 constraintsToString(const llvm::SetVector<const Formula *> &Constraints) {
56 std::string Str;
57 llvm::raw_string_ostream OS(Str);
58 printConstraints(Constraints, OS);
59 return Str;
60 }
61
62 MATCHER_P(EqualsConstraints, Constraints,
63 "constraints are: " + constraintsToString(Constraints)) {
64 if (arg == Constraints)
65 return true;
66
67 if (result_listener->stream()) {
68 llvm::raw_os_ostream OS(*result_listener->stream());
69 OS << "constraints are: ";
70 printConstraints(arg, OS);
71 }
72 return false;
73 }
74
TEST_F(SimplifyConstraintsTest,TriviallySatisfiable)75 TEST_F(SimplifyConstraintsTest, TriviallySatisfiable) {
76 SimplifyConstraintsInfo Info;
77 EXPECT_THAT(simplify(R"(
78 V0
79 )",
80 Info),
81 EqualsConstraints(parse("")));
82 EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
83 EXPECT_THAT(Info.TrueAtoms, ElementsAre(Atom(0)));
84 EXPECT_THAT(Info.FalseAtoms, IsEmpty());
85 }
86
TEST_F(SimplifyConstraintsTest,SimpleContradiction)87 TEST_F(SimplifyConstraintsTest, SimpleContradiction) {
88 SimplifyConstraintsInfo Info;
89 EXPECT_THAT(simplify(R"(
90 V0
91 !V0
92 )",
93 Info),
94 EqualsConstraints(parse("false")));
95 EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
96 EXPECT_THAT(Info.TrueAtoms, IsEmpty());
97 EXPECT_THAT(Info.FalseAtoms, IsEmpty());
98 }
99
TEST_F(SimplifyConstraintsTest,ContradictionThroughEquivalence)100 TEST_F(SimplifyConstraintsTest, ContradictionThroughEquivalence) {
101 SimplifyConstraintsInfo Info;
102 EXPECT_THAT(simplify(R"(
103 (V0 = V1)
104 V0
105 !V1
106 )",
107 Info),
108 EqualsConstraints(parse("false")));
109 EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
110 EXPECT_THAT(Info.TrueAtoms, IsEmpty());
111 EXPECT_THAT(Info.FalseAtoms, IsEmpty());
112 }
113
TEST_F(SimplifyConstraintsTest,EquivalenceChain)114 TEST_F(SimplifyConstraintsTest, EquivalenceChain) {
115 SimplifyConstraintsInfo Info;
116 EXPECT_THAT(simplify(R"(
117 (V0 | V3)
118 (V1 = V2)
119 (V2 = V3)
120 )",
121 Info),
122 EqualsConstraints(parse("(V0 | V1)")));
123 EXPECT_THAT(Info.EquivalentAtoms,
124 ElementsAre(ElementsAre(Atom(1), Atom(2), Atom(3))));
125 EXPECT_THAT(Info.TrueAtoms, IsEmpty());
126 EXPECT_THAT(Info.FalseAtoms, IsEmpty());
127 }
128
TEST_F(SimplifyConstraintsTest,TrueAndFalseAtomsSimplifyOtherExpressions)129 TEST_F(SimplifyConstraintsTest, TrueAndFalseAtomsSimplifyOtherExpressions) {
130 SimplifyConstraintsInfo Info;
131 EXPECT_THAT(simplify(R"(
132 V0
133 !V1
134 (V0 & (V2 => V3))
135 (V1 | (V4 => V5))
136 )",
137 Info),
138 EqualsConstraints(parse(R"(
139 (V2 => V3)
140 (V4 => V5)
141 )")));
142 EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
143 EXPECT_THAT(Info.TrueAtoms, ElementsAre(Atom(0)));
144 EXPECT_THAT(Info.FalseAtoms, ElementsAre(Atom(1)));
145 }
146
TEST_F(SimplifyConstraintsTest,TrueAtomUnlocksEquivalenceChain)147 TEST_F(SimplifyConstraintsTest, TrueAtomUnlocksEquivalenceChain) {
148 SimplifyConstraintsInfo Info;
149 EXPECT_THAT(simplify(R"(
150 V0
151 (V0 & (V1 = V2))
152 (V0 & (V2 = V3))
153 )",
154 Info),
155 EqualsConstraints(parse("")));
156 EXPECT_THAT(Info.EquivalentAtoms,
157 ElementsAre(ElementsAre(Atom(1), Atom(2), Atom(3))));
158 EXPECT_THAT(Info.TrueAtoms, ElementsAre(Atom(0)));
159 EXPECT_THAT(Info.FalseAtoms, IsEmpty());
160 }
161
TEST_F(SimplifyConstraintsTest,TopLevelAndSplitIntoMultipleConstraints)162 TEST_F(SimplifyConstraintsTest, TopLevelAndSplitIntoMultipleConstraints) {
163 SimplifyConstraintsInfo Info;
164 EXPECT_THAT(simplify(R"(
165 ((V0 => V1) & (V2 => V3))
166 )",
167 Info),
168 EqualsConstraints(parse(R"(
169 (V0 => V1)
170 (V2 => V3)
171 )")));
172 EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
173 EXPECT_THAT(Info.TrueAtoms, IsEmpty());
174 EXPECT_THAT(Info.FalseAtoms, IsEmpty());
175 }
176
177 } // namespace
178