271 lines · 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-exception6//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 15namespace {16 17using namespace clang;18using namespace dataflow;19 20using ::testing::IsEmpty;21using ::testing::UnorderedElementsAre;22 23class DataflowAnalysisContextTest : public ::testing::Test {24protected:25 DataflowAnalysisContextTest()26 : Context(std::make_unique<WatchedLiteralsSolver>()), A(Context.arena()) {27 }28 29 DataflowAnalysisContext Context;30 Arena &A;31};32 33TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {34 auto &X = A.makeTopValue();35 auto &Y = A.makeTopValue();36 EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));37}38 39TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionImplies) {40 Atom FC = A.makeFlowConditionToken();41 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));42 EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeLiteral(false)));43 EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));44}45 46TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionAllows) {47 Atom FC = A.makeFlowConditionToken();48 EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeLiteral(true)));49 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));50 EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));51}52 53TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionImpliesAnything) {54 Atom FC = A.makeFlowConditionToken();55 Context.addFlowConditionConstraint(FC, A.makeLiteral(false));56 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));57 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(false)));58 EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));59}60 61TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionAllowsNothing) {62 Atom FC = A.makeFlowConditionToken();63 Context.addFlowConditionConstraint(FC, A.makeLiteral(false));64 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(true)));65 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));66 EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));67}68 69TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {70 Atom FC = A.makeFlowConditionToken();71 auto &C = A.makeAtomRef(A.makeAtom());72 Context.addFlowConditionConstraint(FC, C);73 EXPECT_TRUE(Context.flowConditionImplies(FC, C));74}75 76TEST_F(DataflowAnalysisContextTest, AddInvariant) {77 Atom FC = A.makeFlowConditionToken();78 auto &C = A.makeAtomRef(A.makeAtom());79 Context.addInvariant(C);80 EXPECT_TRUE(Context.flowConditionImplies(FC, C));81}82 83TEST_F(DataflowAnalysisContextTest, InvariantAndFCConstraintInteract) {84 Atom FC = A.makeFlowConditionToken();85 auto &C = A.makeAtomRef(A.makeAtom());86 auto &D = A.makeAtomRef(A.makeAtom());87 Context.addInvariant(A.makeImplies(C, D));88 Context.addFlowConditionConstraint(FC, C);89 EXPECT_TRUE(Context.flowConditionImplies(FC, D));90}91 92TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {93 Atom FC1 = A.makeFlowConditionToken();94 auto &C1 = A.makeAtomRef(A.makeAtom());95 Context.addFlowConditionConstraint(FC1, C1);96 97 // Forked flow condition inherits the constraints of its parent flow98 // condition.99 Atom FC2 = Context.forkFlowCondition(FC1);100 EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));101 102 // Adding a new constraint to the forked flow condition does not affect its103 // parent flow condition.104 auto &C2 = A.makeAtomRef(A.makeAtom());105 Context.addFlowConditionConstraint(FC2, C2);106 EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));107 EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));108}109 110TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {111 auto &C1 = A.makeAtomRef(A.makeAtom());112 auto &C2 = A.makeAtomRef(A.makeAtom());113 auto &C3 = A.makeAtomRef(A.makeAtom());114 115 Atom FC1 = A.makeFlowConditionToken();116 Context.addFlowConditionConstraint(FC1, C1);117 Context.addFlowConditionConstraint(FC1, C3);118 119 Atom FC2 = A.makeFlowConditionToken();120 Context.addFlowConditionConstraint(FC2, C2);121 Context.addFlowConditionConstraint(FC2, C3);122 123 Atom FC3 = Context.joinFlowConditions(FC1, FC2);124 EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));125 EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));126 EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));127}128 129TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {130 auto &X = A.makeAtomRef(A.makeAtom());131 auto &Y = A.makeAtomRef(A.makeAtom());132 auto &Z = A.makeAtomRef(A.makeAtom());133 auto &True = A.makeLiteral(true);134 auto &False = A.makeLiteral(false);135 136 // X == X137 EXPECT_TRUE(Context.equivalentFormulas(X, X));138 // X != Y139 EXPECT_FALSE(Context.equivalentFormulas(X, Y));140 141 // !X != X142 EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));143 // !(!X) = X144 EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));145 146 // (X || X) == X147 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));148 // (X || Y) != X149 EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));150 // (X || True) == True151 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));152 // (X || False) == X153 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));154 155 // (X && X) == X156 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));157 // (X && Y) != X158 EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));159 // (X && True) == X160 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));161 // (X && False) == False162 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));163 164 // (X || Y) == (Y || X)165 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));166 // (X && Y) == (Y && X)167 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));168 169 // ((X || Y) || Z) == (X || (Y || Z))170 EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),171 A.makeOr(X, A.makeOr(Y, Z))));172 // ((X && Y) && Z) == (X && (Y && Z))173 EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),174 A.makeAnd(X, A.makeAnd(Y, Z))));175}176 177using ExportLogicalContextTest = DataflowAnalysisContextTest;178 179TEST_F(ExportLogicalContextTest, EmptySet) {180 EXPECT_THAT(Context.exportLogicalContext({}).TokenDefs, IsEmpty());181}182 183// Only constrainted tokens are included in the output.184TEST_F(ExportLogicalContextTest, UnconstrainedIgnored) {185 Atom FC1 = A.makeFlowConditionToken();186 EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs, IsEmpty());187}188 189TEST_F(ExportLogicalContextTest, SingletonSet) {190 Atom FC1 = A.makeFlowConditionToken();191 auto &C1 = A.makeAtomRef(A.makeAtom());192 Context.addFlowConditionConstraint(FC1, C1);193 EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(),194 UnorderedElementsAre(FC1));195}196 197TEST_F(ExportLogicalContextTest, NoDependency) {198 Atom FC1 = A.makeFlowConditionToken();199 Atom FC2 = A.makeFlowConditionToken();200 Atom FC3 = A.makeFlowConditionToken();201 auto &C1 = A.makeAtomRef(A.makeAtom());202 auto &C2 = A.makeAtomRef(A.makeAtom());203 auto &C3 = A.makeAtomRef(A.makeAtom());204 205 Context.addFlowConditionConstraint(FC1, C1);206 Context.addFlowConditionConstraint(FC2, C2);207 Context.addFlowConditionConstraint(FC3, C3);208 209 // FCs are independent.210 EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(),211 UnorderedElementsAre(FC1));212 EXPECT_THAT(Context.exportLogicalContext({FC2}).TokenDefs.keys(),213 UnorderedElementsAre(FC2));214 EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(),215 UnorderedElementsAre(FC3));216}217 218TEST_F(ExportLogicalContextTest, SimpleDependencyChain) {219 Atom FC1 = A.makeFlowConditionToken();220 const Formula &C = A.makeAtomRef(A.makeAtom());221 Context.addFlowConditionConstraint(FC1, C);222 Atom FC2 = Context.forkFlowCondition(FC1);223 Atom FC3 = Context.forkFlowCondition(FC2);224 225 EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(),226 UnorderedElementsAre(FC1, FC2, FC3));227}228 229TEST_F(ExportLogicalContextTest, DependencyTree) {230 Atom FC1 = A.makeFlowConditionToken();231 const Formula &C = A.makeAtomRef(A.makeAtom());232 Context.addFlowConditionConstraint(FC1, C);233 Atom FC2 = Context.forkFlowCondition(FC1);234 Atom FC3 = A.makeFlowConditionToken();235 Context.addFlowConditionConstraint(FC3, C);236 Atom FC4 = Context.joinFlowConditions(FC2, FC3);237 238 EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(),239 UnorderedElementsAre(FC1, FC2, FC3, FC4));240}241 242TEST_F(ExportLogicalContextTest, DependencyDAG) {243 Atom FC1 = A.makeFlowConditionToken();244 const Formula &C = A.makeAtomRef(A.makeAtom());245 Context.addFlowConditionConstraint(FC1, C);246 247 Atom FC2 = Context.forkFlowCondition(FC1);248 Atom FC3 = Context.forkFlowCondition(FC1);249 Atom FC4 = Context.joinFlowConditions(FC2, FC3);250 251 EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(),252 UnorderedElementsAre(FC1, FC2, FC3, FC4));253}254 255TEST_F(ExportLogicalContextTest, MixedDependencies) {256 Atom FC1 = A.makeFlowConditionToken();257 const Formula &C = A.makeAtomRef(A.makeAtom());258 Context.addFlowConditionConstraint(FC1, C);259 260 Atom FC2 = Context.forkFlowCondition(FC1);261 Atom FC3 = Context.forkFlowCondition(FC2);262 (void)FC3; // unused, and we test below that it is not included.263 264 Atom FC4 = A.makeFlowConditionToken();265 Context.addFlowConditionConstraint(FC4, C);266 267 EXPECT_THAT(Context.exportLogicalContext({FC2, FC4}).TokenDefs.keys(),268 UnorderedElementsAre(FC1, FC2, FC4));269}270} // namespace271