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 @@ -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 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 @@ -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; } diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/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(Val1)) { auto *Expr2 = cast(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()) 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 @@ -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)); diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp +++ b/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>> + 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(Env.getValue(*FooDecl, SkipPast::None)); + + EXPECT_FALSE(Env.flowConditionImplies(FooVal)); + EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal))); + }); +} + } // namespace