[clang][dataflow] Add widening API and implement it for built-in boolean model.

[ymandel]

Summary

• Adds API support for widening of lattice elements and environments,
• Updates the algorithm to apply widening where appropriate,
• Implements widening for boolean values. In the process, moves the unsoundness of comparison from the default implementation of Environment::ValueModel::compare to model-specific handling inside DataflowEnvironment::equivalentTo. This change is intended to clarify the source and location of unsoundess.

This patch is a replacement for, and was based substantially on, https://reviews.llvm.org/D131645.

[xazax.hun]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

68

We should document what is the return value for. Also I see LatticeJoinEffect instead of bool in the code, but I might be confused.

108

I wonder if LatticeJoinEffect is the right name if we also use this for widening. (Also, are we in the process of removing these?)

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

140

First, I was confused, because I thought they could be equivalent as well. But I guess this code is only called for values that are not considered equivalent. Documenting this is really useful.

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

374–378

Shouldn't we have a simple copy ctor from PrefEnv that could populate all these fields?

Also, this makes me wonder if we actually want to move some of these out from environment, since these presumably would not change between basic blocks.

[ymandel]

Rewrite widen-related comments.

[ymandel]

fix typo

[li.zhe.hua]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

166

I think this is missing a word.

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

227

[ymandel]

address comments

[ymandel]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

68

No, you're right. :) I've completely rewritten the comments -- they were outdated and wrong. They now match what we have in TypeErasedDatafllowAnalysis. Most importantly, we've dropped any mention of defaulting to join which is wrong both in fact and conceptually. Our targeted use of widen means it should not default to join -- that would be pointless, since it's prerequisites would guarantee that join(prev, cur) = cur, making the join pointless. It instead defaults to an equivalence check.

108

I had the same thought. How about just LatticeEffect? Open to other suggestions as well. Either way, though, I should update in a separate patch in case that breaks something unexpected.

As for removing -- yes, we should remove from join, because we never use it. But, it actually makes sense here.

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

227

I actually just deleted most of the comment -- I don't think the details were helpful.

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

374–378

Shouldn't we have a simple copy ctor from PrefEnv that could populate all these fields?

We *do* have such a copy constructor. The problem is that it's overkill because we want to build LocToVal ourselves by point-wise widening of the elements. For that matter, I wish we could share, rather than copy, DeclToLoc and ExprToLoc but I don't know of any way to do that. Alternatively: is it possible that we can update in place and don't need a separate WidenedEnv?

Also, this makes me wonder if we actually want to move some of these out from environment, since these presumably would not change between basic blocks.

Agreed. Added a fixme with an associated issue to track.

[xazax.hun]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

108

LatticeEffect sounds good to me.

116

Maybe this is another case where we want to mark the whole class final instead of the individual methods? It is fine to address this in a separate PR.

137

Is there ever a reason to instantiate Rank1? If no, should we do something (like make its ctor private and friends with Rank0?). Although possibly not important enough to worth the hassle.

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

466

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

374–378

For that matter, I wish we could share, rather than copy, DeclToLoc and ExprToLoc.

One way to maximize sharing (and making copies free) is to use the immutable datastructures in LLVM: https://github.com/llvm/llvm-project/blob/main/llvm/include/llvm/ADT/ImmutableMap.h

Unfortunately, these have their own costs so it might not be easy to decide when it is worth to use them. The Clang Static Analyzer was designed from the ground up with immutable data structures in mind.

On the other hand, I see that you want a more ad-hoc/opportunistic sharing. And I actually wonder if we need any sharing at all. If we are 100% sure we will do the widening, do we actually need to preserve the previous environment? Couldn't we "consume" it and move certain fields out instead of doing the more expensive copy operation when it makes sense?

424–425

Isn't some of these tautologically false, as we only read from them?

[ymandel]

reshape widen to update in place.

[ymandel]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

108

Added FIXME

116

Unfortunately not, since this class is used for CRTP.

137

No reason to instantiate it that I can see, but since it's a already private to this class, I think it's good enough. But, I just borrowed this from Eric, so I'm not an expert in this pattern. Happy to take suggested improvements.

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

374–378

We considered immutable data structures early on and decided against them, based on guesses about costs. I'm sure this is worth revisiting, but probably not outside of a comprehensive performance analysis of the framework.

Regarding this API in particular, I was basing off the needs of join, which very much requires a distinct new environment. But, I think that's the wrong model, as I've better understood what we're doing here. That catch22 for join is that you need to create new flow condition which joins the 2 incoming FCs, but you also need to (potentially) read the old FC and update the new FC during the pointwise merge of the store. So, if you update in place, neither update order (store and FC) works. If you update the FC first, then the old FC is inaccesible, but if you update the store first, then the additions to the FC end up mishandled when you create the new FC from the old ones.

