clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

   1 //===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.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/DataflowAnalysisContext.h"
  10 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
  11 #include "gmock/gmock.h"
  12 #include "gtest/gtest.h"
  13 #include <memory>
  14
  15 namespace {
  16
  17 using namespace clang;
  18 using namespace dataflow;
  19
  20 class DataflowAnalysisContextTest : public ::testing::Test {
  21 protected:
  22   DataflowAnalysisContextTest()
  23       : Context(std::make_unique<WatchedLiteralsSolver>()), A(Context.arena()) {
  24   }
  25
  26   DataflowAnalysisContext Context;
  27   Arena &A;
  28 };
  29
  30 TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
  31   auto &X = A.makeTopValue();
  32   auto &Y = A.makeTopValue();
  33   EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
  34 }
  35
  36 TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionImplies) {
  37   Atom FC = A.makeFlowConditionToken();
  38   EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));
  39   EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeLiteral(false)));
  40   EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));
  41 }
  42
  43 TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionAllows) {
  44   Atom FC = A.makeFlowConditionToken();
  45   EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeLiteral(true)));
  46   EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));
  47   EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));
  48 }
  49
  50 TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionImpliesAnything) {
  51   Atom FC = A.makeFlowConditionToken();
  52   Context.addFlowConditionConstraint(FC, A.makeLiteral(false));
  53   EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));
  54   EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(false)));
  55   EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));
  56 }
  57
  58 TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionAllowsNothing) {
  59   Atom FC = A.makeFlowConditionToken();
  60   Context.addFlowConditionConstraint(FC, A.makeLiteral(false));
  61   EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(true)));
  62   EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));
  63   EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));
  64 }
  65
  66 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
  67   Atom FC = A.makeFlowConditionToken();
  68   auto &C = A.makeAtomRef(A.makeAtom());
  69   Context.addFlowConditionConstraint(FC, C);
  70   EXPECT_TRUE(Context.flowConditionImplies(FC, C));
  71 }
  72
  73 TEST_F(DataflowAnalysisContextTest, AddInvariant) {
  74   Atom FC = A.makeFlowConditionToken();
  75   auto &C = A.makeAtomRef(A.makeAtom());
  76   Context.addInvariant(C);
  77   EXPECT_TRUE(Context.flowConditionImplies(FC, C));
  78 }
  79
  80 TEST_F(DataflowAnalysisContextTest, InvariantAndFCConstraintInteract) {
  81   Atom FC = A.makeFlowConditionToken();
  82   auto &C = A.makeAtomRef(A.makeAtom());
  83   auto &D = A.makeAtomRef(A.makeAtom());
  84   Context.addInvariant(A.makeImplies(C, D));
  85   Context.addFlowConditionConstraint(FC, C);
  86   EXPECT_TRUE(Context.flowConditionImplies(FC, D));
  87 }
  88
  89 TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
  90   Atom FC1 = A.makeFlowConditionToken();
  91   auto &C1 = A.makeAtomRef(A.makeAtom());
  92   Context.addFlowConditionConstraint(FC1, C1);
  93
  94   // Forked flow condition inherits the constraints of its parent flow
  95   // condition.
  96   Atom FC2 = Context.forkFlowCondition(FC1);
  97   EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
  98
  99   // Adding a new constraint to the forked flow condition does not affect its
 100   // parent flow condition.
 101   auto &C2 = A.makeAtomRef(A.makeAtom());
 102   Context.addFlowConditionConstraint(FC2, C2);
 103   EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
 104   EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
 105 }
 106
 107 TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
 108   auto &C1 = A.makeAtomRef(A.makeAtom());
 109   auto &C2 = A.makeAtomRef(A.makeAtom());
 110   auto &C3 = A.makeAtomRef(A.makeAtom());
 111
 112   Atom FC1 = A.makeFlowConditionToken();
 113   Context.addFlowConditionConstraint(FC1, C1);
 114   Context.addFlowConditionConstraint(FC1, C3);
 115
 116   Atom FC2 = A.makeFlowConditionToken();
 117   Context.addFlowConditionConstraint(FC2, C2);
 118   Context.addFlowConditionConstraint(FC2, C3);
 119
 120   Atom FC3 = Context.joinFlowConditions(FC1, FC2);
 121   EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
 122   EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
 123   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
 124 }
 125
 126 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
 127   auto &X = A.makeAtomRef(A.makeAtom());
 128   auto &Y = A.makeAtomRef(A.makeAtom());
 129   auto &Z = A.makeAtomRef(A.makeAtom());
 130   auto &True = A.makeLiteral(true);
 131   auto &False = A.makeLiteral(false);
 132
 133   // X == X
 134   EXPECT_TRUE(Context.equivalentFormulas(X, X));
 135   // X != Y
 136   EXPECT_FALSE(Context.equivalentFormulas(X, Y));
 137
 138   // !X != X
 139   EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
 140   // !(!X) = X
 141   EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
 142
 143   // (X || X) == X
 144   EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
 145   // (X || Y) != X
 146   EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
 147   // (X || True) == True
 148   EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
 149   // (X || False) == X
 150   EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
 151
 152   // (X && X) == X
 153   EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
 154   // (X && Y) != X
 155   EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
 156   // (X && True) == X
 157   EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
 158   // (X && False) == False
 159   EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
 160
 161   // (X || Y) == (Y || X)
 162   EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
 163   // (X && Y) == (Y && X)
 164   EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
 165
 166   // ((X || Y) || Z) == (X || (Y || Z))
 167   EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
 168                                          A.makeOr(X, A.makeOr(Y, Z))));
 169   // ((X && Y) && Z) == (X && (Y && Z))
 170   EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),
 171                                          A.makeAnd(X, A.makeAnd(Y, Z))));
 172 }
 173
 174 } // namespace