[clang][dataflow] Fix `Environment::join`'s handling of flow condition merging

[ymandel]

Summary

The current implementation mutates the environment as it performs the
join. However, that interferes with the call to the model's merge operation,
which can modify MergedEnv. Since any modifications are assumed to apply to
the post-join environment, providing the same environment for both is
incorrect. This mismatch is a particular concern for joining the flow
conditions, where modifications in the old environment may not be propagated to
the new one.

[xazax.hun]

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

69

Typo: Val2.

72–73

Would it make sense to make Env1 const?

[ymandel]

address review comments

[ymandel]

Thanks!

[sgatev]

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

339–341

This comment is no longer relevant, right?

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

299

340–344

356

That's guaranteed to be false in compareEquivalent.

364–368

414

422

Add /*[[p3]]*/ after this statement and ensure that the value is implied in the "else" branch.

[ymandel]

address comments

[ymandel]

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

356

I thought just Val1 == Val2 was guaranteed false? Also, I see that the variable naming could be confusing, so I've renamed.

[sgatev]

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

356

Right. I think I misread it. Having IsSet1 == IsSet2 here makes sense to me. Though, if the test only needs the second part, I suggest removing this to simplify the setup.

[ymandel]

address comments

[ymandel]

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

356

agreed. done

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

if (auto *IndVal1 = dyn_cast<IndirectionValue>(Val1)) {
     assert(IndVal1->getKind() == IndVal2->getKind());
     if (&IndVal1->getPointeeLoc() == &IndVal2->getPointeeLoc())
       return true;
   }
 
   return Model.compareEquivalent(Type, *Val1, Env1, *Val2, Env2);
 }
 
-/// Attempts to merge distinct values `Val1` and `Val1` in `Env1` and `Env2`,
+/// 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, Environment &Env1,
-                                  Value *Val2, const Environment &Env2,
+static Value *mergeDistinctValues(QualType Type, Value *Val1,
+                                  const Environment &Env1, Value *Val2,
+                                  const Environment &Env2,
+                                  Environment &MergedEnv,
                                   Environment::ValueModel &Model) {
   // Join distinct boolean values preserving information about the constraints
   // in the respective path conditions. Note: this construction can, in
   // principle, result in exponential growth in the size of boolean values.
   // Potential optimizations may be worth considering. For example, represent
   // the flow condition of each environment using a bool atom and store, in
   // `DataflowAnalysisContext`, a mapping of bi-conditionals between flow
   // condition atoms and flow condition constraints. Something like:
   // \code
   //   FC1 <=> C1 ^ C2
   //   FC2 <=> C2 ^ C3 ^ C4
   //   FC3 <=> (FC1 v FC2) ^ C5
   // \code
   // Then, we can track dependencies between flow conditions (e.g. above `FC3`
   // depends on `FC1` and `FC2`) and modify `flowConditionImplies` to construct
   // a formula that includes the bi-conditionals for all flow condition atoms in
   // the transitive set, before invoking the solver.
   //
   // 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)) {
     for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) {
-      Expr1 = &Env1.makeAnd(*Expr1, *Constraint);
+      Expr1 = &MergedEnv.makeAnd(*Expr1, *Constraint);
     }
     auto *Expr2 = cast<BoolValue>(Val2);
     for (BoolValue *Constraint : Env2.getFlowConditionConstraints()) {
-      Expr2 = &Env1.makeAnd(*Expr2, *Constraint);
+      Expr2 = &MergedEnv.makeAnd(*Expr2, *Constraint);
     }
-    return &Env1.makeOr(*Expr1, *Expr2);
+    return &MergedEnv.makeOr(*Expr1, *Expr2);
   }
 
   // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
   // returns false to avoid storing unneeded values in `DACtx`.
