[clang] 00e9d53 - [clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`.
Dmitri Gribenko via cfe-commits
cfe-commits at lists.llvm.org
Fri Jun 24 14:16:50 PDT 2022
Author: Wei Yi Tee
Date: 2022-06-24T23:16:44+02:00
New Revision: 00e9d53453abc8f2e3d69e9c7fba83dc65a74259
URL: https://github.com/llvm/llvm-project/commit/00e9d53453abc8f2e3d69e9c7fba83dc65a74259
DIFF: https://github.com/llvm/llvm-project/commit/00e9d53453abc8f2e3d69e9c7fba83dc65a74259.diff
LOG: [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
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 48d0eedc49dde..9f89b2ff5b831 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -151,17 +151,29 @@ class DataflowAnalysisContext {
/// `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
index 0a2c75f804c2a..ac49d22995c1d 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -268,7 +268,7 @@ class Environment {
/// 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 @@ class Environment {
/// 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 @@ class Environment {
/// 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
index ffd552b1fdc72..10e7df394f40f 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -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);
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index b8a9ef52504af..1ff7cf1dce9ef 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -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));
}
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
index 51b40f2319878..434bc6b8042ee 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
@@ -33,18 +33,6 @@ class EnvironmentTest : public ::testing::Test {
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)));
More information about the cfe-commits
mailing list