AFAICT, we don't have that issue here, since we're not applying any widening to the FC. So, we can modify the FC during store widening without ill affect. I went ahead and made this change, but let me know if you see a flaw in my reasoning.

424–425

Well, Model's widen function could change them, as much as that seems wrong. I suppose we could specify in the API that it shouldn't, or we could further restructure the environment so that models don't have access to these fields. Either way, if we want these to be assertable, we'll need an API change.

But, more to the point, since I've changed it to update-in-place, we'll now also capture any changes that may have occured between Prev and Current. Those should converge pretty quickly, because they related to static features of the code, so I think this is a reasonable check now.

[ymandel]

tweaks

[xazax.hun]

LGTM, thanks!

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

116

Whoops, indeed, I missed that.

137

Let's leave as is.

[ymandel]

Does anyone else on this review thread want to review? Gabor's accepted the revision so, if not, I'll go ahead and commit.
thx

[sgatev]

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

469

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

420–421

[ymandel]

address comments

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h

 #include <type_traits>
 #include <utility>
 #include <vector>
 
 #include "clang/AST/ASTContext.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.h"
 #include "llvm/ADT/Any.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/Support/Error.h"
 
 namespace clang {
 namespace dataflow {
 
-template <typename AnalysisT, typename LatticeT, typename = std::void_t<>>
-struct HasTransferBranchFor : std::false_type {};
-
-template <typename AnalysisT, typename LatticeT>
-struct HasTransferBranchFor<
-    AnalysisT, LatticeT,
-    std::void_t<decltype(std::declval<AnalysisT>().transferBranch(
-        std::declval<bool>(), std::declval<const Stmt *>(),
-        std::declval<LatticeT &>(), std::declval<Environment &>()))>>
-    : std::true_type {};
 /// Base class template for dataflow analyses built on a single lattice type.
 ///
 /// Requirements:
 ///
 ///  `Derived` must be derived from a specialization of this class template and
 ///  must provide the following public members:
 ///   * `LatticeT initialElement()` - returns a lattice element that models the
 ///     initial state of a basic block;
 ///   * `void transfer(const CFGElement *, LatticeT &, Environment &)` - applies
 ///     the analysis transfer function for a given CFG element and lattice
 ///     element.
 ///
+///  `Derived` can optionally provide the following members:
+///  * `void transferBranch(bool Branch, const Stmt *Stmt, TypeErasedLattice &E,
+///                         Environment &Env)` - applies the analysis transfer
+///    function for a given edge from a CFG block of a conditional statement.
+///
 ///  `Derived` can optionally override the following members:
 ///   * `bool merge(QualType, const Value &, const Value &, Value &,
 ///     Environment &)` -  joins distinct values. This could be a strict
 ///     lattice join or a more general widening operation.
 ///
 ///  `LatticeT` is a bounded join-semilattice that is used by `Derived` and must
 ///  provide the following public members:
 ///   * `LatticeJoinEffect join(const LatticeT &)` - joins the object and the
 ///     argument by computing their least upper bound, modifies the object if
 ///     necessary, and returns an effect indicating whether any changes were
 ///     made to it;
 ///   * `bool operator==(const LatticeT &) const` - returns true if and only if
 ///     the object is equal to the argument.
+///
+/// `LatticeT` can optionally provide the following members:
+///  * `bool widen(const LatticeT &Previous)` - chooses a lattice element that
+///     approximates the join of this element with the argument. Widen is called
+///     at the beginning of loop bodies. It is called on the current lattice
+///     element (object) and the previous element for that program point. If
+///     `widen` is not provided, `join` is used by default.
+///
+///     Widening is needed where a join operation may prevent convergence (for a
+///     lattice of infinite height) or take too many iterations (for a lattice
+///     of finite, but non-trivial, height).
 template <typename Derived, typename LatticeT>
 class DataflowAnalysis : public TypeErasedDataflowAnalysis {
 public:
   /// Bounded join-semilattice that is used in the analysis.
   using Lattice = LatticeT;
 
   explicit DataflowAnalysis(ASTContext &Context) : Context(Context) {}
 
public:
 
   LatticeJoinEffect joinTypeErased(TypeErasedLattice &E1,
                                    const TypeErasedLattice &E2) final {
     Lattice &L1 = llvm::any_cast<Lattice &>(E1.Value);
     const Lattice &L2 = llvm::any_cast<const Lattice &>(E2.Value);
     return L1.join(L2);
   }
 
+  LatticeJoinEffect widenTypeErased(TypeErasedLattice &Current,
+                                    const TypeErasedLattice &Previous) final {
+    Lattice &C = llvm::any_cast<Lattice &>(Current.Value);
+    const Lattice &P = llvm::any_cast<const Lattice &>(Previous.Value);
+    return widenInternal(Rank0{}, C, P);
+  }
+
   bool isEqualTypeErased(const TypeErasedLattice &E1,
                          const TypeErasedLattice &E2) final {
     const Lattice &L1 = llvm::any_cast<const Lattice &>(E1.Value);
     const Lattice &L2 = llvm::any_cast<const Lattice &>(E2.Value);
     return L1 == L2;
   }
 
   void transferTypeErased(const CFGElement *Element, TypeErasedLattice &E,
                           Environment &Env) final {
     Lattice &L = llvm::any_cast<Lattice &>(E.Value);
     static_cast<Derived *>(this)->transfer(Element, L, Env);
   }
 
   void transferBranchTypeErased(bool Branch, const Stmt *Stmt,
                                 TypeErasedLattice &E, Environment &Env) final {
-    if constexpr (HasTransferBranchFor<Derived, LatticeT>::value) {
-      Lattice &L = llvm::any_cast<Lattice &>(E.Value);
-      static_cast<Derived *>(this)->transferBranch(Branch, Stmt, L, Env);
-    }
-    // Silence unused parameter warnings.
-    (void)Branch;
-    (void)Stmt;
+    transferBranchInternal(Rank0{}, *static_cast<Derived *>(this), Branch, Stmt,
+                           E, Env);
   }
 
 private:
+  // These `Rank` structs are used for template metaprogramming to choose
+  // between overloads.
+  struct Rank1 {};
+  struct Rank0 : Rank1 {};
+
+  // The first-choice implementation: use `widen` when it is available.
+  template <typename T>
+  static auto widenInternal(Rank0, T &Current, const T &Prev)
+      -> decltype(Current.widen(Prev)) {
+    return Current.widen(Prev);
+  }
+
+  // The second-choice implementation: `widen` is unavailable. Widening is
+  // merged with equality checking, so when widening is unimplemented, we
+  // default to equality checking.
+  static LatticeJoinEffect widenInternal(Rank1, const Lattice &Current,
+                                         const Lattice &Prev) {
+    return Prev == Current ? LatticeJoinEffect::Unchanged
+                           : LatticeJoinEffect::Changed;
+  }
+
+  // The first-choice implementation: `transferBranch` is implemented.
+  template <typename Analysis>
+  static auto transferBranchInternal(Rank0, Analysis &A, bool Branch,
+                                     const Stmt *Stmt, TypeErasedLattice &L,
+                                     Environment &Env)
+      -> std::void_t<decltype(A.transferBranch(
+          Branch, Stmt, std::declval<LatticeT &>(), Env))> {
+    A.transferBranch(Branch, Stmt, llvm::any_cast<Lattice &>(L.Value), Env);
+  }
+
+  // The second-choice implementation: `transferBranch` is implemented. No-op.
+  template <typename Analysis>
+  static void transferBranchInternal(Rank1, Analysis &A, bool, const Stmt *,
+                                     TypeErasedLattice &, Environment &) {}
+
   ASTContext &Context;
 };
 
 // Model of the program at a given program point.
 template <typename LatticeT> struct DataflowAnalysisState {
   // Model of a program property.
   LatticeT Lattice;
 

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

 #include "clang/AST/Type.h"
 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
+#include "llvm/Support/ErrorHandling.h"
 #include <memory>
 #include <type_traits>
 #include <utility>
 
 namespace clang {
 namespace dataflow {
 
 /// Indicates what kind of indirections should be skipped past when retrieving
public:
     ///
     ///  `Val1` and `Val2` must be assigned to the same storage location in
     ///  `Env1` and `Env2` respectively.
     virtual ComparisonResult compare(QualType Type, const Value &Val1,
                                      const Environment &Env1, const Value &Val2,
                                      const Environment &Env2) {
       // FIXME: Consider adding QualType to StructValue and removing the Type
       // argument here.
-      //
-      // FIXME: default to a sound comparison (`Unknown`) and/or expand the
-      // comparison logic built into the framework to support broader forms of
-      // equivalence than strict pointer equality.
-      return ComparisonResult::Same;
+      return ComparisonResult::Unknown;
     }
 
     /// Modifies `MergedVal` to approximate both `Val1` and `Val2`. This could
     /// be a strict lattice join or a more general widening operation.
     ///
     /// If this function returns true, `MergedVal` will be assigned to a storage
     /// location of type `Type` in `MergedEnv`.
     ///
public:
     ///  `Val1` and `Val2` must be assigned to the same storage location in
     ///  `Env1` and `Env2` respectively.
     virtual bool merge(QualType Type, const Value &Val1,
                        const Environment &Env1, const Value &Val2,
                        const Environment &Env2, Value &MergedVal,
                        Environment &MergedEnv) {
       return true;
     }
+
+    /// This function may widen the current value -- replace it with an
+    /// approximation that can reach a fixed point more quickly than iterated
+    /// application of the transfer function alone. The previous value is
+    /// provided to inform the choice of widened value. The function must also
+    /// serve as a comparison operation, by indicating whether the widened value
+    /// is equivalent to the previous value.
+    ///
+    /// Returns either:
+    ///
+    ///   `nullptr`, if this value is not of interest to the model, or
+    ///
+    ///   `&Prev`, if the widened value is equivalent to `Prev`, or
+    ///
+    ///   A non-null value that approximates `Current`. `Prev` is available to
+    ///   inform the chosen approximation.
+    ///
+    /// `PrevEnv` and `CurrentEnv` can be used to query child values and path
+    /// condition implications of `Prev` and `Current`, respectively.
+    ///
+    /// Requirements:
+    ///
+    ///  `Prev` must precede `Current` in the value ordering.
+    ///
+    ///  `Prev` and `Current` must model values of type `Type`.
+    ///
+    ///  `Prev` and `Current` must be assigned to the same storage location in
+    ///  `PrevEnv` and `CurrentEnv`, respectively.
+    virtual Value *widen(QualType Type, Value &Prev, const Environment &PrevEnv,
+                         Value &Current, const Environment &CurrentEnv,
+                         Environment &WidenedEnv) {
+      // The default implementation reduces to just comparison, since comparison
+      // is required by the API, even if no widening is performed.
+      switch (compare(Type, Prev, PrevEnv, Current, CurrentEnv)) {
+        case ComparisonResult::Same:
+          return &Prev;
+        case ComparisonResult::Different:
+          return &Current;
+        case ComparisonResult::Unknown:
+          return nullptr;
+      }
+      llvm_unreachable("all cases in switch covered");
+    }
   };
 
   /// Creates an environment that uses `DACtx` to store objects that encompass
   /// the state of a program.
   explicit Environment(DataflowAnalysisContext &DACtx);
 
   Environment(const Environment &Other);
   Environment &operator=(const Environment &Other);
public:
   /// merged using `Model`.
   ///
   /// Requirements:
   ///
   ///  `Other` and `this` must use the same `DataflowAnalysisContext`.
   LatticeJoinEffect join(const Environment &Other,
                          Environment::ValueModel &Model);
 
+
+  /// Widens the environment point-wise, using `PrevEnv` as needed to inform the
+  /// approximation. by taking the intersection of storage locations and values
+  /// that are stored in them. Distinct values that are assigned to the same
+  /// storage locations in the environment and `PrevEnv` are widened, using
+  /// `Model` where appropriate.
+  ///
+  /// Requirements:
+  ///
+  ///  `PrevEnv` must precede `this` in the environment ordering.
+  ///  `PrevEnv` and `this` must use the same `DataflowAnalysisContext`.
+  LatticeJoinEffect widen(const Environment &PrevEnv,
+                          Environment::ValueModel &Model);
+
   // FIXME: Rename `createOrGetStorageLocation` to `getOrCreateStorageLocation`,
   // `getStableStorageLocation`, or something more appropriate.
 
   /// Creates a storage location appropriate for `Type`. Does not assign a value
   /// to the returned storage location in the environment.
   ///
   /// Requirements:
   ///
private:
   void pushCallInternal(const FunctionDecl *FuncDecl,
                         ArrayRef<const Expr *> Args);
 
   // `DACtx` is not null and not owned by this object.
   DataflowAnalysisContext *DACtx;
 
   // `DeclContext` of the block being analysed if provided.
   std::vector<const DeclContext *> CallStack;
 
   // In a properly initialized `Environment`, `ReturnLoc` should only be null if
   // its `DeclContext` could not be cast to a `FunctionDecl`.
   StorageLocation *ReturnLoc = nullptr;
   // The storage location of the `this` pointee. Should only be null if the
   // function being analyzed is only a function and not a method.
   StorageLocation *ThisPointeeLoc = nullptr;
 
   // Maps from program declarations and statements to storage locations that are
   // assigned to them. Unlike the maps in `DataflowAnalysisContext`, these
   // include only storage locations that are in scope for a particular basic
   // block.

clang/include/clang/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.h

public:
   virtual TypeErasedLattice typeErasedInitialElement() = 0;
 
   /// Joins two type-erased lattice elements by computing their least upper
   /// bound. Places the join result in the left element and returns an effect
   /// indicating whether any changes were made to it.
   virtual LatticeJoinEffect joinTypeErased(TypeErasedLattice &,
                                            const TypeErasedLattice &) = 0;
 
+  /// Chooses a lattice element that approximates the join of `A` and `B`, where
+  /// `A` is the current abstract element at a program point and `B` was the
+  /// previous abstract element at that same point. Places the widened result in
+  /// the current element (`Current`). Widening is (conceptually) optional: it
+  /// is valid for a lattice to implement `widen` with `join`. Widening is only
+  /// needed to either accelerate convergence (for lattices with non-trivial
+  /// height) or guarantee convergence (for lattices with infinite height).
+  ///
+  /// Returns an indication of whether any changes were made to `Current` in
+  /// order to widen.
+  virtual LatticeJoinEffect
+  widenTypeErased(TypeErasedLattice &Current,
+                  const TypeErasedLattice &Previous) = 0;
+
   /// Returns true if and only if the two given type-erased lattice elements are
   /// equal.
   virtual bool isEqualTypeErased(const TypeErasedLattice &,
                                  const TypeErasedLattice &) = 0;
 
   /// Applies the analysis transfer function for a given control flow graph
   /// element and type-erased lattice element.
   virtual void transferTypeErased(const CFGElement *, TypeErasedLattice &,

clang/include/clang/Analysis/FlowSensitive/Value.h

return Val->getKind() == Kind::TopBool ||
            Val->getKind() == Kind::Negation ||
            Val->getKind() == Kind::Implication ||
            Val->getKind() == Kind::Biconditional;
   }
 };
 
 /// Models the trivially true formula, which is Top in the lattice of boolean
 /// formulas.
-///
-/// FIXME: Given the subtlety of comparison involving `TopBoolValue`, define
-/// `operator==` for `Value`.
 class TopBoolValue final : public BoolValue {
 public:
   TopBoolValue() : BoolValue(Kind::TopBool) {}
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::TopBool;
   }
 };

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

llvm::DenseMap<K, V> intersectDenseMaps(const llvm::DenseMap<K, V> &Map1,
   for (auto &Entry : Map1) {
     auto It = Map2.find(Entry.first);
     if (It != Map2.end() && Entry.second == It->second)
       Result.insert({Entry.first, Entry.second});
   }
   return Result;
 }
 
+static bool compareDistinctValues(QualType Type, Value &Val1,
+                                  const Environment &Env1, Value &Val2,
+                                  const Environment &Env2,
+                                  Environment::ValueModel &Model) {
+  // Note: Potentially costly, but, for booleans, we could check whether both
+  // can be proven equivalent in their respective environments.
+
+  // FIXME: move the reference/pointers logic from `areEquivalentValues` to here
+  // and implement separate, join/widen specific handling for
+  // reference/pointers.
+  switch (Model.compare(Type, Val1, Env1, Val2, Env2)) {
+  case ComparisonResult::Same:
+    return true;
+  case ComparisonResult::Different:
+    return false;
+  case ComparisonResult::Unknown:
+    switch (Val1.getKind()) {
+    case Value::Kind::Integer:
+    case Value::Kind::Reference:
+    case Value::Kind::Pointer:
+    case Value::Kind::Struct:
+      // FIXME: this choice intentionally introduces unsoundness to allow
+      // for convergence. Once we have widening support for the
+      // reference/pointer and struct built-in models, this should be
+      // `false`.
+      return true;
+    default:
+      return false;
+    }
+  }
+  llvm_unreachable("All cases covered in switch");
+}
+
 /// 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,
+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.
-  if (auto *Expr1 = dyn_cast<BoolValue>(Val1)) {
-    auto *Expr2 = cast<BoolValue>(Val2);
+  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.makeIff(MergedVal, *Expr1)),
         MergedEnv.makeAnd(Env2.getFlowConditionToken(),
                           MergedEnv.makeIff(MergedVal, *Expr2))));
     return &MergedVal;
   }
 
   // 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))