-  if (Value *MergedVal = Env1.createValue(Type))
-    if (Model.merge(Type, *Val1, Env1, *Val2, Env2, *MergedVal, Env1))
+  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,
                                     Environment::ValueModel &Model) {
   assert(DACtx == Other.DACtx);
 
   auto Effect = LatticeJoinEffect::Unchanged;
 
-  const unsigned DeclToLocSizeBefore = DeclToLoc.size();
-  DeclToLoc = intersectDenseMaps(DeclToLoc, Other.DeclToLoc);
-  if (DeclToLocSizeBefore != DeclToLoc.size())
+  Environment JoinedEnv(*DACtx);
+
+  JoinedEnv.DeclToLoc = intersectDenseMaps(DeclToLoc, Other.DeclToLoc);
+  if (DeclToLoc.size() != JoinedEnv.DeclToLoc.size())
     Effect = LatticeJoinEffect::Changed;
 
-  const unsigned ExprToLocSizeBefore = ExprToLoc.size();
-  ExprToLoc = intersectDenseMaps(ExprToLoc, Other.ExprToLoc);
-  if (ExprToLocSizeBefore != ExprToLoc.size())
+  JoinedEnv.ExprToLoc = intersectDenseMaps(ExprToLoc, Other.ExprToLoc);
+  if (ExprToLoc.size() != JoinedEnv.ExprToLoc.size())
     Effect = LatticeJoinEffect::Changed;
 
-  const unsigned MemberLocToStructSizeBefore = MemberLocToStruct.size();
-  MemberLocToStruct =
+  JoinedEnv.MemberLocToStruct =
       intersectDenseMaps(MemberLocToStruct, Other.MemberLocToStruct);
-  if (MemberLocToStructSizeBefore != MemberLocToStruct.size())
+  if (MemberLocToStruct.size() != JoinedEnv.MemberLocToStruct.size())
     Effect = LatticeJoinEffect::Changed;
 
+  // FIXME: set `Effect` as needed.
+  JoinedEnv.FlowConditionConstraints = joinConstraints(
+      DACtx, FlowConditionConstraints, Other.FlowConditionConstraints);
+
   // Move `LocToVal` so that `Environment::ValueModel::merge` can safely assign
   // values to storage locations while this code iterates over the current
   // assignments.
-  llvm::DenseMap<const StorageLocation *, Value *> OldLocToVal =
-      std::move(LocToVal);
-  for (auto &Entry : OldLocToVal) {
+  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) {
-      LocToVal.insert({Loc, Val});
+      JoinedEnv.LocToVal.insert({Loc, Val});
       continue;
     }
 
-    if (Value *MergedVal = mergeDistinctValues(Loc->getType(), Val, *this,
-                                               It->second, Other, Model))
-      LocToVal.insert({Loc, MergedVal});
+    if (Value *MergedVal = mergeDistinctValues(
+            Loc->getType(), Val, *this, It->second, Other, JoinedEnv, Model))
+      JoinedEnv.LocToVal.insert({Loc, MergedVal});
   }
-  if (OldLocToVal.size() != LocToVal.size())
+  if (LocToVal.size() != JoinedEnv.LocToVal.size())
     Effect = LatticeJoinEffect::Changed;
 
-  FlowConditionConstraints = joinConstraints(DACtx, FlowConditionConstraints,
-                                             Other.FlowConditionConstraints);
+  *this = std::move(JoinedEnv);
 
   return Effect;
 }
 
 StorageLocation &Environment::createStorageLocation(QualType Type) {
   assert(!Type.isNull());
   if (Type->isStructureOrClassType() || Type->isUnionType()) {
     // FIXME: Explore options to avoid eager initialization of fields as some of

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

 //===- unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp ===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 
 #include "NoopAnalysis.h"
 #include "TestingSupport.h"
 #include "clang/AST/Decl.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/AST/Type.h"
 #include "clang/ASTMatchers/ASTMatchFinder.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
std::string Code = R"(
     }
   )";
   runDataflow(Code, UnorderedElementsAre(
                         Pair("p", HoldsFunctionCallLattice(HasCalledFunctions(
                                       UnorderedElementsAre("baz", "foo"))))));
   // FIXME: Called functions at point `p` should contain only "foo".
 }
 
