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

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