[clang][dataflow] Add support for a Top value in boolean formulas.

[ymandel]

Summary

Currently, our boolean formulas (BoolValue) don't form a lattice, since they
have no Top element. This patch adds such an element, thereby "completing" the
built-in model of bools to be a proper semi-lattice. It still has infinite
height, which is its own problem, but that can be solved separately, through
widening and the like.

Patch 1 for Issue #56931.

[gribozavr2]

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

157

Should we be creating a new top every time, or should it be a singleton like true and false?

It seems like we explicitly don't care about its identity (or else it would be isomorphic to AtomicBool).

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

98

Here and throughout the patch: since we might have a top for other kinds of values, WDYT about renaming this type to TopBoolValue? Similarly createTop -> createTopBool ?

103

Since TopValue is a BoolValue, can we form say a ConjunctionValue where LHS or RHS is Top?

What if we create such a conjunction twice? It seems like such conjunctions would incorrectly compare equal, even though each Top will be replaced with a unique fresh variable.

Would it make sense to change our factory functions for boolean formulas to eagerly open Top?

Then we wouldn't need a recursive walk in unpackValue().

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

376

isa<Top>

clang/lib/Analysis/FlowSensitive/Transfer.cpp

77

llvm_unreachable(); because this can't happen, V is a BoolValue.

124–125

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

237–238

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

472

isa<Top>(...)? and isa<AtomicBool>(...) below?

620

EXPECT_TRUE(isa<Top>(...)) ?

1192

1219–1220

1291

1301–1310

Similarly in tests below.

if (false) theoretically could be handled in a special way in future and could be folded away during CFG construction.

1435–1439

Zab1Decl, Zab2Decl are unused apart from the NotNull check (which does not seem interesting to me).

1453

Could you add a variant of this test?

void target(bool Cond) {
  bool Foo = makeTop();
  // Force a new block.
  if (false) return;
  (void)0;
  /*[[p1]]*/

  bool Zab;
  if (Cond) {
    Zab = Foo;
  } else {
    Zab = Foo;
  }
  (void)0;
  if (Zab == Foo) { return; }
  /*[[p2]]*/
}

Show the loss of precision by checking that the flow condition for p2 is satisfiable.

[xazax.hun]

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

525–526

I feel like this logic is repeated multiple times. I wonder if we should define an operator== for const BoolValue*.

1191

Nit: I usually prefer marking whole classes final rather than individual virtual methods, but feel free to leave as is.

[xazax.hun]

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

157

Good point, a singleton Top might actually simplify some parts of the code.

[ymandel]

Thanks for the thorough reviews! Agreed on all points, and will address.

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

157

Good question. That was my initial implementation, but it ran into the problem that the solver (in buildBooleanFormula) maps each unique (by pointer) subexpression into a fresh SAT variable in . If we use a singleton Top, we need to modify that algorithm appropriately. I'm open to suggestions, though, because of the advantages of a singleton Top.

If we assume that a given Top is never actually shared in a boolean formula (unlike other subexpressions, which may be shared), then we can use a singleton and special case it in buildBooleanFormula. I think that's a good assumption, but am not sure. Thoughts?

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

103

They would only compare equal if we're using a singleton Top. In fact, that's not quite right because we have no deep equality on formulas. But, the caching mechanism would generate the same formula, so the point holds. In that case, we would need to eagerly open the Top, because we would lose any way to distinguish them. But, with different Top instances, this wouldn't be necessary. Overall, it seems like "open top as soon as possible without killing convergence" is probably our best heuristic, so this seems like a win. But, I'm pretty sure there are places where it will prevent convergence (on its own -- widen will still handle it fine I believe).

Avoiding the recursive walk would be nice.

[ymandel]

Address (most) comments.

[ymandel]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

237–238

regarding the latter clause -- its freedom *does* affect satisfiability. e.g. A || Top is trivially satisfiable. I'm just going to drop the "and ...".

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

525–526

Agreed. I want to wait until we settle on the representation and then we can consider this operator. But, if we end up with a singleton Top then I think we can hold off.

1191

Good point. I was following what's done elsewhere in the file -- I think we should update all or nothing. that said, if you mark the class final, then what do you do with each method? nothing or override?

1301–1310

Sure. I went with a different name since it's playing a very specific role that's not related to the test in the way that Cond is.

1453

