[dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext

DataflowAnalysisContext has a few too many responsibilities, this narrows them.

It also allows the Arena to be shared with analysis steps, which need to create
Values, without exposing the whole DACtx API (flow conditions etc).
This means Environment no longer needs to proxy all these methods.
(For now it still does, because there are many callsites to update, and maybe
if we separate bool formulas from values we can avoid churning them twice)

In future, if we untangle the concepts of Values from boolean formulas/atoms,
Arena would also be responsible for creating formulas and managing atom IDs.

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

1 files changed, 21 insertions, 179 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 1fbc375..ad57fd1 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -58,9 +58,9 @@ StorageLocation &DataflowAnalysisContext::createStorageLocation(QualType Type) {
                                             : getReferencedFields(Type);
     for (const FieldDecl *Field : Fields)
       FieldLocs.insert({Field, &createStorageLocation(Field->getType())});
-    return create<AggregateStorageLocation>(Type, std::move(FieldLocs));
+    return arena().create<AggregateStorageLocation>(Type, std::move(FieldLocs));
   }
-  return create<ScalarStorageLocation>(Type);
+  return arena().create<ScalarStorageLocation>(Type);
 }
 
 StorageLocation &
@@ -88,88 +88,23 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
   auto Res = NullPointerVals.try_emplace(CanonicalPointeeType, nullptr);
   if (Res.second) {
     auto &PointeeLoc = createStorageLocation(CanonicalPointeeType);
-    Res.first->second = &create<PointerValue>(PointeeLoc);
+    Res.first->second = &arena().create<PointerValue>(PointeeLoc);
   }
   return *Res.first->second;
 }
 
-static std::pair<BoolValue *, BoolValue *>
-makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
-  auto Res = std::make_pair(&LHS, &RHS);
-  if (&RHS < &LHS)
-    std::swap(Res.first, Res.second);
-  return Res;
-}
-
-BoolValue &DataflowAnalysisContext::getOrCreateConjunction(BoolValue &LHS,
-                                                           BoolValue &RHS) {
-  if (&LHS == &RHS)
-    return LHS;
-
-  auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
-                                         nullptr);
-  if (Res.second)
-    Res.first->second = &create<ConjunctionValue>(LHS, RHS);
-  return *Res.first->second;
-}
-
-BoolValue &DataflowAnalysisContext::getOrCreateDisjunction(BoolValue &LHS,
-                                                           BoolValue &RHS) {
-  if (&LHS == &RHS)
-    return LHS;
-
-  auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
-                                         nullptr);
-  if (Res.second)
-    Res.first->second = &create<DisjunctionValue>(LHS, RHS);
-  return *Res.first->second;
-}
-
-BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) {
-  auto Res = NegationVals.try_emplace(&Val, nullptr);
-  if (Res.second)
-    Res.first->second = &create<NegationValue>(Val);
-  return *Res.first->second;
-}
-
-BoolValue &DataflowAnalysisContext::getOrCreateImplication(BoolValue &LHS,
-                                                           BoolValue &RHS) {
-  if (&LHS == &RHS)
-    return getBoolLiteralValue(true);
-
-  auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
-  if (Res.second)
-    Res.first->second = &create<ImplicationValue>(LHS, RHS);
-  return *Res.first->second;
-}
-
-BoolValue &DataflowAnalysisContext::getOrCreateIff(BoolValue &LHS,
-                                                   BoolValue &RHS) {
-  if (&LHS == &RHS)
-    return getBoolLiteralValue(true);
-
-  auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
-                                           nullptr);
-  if (Res.second)
-    Res.first->second = &create<BiconditionalValue>(LHS, RHS);
-  return *Res.first->second;
-}
-
-AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
-  return create<AtomicBoolValue>();
-}
-
 void DataflowAnalysisContext::addFlowConditionConstraint(
     AtomicBoolValue &Token, BoolValue &Constraint) {
   auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
   if (!Res.second) {
-    Res.first->second = &getOrCreateConjunction(*Res.first->second, Constraint);
+    Res.first->second =
+        &arena().makeAnd(*Res.first->second, Constraint);
   }
 }
 
 AtomicBoolValue &
 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
