[dataflow] use true/false literals in formulas, rather than variables

[sammccall]

Summary

And simplify formulas containing true/false
It's unclear to me how useful this is, it does make formulas more
conveniently self-contained now (we can usefully print them without
carrying around the "true/false" labels)

(while here, simplify !!X to X, too)

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/Formula.h

75

castAsLiteral() ?

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

460

[sammccall]

(this was reverted, I want to reland sometime, but there's a bad interaction with a bug in nullability analysis)

[dyung]

Hi @sammccall, your change seems to be causing a test failure on several bots, can you take a look and revert if you need time to investigate?

******************** TEST 'Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/8/35' FAILED ********************
Script(shard):
--
GTEST_OUTPUT=json:/home/buildbot/buildbot-root/llvm-clang-x86_64-sie-ubuntu-fast/build/tools/clang/unittests/Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests-Clang-Unit-1681597-8-35.json GTEST_SHUFFLE=0 GTEST_TOTAL_SHARDS=35 GTEST_SHARD_INDEX=8 /home/buildbot/buildbot-root/llvm-clang-x86_64-sie-ubuntu-fast/build/tools/clang/unittests/Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests
--
Script:
--
/home/buildbot/buildbot-root/llvm-clang-x86_64-sie-ubuntu-fast/build/tools/clang/unittests/Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests --gtest_filter=BoolValueDebugStringTest.ComplexBooleanWithSomeNames
--
/home/buildbot/buildbot-root/llvm-clang-x86_64-sie-ubuntu-fast/llvm-project/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp:111: Failure
Value of: Actual
Expected: is equal to "((Y & V2) | (X | V3))"
  Actual: "((Y & V3) | (X | V2))"
/home/buildbot/buildbot-root/llvm-clang-x86_64-sie-ubuntu-fast/llvm-project/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp:111
Value of: Actual
Expected: is equal to "((Y & V2) | (X | V3))"
  Actual: "((Y & V3) | (X | V2))"
********************

Some affected bots:

• https://lab.llvm.org/buildbot/#/builders/139/builds/50255
• https://lab.llvm.org/buildbot/#/builders/216/builds/27735
• https://lab.llvm.org/buildbot/#/builders/247/builds/9334

[vvereschaka]

Hi @sammccall,

also failed FAIL: Clang-Unit::69 test on these builders

• https://lab.llvm.org/buildbot/#/builders/86/builds/65581
• https://lab.llvm.org/buildbot/#/builders/60/builds/14027
• https://lab.llvm.org/buildbot/#/builders/119/builds/15226

clang/include/clang/Analysis/FlowSensitive/Arena.h

 #include <vector>
 
 namespace clang::dataflow {
 
 /// The Arena owns the objects that model data within an analysis.
 /// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
 class Arena {
 public:
-  Arena() : True(makeAtom()), False(makeAtom()) {}
+  Arena()
+      : True(Formula::create(Alloc, Formula::Literal, {}, 1)),
+        False(Formula::create(Alloc, Formula::Literal, {}, 0)) {}
   Arena(const Arena &) = delete;
   Arena &operator=(const Arena &) = delete;
 
   /// Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to
   /// the constructor, and returns a reference to it.
   ///
   /// The `DataflowAnalysisContext` takes ownership of the created object. The
   /// object will be destroyed when the `DataflowAnalysisContext` is destroyed.
public:
 
   /// Returns a formula for `LHS <=> RHS`.
   const Formula &makeEquals(const Formula &LHS, const Formula &RHS);
 
   /// Returns a formula for the variable A.
   const Formula &makeAtomRef(Atom A);
 
   /// Returns a formula for a literal true/false.
-  const Formula &makeLiteral(bool Value) {
-    return makeAtomRef(Value ? True : False);
-  }
+  const Formula &makeLiteral(bool Value) { return Value ? True : False; }
 
   /// Returns a new atomic boolean variable, distinct from any other.
   Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
 
   /// Creates a fresh flow condition and returns a token that identifies it. The
   /// token can be used to perform various operations on the flow condition such
   /// as adding constraints to it, forking it, joining it with another flow
   /// condition, or checking implications.
private:
   llvm::DenseMap<const Formula *, const Formula *> Nots;
   llvm::DenseMap<FormulaPair, const Formula *> Implies;
   llvm::DenseMap<FormulaPair, const Formula *> Equals;
   llvm::DenseMap<Atom, const Formula *> AtomRefs;
 
   llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
   unsigned NextAtom = 0;
 
-  Atom True, False;
+  const Formula &True, &False;
 };
 
 } // namespace clang::dataflow
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H

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

public:
   /// Returns a symbolic integer value that models an integer literal equal to
   /// `Value`
   IntegerValue &getIntLiteralValue(llvm::APInt Value) const {
     return arena().makeIntLiteral(Value);
   }
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`
-  AtomicBoolValue &getBoolLiteralValue(bool Value) const {
-    return cast<AtomicBoolValue>(
-        arena().makeBoolValue(arena().makeLiteral(Value)));
+  BoolValue &getBoolLiteralValue(bool Value) const {
+    return arena().makeBoolValue(arena().makeLiteral(Value));
   }
 
   /// Returns an atomic boolean value.
   BoolValue &makeAtomicBoolValue() const {
     return arena().makeAtomValue();
   }
 
   /// Returns a unique instance of boolean Top.

clang/include/clang/Analysis/FlowSensitive/Formula.h

 /// For this reason, Formulas are Arena-allocated and over-aligned.
 class Formula;
 class alignas(const Formula *) Formula {
 public:
   enum Kind : unsigned {
     /// A reference to an atomic boolean variable.
     /// We name these e.g. "V3", where 3 == atom identity == Value.
     AtomRef,
-    // FIXME: add const true/false rather than modeling them as variables
+    /// Constant true or false.
+    Literal,
 
     Not, /// True if its only operand is false
 
     // These kinds connect two operands LHS and RHS
     And,     /// True if LHS and RHS are both true
     Or,      /// True if either LHS or RHS is true
     Implies, /// True if LHS is false or RHS is true
     Equal,   /// True if LHS and RHS have the same truth value
   };
   Kind kind() const { return FormulaKind; }
 
   Atom getAtom() const {
     assert(kind() == AtomRef);
     return static_cast<Atom>(Value);
   }
 
+  bool literal() const {
+    assert(kind() == Literal);
+    return static_cast<bool>(Value);
+  }
+
   ArrayRef<const Formula *> operands() const {
     return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
                     numOperands(kind()));
   }
 
   using AtomNames = llvm::DenseMap<Atom, std::string>;
   // Produce a stable human-readable representation of this formula.
   // For example: (V3 | !(V1 & V2))
   // If AtomNames is provided, these override the default V0, V1... names.
   void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
 
   // Allocate Formulas using Arena rather than calling this function directly.
-  static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+  static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
                                ArrayRef<const Formula *> Operands,
                                unsigned Value = 0);
 
 private:
   Formula() = default;
   Formula(const Formula &) = delete;
   Formula &operator=(const Formula &) = delete;
 
   static unsigned numOperands(Kind K) {
     switch (K) {
     case AtomRef:
+    case Literal:
       return 0;
     case Not:
       return 1;
     case And:
     case Or:
     case Implies:
     case Equal:
       return 2;

clang/lib/Analysis/FlowSensitive/Arena.cpp

 static std::pair<const Formula *, const Formula *>
 canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
   if (&RHS < &LHS) // FIXME: use a deterministic order instead
     std::swap(Res.first, Res.second);
   return Res;
 }
 
-const Formula &Arena::makeAtomRef(Atom A) {
-  auto [It, Inserted] = AtomRefs.try_emplace(A);
+template <class Key, class ComputeFunc>
+const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
+                      ComputeFunc &&Compute) {
+  auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K));
   if (Inserted)
-    It->second =
-        &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+    It->second = Compute();
   return *It->second;
 }
 
+const Formula &Arena::makeAtomRef(Atom A) {
+  return cached(AtomRefs, A, [&] {
+    return &Formula::create(Alloc, Formula::AtomRef, {},
+                            static_cast<unsigned>(A));
+  });
+}
+
 const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
+  return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
     if (&LHS == &RHS)
-    return LHS;
+      return &LHS;
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &LHS;
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &LHS : &RHS;
 
-  auto [It, Inserted] =
-      Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
-  return *It->second;
+    return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
+  return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
     if (&LHS == &RHS)
-    return LHS;
+      return &LHS;
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &LHS : &RHS;
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &RHS : &LHS;
 
-  auto [It, Inserted] =
-      Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
-  return *It->second;
+    return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeNot(const Formula &Val) {
-  auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::Not, {&Val});
-  return *It->second;
+  return cached(Nots, &Val, [&] {
+    if (Val.kind() == Formula::Not)
+      return Val.operands()[0];
+    if (Val.kind() == Formula::Literal)
+      return &makeLiteral(!Val.literal());
+
+    return &Formula::create(Alloc, Formula::Not, {&Val});
+  });
 }
 
 const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
+  return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
     if (&LHS == &RHS)
-    return makeLiteral(true);
+      return &makeLiteral(true);
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &makeLiteral(true);
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &RHS : &makeNot(LHS);
 
-  auto [It, Inserted] =
-      Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
-  return *It->second;
+    return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
+  return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
     if (&LHS == &RHS)
-    return makeLiteral(true);
+      return &makeLiteral(true);
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &makeNot(RHS);
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &LHS : &makeNot(LHS);
 
-  auto [It, Inserted] =
-      Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
-  return *It->second;
+    return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+  });
 }
 
 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
   auto [It, Inserted] = IntegerLiterals.try_emplace(Value, nullptr);
 
   if (Inserted)
     It->second = &create<IntegerValue>();
   return *It->second;

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
   addFlowConditionConstraint(Token,
                              arena().makeOr(arena().makeAtomRef(FirstToken),
                                             arena().makeAtomRef(SecondToken)));
   return Token;
 }
 
 Solver::Result DataflowAnalysisContext::querySolver(
     llvm::SetVector<const Formula *> Constraints) {
-  Constraints.insert(&arena().makeLiteral(true));
-  Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
   return S->solve(Constraints.getArrayRef());
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
                                                    const Formula &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt

 
 void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
                                                 llvm::raw_ostream &OS) {
   llvm::SetVector<const Formula *> Constraints;
   Constraints.insert(&arena().makeAtomRef(Token));
   llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
-  // TODO: have formulas know about true/false directly instead
-  Atom True = arena().makeLiteral(true).getAtom();
-  Atom False = arena().makeLiteral(false).getAtom();
-  Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
-
   for (const auto *Constraint : Constraints) {
-    Constraint->print(OS, &Names);
+    Constraint->print(OS);
     OS << "\n";
   }
 }
 
 const ControlFlowContext *
 DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {
   // Canonicalize the key:
   F = F->getDefinition();

clang/lib/Analysis/FlowSensitive/Formula.cpp

 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Allocator.h"
 #include "llvm/Support/ErrorHandling.h"
 #include <cassert>
 
 namespace clang::dataflow {
 
-Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
-                         ArrayRef<const Formula *> Operands, unsigned Value) {
+const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
+                               ArrayRef<const Formula *> Operands,
+                               unsigned Value) {
   assert(Operands.size() == numOperands(K));
   if (Value != 0) // Currently, formulas have values or operands, not both.
     assert(numOperands(K) == 0);
   void *Mem = Alloc.Allocate(sizeof(Formula) +
                                  Operands.size() * sizeof(Operands.front()),
                              alignof(Formula));
   Formula *Result = new (Mem) Formula();
   Result->FormulaKind = K;
   Result->Value = Value;
   // Operands are stored as `const Formula *`s after the formula itself.
   // We don't need to construct an object as pointers are trivial types.
   // Formula is alignas(const Formula *), so alignment is satisfied.
   llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
   return *Result;
 }
 
 static llvm::StringLiteral sigil(Formula::Kind K) {
   switch (K) {
   case Formula::AtomRef:
+  case Formula::Literal:
     return "";
   case Formula::Not:
     return "!";
   case Formula::And:
     return " & ";
   case Formula::Or:
     return " | ";
   case Formula::Implies:
     return " => ";
   case Formula::Equal:
     return " = ";
   }
   llvm_unreachable("unhandled formula kind");
 }
 
 void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
   if (Names && kind() == AtomRef)
     if (auto It = Names->find(getAtom()); It != Names->end()) {
       OS << It->second;
       return;
     }
 
   switch (numOperands(kind())) {
   case 0:
+    switch (kind()) {
+    case AtomRef:
       OS << getAtom();
       break;
+    case Literal:
+      OS << (literal() ? "true" : "false");
+      break;
+    default:
+      llvm_unreachable("unhandled formula kind");
+    }
+    break;
   case 1:
     OS << sigil(kind());
     operands()[0]->print(OS, Names);
     break;
   case 2:
     OS << '(';
     operands()[0]->print(OS, Names);
     OS << sigil(kind());
     operands()[1]->print(OS, Names);
     OS << ')';
     break;
   default:
     llvm_unreachable("unhandled formula arity");
   }
 }
 
 } // namespace clang::dataflow
 No newline at end of file

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

while (!UnprocessedSubVals.empty()) {
 
     if (ProcessedSubVals[Var])
       continue;
     ProcessedSubVals[Var] = true;
 
     switch (Val->kind()) {
     case Formula::AtomRef:
       break;
+    case Formula::Literal:
+      CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
+      break;
     case Formula::And: {
       const Variable LHS = GetVar(Val->operands()[0]);
       const Variable RHS = GetVar(Val->operands()[1]);
 
       if (LHS == RHS) {
         // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

 }
 
 TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
   auto &X = A.makeTopValue();
   auto &Y = A.makeTopValue();
   EXPECT_NE(&X, &Y);
 }
 
-TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.makeAtomRef(A.makeAtom());
-  auto &XAndX = A.makeAnd(X, X);
-  EXPECT_EQ(&XAndX, &X);
-}
-
 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XAndY1 = A.makeAnd(X, Y);
   auto &XAndY2 = A.makeAnd(X, Y);
   EXPECT_EQ(&XAndY1, &XAndY2);
 
   auto &YAndX = A.makeAnd(Y, X);
   EXPECT_EQ(&XAndY1, &YAndX);
 
   auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XAndZ = A.makeAnd(X, Z);
   EXPECT_NE(&XAndY1, &XAndZ);
 }
 
-TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.makeAtomRef(A.makeAtom());
-  auto &XOrX = A.makeOr(X, X);
-  EXPECT_EQ(&XOrX, &X);
-}
-
 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XOrY1 = A.makeOr(X, Y);
   auto &XOrY2 = A.makeOr(X, Y);
   EXPECT_EQ(&XOrY1, &XOrY2);
 
   auto &YOrX = A.makeOr(Y, X);
TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
   auto &NotX1 = A.makeNot(X);
   auto &NotX2 = A.makeNot(X);
   EXPECT_EQ(&NotX1, &NotX2);
   auto &Y = A.makeAtomRef(A.makeAtom());
   auto &NotY = A.makeNot(Y);
   EXPECT_NE(&NotX1, &NotY);
 }
 
-TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
-  auto &X = A.makeAtomRef(A.makeAtom());
-  auto &XImpliesX = A.makeImplies(X, X);
-  EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
-}
-
 TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XImpliesY1 = A.makeImplies(X, Y);
   auto &XImpliesY2 = A.makeImplies(X, Y);
   EXPECT_EQ(&XImpliesY1, &XImpliesY2);
 
   auto &YImpliesX = A.makeImplies(Y, X);
   EXPECT_NE(&XImpliesY1, &YImpliesX);
 
   auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XImpliesZ = A.makeImplies(X, Z);
   EXPECT_NE(&XImpliesY1, &XImpliesZ);
 }
 
-TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
-  auto &X = A.makeAtomRef(A.makeAtom());
-  auto &XIffX = A.makeEquals(X, X);
-  EXPECT_EQ(&XIffX, &A.makeLiteral(true));
-}
-
 TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
   auto &X = A.makeAtomRef(A.makeAtom());
   auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XIffY1 = A.makeEquals(X, Y);
   auto &XIffY2 = A.makeEquals(X, Y);
   EXPECT_EQ(&XIffY1, &XIffY2);
 
   auto &YIffX = A.makeEquals(Y, X);
TEST_F(ArenaTest, Interning) {
   const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
   EXPECT_EQ(&F1, &F2);
   BoolValue &B1 = A.makeBoolValue(F1);
   BoolValue &B2 = A.makeBoolValue(F2);
   EXPECT_EQ(&B1, &B2);
   EXPECT_EQ(&B1.formula(), &F1);
 }
 
+TEST_F(ArenaTest, IdentitySimplification) {
+  auto &X = A.makeAtomRef(A.makeAtom());
+
+  EXPECT_EQ(&X, &A.makeAnd(X, X));
+  EXPECT_EQ(&X, &A.makeOr(X, X));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
+  EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
+}
+
+TEST_F(ArenaTest, LiteralSimplification) {
+  auto &X = A.makeAtomRef(A.makeAtom());
+
+  EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
+
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
+  EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
+
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
+  EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
+
+  EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
+
+  EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
+  EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
+}
+
 } // namespace
 } // namespace clang::dataflow

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

 TEST(BoolValueDebugStringTest, AtomicBoolean) {
   ConstraintContext Ctx;
   auto B = Ctx.atom();
 
   auto Expected = "V0";
   EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
+TEST(BoolValueDebugStringTest, Literal) {
+  ConstraintContext Ctx;
+  EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true)));
+  EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false)));
+}
+
 TEST(BoolValueDebugStringTest, Negation) {
   ConstraintContext Ctx;
   auto B = Ctx.neg(Ctx.atom());
 
   auto Expected = "!V0";
   EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
TEST(BoolValueDebugStringTest, NestedBoolean) {
   auto B = Ctx.conj(V0, Ctx.disj(V1, Ctx.conj(V2, Ctx.disj(V3, V4))));
 
   auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
   EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
   ConstraintContext Ctx;
-  auto True = Ctx.atom();
-  auto False = Ctx.atom();
-  auto V2 = Ctx.atom();
-  auto V3 = Ctx.atom();
+  auto X = Ctx.atom();
+  auto Y = Ctx.atom();
   Formula::AtomNames Names;
-  Names[True->getAtom()] = "true";
-  Names[False->getAtom()] = "false";
-  auto B = Ctx.disj(Ctx.conj(False, V2), Ctx.disj(True, V3));
+  Names[X->getAtom()] = "X";
+  Names[Y->getAtom()] = "Y";
+  auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom()));
 
-  auto Expected = R"(((false & V2) | (true | V3)))";
+  auto Expected = R"(((Y & V2) | (X | V3)))";
   std::string Actual;
   llvm::raw_string_ostream OS(Actual);
   B->print(OS, &Names);
   EXPECT_THAT(Actual, StrEq(Expected));
 }
 
 } // namespace

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

class ConstraintContext {
   }
 
 public:
   // Returns a reference to a fresh atomic variable.
   const Formula *atom() {
     return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
   }
 
+  // Returns a reference to a literal boolean value.
+  const Formula *literal(bool B) {
+    return &Formula::create(A, Formula::Literal, {}, B);
+  }
+
   // Creates a boolean conjunction.
   const Formula *conj(const Formula *LHS, const Formula *RHS) {
     return make(Formula::And, {LHS, RHS});
   }
 
   // Creates a boolean disjunction.
   const Formula *disj(const Formula *LHS, const Formula *RHS) {
     return make(Formula::Or, {LHS, RHS});

clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

runDataflow(
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const auto *FooVal =
-            dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
         ASSERT_THAT(FooVal, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
         const auto *BarVal =
-            dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*BarDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
         ASSERT_THAT(BarVal, NotNull());
 
         EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true));
         EXPECT_EQ(BarVal, &Env.getBoolLiteralValue(false));
       });
 }
 
 TEST(TransferTest, AssignFromCompositeBoolExpression) {
runDataflow(
          ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
         const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
 
         const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
         ASSERT_THAT(FooDecl, NotNull());
 
         const auto *FooVal =
-            dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
         ASSERT_THAT(FooVal, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
         const auto *BarVal =
             dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
         ASSERT_THAT(BarVal, NotNull());