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

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)

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

4 files changed, 78 insertions, 51 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index a12da2d..a61887a 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -19,63 +19,83 @@ canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
   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::makeAnd(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return LHS;
+const Formula &Arena::makeAtomRef(Atom A) {
+  return cached(AtomRefs, A, [&] {
+    return &Formula::create(Alloc, Formula::AtomRef, {},
+                            static_cast<unsigned>(A));
+  });
+}
 
-  auto [It, Inserted] =
-      Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
-  if (Inserted)
-    It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
-  return *It->second;
+const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
+  return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
+    if (&LHS == &RHS)
+      return &LHS;
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &RHS : &LHS;
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &LHS : &RHS;
+
+    return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return 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 cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
+    if (&LHS == &RHS)
+      return &LHS;
+    if (LHS.kind() == Formula::Literal)
+      return LHS.literal() ? &LHS : &RHS;
+    if (RHS.kind() == Formula::Literal)
+      return RHS.literal() ? &RHS : &LHS;
+
+    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) {
-  if (&LHS == &RHS)
-    return makeLiteral(true);
-
-  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 cached(Implies, std::make_pair(&LHS, &RHS), [&] {
+    if (&LHS == &RHS)
+      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);
+
+    return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
+  });
 }
 
 const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
-  if (&LHS == &RHS)
-    return makeLiteral(true);
-
-  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 cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
+    if (&LHS == &RHS)
+      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);
+
+    return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+  });
 }
 
 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index a807ef8..2971df6 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -131,8 +131,6 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
 
 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());
 }
 
@@ -201,13 +199,8 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom 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";
   }
 }
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
index 504ad2f..12f4e25 100644
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -16,8 +16,9 @@
 
 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);
@@ -37,6 +38,7 @@ Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
 static llvm::StringLiteral sigil(Formula::Kind K) {
   switch (K) {
   case Formula::AtomRef:
+  case Formula::Literal:
     return "";
   case Formula::Not:
     return "!";
@@ -61,7 +63,16 @@ void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
 
   switch (numOperands(kind())) {
   case 0:
-    OS << getAtom();
+    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());
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index 037886d..bf48a1f 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -241,6 +241,9 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
     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]);