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

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 llvm#56931.

Differential Revision: https://reviews.llvm.org/D135397

Author: ymand

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

@@ -153,6 +153,18 @@ class DataflowAnalysisContext {
     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

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

@@ -288,6 +288,11 @@ class Environment {
     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

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

@@ -38,6 +38,7 @@ class Value {
     Struct,
 
     // Synthetic boolean values are either atomic values or logical connectives.
+    TopBool,
     AtomicBool,
     Conjunction,
     Disjunction,
@@ -82,7 +83,8 @@ class BoolValue : public Value {
   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 ||
@@ -91,6 +93,20 @@ class BoolValue : public Value {
   }
 };
 
+/// 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:

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

@@ -66,7 +66,8 @@ 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);
 }
 
@@ -371,7 +372,8 @@ LatticeJoinEffect Environment::join(const Environment &Other,
       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;
     }

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

@@ -44,6 +44,8 @@ llvm::StringRef debugString(Value::Kind Kind) {
     return "Struct";
   case Value::Kind::AtomicBool:
     return "AtomicBool";
+  case Value::Kind::TopBool:
+    return "TopBool";
   case Value::Kind::Conjunction:
     return "Conjunction";
   case Value::Kind::Disjunction:

clang/lib/Analysis/FlowSensitive/Transfer.cpp

@@ -28,6 +28,7 @@
 #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>
@@ -46,6 +47,84 @@ static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
   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,
@@ -222,7 +301,9 @@ class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
     }
 
     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;
 

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

@@ -233,6 +233,11 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
         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;

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

@@ -32,6 +32,19 @@ TEST_F(DataflowAnalysisContextTest,
   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();

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

@@ -10,7 +10,6 @@
 
 #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"
@@ -24,6 +23,7 @@ using namespace dataflow;
 using test::ConstraintContext;
 using testing::_;
 using testing::AnyOf;
+using testing::IsEmpty;
 using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
@@ -88,6 +88,32 @@ TEST(SolverTest, DistinctVars) {
                            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();

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

@@ -372,6 +372,12 @@ class ConstraintContext {
     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(