Added, but there's no loss of precision and so the test demonstrates that. My initial instinct was that there would be loss, but the guard of Cond actually preserves the precision. The cost is complexity -- Zab is a fresh atomic and the flow condition encoded enough information to recover its equivalence to Foo. But, it is not _equal_ to Foo, which would be nice.

The case where we lose precision is a loop, where the incoming edge doesn't carry a condition.

[gribozavr2]

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

157

I see. Could you add some direct tests for the SAT solver with formulas that include Top to check the behavior we care about?

[sgatev]

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

156

Please add a comment.

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

291

Please add a comment.

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

100

explicit seems unnecessary.

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

237–238

Where? Does that mean that TopBool never reaches the solver? I think it'd be good to clarify.

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

1223

Why do we need to check two code points here and in the test below? It's not obvious what the difference between p1 and p2 is.

[xazax.hun]

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

157

Given the discussion so far, it looks like having a singleton top has its own problems. I'm fine with the current solution for now, let's see if the overall approach works and we will see if this needs any further optimization later. +1 to Dmitry, some unit tests like Top && Top generated multiple times will not yield the same expression could be useful. If someone in the future tries to introduce singleton Top, they will see those tests fail and see why we did not have that in the first place and what problems need to be solved to introduce it.

[ymandel]

Address comments.

[ymandel]

Add explicit test for creation of multiple tops.

[ymandel]

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

157

I've added a test that direct creation of two Tops results in distinct values (by pointer) and inequivalent (per the solver), and some tests relating to the solver which will fail if you switch to a singleton Top. I didn't see much room for a Top && Top test, since that seems redundant with the simpler tests. I think the inequivalence tests satisfies Dmitri's concern with conjunctions involving Top, but, happy to add more if you disagree.

I should note, though: Top iff Top is true when both Tops are identical values (pointer equality) but not when they are distinct values. This doesn't seem right to me -- I think we should have one answer for Top iff Top and I think it should be false. So, in some sense, even the current scheme suffers from the some of the drawbacks of the singleton scheme. I think this is ok for now, but it does seem to encourage improvement in further patches.

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

100

agreed. looks like a copy-paste error on my part.

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

1223

added comments to both tests to explain motivation. The second one is actually a regression test since my original version had a bug in its handling of lvalues *not* in rvalue position.

[ymandel]

added another test

[xazax.hun]

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

157

I think we should have one answer for Top iff Top and I think it should be false.

I'd love to see this as a TODO comment.

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

525–526

We ended up not going with a singleton Top, let's reconsider the overloaded operator.

[xazax.hun]

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

1191

I prefer override on the methods in that scenario. But I agree that refactoring changes like this might be better done in a separate NFC commit.

[ymandel]

Added FIXMEs for noted issues.

[ymandel]

fix typos

[ymandel]

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

525–526

added FIXME.

[gribozavr2]

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

69

Why delete this test?

[ymandel]

Adding back accidentally deleted test

[ymandel]

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

69

That was a mistake. I've added it back

[ymandel]

rebase onto a recent HEAD

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

AtomicBoolValue &getBoolLiteralValue(bool Value) const {
     return Value ? TrueVal : FalseVal;
   }
 
   /// Creates an atomic boolean value.
   AtomicBoolValue &createAtomicBoolValue() {
     return takeOwnership(std::make_unique<AtomicBoolValue>());
   }
 
+  /// Creates a Top value for booleans. Each instance is unique and can be
+  /// assigned a distinct truth value during solving.
+  ///
+  /// FIXME: `Top iff Top` is true when both Tops are identical (by pointer
+  /// equality), but not when they are distinct values. We should improve the
+  /// implementation so that `Top iff Top` has a consistent meaning, regardless
+  /// of the identity of `Top`. Moreover, I think the meaning should be
+  /// `false`.
+  TopBoolValue &createTopBoolValue() {
+    return takeOwnership(std::make_unique<TopBoolValue>());
+  }
+
   /// Returns a boolean value that represents the conjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
   BoolValue &getOrCreateConjunction(BoolValue &LHS, BoolValue &RHS);
 
   /// Returns a boolean value that represents the disjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their

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

AtomicBoolValue &getBoolLiteralValue(bool Value) const {
     return DACtx->getBoolLiteralValue(Value);
   }
 
   /// Returns an atomic boolean value.
   BoolValue &makeAtomicBoolValue() const {
     return DACtx->createAtomicBoolValue();
   }
 
