samestep updated this revision to Diff 447656.
samestep added a comment.
Rebase and add Yitzie's assertion
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D130270/new/
https://reviews.llvm.org/D130270
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -1175,4 +1175,33 @@
});
}
+TEST_F(FlowConditionTest, JoinBackedge) {
+ std::string Code = R"(
+ void target(bool Cond) {
+ bool Foo = true;
+ while (true) {
+ (void)0;
+ // [[p]]
+ Foo = false;
+ }
+ }
+ )";
+ runDataflow(
+ Code, [](llvm::ArrayRef<
+ std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+ Results,
+ ASTContext &ASTCtx) {
+ ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+ const Environment &Env = Results[0].second.Env;
+
+ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+ ASSERT_THAT(FooDecl, NotNull());
+
+ auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+
+ EXPECT_FALSE(Env.flowConditionImplies(FooVal));
+ EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
+ });
+}
+
} // namespace
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -179,7 +179,8 @@
Context.addFlowConditionConstraint(FC2, C2);
Context.addFlowConditionConstraint(FC2, C3);
- auto &FC3 = Context.joinFlowConditions(FC1, FC2);
+ auto &B = Context.createAtomicBoolValue();
+ auto &FC3 = Context.joinFlowConditions(FC1, FC2, B);
EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
@@ -435,38 +436,49 @@
// FC2 = Y
auto &FC2 = Context.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, Y);
- // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
- auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
+ // JoinedFC = ((!B && FC1) || (B && FC2)) && Z = ((!B && X) || (B && Y)) && Z
+ auto &B = Context.createAtomicBoolValue();
+ auto &JoinedFC = Context.joinFlowConditions(FC1, FC2, B);
Context.addFlowConditionConstraint(JoinedFC, Z);
- // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
- // to evaluating the remaining Z
- auto &JoinedFCWithXTrue =
- Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
- auto &JoinedFCWithYTrue =
- Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
+ // If any of (!B && X), (B && Y) is true in JoinedFC,
+ // JoinedFC = ((!B && X) || (B && Y)) && Z is equivalent to evaluating the
+ // remaining Z
+ auto &JoinedFCWithXTrue = Context.buildAndSubstituteFlowCondition(
+ JoinedFC, {{&B, &False}, {&X, &True}});
+ auto &JoinedFCWithYTrue = Context.buildAndSubstituteFlowCondition(
+ JoinedFC, {{&B, &True}, {&Y, &True}});
EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
- // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
- // evaluating the remaining disjunction (X || Y)
+ // If Z is true in JoinedFC, JoinedFC = ((!B && X) || (B && Y)) && Z is
+ // equivalent to evaluating the remaining disjunction ((!B && X) || (B && Y))
auto &JoinedFCWithZTrue =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
EXPECT_TRUE(Context.equivalentBoolValues(
- JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
-
- // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
- // to evaluating the conjunction of the other value and Z
+ JoinedFCWithZTrue,
+ Context.getOrCreateDisjunction(
+ Context.getOrCreateConjunction(Context.getOrCreateNegation(B), X),
+ Context.getOrCreateConjunction(B, Y))));
+
+ // If any of X, Y is false in JoinedFC,
+ // JoinedFC = ((!B && X) || (B && Y)) && Z is equivalent to evaluating the
+ // conjunction of the other disjunct and Z
auto &JoinedFCWithXFalse =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
auto &JoinedFCWithYFalse =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
EXPECT_TRUE(Context.equivalentBoolValues(
- JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
+ JoinedFCWithXFalse,
+ Context.getOrCreateConjunction(Context.getOrCreateConjunction(B, Y), Z)));
EXPECT_TRUE(Context.equivalentBoolValues(
- JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
+ JoinedFCWithYFalse,
+ Context.getOrCreateConjunction(
+ Context.getOrCreateConjunction(Context.getOrCreateNegation(B), X),
+ Z)));
- // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
+ // If Z is false in JoinedFC, JoinedFC = ((!B && X) || (B && Y)) && Z must be
+ // false
auto &JoinedFCWithZFalse =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -77,19 +77,17 @@
const Environment &Env1, Value *Val2,
const Environment &Env2,
Environment &MergedEnv,
- Environment::ValueModel &Model) {
+ Environment::ValueModel &Model,
+ AtomicBoolValue &TookSecondBranch) {
// Join distinct boolean values preserving information about the constraints
// in the respective path conditions.
- //
- // FIXME: Does not work for backedges, since the two (or more) paths will not
- // have mutually exclusive conditions.
if (auto *Expr1 = dyn_cast<BoolValue>(Val1)) {
auto *Expr2 = cast<BoolValue>(Val2);
auto &MergedVal = MergedEnv.makeAtomicBoolValue();
MergedEnv.addToFlowCondition(MergedEnv.makeOr(
- MergedEnv.makeAnd(Env1.getFlowConditionToken(),
+ MergedEnv.makeAnd(MergedEnv.makeNot(TookSecondBranch),
MergedEnv.makeIff(MergedVal, *Expr1)),
- MergedEnv.makeAnd(Env2.getFlowConditionToken(),
+ MergedEnv.makeAnd(TookSecondBranch,
MergedEnv.makeIff(MergedVal, *Expr2))));
return &MergedVal;
}
@@ -251,9 +249,11 @@
if (MemberLocToStruct.size() != JoinedEnv.MemberLocToStruct.size())
Effect = LatticeJoinEffect::Changed;
+ auto &TookSecondBranch = DACtx->createAtomicBoolValue();
+
// FIXME: set `Effect` as needed.
JoinedEnv.FlowConditionToken = &DACtx->joinFlowConditions(
- *FlowConditionToken, *Other.FlowConditionToken);
+ *FlowConditionToken, *Other.FlowConditionToken, TookSecondBranch);
for (auto &Entry : LocToVal) {
const StorageLocation *Loc = Entry.first;
@@ -272,8 +272,9 @@
continue;
}
- if (Value *MergedVal = mergeDistinctValues(
- Loc->getType(), Val, *this, It->second, Other, JoinedEnv, Model))
+ if (Value *MergedVal =
+ mergeDistinctValues(Loc->getType(), Val, *this, It->second, Other,
+ JoinedEnv, Model, TookSecondBranch))
JoinedEnv.LocToVal.insert({Loc, MergedVal});
}
if (LocToVal.size() != JoinedEnv.LocToVal.size())
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -147,12 +147,16 @@
AtomicBoolValue &
DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
- AtomicBoolValue &SecondToken) {
+ AtomicBoolValue &SecondToken,
+ AtomicBoolValue &TookSecondBranch) {
auto &Token = makeFlowConditionToken();
FlowConditionDeps[&Token].insert(&FirstToken);
FlowConditionDeps[&Token].insert(&SecondToken);
- addFlowConditionConstraint(Token,
- getOrCreateDisjunction(FirstToken, SecondToken));
+ addFlowConditionConstraint(
+ Token, getOrCreateDisjunction(
+ getOrCreateConjunction(getOrCreateNegation(TookSecondBranch),
+ FirstToken),
+ getOrCreateConjunction(TookSecondBranch, SecondToken)));
return Token;
}
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -212,11 +212,13 @@
/// condition identified by `Token` and returns its token.
AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
- /// Creates a new flow condition that represents the disjunction of the flow
- /// conditions identified by `FirstToken` and `SecondToken`, and returns its
- /// token.
+ /// Creates and returns a token for a new flow condition asserting that if
+ /// `TookSecondBranch` is false then the flow condition identified by
+ /// `FirstToken` is true, and if `TookSecondBranch` is true then the flow
+ /// condition identified by `SecondToken` is true.
AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
- AtomicBoolValue &SecondToken);
+ AtomicBoolValue &SecondToken,
+ AtomicBoolValue &TookSecondBranch);
// FIXME: This function returns the flow condition expressed directly as its
// constraints: (C1 AND C2 AND ...). This differs from the general approach in
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
