clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

   1 //===- ArenaTest.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/Arena.h"
  10 #include "llvm/Support/ScopedPrinter.h"
  11 #include "llvm/Testing/Support/Error.h"
  12 #include "gmock/gmock.h"
  13 #include "gtest/gtest.h"
  14
  15 namespace clang::dataflow {
  16 namespace {
  17 using llvm::HasValue;
  18 using testing::Ref;
  19
  20 class ArenaTest : public ::testing::Test {
  21 protected:
  22   Arena A;
  23 };
  24
  25 TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
  26   auto &X = A.makeAtomValue();
  27   auto &Y = A.makeAtomValue();
  28   EXPECT_NE(&X, &Y);
  29 }
  30
  31 TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
  32   auto &X = A.makeTopValue();
  33   auto &Y = A.makeTopValue();
  34   EXPECT_NE(&X, &Y);
  35 }
  36
  37 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
  38   auto &X = A.makeAtomRef(A.makeAtom());
  39   auto &Y = A.makeAtomRef(A.makeAtom());
  40   auto &XAndY1 = A.makeAnd(X, Y);
  41   auto &XAndY2 = A.makeAnd(X, Y);
  42   EXPECT_EQ(&XAndY1, &XAndY2);
  43
  44   auto &YAndX = A.makeAnd(Y, X);
  45   EXPECT_EQ(&XAndY1, &YAndX);
  46
  47   auto &Z = A.makeAtomRef(A.makeAtom());
  48   auto &XAndZ = A.makeAnd(X, Z);
  49   EXPECT_NE(&XAndY1, &XAndZ);
  50 }
  51
  52 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
  53   auto &X = A.makeAtomRef(A.makeAtom());
  54   auto &Y = A.makeAtomRef(A.makeAtom());
  55   auto &XOrY1 = A.makeOr(X, Y);
  56   auto &XOrY2 = A.makeOr(X, Y);
  57   EXPECT_EQ(&XOrY1, &XOrY2);
  58
  59   auto &YOrX = A.makeOr(Y, X);
  60   EXPECT_EQ(&XOrY1, &YOrX);
  61
  62   auto &Z = A.makeAtomRef(A.makeAtom());
  63   auto &XOrZ = A.makeOr(X, Z);
  64   EXPECT_NE(&XOrY1, &XOrZ);
  65 }
  66
  67 TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
  68   auto &X = A.makeAtomRef(A.makeAtom());
  69   auto &NotX1 = A.makeNot(X);
  70   auto &NotX2 = A.makeNot(X);
  71   EXPECT_EQ(&NotX1, &NotX2);
  72   auto &Y = A.makeAtomRef(A.makeAtom());
  73   auto &NotY = A.makeNot(Y);
  74   EXPECT_NE(&NotX1, &NotY);
  75 }
  76
  77 TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
  78   auto &X = A.makeAtomRef(A.makeAtom());
  79   auto &Y = A.makeAtomRef(A.makeAtom());
  80   auto &XImpliesY1 = A.makeImplies(X, Y);
  81   auto &XImpliesY2 = A.makeImplies(X, Y);
  82   EXPECT_EQ(&XImpliesY1, &XImpliesY2);
  83
  84   auto &YImpliesX = A.makeImplies(Y, X);
  85   EXPECT_NE(&XImpliesY1, &YImpliesX);
  86
  87   auto &Z = A.makeAtomRef(A.makeAtom());
  88   auto &XImpliesZ = A.makeImplies(X, Z);
  89   EXPECT_NE(&XImpliesY1, &XImpliesZ);
  90 }
  91
  92 TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
  93   auto &X = A.makeAtomRef(A.makeAtom());
  94   auto &Y = A.makeAtomRef(A.makeAtom());
  95   auto &XIffY1 = A.makeEquals(X, Y);
  96   auto &XIffY2 = A.makeEquals(X, Y);
  97   EXPECT_EQ(&XIffY1, &XIffY2);
  98
  99   auto &YIffX = A.makeEquals(Y, X);
 100   EXPECT_EQ(&XIffY1, &YIffX);
 101
 102   auto &Z = A.makeAtomRef(A.makeAtom());
 103   auto &XIffZ = A.makeEquals(X, Z);
 104   EXPECT_NE(&XIffY1, &XIffZ);
 105 }
 106
 107 TEST_F(ArenaTest, Interning) {
 108   Atom X = A.makeAtom();
 109   Atom Y = A.makeAtom();
 110   const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));
 111   const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
 112   EXPECT_EQ(&F1, &F2);
 113   BoolValue &B1 = A.makeBoolValue(F1);
 114   BoolValue &B2 = A.makeBoolValue(F2);
 115   EXPECT_EQ(&B1, &B2);
 116   EXPECT_EQ(&B1.formula(), &F1);
 117 }
 118
 119 TEST_F(ArenaTest, ParseFormula) {
 120   Atom V5{5};
 121   Atom V6{6};
 122   EXPECT_THAT_EXPECTED(A.parseFormula("V5"), HasValue(Ref(A.makeAtomRef(V5))));
 123   EXPECT_THAT_EXPECTED(A.parseFormula("true"),
 124                        HasValue(Ref(A.makeLiteral(true))));
 125   EXPECT_THAT_EXPECTED(A.parseFormula("!V5"),
 126                        HasValue(Ref(A.makeNot(A.makeAtomRef(V5)))));
 127
 128   EXPECT_THAT_EXPECTED(
 129       A.parseFormula("(V5 = V6)"),
 130       HasValue(Ref(A.makeEquals(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
 131   EXPECT_THAT_EXPECTED(
 132       A.parseFormula("(V5 => V6)"),
 133       HasValue(Ref(A.makeImplies(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
 134   EXPECT_THAT_EXPECTED(
 135       A.parseFormula("(V5 & V6)"),
 136       HasValue(Ref(A.makeAnd(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
 137   EXPECT_THAT_EXPECTED(
 138       A.parseFormula("(V5 | V6)"),
 139       HasValue(Ref(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
 140
 141   EXPECT_THAT_EXPECTED(
 142       A.parseFormula("((V5 & (V6 & !false)) => ((V5 | V6) | false))"),
 143       HasValue(Ref(
 144           A.makeImplies(A.makeAnd(A.makeAtomRef(V5),
 145                                   A.makeAnd(A.makeAtomRef(V6),
 146                                             A.makeNot(A.makeLiteral(false)))),
 147                         A.makeOr(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)),
 148                                  A.makeLiteral(false))))));
 149
 150   EXPECT_THAT_EXPECTED(
 151       A.parseFormula("(V0 => error)"), llvm::FailedWithMessage(R"(bad formula at offset 7
 152 (V0 => error)
 153        ^)"));
 154   EXPECT_THAT_EXPECTED(
 155       A.parseFormula("V1 V2"), llvm::FailedWithMessage(R"(bad formula at offset 3
 156 V1 V2
 157    ^)"));
 158 }
 159
 160 TEST_F(ArenaTest, IdentitySimplification) {
 161   auto &X = A.makeAtomRef(A.makeAtom());
 162
 163   EXPECT_EQ(&X, &A.makeAnd(X, X));
 164   EXPECT_EQ(&X, &A.makeOr(X, X));
 165   EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
 166   EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
 167   EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
 168 }
 169
 170 TEST_F(ArenaTest, LiteralSimplification) {
 171   auto &X = A.makeAtomRef(A.makeAtom());
 172
 173   EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
 174   EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
 175
 176   EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
 177   EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
 178
 179   EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
 180   EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
 181   EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
 182   EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
 183
 184   EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
 185   EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
 186
 187   EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
 188   EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
 189 }
 190
 191 } // namespace
 192 } // namespace clang::dataflow