+  /// Returns a unique instance of boolean Top.
+  BoolValue &makeTopBoolValue() const {
+    return DACtx->createTopBoolValue();
+  }
+
   /// Returns a boolean value that represents the conjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
   BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
     return DACtx->getOrCreateConjunction(LHS, RHS);
   }
 

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

 public:
   enum class Kind {
     Integer,
     Reference,
     Pointer,
     Struct,
 
     // Synthetic boolean values are either atomic values or logical connectives.
+    TopBool,
     AtomicBool,
     Conjunction,
     Disjunction,
     Negation,
     Implication,
     Biconditional,
   };
 

 };
 
 /// Models a boolean.
 class BoolValue : public Value {
 public:
   explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
 
   static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::AtomicBool ||
+    return Val->getKind() == Kind::TopBool ||
+           Val->getKind() == Kind::AtomicBool ||
            Val->getKind() == Kind::Conjunction ||
            Val->getKind() == Kind::Disjunction ||
            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;
+  }
+};
+
 /// Models an atomic boolean.
 class AtomicBoolValue : public BoolValue {
 public:
   explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {}
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::AtomicBool;
   }

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

static bool areEquivalentIndirectionValues(Value *Val1, Value *Val2) {
   return false;
 }
 
 /// Returns true if and only if `Val1` is equivalent to `Val2`.
 static bool equivalentValues(QualType Type, Value *Val1,
                              const Environment &Env1, Value *Val2,
                              const Environment &Env2,
                              Environment::ValueModel &Model) {
-  return Val1 == Val2 || areEquivalentIndirectionValues(Val1, Val2) ||
+  return Val1 == Val2 || (isa<TopBoolValue>(Val1) && isa<TopBoolValue>(Val2)) ||
+         areEquivalentIndirectionValues(Val1, Val2) ||
          Model.compareEquivalent(Type, *Val1, Env1, *Val2, 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,
for (auto &Entry : LocToVal) {
     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) {
+    if (Val == It->second ||
+        (isa<TopBoolValue>(Val) && isa<TopBoolValue>(It->second))) {
       JoinedEnv.LocToVal.insert({Loc, Val});
       continue;
     }
 
     if (Value *MergedVal = mergeDistinctValues(
             Loc->getType(), Val, *this, It->second, Other, JoinedEnv, Model))
       JoinedEnv.LocToVal.insert({Loc, MergedVal});
   }

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

llvm::StringRef debugString(Value::Kind Kind) {
   case Value::Kind::Reference:
     return "Reference";
   case Value::Kind::Pointer:
     return "Pointer";
   case Value::Kind::Struct:
     return "Struct";
   case Value::Kind::AtomicBool:
     return "AtomicBool";
+  case Value::Kind::TopBool:
+    return "TopBool";
   case Value::Kind::Conjunction:
     return "Conjunction";
   case Value::Kind::Disjunction:
     return "Disjunction";
   case Value::Kind::Negation:
     return "Negation";
   case Value::Kind::Implication:
     return "Implication";

clang/lib/Analysis/FlowSensitive/Transfer.cpp

 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Basic/Builtins.h"
 #include "clang/Basic/OperatorKinds.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/Support/Casting.h"
+#include "llvm/Support/ErrorHandling.h"
 #include <cassert>
 #include <memory>
 #include <tuple>
 
 namespace clang {
 namespace dataflow {
 
 static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
                                           Environment &Env) {
   if (auto *LHSValue =
           dyn_cast_or_null<BoolValue>(Env.getValue(LHS, SkipPast::Reference)))
     if (auto *RHSValue =
             dyn_cast_or_null<BoolValue>(Env.getValue(RHS, SkipPast::Reference)))
       return Env.makeIff(*LHSValue, *RHSValue);
 
   return Env.makeAtomicBoolValue();
 }
 
+// Functionally updates `V` such that any instances of `TopBool` are replaced
+// with fresh atomic bools. Note: This implementation assumes that `B` is a
+// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
+// present in the original .
+static BoolValue &unpackValue(BoolValue &V, Environment &Env);
+
+template <typename Derived, typename M>
+BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
+  auto &V = *cast<Derived>(&B);
+  BoolValue &Left = V.getLeftSubValue();
+  BoolValue &Right = V.getRightSubValue();
+  BoolValue &ULeft = unpackValue(Left, Env);
+  BoolValue &URight = unpackValue(Right, Env);
+
+  if (&ULeft == &Left && &URight == &Right)
+    return V;
+
+  return (Env.*build)(ULeft, URight);
+}
+
+static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
+  switch (V.getKind()) {
+  case Value::Kind::Integer:
+  case Value::Kind::Reference:
+  case Value::Kind::Pointer:
+  case Value::Kind::Struct:
+    llvm_unreachable("BoolValue cannot have any of these kinds.");
+
+  case Value::Kind::AtomicBool:
+    return V;
+
+  case Value::Kind::TopBool:
+    // Unpack `TopBool` into a fresh atomic bool.
+    return Env.makeAtomicBoolValue();
+
+  case Value::Kind::Negation: {
+    auto &N = *cast<NegationValue>(&V);
+    BoolValue &Sub = N.getSubVal();
+    BoolValue &USub = unpackValue(Sub, Env);
+
+    if (&USub == &Sub)
+      return V;
+    return Env.makeNot(USub);
+  }
+  case Value::Kind::Conjunction:
+    return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
+                                                   &Environment::makeAnd);
+  case Value::Kind::Disjunction:
+    return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
+                                                   &Environment::makeOr);
+  case Value::Kind::Implication:
+    return unpackBinaryBoolValue<ImplicationValue>(
+        Env, V, &Environment::makeImplication);
+  case Value::Kind::Biconditional:
+    return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
+                                                     &Environment::makeIff);
+  }
+}
+
+// Unpacks the value (if any) associated with `E` and updates `E` to the new
+// value, if any unpacking occured.
+static Value *maybeUnpackLValueExpr(const Expr &E, Environment &Env) {
+  auto *Loc = Env.getStorageLocation(E, SkipPast::Reference);
+  if (Loc == nullptr)
+    return nullptr;
+  auto *Val = Env.getValue(*Loc);
+
+  auto *B = dyn_cast_or_null<BoolValue>(Val);
+  if (B == nullptr)
+    return Val;
+
+  auto &UnpackedVal = unpackValue(*B, Env);
+  if (&UnpackedVal == Val)
+    return Val;
+  Env.setValue(*Loc, UnpackedVal);
+  return &UnpackedVal;
+}
+
 class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
 public:
   TransferVisitor(const StmtToEnvMap &StmtToEnv, Environment &Env,
                   TransferOptions Options)
       : StmtToEnv(StmtToEnv), Env(Env), Options(Options) {}
 
   void VisitBinaryOperator(const BinaryOperator *S) {
     const Expr *LHS = S->getLHS();
case CK_IntegralToBoolean: {
       else
         // FIXME: If integer modeling is added, then update this code to create
         // the boolean based on the integer model.
         Env.setValue(Loc, Env.makeAtomicBoolValue());
       break;
     }
 
     case CK_LValueToRValue: {
-      auto *SubExprVal = Env.getValue(*SubExpr, SkipPast::Reference);
+      // When an L-value is used as an R-value, it may result in sharing, so we
+      // need to unpack any nested `Top`s.
+      auto *SubExprVal = maybeUnpackLValueExpr(*SubExpr, Env);
       if (SubExprVal == nullptr)
         break;
 
       auto &ExprLoc = Env.createStorageLocation(*S);
       Env.setStorageLocation(*S, ExprLoc);
       Env.setValue(ExprLoc, *SubExprVal);
       break;
     }

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

while (!UnprocessedSubVals.empty()) {
         break;
       }
       case Value::Kind::Biconditional: {
         auto *B = cast<BiconditionalValue>(Val);
         UnprocessedSubVals.push(&B->getLeftSubValue());
         UnprocessedSubVals.push(&B->getRightSubValue());
         break;
       }
+      case Value::Kind::TopBool:
+        // Nothing more to do. This `TopBool` instance has already been mapped
+        // to a fresh solver variable (`NextVar`, above) and is thereafter
+        // anonymous. The solver never sees `Top`.
+        break;
       case Value::Kind::AtomicBool: {
         Atomics[Var] = cast<AtomicBoolValue>(Val);
         break;
       }
       default:
         llvm_unreachable("buildBooleanFormula: unhandled value kind");
       }
     }

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

 TEST_F(DataflowAnalysisContextTest,
        CreateAtomicBoolValueReturnsDistinctValues) {
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
   EXPECT_NE(&X, &Y);
 }
 
 TEST_F(DataflowAnalysisContextTest,
+       CreateTopBoolValueReturnsDistinctValues) {
+  auto &X = Context.createTopBoolValue();
+  auto &Y = Context.createTopBoolValue();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
+  auto &X = Context.createTopBoolValue();
+  auto &Y = Context.createTopBoolValue();
+  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+}
+
+TEST_F(DataflowAnalysisContextTest,
        GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
   auto &X = Context.createAtomicBoolValue();
   auto &XAndX = Context.getOrCreateConjunction(X, X);
   EXPECT_EQ(&XAndX, &X);
 }
 
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

 //===- unittests/Analysis/FlowSensitive/SolverTest.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 <utility>
 
 #include "TestingSupport.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "TestingSupport.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
 namespace {
 
 using namespace clang;
 using namespace dataflow;
 
 using test::ConstraintContext;
 using testing::_;
 using testing::AnyOf;
+using testing::IsEmpty;
 using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
 
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
 Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
   return WatchedLiteralsSolver().solve(std::move(Vals));
TEST(SolverTest, NegatedVar) {
   auto NotX = Ctx.neg(X);
 
   // !X
   expectSatisfiable(
       solve({NotX}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
 }
 
 TEST(SolverTest, UnitConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
 
   // X ^ !X
   expectUnsatisfiable(solve({X, NotX}));
 }
 
 TEST(SolverTest, DistinctVars) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto NotY = Ctx.neg(Y);
 
   // X ^ !Y
   expectSatisfiable(
       solve({X, NotY}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
                            Pair(Y, Solver::Result::Assignment::AssignedFalse)));
 }
 
+TEST(SolverTest, Top) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+
+  // X. Since Top is anonymous, we do not get any results in the solution.
+  expectSatisfiable(solve({X}), IsEmpty());
+}
+
+TEST(SolverTest, NegatedTop) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+
+  // !X
+  expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
+}
+
+TEST(SolverTest, DistinctTops) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+  auto Y = Ctx.top();
+  auto NotY = Ctx.neg(Y);
+
+  // X ^ !Y
+  expectSatisfiable(solve({X, NotY}), IsEmpty());
+}
+
 TEST(SolverTest, DoubleNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto NotNotX = Ctx.neg(NotX);
 
   // !!X ^ !X
   expectUnsatisfiable(solve({NotNotX, NotX}));

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

 class ConstraintContext {
 public:
   // Creates an atomic boolean value.
   BoolValue *atom() {
     Vals.push_back(std::make_unique<AtomicBoolValue>());
     return Vals.back().get();
   }
 
+  // Creates an instance of the Top boolean value.
+  BoolValue *top() {
+    Vals.push_back(std::make_unique<TopBoolValue>());
+    return Vals.back().get();
+  }
+
   // Creates a boolean conjunction value.
   BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
     Vals.push_back(
         std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
     return Vals.back().get();
   }
 
   // Creates a boolean disjunction value.

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

 #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/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Tooling/Tooling.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/SmallSet.h"
 #include "llvm/ADT/StringMap.h"
explicit FunctionCallAnalysis(ASTContext &Context)
       : DataflowAnalysis<FunctionCallAnalysis, FunctionCallLattice>(Context) {}
 
   static FunctionCallLattice initialElement() { return {}; }
 
   void transfer(const CFGElement *Elt, FunctionCallLattice &E, Environment &) {
     auto CS = Elt->getAs<CFGStmt>();
     if (!CS)
       return;
-    auto S = CS->getStmt();
+    const auto *S = CS->getStmt();
     if (auto *C = dyn_cast<CallExpr>(S)) {
       if (auto *F = dyn_cast<FunctionDecl>(C->getCalleeDecl())) {
         E.CalledFunctions.insert(F->getNameInfo().getAsString());
       }
     }
   }
 };
 
TEST_F(NoreturnDestructorTest, ConditionalOperatorNestedBranchReturns) {
   )";
   runDataflow(Code, UnorderedElementsAre(IsStringMapEntry(
                         "p", HoldsFunctionCallLattice(HasCalledFunctions(
                                  UnorderedElementsAre("baz", "foo"))))));
   // FIXME: Called functions at point `p` should contain only "foo".
 }
 
 // Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
 class SpecialBoolAnalysis
     : public DataflowAnalysis<SpecialBoolAnalysis, NoopLattice> {
 public:
   explicit SpecialBoolAnalysis(ASTContext &Context)
       : DataflowAnalysis<SpecialBoolAnalysis, NoopLattice>(Context) {}
 
   static NoopLattice initialElement() { return {}; }
 
   void transfer(const CFGElement *Elt, NoopLattice &, Environment &Env) {
     auto CS = Elt->getAs<CFGStmt>();
     if (!CS)
       return;
-    auto S = CS->getStmt();
+    const auto *S = CS->getStmt();
     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 = *Env.createValue(E->getType());
       ConstructorVal.setProperty("is_set", Env.getBoolLiteralValue(false));
runDataflow(
 
         EXPECT_FALSE(Env1.flowConditionImplies(*GetFooValue(Env1)));
         EXPECT_TRUE(Env2.flowConditionImplies(*GetFooValue(Env2)));
         EXPECT_TRUE(Env3.flowConditionImplies(*GetFooValue(Env3)));
         EXPECT_TRUE(Env4.flowConditionImplies(*GetFooValue(Env3)));
       });
 }
 
 class OptionalIntAnalysis
     : public DataflowAnalysis<OptionalIntAnalysis, NoopLattice> {
 public:
-  explicit OptionalIntAnalysis(ASTContext &Context, BoolValue &HasValueTop)
-      : DataflowAnalysis<OptionalIntAnalysis, NoopLattice>(Context),
-        HasValueTop(HasValueTop) {}
+  explicit OptionalIntAnalysis(ASTContext &Context)
+      : DataflowAnalysis<OptionalIntAnalysis, NoopLattice>(Context) {}
 
   static NoopLattice initialElement() { return {}; }
 
   void transfer(const CFGElement *Elt, NoopLattice &, Environment &Env) {
     auto CS = Elt->getAs<CFGStmt>();
     if (!CS)
       return;
-    auto S = CS->getStmt();
+    const Stmt *S = CS->getStmt();
     auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
     auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
 
+    SmallVector<BoundNodes, 1> Matches = match(
+        stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+                   cxxOperatorCallExpr(
+                       callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl))))
+                       .bind("operator"))),
+        *S, getASTContext());
     if (const auto *E = selectFirst<CXXConstructExpr>(
-            "call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
-                          getASTContext()))) {
+            "construct", Matches)) {
       auto &ConstructorVal = *Env.createValue(E->getType());
       ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
       Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-    } else if (const auto *E = selectFirst<CXXOperatorCallExpr>(
-                   "call",
-                   match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
-                                                 OptionalIntRecordDecl))))
-                             .bind("call"),
-                         *S, getASTContext()))) {
+    } else if (const auto *E =
+                   selectFirst<CXXOperatorCallExpr>("operator", Matches)) {
       assert(E->getNumArgs() > 0);
       auto *Object = E->getArg(0);
       assert(Object != nullptr);
 
       auto *ObjectLoc =
           Env.getStorageLocation(*Object, SkipPast::ReferenceThenPointer);
       assert(ObjectLoc != nullptr);
 
       auto &ConstructorVal = *Env.createValue(Object->getType());
       ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(true));
       Env.setValue(*ObjectLoc, ConstructorVal);
     }
   }
 
   bool compareEquivalent(QualType Type, const Value &Val1,
                          const Environment &Env1, const Value &Val2,
                          const Environment &Env2) final {
     // Nothing to say about a value that does not model an `OptionalInt`.
     if (!Type->isRecordType() ||
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
       return false;
 
-    return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+    auto *Prop1  = Val1.getProperty("has_value");
+    auto *Prop2 = Val2.getProperty("has_value");
+    return Prop1 == Prop2 ||
+           (Prop1 != nullptr && Prop2 != nullptr && isa<TopBoolValue>(Prop1) &&
+            isa<TopBoolValue>(Prop2));
   }
 
   bool merge(QualType Type, const Value &Val1, const Environment &Env1,
              const Value &Val2, const Environment &Env2, Value &MergedVal,
              Environment &MergedEnv) final {
     // Nothing to say about a value that does not model an `OptionalInt`.
     if (!Type->isRecordType() ||
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
       return false;
 
     auto *HasValue1 = cast_or_null<BoolValue>(Val1.getProperty("has_value"));
     if (HasValue1 == nullptr)
       return false;
 
     auto *HasValue2 = cast_or_null<BoolValue>(Val2.getProperty("has_value"));
     if (HasValue2 == nullptr)
       return false;
 
     if (HasValue1 == HasValue2)
       MergedVal.setProperty("has_value", *HasValue1);
     else
-      MergedVal.setProperty("has_value", HasValueTop);
+      MergedVal.setProperty("has_value", MergedEnv.makeTopBoolValue());
     return true;
   }
-
-  BoolValue &HasValueTop;
 };
 
 class WideningTest : public Test {
 protected:
   template <typename Matcher>
   void runDataflow(llvm::StringRef Code, Matcher Match) {
     tooling::FileContentMappings FilesContents;
     FilesContents.push_back(
         std::make_pair<std::string, std::string>("widening_test_defs.h", R"(
       struct OptionalInt {
         OptionalInt() = default;
         OptionalInt& operator=(int);
       };
     )"));
     ASSERT_THAT_ERROR(
         checkDataflow<OptionalIntAnalysis>(
             AnalysisInputs<OptionalIntAnalysis>(
                 Code, ast_matchers::hasName("target"),
-                [this](ASTContext &Context, Environment &Env) {
-                  assert(HasValueTop == nullptr);
-                  HasValueTop =
-                      &Env.takeOwnership(std::make_unique<AtomicBoolValue>());
-                  return OptionalIntAnalysis(Context, *HasValueTop);
+                [](ASTContext &Context, Environment &Env) {
+                  return OptionalIntAnalysis(Context);
                 })
                 .withASTBuildArgs({"-fsyntax-only", "-std=c++17"})
                 .withASTBuildVirtualMappedFiles(std::move(FilesContents)),
             /*VerifyResults=*/[&Match](const llvm::StringMap<
                                            DataflowAnalysisState<NoopLattice>>
                                            &Results,
                                        const AnalysisOutputs
                                            &AO) { Match(Results, AO.ASTCtx); }),
         llvm::Succeeded());
   }
-
-  BoolValue *HasValueTop = nullptr;
 };
 
 TEST_F(WideningTest, JoinDistinctValuesWithDistinctProperties) {
   std::string Code = R"(
     #include "widening_test_defs.h"
 
     void target(bool Cond) {
       OptionalInt Foo;
       /*[[p1]]*/
       if (Cond) {
         Foo = 1;
         /*[[p2]]*/
       }
       (void)0;
       /*[[p3]]*/
     }
   )";
   runDataflow(
       Code,
-      [this](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
-             ASTContext &ASTCtx) {
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2", "p3"));
         const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
         const Environment &Env3 = getEnvironmentAtAnnotation(Results, "p3");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         auto GetFooValue = [FooDecl](const Environment &Env) {
           return Env.getValue(*FooDecl, SkipPast::None);
         };
 
         EXPECT_EQ(GetFooValue(Env1)->getProperty("has_value"),
                   &Env1.getBoolLiteralValue(false));
         EXPECT_EQ(GetFooValue(Env2)->getProperty("has_value"),
                   &Env2.getBoolLiteralValue(true));
-        EXPECT_EQ(GetFooValue(Env3)->getProperty("has_value"), HasValueTop);
+        EXPECT_TRUE(
+            isa<TopBoolValue>(GetFooValue(Env3)->getProperty("has_value")));
       });
 }
 
 TEST_F(WideningTest, JoinDistinctValuesWithSameProperties) {
   std::string Code = R"(
     #include "widening_test_defs.h"
 
     void target(bool Cond) {
runDataflow(
 
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
         auto &FooVal2 =
             *cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::Reference));
         EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
       });
 }
 