+    if (Model.merge(Type, Val1, Env1, Val2, Env2, *MergedVal, MergedEnv))
       return MergedVal;
 
   return nullptr;
 }
 
+// When widening does not change the result, return value will equal `&Prev`.
+static Value &widenDistinctValues(QualType Type, Value &Prev,
+                                  const Environment &PrevEnv, Value &Current,
+                                  const Environment &CurrentEnv,
+                                  Environment &WidenedEnv,
+                                  Environment::ValueModel &Model) {
+  // Boolean-model widening.
+  if (isa<BoolValue>(&Prev)) {
+    assert(isa<BoolValue>(Current));
+    // Widen to Top, because we know they are different values. If previous was
+    // already Top, re-use that to (implicitly) indicate that no change occured.
+    if (isa<TopBoolValue>(Prev))
+      return Prev;
+    return WidenedEnv.makeTopBoolValue();
+  }
+
+  // FIXME: Add other built-in model widening.
+
+  // Custom-model widening.
+  if (auto *W =
+          Model.widen(Type, Prev, PrevEnv, Current, CurrentEnv, WidenedEnv))
+    return *W;
+
+  // Default of widening is a no-op: leave the current value unchanged.
+  return Current;
+}
+
 /// Initializes a global storage value.
 static void initGlobalVar(const VarDecl &D, Environment &Env) {
   if (!D.hasGlobalStorage() ||
       Env.getStorageLocation(D, SkipPast::None) != nullptr)
     return;
 
   auto &Loc = Env.createStorageLocation(D);
   Env.setStorageLocation(D, Loc);
for (auto &Entry : LocToVal) {
     assert(Val != nullptr);
 
     auto It = Other.LocToVal.find(Loc);
     if (It == Other.LocToVal.end())
       continue;
     assert(It->second != nullptr);
 
     if (!areEquivalentValues(*Val, *It->second) &&
-        Model.compare(Loc->getType(), *Val, *this, *It->second, Other) !=
-            ComparisonResult::Same)
+        !compareDistinctValues(Loc->getType(), *Val, *this, *It->second, Other,
+                               Model))
       return false;
   }
 
   return true;
 }
 