-  auto &ForkToken = makeFlowConditionToken();
+  auto &ForkToken = arena().makeFlowConditionToken();
   FlowConditionDeps[&ForkToken].insert(&Token);
   addFlowConditionConstraint(ForkToken, Token);
   return ForkToken;
@@ -178,18 +113,19 @@ DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
 AtomicBoolValue &
 DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
                                             AtomicBoolValue &SecondToken) {
-  auto &Token = makeFlowConditionToken();
+  auto &Token = arena().makeFlowConditionToken();
   FlowConditionDeps[&Token].insert(&FirstToken);
   FlowConditionDeps[&Token].insert(&SecondToken);
-  addFlowConditionConstraint(Token,
-                             getOrCreateDisjunction(FirstToken, SecondToken));
+  addFlowConditionConstraint(
+      Token, arena().makeOr(FirstToken, SecondToken));
   return Token;
 }
 
 Solver::Result
 DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
-  Constraints.insert(&getBoolLiteralValue(true));
-  Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false)));
+  Constraints.insert(&arena().makeLiteral(true));
+  Constraints.insert(
+      &arena().makeNot(arena().makeLiteral(false)));
   return S->solve(std::move(Constraints));
 }
 
@@ -200,7 +136,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
-  llvm::DenseSet<BoolValue *> Constraints = {&Token, &getOrCreateNegation(Val)};
+  llvm::DenseSet<BoolValue *> Constraints = {&Token,
+                                             &arena().makeNot(Val)};
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
@@ -209,7 +146,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
-  llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
+  llvm::DenseSet<BoolValue *> Constraints = {
+      &arena().makeNot(Token)};
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
@@ -218,7 +156,7 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
 bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
                                                    BoolValue &Val2) {
   llvm::DenseSet<BoolValue *> Constraints = {
-      &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
+      &arena().makeNot(arena().makeEquals(Val1, Val2))};
   return isUnsatisfiable(Constraints);
 }
 
@@ -235,7 +173,7 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   } else {
     // Bind flow condition token via `iff` to its set of constraints:
     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
-    Constraints.insert(&getOrCreateIff(Token, *ConstraintsIt->second));
+    Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
   }
 
   auto DepsIt = FlowConditionDeps.find(&Token);
@@ -247,101 +185,6 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   }
 }
 
