diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -151,17 +151,29 @@ /// `RHS`. Subsequent calls with the same arguments, regardless of their /// order, will return the same result. If the given boolean values represent /// the same value, the result will be the value itself. - BoolValue &getOrCreateConjunctionValue(BoolValue &LHS, BoolValue &RHS); + BoolValue &getOrCreateConjunction(BoolValue &LHS, BoolValue &RHS); /// Returns a boolean value that represents the disjunction of `LHS` and /// `RHS`. Subsequent calls with the same arguments, regardless of their /// order, will return the same result. If the given boolean values represent /// the same value, the result will be the value itself. - BoolValue &getOrCreateDisjunctionValue(BoolValue &LHS, BoolValue &RHS); + BoolValue &getOrCreateDisjunction(BoolValue &LHS, BoolValue &RHS); /// Returns a boolean value that represents the negation of `Val`. Subsequent /// calls with the same argument will return the same result. - BoolValue &getOrCreateNegationValue(BoolValue &Val); + BoolValue &getOrCreateNegation(BoolValue &Val); + + /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls + /// with the same arguments, will return the same result. If the given boolean + /// values represent the same value, the result will be a value that + /// represents the true boolean literal. + BoolValue &getOrCreateImplication(BoolValue &LHS, BoolValue &RHS); + + /// Returns a boolean value that represents `LHS <=> RHS`. Subsequent calls + /// with the same arguments, regardless of their order, will return the same + /// result. If the given boolean values represent the same value, the result + /// will be a value that represents the true boolean literal. + BoolValue &getOrCreateIff(BoolValue &LHS, BoolValue &RHS); /// Creates a fresh flow condition and returns a token that identifies it. The /// token can be used to perform various operations on the flow condition such diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -268,7 +268,7 @@ /// order, will return the same result. If the given boolean values represent /// the same value, the result will be the value itself. BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const { - return DACtx->getOrCreateConjunctionValue(LHS, RHS); + return DACtx->getOrCreateConjunction(LHS, RHS); } /// Returns a boolean value that represents the disjunction of `LHS` and @@ -276,21 +276,21 @@ /// order, will return the same result. If the given boolean values represent /// the same value, the result will be the value itself. BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const { - return DACtx->getOrCreateDisjunctionValue(LHS, RHS); + return DACtx->getOrCreateDisjunction(LHS, RHS); } /// Returns a boolean value that represents the negation of `Val`. Subsequent /// calls with the same argument will return the same result. BoolValue &makeNot(BoolValue &Val) const { - return DACtx->getOrCreateNegationValue(Val); + return DACtx->getOrCreateNegation(Val); } /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with - /// the same arguments, regardless of their order, will return the same - /// result. If the given boolean values represent the same value, the result - /// will be a value that represents the true boolean literal. + /// the same arguments, will return the same result. If the given boolean + /// values represent the same value, the result will be a value that + /// represents the true boolean literal. BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const { - return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(LHS), RHS); + return DACtx->getOrCreateImplication(LHS, RHS); } /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with @@ -298,9 +298,7 @@ /// result. If the given boolean values represent the same value, the result /// will be a value that represents the true boolean literal. BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const { - return &LHS == &RHS - ? getBoolLiteralValue(true) - : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS)); + return DACtx->getOrCreateIff(LHS, RHS); } /// Returns the token that identifies the flow condition of the environment. diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -30,9 +30,8 @@ return Res; } -BoolValue & -DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS, - BoolValue &RHS) { +BoolValue &DataflowAnalysisContext::getOrCreateConjunction(BoolValue &LHS, + BoolValue &RHS) { if (&LHS == &RHS) return LHS; @@ -44,9 +43,8 @@ return *Res.first->second; } -BoolValue & -DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS, - BoolValue &RHS) { +BoolValue &DataflowAnalysisContext::getOrCreateDisjunction(BoolValue &LHS, + BoolValue &RHS) { if (&LHS == &RHS) return LHS; @@ -58,13 +56,27 @@ return *Res.first->second; } -BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) { +BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) { auto Res = NegationVals.try_emplace(&Val, nullptr); if (Res.second) Res.first->second = &takeOwnership(std::make_unique(Val)); return *Res.first->second; } +BoolValue &DataflowAnalysisContext::getOrCreateImplication(BoolValue &LHS, + BoolValue &RHS) { + return &LHS == &RHS ? getBoolLiteralValue(true) + : getOrCreateDisjunction(getOrCreateNegation(LHS), RHS); +} + +BoolValue &DataflowAnalysisContext::getOrCreateIff(BoolValue &LHS, + BoolValue &RHS) { + return &LHS == &RHS + ? getBoolLiteralValue(true) + : getOrCreateConjunction(getOrCreateImplication(LHS, RHS), + getOrCreateImplication(RHS, LHS)); +} + AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() { return createAtomicBoolValue(); } @@ -73,8 +85,7 @@ AtomicBoolValue &Token, BoolValue &Constraint) { auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint); if (!Res.second) { - Res.first->second = - &getOrCreateConjunctionValue(*Res.first->second, Constraint); + Res.first->second = &getOrCreateConjunction(*Res.first->second, Constraint); } } @@ -92,8 +103,8 @@ auto &Token = makeFlowConditionToken(); FlowConditionDeps[&Token].insert(&FirstToken); FlowConditionDeps[&Token].insert(&SecondToken); - addFlowConditionConstraint( - Token, getOrCreateDisjunctionValue(FirstToken, SecondToken)); + addFlowConditionConstraint(Token, + getOrCreateDisjunction(FirstToken, SecondToken)); return Token; } @@ -107,8 +118,8 @@ llvm::DenseSet Constraints = { &Token, &getBoolLiteralValue(true), - &getOrCreateNegationValue(getBoolLiteralValue(false)), - &getOrCreateNegationValue(Val), + &getOrCreateNegation(getBoolLiteralValue(false)), + &getOrCreateNegation(Val), }; llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); @@ -120,8 +131,8 @@ // ever be false. llvm::DenseSet Constraints = { &getBoolLiteralValue(true), - &getOrCreateNegationValue(getBoolLiteralValue(false)), - &getOrCreateNegationValue(Token), + &getOrCreateNegation(getBoolLiteralValue(false)), + &getOrCreateNegation(Token), }; llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); @@ -141,11 +152,7 @@ } else { // Bind flow condition token via `iff` to its set of constraints: // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints - Constraints.insert(&getOrCreateConjunctionValue( - getOrCreateDisjunctionValue( - Token, getOrCreateNegationValue(*ConstraintsIT->second)), - getOrCreateDisjunctionValue(getOrCreateNegationValue(Token), - *ConstraintsIT->second))); + Constraints.insert(&getOrCreateIff(Token, *ConstraintsIT->second)); } auto DepsIT = FlowConditionDeps.find(&Token); diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -33,63 +33,108 @@ } TEST_F(DataflowAnalysisContextTest, - GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) { + GetOrCreateConjunctionReturnsSameExprGivenSameArgs) { auto &X = Context.createAtomicBoolValue(); - auto &XAndX = Context.getOrCreateConjunctionValue(X, X); + auto &XAndX = Context.getOrCreateConjunction(X, X); EXPECT_EQ(&XAndX, &X); } TEST_F(DataflowAnalysisContextTest, - GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) { + GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { auto &X = Context.createAtomicBoolValue(); auto &Y = Context.createAtomicBoolValue(); - auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y); - auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y); + auto &XAndY1 = Context.getOrCreateConjunction(X, Y); + auto &XAndY2 = Context.getOrCreateConjunction(X, Y); EXPECT_EQ(&XAndY1, &XAndY2); - auto &YAndX = Context.getOrCreateConjunctionValue(Y, X); + auto &YAndX = Context.getOrCreateConjunction(Y, X); EXPECT_EQ(&XAndY1, &YAndX); auto &Z = Context.createAtomicBoolValue(); - auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z); + auto &XAndZ = Context.getOrCreateConjunction(X, Z); EXPECT_NE(&XAndY1, &XAndZ); } TEST_F(DataflowAnalysisContextTest, - GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) { + GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) { auto &X = Context.createAtomicBoolValue(); - auto &XOrX = Context.getOrCreateDisjunctionValue(X, X); + auto &XOrX = Context.getOrCreateDisjunction(X, X); EXPECT_EQ(&XOrX, &X); } TEST_F(DataflowAnalysisContextTest, - GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) { + GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { auto &X = Context.createAtomicBoolValue(); auto &Y = Context.createAtomicBoolValue(); - auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y); - auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y); + auto &XOrY1 = Context.getOrCreateDisjunction(X, Y); + auto &XOrY2 = Context.getOrCreateDisjunction(X, Y); EXPECT_EQ(&XOrY1, &XOrY2); - auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X); + auto &YOrX = Context.getOrCreateDisjunction(Y, X); EXPECT_EQ(&XOrY1, &YOrX); auto &Z = Context.createAtomicBoolValue(); - auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z); + auto &XOrZ = Context.getOrCreateDisjunction(X, Z); EXPECT_NE(&XOrY1, &XOrZ); } TEST_F(DataflowAnalysisContextTest, - GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) { + GetOrCreateNegationReturnsSameExprOnSubsequentCalls) { auto &X = Context.createAtomicBoolValue(); - auto &NotX1 = Context.getOrCreateNegationValue(X); - auto &NotX2 = Context.getOrCreateNegationValue(X); + auto &NotX1 = Context.getOrCreateNegation(X); + auto &NotX2 = Context.getOrCreateNegation(X); EXPECT_EQ(&NotX1, &NotX2); auto &Y = Context.createAtomicBoolValue(); - auto &NotY = Context.getOrCreateNegationValue(Y); + auto &NotY = Context.getOrCreateNegation(Y); EXPECT_NE(&NotX1, &NotY); } +TEST_F(DataflowAnalysisContextTest, + GetOrCreateImplicationReturnsTrueGivenSameArgs) { + auto &X = Context.createAtomicBoolValue(); + auto &XImpliesX = Context.getOrCreateImplication(X, X); + EXPECT_EQ(&XImpliesX, &Context.getBoolLiteralValue(true)); +} + +TEST_F(DataflowAnalysisContextTest, + GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) { + auto &X = Context.createAtomicBoolValue(); + auto &Y = Context.createAtomicBoolValue(); + auto &XImpliesY1 = Context.getOrCreateImplication(X, Y); + auto &XImpliesY2 = Context.getOrCreateImplication(X, Y); + EXPECT_EQ(&XImpliesY1, &XImpliesY2); + + auto &YImpliesX = Context.getOrCreateImplication(Y, X); + EXPECT_NE(&XImpliesY1, &YImpliesX); + + auto &Z = Context.createAtomicBoolValue(); + auto &XImpliesZ = Context.getOrCreateImplication(X, Z); + EXPECT_NE(&XImpliesY1, &XImpliesZ); +} + +TEST_F(DataflowAnalysisContextTest, GetOrCreateIffReturnsTrueGivenSameArgs) { + auto &X = Context.createAtomicBoolValue(); + auto &XIffX = Context.getOrCreateIff(X, X); + EXPECT_EQ(&XIffX, &Context.getBoolLiteralValue(true)); +} + +TEST_F(DataflowAnalysisContextTest, + GetOrCreateIffReturnsSameExprOnSubsequentCalls) { + auto &X = Context.createAtomicBoolValue(); + auto &Y = Context.createAtomicBoolValue(); + auto &XIffY1 = Context.getOrCreateIff(X, Y); + auto &XIffY2 = Context.getOrCreateIff(X, Y); + EXPECT_EQ(&XIffY1, &XIffY2); + + auto &YIffX = Context.getOrCreateIff(Y, X); + EXPECT_EQ(&XIffY1, &YIffX); + + auto &Z = Context.createAtomicBoolValue(); + auto &XIffZ = Context.getOrCreateIff(X, Z); + EXPECT_NE(&XIffY1, &XIffZ); +} + TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) { auto &FC = Context.makeFlowConditionToken(); auto &C = Context.createAtomicBoolValue(); @@ -164,8 +209,7 @@ // ... but we can prove A || !A is true. auto &FC5 = Context.makeFlowConditionToken(); Context.addFlowConditionConstraint( - FC5, Context.getOrCreateDisjunctionValue( - C1, Context.getOrCreateNegationValue(C1))); + FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1))); EXPECT_TRUE(Context.flowConditionIsTautology(FC5)); } diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp @@ -33,18 +33,6 @@ Environment Env; }; -TEST_F(EnvironmentTest, MakeImplicationReturnsTrueGivenSameArgs) { - auto &X = Env.makeAtomicBoolValue(); - auto &XEqX = Env.makeImplication(X, X); - EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true)); -} - -TEST_F(EnvironmentTest, MakeIffReturnsTrueGivenSameArgs) { - auto &X = Env.makeAtomicBoolValue(); - auto &XEqX = Env.makeIff(X, X); - EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true)); -} - TEST_F(EnvironmentTest, FlowCondition) { EXPECT_TRUE(Env.flowConditionImplies(Env.getBoolLiteralValue(true))); EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));