clang/unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.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-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:
  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, A, &Info);
  36     return Constraints;
  37   }
  38
  39   Arena A;
  40 };
  41
  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
  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
  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
  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
 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
 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
 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
 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
 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