-BoolValue &DataflowAnalysisContext::substituteBoolValue(
-    BoolValue &Val,
-    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
-  auto It = SubstitutionsCache.find(&Val);
-  if (It != SubstitutionsCache.end()) {
-    // Return memoized result of substituting this boolean value.
-    return *It->second;
-  }
-
-  // Handle substitution on the boolean value (and its subvalues), saving the
-  // result into `SubstitutionsCache`.
-  BoolValue *Result;
-  switch (Val.getKind()) {
-  case Value::Kind::AtomicBool: {
-    Result = &Val;
-    break;
-  }
-  case Value::Kind::Negation: {
-    auto &Negation = *cast<NegationValue>(&Val);
-    auto &Sub = substituteBoolValue(Negation.getSubVal(), SubstitutionsCache);
-    Result = &getOrCreateNegation(Sub);
-    break;
-  }
-  case Value::Kind::Disjunction: {
-    auto &Disjunct = *cast<DisjunctionValue>(&Val);
-    auto &LeftSub =
-        substituteBoolValue(Disjunct.getLeftSubValue(), SubstitutionsCache);
-    auto &RightSub =
-        substituteBoolValue(Disjunct.getRightSubValue(), SubstitutionsCache);
-    Result = &getOrCreateDisjunction(LeftSub, RightSub);
-    break;
-  }
-  case Value::Kind::Conjunction: {
-    auto &Conjunct = *cast<ConjunctionValue>(&Val);
-    auto &LeftSub =
-        substituteBoolValue(Conjunct.getLeftSubValue(), SubstitutionsCache);
-    auto &RightSub =
-        substituteBoolValue(Conjunct.getRightSubValue(), SubstitutionsCache);
-    Result = &getOrCreateConjunction(LeftSub, RightSub);
-    break;
-  }
-  case Value::Kind::Implication: {
-    auto &IV = *cast<ImplicationValue>(&Val);
-    auto &LeftSub =
-        substituteBoolValue(IV.getLeftSubValue(), SubstitutionsCache);
-    auto &RightSub =
-        substituteBoolValue(IV.getRightSubValue(), SubstitutionsCache);
-    Result = &getOrCreateImplication(LeftSub, RightSub);
-    break;
-  }
-  case Value::Kind::Biconditional: {
-    auto &BV = *cast<BiconditionalValue>(&Val);
-    auto &LeftSub =
-        substituteBoolValue(BV.getLeftSubValue(), SubstitutionsCache);
-    auto &RightSub =
-        substituteBoolValue(BV.getRightSubValue(), SubstitutionsCache);
-    Result = &getOrCreateIff(LeftSub, RightSub);
-    break;
-  }
-  default:
-    llvm_unreachable("Unhandled Value Kind");
-  }
-  SubstitutionsCache[&Val] = Result;
-  return *Result;
-}
-
-BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowCondition(
-    AtomicBoolValue &Token,
-    llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions) {
-  assert(!Substitutions.contains(&getBoolLiteralValue(true)) &&
-         !Substitutions.contains(&getBoolLiteralValue(false)) &&
-         "Do not substitute true/false boolean literals");
-  llvm::DenseMap<BoolValue *, BoolValue *> SubstitutionsCache(
-      Substitutions.begin(), Substitutions.end());
-  return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
-}
-
-BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
-    AtomicBoolValue &Token,
-    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
-  auto ConstraintsIt = FlowConditionConstraints.find(&Token);
-  if (ConstraintsIt == FlowConditionConstraints.end()) {
-    return getBoolLiteralValue(true);
-  }
-  auto DepsIt = FlowConditionDeps.find(&Token);
-  if (DepsIt != FlowConditionDeps.end()) {
-    for (AtomicBoolValue *DepToken : DepsIt->second) {
-      auto &NewDep = buildAndSubstituteFlowConditionWithCache(
-          *DepToken, SubstitutionsCache);
-      SubstitutionsCache[DepToken] = &NewDep;
-    }
-  }
-  return substituteBoolValue(*ConstraintsIt->second, SubstitutionsCache);
-}
-
 void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
                                                 llvm::raw_ostream &OS) {
   llvm::DenseSet<BoolValue *> Constraints = {&Token};
@@ -349,8 +192,8 @@ void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
   llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
-      {&getBoolLiteralValue(false), "False"},
-      {&getBoolLiteralValue(true), "True"}};
+      {&arena().makeLiteral(false), "False"},
+      {&arena().makeLiteral(true), "True"}};
   OS << debugString(Constraints, AtomNames);
 }
 
@@ -377,8 +220,7 @@ DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {
 
 DataflowAnalysisContext::DataflowAnalysisContext(std::unique_ptr<Solver> S,
                                                  Options Opts)
-    : S(std::move(S)), TrueVal(create<AtomicBoolValue>()),
-      FalseVal(create<AtomicBoolValue>()), Opts(Opts) {
+    : S(std::move(S)), A(std::make_unique<Arena>()), Opts(Opts) {
   assert(this->S != nullptr);
   // If the -dataflow-log command-line flag was set, synthesize a logger.
   // This is ugly but provides a uniform method for ad-hoc debugging dataflow-