+// Models an analysis that uses the flow conditions.
+class SpecialBoolAnalysis
+    : public DataflowAnalysis<SpecialBoolAnalysis, NoopLattice> {
+public:
+  explicit SpecialBoolAnalysis(ASTContext &Context)
+      : DataflowAnalysis<SpecialBoolAnalysis, NoopLattice>(Context) {}
+
+  static NoopLattice initialElement() { return {}; }
+
+  void transfer(const Stmt *S, NoopLattice &, Environment &Env) {
+    auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
+    auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
+
+    if (const auto *E = selectFirst<CXXConstructExpr>(
+            "call", match(cxxConstructExpr(HasSpecialBoolType).bind("call"), *S,
+                          getASTContext()))) {
+      auto &ConstructorVal = *cast<StructValue>(Env.createValue(E->getType()));
+      ConstructorVal.setProperty("is_set", Env.getBoolLiteralValue(false));
+      Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
+    } else if (const auto *E = selectFirst<CXXMemberCallExpr>(
+                   "call", match(cxxMemberCallExpr(callee(cxxMethodDecl(ofClass(
+                                                       SpecialBoolRecordDecl))))
+                                     .bind("call"),
+                                 *S, getASTContext()))) {
+      auto *Object = E->getImplicitObjectArgument();
+      assert(Object != nullptr);
+
+      auto *ObjectLoc =
+          Env.getStorageLocation(*Object, SkipPast::ReferenceThenPointer);
+      assert(ObjectLoc != nullptr);
+
+      auto &ConstructorVal =
+          *cast<StructValue>(Env.createValue(Object->getType()));
+      ConstructorVal.setProperty("is_set", Env.getBoolLiteralValue(true));
+      Env.setValue(*ObjectLoc, ConstructorVal);
+    }
+  }
+
+  bool compareEquivalent(QualType Type, const Value &Val1,
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) final {
+    if (!Type->isRecordType())
+      return false;
+    const auto *Decl = Type->getAsCXXRecordDecl();
+    if (Decl->getIdentifier() == nullptr || Decl->getName() != "SpecialBool")
+      return false;
+
+    auto *V1 = cast_or_null<BoolValue>(
+        cast<StructValue>(&Val1)->getProperty("is_set"));
+    if (V1 == nullptr)
+      return true;
+
+    auto *V2 = cast_or_null<BoolValue>(
+        cast<StructValue>(&Val2)->getProperty("is_set"));
+    if (V2 == nullptr)
+      return false;
+
+    return V1 == V2 ||
+           Env1.flowConditionImplies(*V1) == Env2.flowConditionImplies(*V2);
+  }
+
+  // Always returns `true` to accept the `MergedVal`.
+  bool merge(QualType Type, const Value &Val1, const Environment &Env1,
+             const Value &Val2, const Environment &Env2, Value &MergedVal,
+             Environment &MergedEnv) final {
+    if (!Type->isRecordType())
+      return true;
+    const auto *Decl = Type->getAsCXXRecordDecl();
+    if (Decl->getIdentifier() == nullptr || Decl->getName() != "SpecialBool")
+      return true;
+
+    auto *V1 = cast_or_null<BoolValue>(
+        cast<StructValue>(&Val1)->getProperty("is_set"));
+    if (V1 == nullptr)
+      return true;
+
+    auto *V2 = cast_or_null<BoolValue>(
+        cast<StructValue>(&Val2)->getProperty("is_set"));
+    if (V2 == nullptr)
+      return true;
+
+    auto &V = MergedEnv.makeAtomicBoolValue();
+    cast<StructValue>(&MergedVal)->setProperty("is_set", V);
+    if (Env1.flowConditionImplies(*V1) && Env2.flowConditionImplies(*V2))
+      MergedEnv.addToFlowCondition(V);
+
+    return true;
+  }
+};
+
+class JoinFlowConditionsTest : public Test {
+protected:
+  template <typename Matcher>
+  void runDataflow(llvm::StringRef Code, Matcher Match) {
+    ASSERT_THAT_ERROR(
+        test::checkDataflow<SpecialBoolAnalysis>(
+            Code, "target",
+            [](ASTContext &Context, Environment &Env) {
+              return SpecialBoolAnalysis(Context);
+            },
+            [&Match](
+                llvm::ArrayRef<
+                    std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                    Results,
+                ASTContext &ASTCtx) { Match(Results, ASTCtx); },
+            {"-fsyntax-only", "-std=c++17"}),
+        llvm::Succeeded());
+  }
+};
+
+TEST_F(JoinFlowConditionsTest, JoinDistinctButProvablyEquivalentValues) {
+  std::string Code = R"(
+    struct SpecialBool {
+      SpecialBool() = default;
+      void set();
+    };
+    void target(bool Cond) {
+      SpecialBool Foo;
+      /*[[p1]]*/
+      if (Cond) {
+        Foo.set();
+        /*[[p2]]*/
+      } else {
+        Foo.set();
+      }
+      (void)0;
+      /*[[p3]]*/
+    }
+  )";
+  runDataflow(
+      Code, [](llvm::ArrayRef<
+                   std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                   Results,
+               ASTContext &ASTCtx) {
+        ASSERT_THAT(Results,
+                    ElementsAre(Pair("p3", _), Pair("p2", _), Pair("p1", _)));
+        const Environment &Env1 = Results[2].second.Env;
+        const Environment &Env2 = Results[1].second.Env;
+        const Environment &Env3 = Results[0].second.Env;
+
+        const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return cast<BoolValue>(
+              cast<StructValue>(Env.getValue(*FooDecl, SkipPast::None))
+                  ->getProperty("is_set"));
+        };
+
+        EXPECT_FALSE(Env1.flowConditionImplies(*GetFooValue(Env1)));
+        EXPECT_TRUE(Env2.flowConditionImplies(*GetFooValue(Env2)));
+        EXPECT_TRUE(Env3.flowConditionImplies(*GetFooValue(Env3)));
+      });
+}
+
 class OptionalIntAnalysis
     : public DataflowAnalysis<OptionalIntAnalysis, NoopLattice> {
 public:
   explicit OptionalIntAnalysis(ASTContext &Context, BoolValue &HasValueTop)
       : DataflowAnalysis<OptionalIntAnalysis, NoopLattice>(Context),
         HasValueTop(HasValueTop) {}
 
   static NoopLattice initialElement() { return {}; }