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

[samestep]

Summary

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 two additional AtomicBoolValues to directly represent which branch we took, and uses those directly within mergeDistinctValues. As currently written, this doesn't quite work: it compiles, but 20 tests from ClangAnalysisFlowSensitiveTests fail. This patch is therefore simply meant as a starting point for discussion on how to properly resolve this issue.

[ymandel]

Can you give some examples (or the whole list) of failing tests?

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

154–156

Should we also include TookFirstBranchToken \/ TookSecondBranchToken? If so, i suppose we could also rephrase as (NOT First AND Second) OR (First AND NOT Second) which may get at the point a bit more directly.

[samestep]

In D129289#3638756, @ymandel wrote:

Can you give some examples (or the whole list) of failing tests?

Yeah, I was going to do that originally but the log was too long so I couldn't scroll all the way up in my terminal history. Anyways, here's a pastebin: https://pastebin.com/uir7YKNL

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

154–156

That should already be covered by the other constraint added below, right? Although actually, now I'm thinking that since we have exactly two choices, maybe we should just use one single TookFirstBranchToken, where "true" means we took the first branch and "false" means we took the second branch.

[ymandel]

In D129289#3638847, @samestep wrote:

In D129289#3638756, @ymandel wrote:

Can you give some examples (or the whole list) of failing tests?

Yeah, I was going to do that originally but the log was too long so I couldn't scroll all the way up in my terminal history. Anyways, here's a pastebin: https://pastebin.com/uir7YKNL

Based on those failures, looks like it broke something fundamental. Basically, lots of conditions are now true that shouldn't be. I'd start with the FlowConditionTest cases since those are simple and their failure will probably indicate the problem pretty quickly. But, I'd first recommend making the single-bool change you mentioned.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

154–156

right. I hadn't thought it through. that said, I agree with your intuition of just using one boolean.

[sgatev]

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

219

Let's not call the new params "tokens" since they are plain bool values, not flow condition tokens.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

151–152

This shouldn't be necessary - TookFirstBranchToken and TookSecondBranchToken are not flow condition tokens.

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

public:
   /// 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.
   AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
-                                      AtomicBoolValue &SecondToken);
+                                      AtomicBoolValue &SecondToken,
+                                      AtomicBoolValue &TookFirstBranchToken,
+                                      AtomicBoolValue &TookSecondBranchToken);
 
   // 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

 AtomicBoolValue &
 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
   auto &ForkToken = makeFlowConditionToken();
   FlowConditionDeps[&ForkToken].insert(&Token);
   addFlowConditionConstraint(ForkToken, Token);
   return ForkToken;
 }
 
-AtomicBoolValue &
-DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
-                                            AtomicBoolValue &SecondToken) {
+AtomicBoolValue &DataflowAnalysisContext::joinFlowConditions(
+    AtomicBoolValue &FirstToken, AtomicBoolValue &SecondToken,
+    AtomicBoolValue &TookFirstBranchToken,
+    AtomicBoolValue &TookSecondBranchToken) {
   auto &Token = makeFlowConditionToken();
+  FlowConditionDeps[&Token].insert(&TookFirstBranchToken);
+  FlowConditionDeps[&Token].insert(&TookSecondBranchToken);
+  addFlowConditionConstraint(
+      Token, getOrCreateDisjunction(
+                 getOrCreateNegation(TookFirstBranchToken),
+                 getOrCreateNegation(TookSecondBranchToken)));
   FlowConditionDeps[&Token].insert(&FirstToken);
   FlowConditionDeps[&Token].insert(&SecondToken);
-  addFlowConditionConstraint(Token,
-                             getOrCreateDisjunction(FirstToken, SecondToken));
+  addFlowConditionConstraint(
+      Token, getOrCreateDisjunction(
+                 getOrCreateConjunction(TookFirstBranchToken, FirstToken),
+                 getOrCreateConjunction(TookSecondBranchToken, 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 &TookLeftBranchToken,
+                                  AtomicBoolValue &TookRightBranchToken) {
   // 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(TookLeftBranchToken,
                           MergedEnv.makeIff(MergedVal, *Expr1)),
-        MergedEnv.makeAnd(Env2.getFlowConditionToken(),
+        MergedEnv.makeAnd(TookRightBranchToken,
                           MergedEnv.makeIff(MergedVal, *Expr2))));
     return &MergedVal;
   }
 
   // FIXME: add unit tests that cover this statement.
   if (areEquivalentIndirectionValues(Val1, Val2)) {
     return Val1;
   }
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 &TookLeftBranchToken = DACtx->createAtomicBoolValue();
+  auto &TookRightBranchToken = DACtx->createAtomicBoolValue();
+
   // FIXME: set `Effect` as needed.
-  JoinedEnv.FlowConditionToken = &DACtx->joinFlowConditions(
-      *FlowConditionToken, *Other.FlowConditionToken);
+  JoinedEnv.FlowConditionToken =
+      &DACtx->joinFlowConditions(*FlowConditionToken, *Other.FlowConditionToken,
+                                 TookLeftBranchToken, TookRightBranchToken);
 
   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))
+            Loc->getType(), Val, *this, It->second, Other, JoinedEnv, Model,
+            TookLeftBranchToken, TookRightBranchToken))
       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 &B1 = Context.createAtomicBoolValue();
+  auto &B2 = Context.createAtomicBoolValue();
+  auto &FC3 = Context.joinFlowConditions(FC1, FC2, B1, B2);
   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) {
 
   // 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);
+  auto &B1 = Context.createAtomicBoolValue();
+  auto &B2 = Context.createAtomicBoolValue();
+  auto &JoinedFC = Context.joinFlowConditions(FC1, FC2, B1, B2);
   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}});