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
15namespace {
16
17using namespace clang;
18using namespace dataflow;
19
20using ::testing::ElementsAre;
21using ::testing::IsEmpty;
22
23class SimplifyConstraintsTest : public ::testing::Test {
24protected:
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
32 llvm::SetVector<const Formula *> simplify(StringRef Lines,
33 SimplifyConstraintsInfo &Info) {
34 llvm::SetVector<const Formula *> Constraints = parse(Lines);
35 simplifyConstraints(Constraints, arena&: A, Info: &Info);
36 return Constraints;
37 }
38
39 Arena A;
40};
41
42void 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
54std::string
55constraintsToString(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
62MATCHER_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
75TEST_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
87TEST_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
100TEST_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
114TEST_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
129TEST_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
147TEST_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
162TEST_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

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