1ae60884dSStanislav Gatev //===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp ---===// 2ae60884dSStanislav Gatev // 3ae60884dSStanislav Gatev // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4ae60884dSStanislav Gatev // See https://llvm.org/LICENSE.txt for license information. 5ae60884dSStanislav Gatev // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6ae60884dSStanislav Gatev // 7ae60884dSStanislav Gatev //===----------------------------------------------------------------------===// 8ae60884dSStanislav Gatev 9ae60884dSStanislav Gatev #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h" 10ae60884dSStanislav Gatev #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" 11ae60884dSStanislav Gatev #include "gmock/gmock.h" 12ae60884dSStanislav Gatev #include "gtest/gtest.h" 13ae60884dSStanislav Gatev #include <memory> 14ae60884dSStanislav Gatev 15ae60884dSStanislav Gatev namespace { 16ae60884dSStanislav Gatev 17ae60884dSStanislav Gatev using namespace clang; 18ae60884dSStanislav Gatev using namespace dataflow; 19ae60884dSStanislav Gatev 20ae60884dSStanislav Gatev class DataflowAnalysisContextTest : public ::testing::Test { 21ae60884dSStanislav Gatev protected: 22ae60884dSStanislav Gatev DataflowAnalysisContextTest() 23ae60884dSStanislav Gatev : Context(std::make_unique<WatchedLiteralsSolver>()) {} 24ae60884dSStanislav Gatev 25ae60884dSStanislav Gatev DataflowAnalysisContext Context; 26ae60884dSStanislav Gatev }; 27ae60884dSStanislav Gatev 28ae60884dSStanislav Gatev TEST_F(DataflowAnalysisContextTest, 29ae60884dSStanislav Gatev CreateAtomicBoolValueReturnsDistinctValues) { 30ae60884dSStanislav Gatev auto &X = Context.createAtomicBoolValue(); 31ae60884dSStanislav Gatev auto &Y = Context.createAtomicBoolValue(); 32ae60884dSStanislav Gatev EXPECT_NE(&X, &Y); 33ae60884dSStanislav Gatev } 34ae60884dSStanislav Gatev 35ae60884dSStanislav Gatev TEST_F(DataflowAnalysisContextTest, 36ae60884dSStanislav Gatev GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) { 37ae60884dSStanislav Gatev auto &X = Context.createAtomicBoolValue(); 38ae60884dSStanislav Gatev auto &XAndX = Context.getOrCreateConjunctionValue(X, X); 39ae60884dSStanislav Gatev EXPECT_EQ(&XAndX, &X); 40ae60884dSStanislav Gatev } 41ae60884dSStanislav Gatev 42ae60884dSStanislav Gatev TEST_F(DataflowAnalysisContextTest, 43ae60884dSStanislav Gatev GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) { 44ae60884dSStanislav Gatev auto &X = Context.createAtomicBoolValue(); 45ae60884dSStanislav Gatev auto &Y = Context.createAtomicBoolValue(); 46ae60884dSStanislav Gatev auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y); 47ae60884dSStanislav Gatev auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y); 48ae60884dSStanislav Gatev EXPECT_EQ(&XAndY1, &XAndY2); 49ae60884dSStanislav Gatev 50ae60884dSStanislav Gatev auto &YAndX = Context.getOrCreateConjunctionValue(Y, X); 51ae60884dSStanislav Gatev EXPECT_EQ(&XAndY1, &YAndX); 52ae60884dSStanislav Gatev 53ae60884dSStanislav Gatev auto &Z = Context.createAtomicBoolValue(); 54ae60884dSStanislav Gatev auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z); 55ae60884dSStanislav Gatev EXPECT_NE(&XAndY1, &XAndZ); 56ae60884dSStanislav Gatev } 57ae60884dSStanislav Gatev 58ae60884dSStanislav Gatev TEST_F(DataflowAnalysisContextTest, 59ae60884dSStanislav Gatev GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) { 60ae60884dSStanislav Gatev auto &X = Context.createAtomicBoolValue(); 61ae60884dSStanislav Gatev auto &XOrX = Context.getOrCreateDisjunctionValue(X, X); 62ae60884dSStanislav Gatev EXPECT_EQ(&XOrX, &X); 63ae60884dSStanislav Gatev } 64ae60884dSStanislav Gatev 65ae60884dSStanislav Gatev TEST_F(DataflowAnalysisContextTest, 66ae60884dSStanislav Gatev GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) { 67ae60884dSStanislav Gatev auto &X = Context.createAtomicBoolValue(); 68ae60884dSStanislav Gatev auto &Y = Context.createAtomicBoolValue(); 69ae60884dSStanislav Gatev auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y); 70ae60884dSStanislav Gatev auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y); 71ae60884dSStanislav Gatev EXPECT_EQ(&XOrY1, &XOrY2); 72ae60884dSStanislav Gatev 73ae60884dSStanislav Gatev auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X); 74ae60884dSStanislav Gatev EXPECT_EQ(&XOrY1, &YOrX); 75ae60884dSStanislav Gatev 76ae60884dSStanislav Gatev auto &Z = Context.createAtomicBoolValue(); 77ae60884dSStanislav Gatev auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z); 78ae60884dSStanislav Gatev EXPECT_NE(&XOrY1, &XOrZ); 79ae60884dSStanislav Gatev } 80ae60884dSStanislav Gatev 81ae60884dSStanislav Gatev TEST_F(DataflowAnalysisContextTest, 82ae60884dSStanislav Gatev GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) { 83ae60884dSStanislav Gatev auto &X = Context.createAtomicBoolValue(); 84ae60884dSStanislav Gatev auto &NotX1 = Context.getOrCreateNegationValue(X); 85ae60884dSStanislav Gatev auto &NotX2 = Context.getOrCreateNegationValue(X); 86ae60884dSStanislav Gatev EXPECT_EQ(&NotX1, &NotX2); 87ae60884dSStanislav Gatev 88ae60884dSStanislav Gatev auto &Y = Context.createAtomicBoolValue(); 89ae60884dSStanislav Gatev auto &NotY = Context.getOrCreateNegationValue(Y); 90ae60884dSStanislav Gatev EXPECT_NE(&NotX1, &NotY); 91ae60884dSStanislav Gatev } 92ae60884dSStanislav Gatev 93955a05a2SStanislav Gatev TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) { 94955a05a2SStanislav Gatev auto &FC = Context.makeFlowConditionToken(); 95955a05a2SStanislav Gatev auto &C = Context.createAtomicBoolValue(); 96955a05a2SStanislav Gatev EXPECT_FALSE(Context.flowConditionImplies(FC, C)); 97955a05a2SStanislav Gatev } 98955a05a2SStanislav Gatev 99955a05a2SStanislav Gatev TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) { 100955a05a2SStanislav Gatev auto &FC = Context.makeFlowConditionToken(); 101955a05a2SStanislav Gatev auto &C = Context.createAtomicBoolValue(); 102955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC, C); 103955a05a2SStanislav Gatev EXPECT_TRUE(Context.flowConditionImplies(FC, C)); 104955a05a2SStanislav Gatev } 105955a05a2SStanislav Gatev 106955a05a2SStanislav Gatev TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) { 107955a05a2SStanislav Gatev auto &FC1 = Context.makeFlowConditionToken(); 108955a05a2SStanislav Gatev auto &C1 = Context.createAtomicBoolValue(); 109955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC1, C1); 110955a05a2SStanislav Gatev 111955a05a2SStanislav Gatev // Forked flow condition inherits the constraints of its parent flow 112955a05a2SStanislav Gatev // condition. 113955a05a2SStanislav Gatev auto &FC2 = Context.forkFlowCondition(FC1); 114955a05a2SStanislav Gatev EXPECT_TRUE(Context.flowConditionImplies(FC2, C1)); 115955a05a2SStanislav Gatev 116955a05a2SStanislav Gatev // Adding a new constraint to the forked flow condition does not affect its 117955a05a2SStanislav Gatev // parent flow condition. 118955a05a2SStanislav Gatev auto &C2 = Context.createAtomicBoolValue(); 119955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC2, C2); 120955a05a2SStanislav Gatev EXPECT_TRUE(Context.flowConditionImplies(FC2, C2)); 121955a05a2SStanislav Gatev EXPECT_FALSE(Context.flowConditionImplies(FC1, C2)); 122955a05a2SStanislav Gatev } 123955a05a2SStanislav Gatev 124955a05a2SStanislav Gatev TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) { 125955a05a2SStanislav Gatev auto &C1 = Context.createAtomicBoolValue(); 126955a05a2SStanislav Gatev auto &C2 = Context.createAtomicBoolValue(); 127955a05a2SStanislav Gatev auto &C3 = Context.createAtomicBoolValue(); 128955a05a2SStanislav Gatev 129955a05a2SStanislav Gatev auto &FC1 = Context.makeFlowConditionToken(); 130955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC1, C1); 131955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC1, C3); 132955a05a2SStanislav Gatev 133955a05a2SStanislav Gatev auto &FC2 = Context.makeFlowConditionToken(); 134955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC2, C2); 135955a05a2SStanislav Gatev Context.addFlowConditionConstraint(FC2, C3); 136955a05a2SStanislav Gatev 137955a05a2SStanislav Gatev auto &FC3 = Context.joinFlowConditions(FC1, FC2); 138955a05a2SStanislav Gatev EXPECT_FALSE(Context.flowConditionImplies(FC3, C1)); 139955a05a2SStanislav Gatev EXPECT_FALSE(Context.flowConditionImplies(FC3, C2)); 140955a05a2SStanislav Gatev EXPECT_TRUE(Context.flowConditionImplies(FC3, C3)); 141955a05a2SStanislav Gatev } 142955a05a2SStanislav Gatev 143*58abe36aSEric Li TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) { 144*58abe36aSEric Li // Fresh flow condition with empty/no constraints is always true. 145*58abe36aSEric Li auto &FC1 = Context.makeFlowConditionToken(); 146*58abe36aSEric Li EXPECT_TRUE(Context.flowConditionIsTautology(FC1)); 147*58abe36aSEric Li 148*58abe36aSEric Li // Literal `true` is always true. 149*58abe36aSEric Li auto &FC2 = Context.makeFlowConditionToken(); 150*58abe36aSEric Li Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true)); 151*58abe36aSEric Li EXPECT_TRUE(Context.flowConditionIsTautology(FC2)); 152*58abe36aSEric Li 153*58abe36aSEric Li // Literal `false` is never true. 154*58abe36aSEric Li auto &FC3 = Context.makeFlowConditionToken(); 155*58abe36aSEric Li Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false)); 156*58abe36aSEric Li EXPECT_FALSE(Context.flowConditionIsTautology(FC3)); 157*58abe36aSEric Li 158*58abe36aSEric Li // We can't prove that an arbitrary bool A is always true... 159*58abe36aSEric Li auto &C1 = Context.createAtomicBoolValue(); 160*58abe36aSEric Li auto &FC4 = Context.makeFlowConditionToken(); 161*58abe36aSEric Li Context.addFlowConditionConstraint(FC4, C1); 162*58abe36aSEric Li EXPECT_FALSE(Context.flowConditionIsTautology(FC4)); 163*58abe36aSEric Li 164*58abe36aSEric Li // ... but we can prove A || !A is true. 165*58abe36aSEric Li auto &FC5 = Context.makeFlowConditionToken(); 166*58abe36aSEric Li Context.addFlowConditionConstraint( 167*58abe36aSEric Li FC5, Context.getOrCreateDisjunctionValue( 168*58abe36aSEric Li C1, Context.getOrCreateNegationValue(C1))); 169*58abe36aSEric Li EXPECT_TRUE(Context.flowConditionIsTautology(FC5)); 170*58abe36aSEric Li } 171*58abe36aSEric Li 172ae60884dSStanislav Gatev } // namespace 173