+LatticeJoinEffect Environment::widen(const Environment &PrevEnv,
+                                     Environment::ValueModel &Model) {
+  assert(DACtx == PrevEnv.DACtx);
+  assert(ReturnLoc == PrevEnv.ReturnLoc);
+  assert(ThisPointeeLoc == PrevEnv.ThisPointeeLoc);
+  assert(CallStack == PrevEnv.CallStack);
+
+  auto Effect = LatticeJoinEffect::Unchanged;
+  Environment WidenedEnv(*DACtx);
+
+  WidenedEnv.CallStack = CallStack;
+  WidenedEnv.ReturnLoc = ReturnLoc;
+  WidenedEnv.ThisPointeeLoc = ThisPointeeLoc;
+
+  // By the API, `PrevEnv` <= `*this`, meaning `join(PrevEnv, *this) =
+  // *this`. That guarantees that these maps are subsets of the maps in
+  // `PrevEnv`. So, we don't need change their current values to widen (in
+  // contrast to `join`).
+  //
+  // FIXME: The above is violated for `MemberLocToStruct`, because `join` can
+  // cause the map size to increase (when we add fresh data in places of
+  // conflict). Once this issue with join is resolved, re-enable the assertion
+  // below or replace with something that captures the desired invariant.
+  assert(DeclToLoc.size() <= PrevEnv.DeclToLoc.size());
+  assert(ExprToLoc.size() <= PrevEnv.ExprToLoc.size());
+  // assert(MemberLocToStruct.size() <= PrevEnv.MemberLocToStruct.size());
+
+  // FIXME: Can we copying `DeclToLoc` and `ExprToLoc` and instead share with
+  // `this`, since the widening operation will only read from them?
+  WidenedEnv.DeclToLoc = DeclToLoc;
+  WidenedEnv.ExprToLoc = ExprToLoc;
+  WidenedEnv.MemberLocToStruct = MemberLocToStruct;
+  WidenedEnv.FlowConditionToken = FlowConditionToken;
+
+  for (auto &Entry : LocToVal) {
+    const StorageLocation *Loc = Entry.first;
+    assert(Loc != nullptr);
+
+    Value *Val = Entry.second;
+    assert(Val != nullptr);
+
+    auto PrevIt = PrevEnv.LocToVal.find(Loc);
+    if (PrevIt == PrevEnv.LocToVal.end())
+      continue;
+    assert(PrevIt->second != nullptr);
+
+    if (areEquivalentValues(*Val, *PrevIt->second)) {
+      WidenedEnv.LocToVal.insert({Loc, Val});
+      continue;
+    }
+
+    Value &WidenedVal =
+        widenDistinctValues(Loc->getType(), *PrevIt->second, PrevEnv, *Val,
+                            *this, WidenedEnv, Model);
+    WidenedEnv.LocToVal.insert({Loc, &WidenedVal});
+    if (&WidenedVal != PrevIt->second)
+      Effect = LatticeJoinEffect::Changed;
+  }
+  if (WidenedEnv.DeclToLoc.size() != PrevEnv.DeclToLoc.size() ||
+      WidenedEnv.ExprToLoc.size() != PrevEnv.ExprToLoc.size() ||
+      WidenedEnv.LocToVal.size() != PrevEnv.LocToVal.size() ||
+      WidenedEnv.MemberLocToStruct.size() != PrevEnv.MemberLocToStruct.size())
+    Effect = LatticeJoinEffect::Changed;
+
+  *this = std::move(WidenedEnv);
+
+  return Effect;
+}
+
 LatticeJoinEffect Environment::join(const Environment &Other,
                                     Environment::ValueModel &Model) {
   assert(DACtx == Other.DACtx);
   assert(ReturnLoc == Other.ReturnLoc);
   assert(ThisPointeeLoc == Other.ThisPointeeLoc);
   assert(CallStack == Other.CallStack);
 
   auto Effect = LatticeJoinEffect::Unchanged;
if (DeclToLoc.size() != JoinedEnv.DeclToLoc.size())
     Effect = LatticeJoinEffect::Changed;
 
   JoinedEnv.ExprToLoc = intersectDenseMaps(ExprToLoc, Other.ExprToLoc);
   if (ExprToLoc.size() != JoinedEnv.ExprToLoc.size())
     Effect = LatticeJoinEffect::Changed;
 
   JoinedEnv.MemberLocToStruct =
       intersectDenseMaps(MemberLocToStruct, Other.MemberLocToStruct);
+  assert(JoinedEnv.MemberLocToStruct.size() <=
+         std::min(MemberLocToStruct.size(), Other.MemberLocToStruct.size()));
+
+  intersectDenseMaps(MemberLocToStruct, Other.MemberLocToStruct);
   if (MemberLocToStruct.size() != JoinedEnv.MemberLocToStruct.size())
     Effect = LatticeJoinEffect::Changed;
 
   // FIXME: set `Effect` as needed.
+  // FIXME: update join to detect backedges and simplify the flow condition
+  // accordingly.
   JoinedEnv.FlowConditionToken = &DACtx->joinFlowConditions(
       *FlowConditionToken, *Other.FlowConditionToken);
 
   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 (areEquivalentValues(*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)) {
       JoinedEnv.LocToVal.insert({Loc, MergedVal});
+      Effect = LatticeJoinEffect::Changed;
+    }
   }
   if (LocToVal.size() != JoinedEnv.LocToVal.size())
     Effect = LatticeJoinEffect::Changed;
 
   *this = std::move(JoinedEnv);
 
   return Effect;
 }
