177 lines · cpp
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-exception6//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, A, &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::string54constraintsToString(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 V078 )",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 V090 !V091 )",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 V0104 !V1105 )",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 V0132 !V1133 (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 V0150 (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} // namespace177