maxjhandsome
/
llvm-project
forked from OSchip/llvm-project
1
0
Fork 0
Code Issues Pull Requests Packages Releases Wiki Activity

[clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`. 

To keep functionality of creating boolean expressions in a consistent location.

Depends On D128357

Reviewed By: gribozavr2, sgatev, xazax.hun

Differential Revision: https://reviews.llvm.org/D128519
This commit is contained in:
Wei Yi Tee 2022-06-24 21:59:16 +02:00 committed by Dmitri Gribenko
parent b8e8012aa2
commit 00e9d53453
5 changed files with 114 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
View File

@ -151,17 +151,29 @@ public:
/// `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

18
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
View File

@ -268,7 +268,7 @@ public:
/// 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 @@ public:
/// 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 @@ public:
/// 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.

47
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
View File

@ -30,9 +30,8 @@ makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
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 @@ DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
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 @@ DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
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<NegationValue>(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 @@ void DataflowAnalysisContext::addFlowConditionConstraint(
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 @@ DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
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 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
llvm::DenseSet<BoolValue *> Constraints = {
&Token,
&getBoolLiteralValue(true),
&getOrCreateNegationValue(getBoolLiteralValue(false)),
&getOrCreateNegationValue(Val),
&getOrCreateNegation(getBoolLiteralValue(false)),
&getOrCreateNegation(Val),
};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
@ -120,8 +131,8 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
// ever be false.
llvm::DenseSet<BoolValue *> Constraints = {
&getBoolLiteralValue(true),
&getOrCreateNegationValue(getBoolLiteralValue(false)),
&getOrCreateNegationValue(Token),
&getOrCreateNegation(getBoolLiteralValue(false)),
&getOrCreateNegation(Token),
};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
@ -141,11 +152,7 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
} 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);

84
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
View File

@ -33,63 +33,108 @@ TEST_F(DataflowAnalysisContextTest,
}
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 @@ TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
// ... 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));
}

12
clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
View File

@ -33,18 +33,6 @@ protected:
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)));