if ((Depth > 1 && CreatedValuesCount > MaxCompositeValueSize) ||
     return nullptr;
 
   if (Type->isBooleanType()) {
     CreatedValuesCount++;
     return &makeAtomicBoolValue();
   }
 
   if (Type->isIntegerType()) {
+    // FIXME: consider instead `return nullptr`, given that we do nothing useful
+    // with integers, and so distinguishing them serves no purpose, but could
+    // prevent convergence.
     CreatedValuesCount++;
     return &takeOwnership(std::make_unique<IntegerValue>());
   }
 
   if (Type->isReferenceType()) {
     CreatedValuesCount++;
     QualType PointeeType = Type->castAs<ReferenceType>()->getPointeeType();
     auto &PointeeLoc = createStorageLocation(PointeeType);

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

 #include <vector>
 
 #include "clang/AST/DeclCXX.h"
 #include "clang/AST/OperationKinds.h"
 #include "clang/AST/StmtVisitor.h"
 #include "clang/Analysis/Analyses/PostOrderCFGView.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/DataflowWorklist.h"
 #include "clang/Analysis/FlowSensitive/Transfer.h"
 #include "clang/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
static int blockIndexInPredecessor(const CFGBlock &Pred,
                                    const CFGBlock &Block) {
   auto BlockPos = llvm::find_if(
       Pred.succs(), [&Block](const CFGBlock::AdjacentBlock &Succ) {
         return Succ && Succ->getBlockID() == Block.getBlockID();
       });
   return BlockPos - Pred.succ_begin();
 }
 
+static bool isLoopHead(const CFGBlock &B) {
+  if (const auto *T = B.getTerminatorStmt())
+    switch (T->getStmtClass()) {
+      case Stmt::WhileStmtClass:
+      case Stmt::DoStmtClass:
+      case Stmt::ForStmtClass:
+        return true;
+      default:
+        return false;
+    }
+
+  return false;
+}
+
 // The return type of the visit functions in TerminatorVisitor. The first
 // element represents the terminator expression (that is the conditional
 // expression in case of a path split in the CFG). The second element
 // represents whether the condition was true or false.
 using TerminatorVisitorRetTy = std::pair<const Expr *, bool>;
 
 /// Extends the flow condition of an environment based on a terminator
 /// statement.
if (++Iterations > MaxIterations) {
                                      "maximum number of iterations reached");
     }
 
     const llvm::Optional<TypeErasedDataflowAnalysisState> &OldBlockState =
         BlockStates[Block->getBlockID()];
     TypeErasedDataflowAnalysisState NewBlockState =
         transferCFGBlock(*Block, AC);
 
-    if (OldBlockState &&
-        Analysis.isEqualTypeErased(OldBlockState.value().Lattice,
+    if (OldBlockState) {
+      if (isLoopHead(*Block)) {
+        LatticeJoinEffect Effect1 = Analysis.widenTypeErased(
+            NewBlockState.Lattice, OldBlockState.value().Lattice);
+        LatticeJoinEffect Effect2 =
+            NewBlockState.Env.widen(OldBlockState->Env, Analysis);
+        if (Effect1 == LatticeJoinEffect::Unchanged &&
+            Effect2 == LatticeJoinEffect::Unchanged)
+          // The state of `Block` didn't change from widening so there's no need
+          // to revisit its successors.
+          continue;
+      } else if (Analysis.isEqualTypeErased(OldBlockState.value().Lattice,
                                             NewBlockState.Lattice) &&
                  OldBlockState->Env.equivalentTo(NewBlockState.Env, Analysis)) {
-      // The state of `Block` didn't change after transfer so there's no need to
-      // revisit its successors.
+        // The state of `Block` didn't change after transfer so there's no need
+        // to revisit its successors.
         continue;
       }
+    }
 
     BlockStates[Block->getBlockID()] = std::move(NewBlockState);
 
     // Do not add unreachable successor blocks to `Worklist`.
     if (Block->hasNoReturnElement())
       continue;
 
     Worklist.enqueueSuccessors(Block);

clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

 //===- unittests/Analysis/FlowSensitive/TransferTest.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 "TestingSupport.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/Decl.h"
-#include "clang/ASTMatchers/ASTMatchFinder.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Basic/LangStandard.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/StringRef.h"
ASSERT_THAT_ERROR(
       llvm::Succeeded());
 }
 
 template <typename Matcher>
 void runDataflow(llvm::StringRef Code, Matcher Match,
                  LangStandard::Kind Std = LangStandard::lang_cxx17,
                  bool ApplyBuiltinTransfer = true,
                  llvm::StringRef TargetFun = "target") {
-  runDataflow(Code, Match,
+  runDataflow(Code, std::move(Match),
               {ApplyBuiltinTransfer ? TransferOptions{}
                                     : llvm::Optional<TransferOptions>()},
               Std, TargetFun);
 }
 
 TEST(TransferTest, IntVarDeclNotTrackedWhenTransferDisabled) {
   std::string Code = R"(
     void target() {
runDataflow(
           auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl, SkipPast::None));
           EXPECT_TRUE(Env.flowConditionImplies(CVal));
         }
       });
 }
 
 TEST(TransferTest, LoopWithAssignmentConverges) {
   std::string Code = R"(
-
-    bool &foo();
+    bool foo();
 
     void target() {
        do {
         bool Bar = foo();
         if (Bar) break;
         (void)Bar;
         /*[[p]]*/
       } while (true);
runDataflow(
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
         auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl, SkipPast::None));
         EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
       });
 }
 