+class TopAnalysis final : public DataflowAnalysis<TopAnalysis, NoopLattice> {
+public:
+  explicit TopAnalysis(ASTContext &Context)
+      : DataflowAnalysis<TopAnalysis, NoopLattice>(Context) {}
+
+  static NoopLattice initialElement() { return {}; }
+
+  void transfer(const CFGElement *Elt, NoopLattice &, Environment &Env) {
+    auto CS = Elt->getAs<CFGStmt>();
+    if (!CS)
+      return;
+    const Stmt *S = CS->getStmt();
+    SmallVector<BoundNodes, 1> Matches =
+        match(callExpr(callee(functionDecl(hasName("makeTop")))).bind("top"),
+              *S, getASTContext());
+    if (const auto *E = selectFirst<CallExpr>("top", Matches)) {
+      auto &Loc = Env.createStorageLocation(*E);
+      Env.setValue(Loc, Env.makeTopBoolValue());
+      Env.setStorageLocation(*E, Loc);
+    }
+  }
+
+  bool compareEquivalent(QualType Type, const Value &Val1,
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) override {
+    // Changes to a sound approximation, which allows us to test whether we can
+    // (soundly) converge for some loops.
+    return false;
+  }
+};
+
+class TopTest : public Test {
+protected:
+  template <typename Matcher>
+  void runDataflow(llvm::StringRef Code, Matcher VerifyResults) {
+    ASSERT_THAT_ERROR(
+        checkDataflow<TopAnalysis>(
+            AnalysisInputs<TopAnalysis>(
+                Code, ast_matchers::hasName("target"),
+                [](ASTContext &Context, Environment &Env) {
+                  return TopAnalysis(Context);
+                })
+                .withASTBuildArgs({"-fsyntax-only", "-std=c++17"}),
+            VerifyResults),
+        llvm::Succeeded());
+  }
+};
+
+// Tests that when Top is unused it remains Top.
+TEST_F(TopTest, UnusedTopInitializer) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target() {
+      bool Foo = makeTop();
+      /*[[p1]]*/
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(),
+                    UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+        EXPECT_EQ(FooVal1, FooVal2);
+      });
+}
+
+// Tests that when Top is unused it remains Top. Like above, but uses the
+// assignment form rather than initialization, which uses Top as an lvalue that
+// is *not* in an rvalue position.
+TEST_F(TopTest, UnusedTopAssignment) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target() {
+      bool Foo;
+      Foo = makeTop();
+      /*[[p1]]*/
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(),
+                    UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+        EXPECT_EQ(FooVal1, FooVal2);
+      });
+}
+
+TEST_F(TopTest, UnusedTopJoinsToTop) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      bool Zab1;
+      bool Zab2;
+      if (Cond) {
+        Zab1 = true;
+      } else {
+        Zab2 = true;
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+      });
+}
+
+TEST_F(TopTest, TopUsedBeforeBranchJoinsToSameAtomicBool) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      /*[[p0]]*/
+
+      // Use `Top`.
+      bool Bar = Foo;
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      bool Zab1;
+      bool Zab2;
+      if (Cond) {
+        Zab1 = true;
+      } else {
+        Zab2 = true;
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(),
+                    UnorderedElementsAre("p0", "p1", "p2"));
+        const Environment &Env0 = getEnvironmentAtAnnotation(Results, "p0");
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal0 = GetFooValue(Env0);
+        ASSERT_THAT(FooVal0, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal0))
+            << debugString(FooVal0->getKind());
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<AtomicBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<AtomicBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+        EXPECT_EQ(FooVal2, FooVal1);
+      });
+}
+
+TEST_F(TopTest, TopUsedInBothBranchesJoinsToAtomic) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      bool Zab1;
+      bool Zab2;
+      if (Cond) {
+        Zab1 = Foo;
+      } else {
+        Zab2 = Foo;
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<AtomicBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+      });
+}
+
+TEST_F(TopTest, TopUsedInBothBranchesWithoutPrecisionLoss) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+
+      bool Bar;
+      if (Cond) {
+        Bar = Foo;
+      } else {
+        Bar = Foo;
+      }
+      (void)0;
+      /*[[p]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
+        const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        const ValueDecl *BarDecl = findValueDecl(AO.ASTCtx, "Bar");
+        ASSERT_THAT(BarDecl, NotNull());
+
+        auto *FooVal =
+            dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+        ASSERT_THAT(FooVal, NotNull());
+
+        auto *BarVal =
+            dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl, SkipPast::None));
+        ASSERT_THAT(BarVal, NotNull());
+
+        EXPECT_TRUE(Env.flowConditionImplies(Env.makeIff(*FooVal, *BarVal)));
+      });
+}
+
+TEST_F(TopTest, TopUnusedBeforeLoopHeadJoinsToTop) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      while (Cond) {
+        // Use `Foo`.
+        bool Zab = Foo;
+        Zab = false;
+        Foo = makeTop();
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+      });
+}
 } // namespace