[clang][dataflow] Use a dedicated bool to encode which branch was taken

[samestep]

Summary

This is a continuation of D129289 using @sgatev's feedback.

This patch attempts to resolve a FIXME in DataflowEnvironment.cpp about merging BoolValues when the two flow conditions are not mutually exclusive. The issue here is that we are using the truth value of each flow condition as a proxy for the idea of whether or not we took that branch, which breaks down on backedges.

To try to resolve the issue, this patch creates one additional AtomicBoolValue to explicitly represent which branch we took, and uses that directly within mergeDistinctValues. As currently written, this doesn't quite seem to work: the JoinBackedge test added by this patch fails both before and after the patch is applied.

[ymandel]

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

439–441

I'm a bit concerned by the need to update this (essentially) unrelated test. It implies the test is depending on implementation details that it shouldn't be concerned with.

Not for this patch, but if you have thoughts on how to simplify this test to do what it needs w/o being tied to the details of how joins work, that would be appreciated. At least, it seems worth a FIXME.

thanks

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

1202

should we also test the inverse?

EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));

That is, I would think we want to show that neither is provable.

[samestep]

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

439–441

Agreed, this test seems a bit awkward; in this patch I was just focusing on updating it instead of rethinking it.

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

1202

Sure, that makes sense; if I remember correctly, the inverse of FooVal is indeed not provable already. You're right that it would be good to test both here, though.

[gribozavr2]

Sorry, could you rebase the patch? It does not apply cleanly anymore.

[samestep]

Rebase and add Yitzie's assertion

[samestep]

In D130270#3679273, @gribozavr2 wrote:

Sorry, could you rebase the patch? It does not apply cleanly anymore.

Done; I didn't see any conflicts when I rebased, but hopefully the issue on your end is resolved now?

[samestep]

Rebase

[samestep]

@gribozavr2 I rebased again, should work now.

[sgatev]

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

103

We should probably pass TookSecondBranch here so that models can also use it in the implementation of merge. Could be in a follow up, but let's leave a FIXME.

[samestep]

Add FIXME about passing TookSecondBranch to merge

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

103

FIXME added; thanks!

[ymandel]

It turns out that this change wasn't necessary. I've deleted the relevant FIXME in https://reviews.llvm.org/rGabc16c7a5b0a63d14172262153608b3d24de957f.

AFAICT, the reason that the new test JoinBackedge fails at HEAD is because we discard the results of analyzing the function body, so the update Foo = false is simply ignored. This hypothesis rests on observing that each block is visited only once during analysis of the test. It's also consistent with the known (broken) behavior of our comparison operator. Interestingly, this is a nicely stark illustration of the unsoundness of our current approach. :( So, this test will be useful in the future when add proper widening.

[samestep]

@ymandel Huh, interesting! I'll go ahead and abandon this patch, then?

[ymandel]

In D130270#3780705, @samestep wrote:

@ymandel Huh, interesting! I'll go ahead and abandon this patch, then?

Please. Sorry I didn't catch this earlier!

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

public:
   /// Adds `Constraint` to the flow condition identified by `Token`.
   void addFlowConditionConstraint(AtomicBoolValue &Token,
                                   BoolValue &Constraint);
 
   /// Creates a new flow condition with the same constraints as the flow
   /// 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
   // the framework where a flow condition is represented as a token (an atomic
   // boolean) with dependencies and constraints tracked in `FlowConditionDeps`
   // and `FlowConditionConstraints`: (FC <=> C1 AND C2 AND ...).
   // Consider if we should make the representation of flow condition consistent,
   // returning an atomic boolean token with separate constraints instead.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
   auto &ForkToken = makeFlowConditionToken();
   FlowConditionDeps[&ForkToken].insert(&Token);
   addFlowConditionConstraint(ForkToken, Token);
   return ForkToken;
 }
 
 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;
 }
 
 Solver::Result
 DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
   Constraints.insert(&getBoolLiteralValue(true));
   Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false)));
   return S->solve(std::move(Constraints));

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

 /// Attempts to merge distinct values `Val1` and `Val2` in `Env1` and `Env2`,
 /// respectively, of the same type `Type`. Merging generally produces a single
 /// value that (soundly) approximates the two inputs, although the actual
 /// meaning depends on `Model`.
 static Value *mergeDistinctValues(QualType Type, Value *Val1,
                                   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;
   }
 
   // FIXME: add unit tests that cover this statement.
   if (areEquivalentIndirectionValues(Val1, Val2)) {
     return Val1;
   }
 
   // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
   // returns false to avoid storing unneeded values in `DACtx`.
   if (Value *MergedVal = MergedEnv.createValue(Type))
     if (Model.merge(Type, *Val1, Env1, *Val2, Env2, *MergedVal, MergedEnv))
       return MergedVal;
 
   return nullptr;
 }
 
 /// Initializes a global storage value.
 static void initGlobalVar(const VarDecl &D, Environment &Env) {
   if (!D.hasGlobalStorage() ||
LatticeJoinEffect Environment::join(const Environment &Other,
   if (ExprToLoc.size() != JoinedEnv.ExprToLoc.size())
     Effect = LatticeJoinEffect::Changed;
 
   JoinedEnv.MemberLocToStruct =
       intersectDenseMaps(MemberLocToStruct, Other.MemberLocToStruct);
   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;
     assert(Loc != nullptr);
 
     Value *Val = Entry.second;
     assert(Val != nullptr);
 
     auto It = Other.LocToVal.find(Loc);
     if (It == Other.LocToVal.end())
       continue;
     assert(It->second != nullptr);
 
     if (Val == It->second) {
       JoinedEnv.LocToVal.insert({Loc, Val});
       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())
     Effect = LatticeJoinEffect::Changed;
 
   *this = std::move(JoinedEnv);
 
   return Effect;

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
   auto &FC1 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC1, C1);
   Context.addFlowConditionConstraint(FC1, C3);
 
   auto &FC2 = Context.makeFlowConditionToken();
   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));
 }
 
 TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
   // Fresh flow condition with empty/no constraints is always true.
   auto &FC1 = Context.makeFlowConditionToken();
TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
   auto &False = Context.getBoolLiteralValue(false);
 
   // FC1 = X
   auto &FC1 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC1, X);
   // 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));
 }
 
 } // namespace

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

runDataflow(
 
         const Environment &Env2 = Results[0].second.Env;
         auto &FooVal2 =
             *cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::Reference));
         EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
       });
 }
 
+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