-TEST(TransferTest, LoopWithReferenceAssignmentConverges) {
+TEST(TransferTest, LoopWithStagedAssignments) {
   std::string Code = R"(
+    bool foo();
+
+    void target() {
+      bool Bar = false;
+      bool Err = false;
+      while (foo()) {
+        if (Bar)
+          Err = true;
+        Bar = true;
+        /*[[p]]*/
+      }
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         ASTContext &ASTCtx) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
+        const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
+
+        const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+        ASSERT_THAT(BarDecl, NotNull());
+        const ValueDecl *ErrDecl = findValueDecl(ASTCtx, "Err");
+        ASSERT_THAT(ErrDecl, NotNull());
+
+        auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl, SkipPast::None));
+        auto &ErrVal = *cast<BoolValue>(Env.getValue(*ErrDecl, SkipPast::None));
+        EXPECT_TRUE(Env.flowConditionImplies(BarVal));
+        // An unsound analysis, for example only evaluating the loop once, can
+        // conclude that `Err` is false. So, we test that this conclusion is not
+        // reached.
+        EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(ErrVal)));
+      });
+}
 
+TEST(TransferTest, LoopWithReferenceAssignmentConverges) {
+  std::string Code = R"(
     bool &foo();
 
     void target() {
        do {
         bool& Bar = foo();
         if (Bar) break;
         (void)Bar;
         /*[[p]]*/
       } while (true);
     }
   )";
-  // The key property that we are verifying is implicit in `runDataflow` --
-  // namely, that the analysis succeeds, rather than hitting the maximum number
-  // of iterations.
+  // The key property that we are verifying is that the analysis succeeds,
+  // rather than hitting the maximum number of iterations.
   runDataflow(
       Code,
       [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");