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

[sammccall]

Summary

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.

[gribozavr2]

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

16–17

[mboehme]

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

16–17

While we're at it, put Arena in backticks as well?

[sammccall]

Tweak comment
Drop flow-condition substitution instead of moving into Arena, it's dead.

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

16–17

Added triple-slashes and changed to "example" so it's less prone to getting out of date (which I think was the point?).

I kept this split as two sentences to preserve a self-contained one-line description for readability.

Quoting the name of the class itself breaks the flow of the sentence to emphasize that this is a reference, but that doesn't seem necessary in the class declaration.

[sgatev]

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

91–97

This can be removed.

[ymandel]

Love it! Thanks.

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

129

add newline?

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

+//===-- Arena.h -------------------------------*- C++ -------------------*-===//
+//
+// 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 "clang/Analysis/FlowSensitive/StorageLocation.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include <vector>
+
+namespace clang::dataflow {
+
+/// The Arena owns the objects that model data within an analysis.
+/// For example, `Value` and `StorageLocation`.
+class Arena {
+public:
+  Arena()
+      : TrueVal(create<AtomicBoolValue>()),
+        FalseVal(create<AtomicBoolValue>()) {}
+  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.
+  template <typename T, typename... Args>
+  std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
+  create(Args &&...args) {
+    // Note: If allocation of individual `StorageLocation`s turns out to be
+    // costly, consider creating specializations of `create<T>` for commonly
+    // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`.
+    return *cast<T>(
+        Locs.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
+            .get());
+  }
+
+  /// Creates a `T` (some subclass of `Value`), 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.
+  template <typename T, typename... Args>
+  std::enable_if_t<std::is_base_of<Value, T>::value, T &>
+  create(Args &&...args) {
+    // Note: If allocation of individual `Value`s turns out to be costly,
+    // consider creating specializations of `create<T>` for commonly used
+    // `Value` subclasses and make them use a `BumpPtrAllocator`.
+    return *cast<T>(
+        Vals.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
+            .get());
+  }
+
+  /// 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);
+
+  /// Returns a boolean value that represents the disjunction 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 &makeOr(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the negation of `Val`. Subsequent
+  /// calls with the same argument will return the same result.
+  BoolValue &makeNot(BoolValue &Val);
+
+  /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls
+  /// with the same arguments, will return the same result. If the given boolean
+  /// values represent the same value, the result will be a value that
+  /// represents the true boolean literal.
+  BoolValue &makeImplies(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents `LHS <=> 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 a value that represents the true boolean literal.
+  BoolValue &makeEquals(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a symbolic boolean value that models a boolean literal equal to
+  /// `Value`. These literals are the same every time.
+  AtomicBoolValue &makeLiteral(bool Value) const {
+    return Value ? TrueVal : FalseVal;
+  }
+
+  /// Returns a boolean value as a result of substituting `Val` and its sub
+  /// values based on entries in `SubstitutionsCache`. Intermediate results are
+  /// stored in `SubstitutionsCache` to avoid reprocessing values that have
+  /// already been visited.
+  BoolValue &substituteBoolValue(
+      BoolValue &Val,
+      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
+  /// 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.
+  AtomicBoolValue &makeFlowConditionToken() {
+    return create<AtomicBoolValue>();
+  }
+
+private:
+  // Storage for the state of a program.
+  std::vector<std::unique_ptr<StorageLocation>> Locs;
+  std::vector<std::unique_ptr<Value>> Vals;
+
+  // Indices that are used to avoid recreating the same composite boolean
+  // values.
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+      ConjunctionVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+      DisjunctionVals;
+  llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
+      ImplicationVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
+      BiconditionalVals;
+
+  AtomicBoolValue &TrueVal;
+  AtomicBoolValue &FalseVal;
+};
+
+} // namespace clang::dataflow
 No newline at end of file

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

 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
 
 #include "clang/AST/Decl.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/TypeOrdering.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/Support/Compiler.h"
 #include <cassert>
public:
   ///
   ///  `S` must not be null.
   DataflowAnalysisContext(std::unique_ptr<Solver> S,
                           Options Opts = Options{
                               /*ContextSensitiveOpts=*/std::nullopt,
                               /*Logger=*/nullptr});
   ~DataflowAnalysisContext();
 
-  /// 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.
-  template <typename T, typename... Args>
-  std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
-  create(Args &&...args) {
-    // Note: If allocation of individual `StorageLocation`s turns out to be
-    // costly, consider creating specializations of `create<T>` for commonly
-    // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`.
-    return *cast<T>(
-        Locs.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
-            .get());
-  }
-
-  /// Creates a `T` (some subclass of `Value`), 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.
-  template <typename T, typename... Args>
-  std::enable_if_t<std::is_base_of<Value, T>::value, T &>
-  create(Args &&...args) {
-    // Note: If allocation of individual `Value`s turns out to be costly,
-    // consider creating specializations of `create<T>` for commonly used
-    // `Value` subclasses and make them use a `BumpPtrAllocator`.
-    return *cast<T>(
-        Vals.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
-            .get());
-  }
-
-  /// Takes ownership of `Loc` and returns a reference to it.
-  ///
-  /// This function is deprecated. Instead of
-  /// `takeOwnership(std::make_unique<SomeStorageLocation>(args))`, prefer
-  /// `create<SomeStorageLocation>(args)`.
-  ///
-  /// Requirements:
-  ///
-  ///  `Loc` must not be null.
-  template <typename T>
-  LLVM_DEPRECATED("use create<T> instead", "")
-  std::enable_if_t<std::is_base_of<StorageLocation, T>::value,
-                   T &> takeOwnership(std::unique_ptr<T> Loc) {
-    assert(Loc != nullptr);
-    Locs.push_back(std::move(Loc));
-    return *cast<T>(Locs.back().get());
-  }
-
-  /// Takes ownership of `Val` and returns a reference to it.
-  ///
-  /// This function is deprecated. Instead of
-  /// `takeOwnership(std::make_unique<SomeValue>(args))`, prefer
-  /// `create<SomeValue>(args)`.
-  ///
-  /// Requirements:
-  ///
-  ///  `Val` must not be null.
-  template <typename T>
-  LLVM_DEPRECATED("use create<T> instead", "")
-  std::enable_if_t<std::is_base_of<Value, T>::value, T &> takeOwnership(
-      std::unique_ptr<T> Val) {
-    assert(Val != nullptr);
-    Vals.push_back(std::move(Val));
-    return *cast<T>(Vals.back().get());
-  }
-
   /// Returns a new storage location appropriate for `Type`.
   ///
   /// A null `Type` is interpreted as the pointee type of `std::nullptr_t`.
   StorageLocation &createStorageLocation(QualType Type);
 
   /// Returns a stable storage location for `D`.
   StorageLocation &getStableStorageLocation(const VarDecl &D);
 
StorageLocation *getStorageLocation(const Expr &E) const {
     return It == ExprToLoc.end() ? nullptr : It->second;
   }
 
   /// Returns a pointer value that represents a null pointer. Calls with
   /// `PointeeType` that are canonically equivalent will return the same result.
   /// A null `PointeeType` can be used for the pointee of `std::nullptr_t`.
   PointerValue &getOrCreateNullPointerValue(QualType PointeeType);
 
-  /// Returns a symbolic boolean value that models a boolean literal equal to
-  /// `Value`.
-  AtomicBoolValue &getBoolLiteralValue(bool Value) const {
-    return Value ? TrueVal : FalseVal;
-  }
-
-  /// Creates an atomic boolean value.
-  LLVM_DEPRECATED("use create<AtomicBoolValue> instead",
-                  "create<AtomicBoolValue>")
-  AtomicBoolValue &createAtomicBoolValue() { return create<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`.
-  LLVM_DEPRECATED("use create<TopBoolValue> instead", "create<TopBoolValue>")
-  TopBoolValue &createTopBoolValue() { return create<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
-  /// order, will return the same result. If the given boolean values represent
-  /// the same value, the result will be the value itself.
-  BoolValue &getOrCreateDisjunction(BoolValue &LHS, BoolValue &RHS);
-
-  /// Returns a boolean value that represents the negation of `Val`. Subsequent
-  /// calls with the same argument will return the same result.
-  BoolValue &getOrCreateNegation(BoolValue &Val);
-
-  /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls
-  /// with the same arguments, will return the same result. If the given boolean
-  /// values represent the same value, the result will be a value that
-  /// represents the true boolean literal.
-  BoolValue &getOrCreateImplication(BoolValue &LHS, BoolValue &RHS);
-
-  /// Returns a boolean value that represents `LHS <=> 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 a value that represents the true boolean literal.
-  BoolValue &getOrCreateIff(BoolValue &LHS, BoolValue &RHS);
-
-  /// 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.
-  AtomicBoolValue &makeFlowConditionToken();
-
   /// Adds `Constraint` to the flow condition identified by `Token`.
   void addFlowConditionConstraint(AtomicBoolValue &Token,
                                   BoolValue &Constraint);
 
   /// Creates a new flow condition with the same constraints as the flow
   /// condition identified by `Token` and returns its token.
   AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
 
   /// Creates a new flow condition that represents the disjunction of the flow
   /// conditions identified by `FirstToken` and `SecondToken`, and returns its
   /// token.
   AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
                                       AtomicBoolValue &SecondToken);
 
-  // FIXME: This function returns the flow condition expressed directly as its
-  // constraints: (C1 AND C2 AND ...). This differs from the general approach in
-  // the framework where a flow condition is represented as a token (an atomic
-  // boolean) with dependencies and constraints tracked in `FlowConditionDeps`
-  // and `FlowConditionConstraints`: (FC <=> C1 AND C2 AND ...).
-  // Consider if we should make the representation of flow condition consistent,
-  // returning an atomic boolean token with separate constraints instead.
-  //
-  /// Builds and returns the logical formula defining the flow condition
-  /// identified by `Token`. If a value in the formula is present as a key in
-  /// `Substitutions`, it will be substituted with the value it maps to.
-  /// As an example, say we have flow condition tokens FC1, FC2, FC3 and
-  /// FlowConditionConstraints: { FC1: C1,
-  ///                             FC2: C2,
-  ///                             FC3: (FC1 v FC2) ^ C3 }
-  /// buildAndSubstituteFlowCondition(FC3, {{C1 -> C1'}}) will return a value
-  /// corresponding to (C1' v C2) ^ C3.
-  BoolValue &buildAndSubstituteFlowCondition(
-      AtomicBoolValue &Token,
-      llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions);
-
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` imply that `Val` is true.
   bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
 
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` are always true.
   bool flowConditionIsTautology(AtomicBoolValue &Token);
 
   /// Returns true if `Val1` is equivalent to `Val2`.
   /// Note: This function doesn't take into account constraints on `Val1` and
   /// `Val2` imposed by the flow condition.
   bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
 
   LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
                                           llvm::raw_ostream &OS = llvm::dbgs());
 
   /// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
   /// returns null.
   const ControlFlowContext *getControlFlowContext(const FunctionDecl *F);
 
   const Options &getOptions() { return Opts; }
 
+  Arena &arena() { return *A; }
+
 private:
   friend class Environment;
 
   struct NullableQualTypeDenseMapInfo : private llvm::DenseMapInfo<QualType> {
     static QualType getEmptyKey() {
       // Allow a NULL `QualType` by using a different value as the empty key.
       return QualType::getFromOpaquePtr(reinterpret_cast<Type *>(1));
     }
private:
 
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
     return querySolver(std::move(Constraints)).getStatus() ==
            Solver::Result::Status::Unsatisfiable;
   }
 
-  /// Returns a boolean value as a result of substituting `Val` and its sub
-  /// values based on entries in `SubstitutionsCache`. Intermediate results are
-  /// stored in `SubstitutionsCache` to avoid reprocessing values that have
-  /// already been visited.
-  BoolValue &substituteBoolValue(
-      BoolValue &Val,
-      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
-
-  /// Builds and returns the logical formula defining the flow condition
-  /// identified by `Token`, sub values may be substituted based on entries in
-  /// `SubstitutionsCache`. Intermediate results are stored in
-  /// `SubstitutionsCache` to avoid reprocessing values that have already been
-  /// visited.
-  BoolValue &buildAndSubstituteFlowConditionWithCache(
-      AtomicBoolValue &Token,
-      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
-
   std::unique_ptr<Solver> S;
-
-  // Storage for the state of a program.
-  std::vector<std::unique_ptr<StorageLocation>> Locs;
-  std::vector<std::unique_ptr<Value>> Vals;
+  std::unique_ptr<Arena> A;
 
   // Maps from program declarations and statements to storage locations that are
   // assigned to them. These assignments are global (aggregated across all basic
   // blocks) and are used to produce stable storage locations when the same
   // basic blocks are evaluated multiple times. The storage locations that are
   // in scope for a particular basic block are stored in `Environment`.
   llvm::DenseMap<const ValueDecl *, StorageLocation *> DeclToLoc;
   llvm::DenseMap<const Expr *, StorageLocation *> ExprToLoc;
 
   // Null pointer values, keyed by the canonical pointee type.
   //
   // FIXME: The pointer values are indexed by the pointee types which are
   // required to initialize the `PointeeLoc` field in `PointerValue`. Consider
   // creating a type-independent `NullPointerValue` without a `PointeeLoc`
   // field.
   llvm::DenseMap<QualType, PointerValue *, NullableQualTypeDenseMapInfo>
       NullPointerVals;
 
-  AtomicBoolValue &TrueVal;
-  AtomicBoolValue &FalseVal;
-
   Options Opts;
 
-  // Indices that are used to avoid recreating the same composite boolean
-  // values.
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
-      ConjunctionVals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
-      DisjunctionVals;
-  llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
-      ImplicationVals;
-  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
-      BiconditionalVals;
-
   // Flow conditions are tracked symbolically: each unique flow condition is
   // associated with a fresh symbolic variable (token), bound to the clause that
   // defines the flow condition. Conceptually, each binding corresponds to an
   // "iff" of the form `FC <=> (C1 ^ C2 ^ ...)` where `FC` is a flow condition
   // token (an atomic boolean) and `Ci`s are the set of constraints in the flow
   // flow condition clause. The set of constraints (C1 ^ C2 ^ ...) are stored in
   // the `FlowConditionConstraints` map, keyed by the token of the flow
   // condition.

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

public:
   /// If `DeclCtx` is a non-static member function, initializes the environment
   /// with a symbolic representation of the `this` pointee.
   Environment(DataflowAnalysisContext &DACtx, const DeclContext &DeclCtx);
 
   const DataflowAnalysisContext::Options &getAnalysisOptions() const {
     return DACtx->getOptions();
   }
 
+  Arena &arena() const { return DACtx->arena(); }
+
   Logger &logger() const { return *DACtx->getOptions().Log; }
 
   /// Creates and returns an environment to use for an inline analysis  of the
   /// callee. Uses the storage location from each argument in the `Call` as the
   /// storage location for the corresponding parameter in the callee.
   ///
   /// Requirements:
   ///
public:
   /// Equivalent to `getValue(getStorageLocation(D, SP), SkipPast::None)` if `D`
   /// is assigned a storage location in the environment, otherwise returns null.
   Value *getValue(const ValueDecl &D, SkipPast SP) const;
 
   /// Equivalent to `getValue(getStorageLocation(E, SP), SkipPast::None)` if `E`
   /// is assigned a storage location in the environment, otherwise returns null.
   Value *getValue(const Expr &E, SkipPast SP) const;
 
-  /// Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to
-  /// the constructor, and returns a reference to it.
-  ///
-  /// The analysis context takes ownership of the created object. The object
-  /// will be destroyed when the analysis context is destroyed.
-  template <typename T, typename... Args>
-  std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
-  create(Args &&...args) {
-    return DACtx->create<T>(std::forward<Args>(args)...);
-  }
+  // FIXME: should we deprecate the following & call arena().create() directly?
 
   /// Creates a `T` (some subclass of `Value`), forwarding `args` to the
   /// constructor, and returns a reference to it.
   ///
   /// The analysis context takes ownership of the created object. The object
   /// will be destroyed when the analysis context is destroyed.
   template <typename T, typename... Args>
   std::enable_if_t<std::is_base_of<Value, T>::value, T &>
   create(Args &&...args) {
-    return DACtx->create<T>(std::forward<Args>(args)...);
-  }
-
-  /// Transfers ownership of `Loc` to the analysis context and returns a
-  /// reference to it.
-  ///
-  /// This function is deprecated. Instead of
-  /// `takeOwnership(std::make_unique<SomeStorageLocation>(args))`, prefer
-  /// `create<SomeStorageLocation>(args)`.
-  ///
-  /// Requirements:
-  ///
-  ///  `Loc` must not be null.
-  template <typename T>
-  LLVM_DEPRECATED("use create<T> instead", "")
-  std::enable_if_t<std::is_base_of<StorageLocation, T>::value,
-                   T &> takeOwnership(std::unique_ptr<T> Loc) {
-    return DACtx->takeOwnership(std::move(Loc));
-  }
-
-  /// Transfers ownership of `Val` to the analysis context and returns a
-  /// reference to it.
-  ///
-  /// This function is deprecated. Instead of
-  /// `takeOwnership(std::make_unique<SomeValue>(args))`, prefer
-  /// `create<SomeValue>(args)`.
-  ///
-  /// Requirements:
-  ///
-  ///  `Val` must not be null.
-  template <typename T>
-  LLVM_DEPRECATED("use create<T> instead", "")
-  std::enable_if_t<std::is_base_of<Value, T>::value, T &> takeOwnership(
-      std::unique_ptr<T> Val) {
-    return DACtx->takeOwnership(std::move(Val));
+    return arena().create<T>(std::forward<Args>(args)...);
   }
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`
   AtomicBoolValue &getBoolLiteralValue(bool Value) const {
-    return DACtx->getBoolLiteralValue(Value);
+    return arena().makeLiteral(Value);
   }
 
   /// Returns an atomic boolean value.
   BoolValue &makeAtomicBoolValue() const {
-    return DACtx->create<AtomicBoolValue>();
+    return arena().create<AtomicBoolValue>();
   }
 
   /// Returns a unique instance of boolean Top.
   BoolValue &makeTopBoolValue() const {
-    return DACtx->create<TopBoolValue>();
+    return arena().create<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 &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->getOrCreateConjunction(LHS, RHS);
+    return arena().makeAnd(LHS, RHS);
   }
 
   /// Returns a boolean value that represents the disjunction 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 &makeOr(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->getOrCreateDisjunction(LHS, RHS);
+    return arena().makeOr(LHS, RHS);
   }
 
   /// Returns a boolean value that represents the negation of `Val`. Subsequent
   /// calls with the same argument will return the same result.
   BoolValue &makeNot(BoolValue &Val) const {
-    return DACtx->getOrCreateNegation(Val);
+    return arena().makeNot(Val);
   }
 
   /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
   /// the same arguments, will return the same result. If the given boolean
   /// values represent the same value, the result will be a value that
   /// represents the true boolean literal.
   BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->getOrCreateImplication(LHS, RHS);
+    return arena().makeImplies(LHS, RHS);
   }
 
   /// Returns a boolean value represents `LHS` <=> `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 a value that represents the true boolean literal.
   BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->getOrCreateIff(LHS, RHS);
+    return arena().makeEquals(LHS, RHS);
   }
 
   /// Returns the token that identifies the flow condition of the environment.
   AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
 
-  /// Builds and returns the logical formula defining the flow condition
-  /// identified by `Token`. If a value in the formula is present as a key in
-  /// `Substitutions`, it will be substituted with the value it maps to.
-  BoolValue &buildAndSubstituteFlowCondition(
-      AtomicBoolValue &Token,
-      llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions) {
-    return DACtx->buildAndSubstituteFlowCondition(Token,
-                                                  std::move(Substitutions));
-  }
-
   /// Adds `Val` to the set of clauses that constitute the flow condition.
   void addToFlowCondition(BoolValue &Val);
 
   /// Returns true if and only if the clauses that constitute the flow condition
   /// imply that `Val` is true.
   bool flowConditionImplies(BoolValue &Val) const;
 
   /// Returns the `DeclContext` of the block being analysed, if any. Otherwise,

clang/lib/Analysis/FlowSensitive/Arena.cpp

+//===-- Arena.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 "clang/Analysis/FlowSensitive/Arena.h"
+
+namespace clang::dataflow {
+
+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 &Arena::makeAnd(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 &Arena::makeOr(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 &Arena::makeNot(BoolValue &Val) {
+  auto Res = NegationVals.try_emplace(&Val, nullptr);
+  if (Res.second)
+    Res.first->second = &create<NegationValue>(Val);
+  return *Res.first->second;
+}
+
+BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return makeLiteral(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 &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return makeLiteral(true);
+
+  auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                           nullptr);
+  if (Res.second)
+    Res.first->second = &create<BiconditionalValue>(LHS, RHS);
+  return *Res.first->second;
+}
+
+} // namespace clang::dataflow

clang/lib/Analysis/FlowSensitive/CMakeLists.txt

 add_clang_library(clangAnalysisFlowSensitive
+  Arena.cpp
   ControlFlowContext.cpp
   DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
   Logger.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp
   Value.cpp
   WatchedLiteralsSolver.cpp

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

if (!Type.isNull() && Type->isRecordType()) {
     // the allocation occurs, we can't apply that filter when performing
     // context-sensitive analysis. But, this only applies to storage locations,
     // since field access it not allowed to fail. In contrast, field *values*
     // don't need this allowance, since the API allows for uninitialized fields.
     auto Fields = Opts.ContextSensitiveOpts ? getObjectFields(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 &
 DataflowAnalysisContext::getStableStorageLocation(const VarDecl &D) {
   if (auto *Loc = getStorageLocation(D))
     return *Loc;
   auto &Loc = createStorageLocation(D.getType());
   setStorageLocation(D, Loc);

 
 PointerValue &
 DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
   auto CanonicalPointeeType =
       PointeeType.isNull() ? PointeeType : PointeeType.getCanonicalType();
   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;
 }
 
 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));
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
                                                    BoolValue &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
   // 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));
 }
 
 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));
 }
 
 bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
                                                    BoolValue &Val2) {
   llvm::DenseSet<BoolValue *> Constraints = {
-      &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
+      &arena().makeNot(arena().makeEquals(Val1, Val2))};
   return isUnsatisfiable(Constraints);
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
   auto ConstraintsIt = FlowConditionConstraints.find(&Token);
   if (ConstraintsIt == FlowConditionConstraints.end()) {
     Constraints.insert(&Token);
   } 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);
   if (DepsIt != FlowConditionDeps.end()) {
     for (AtomicBoolValue *DepToken : DepsIt->second) {
       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
-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};
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   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);
 }
 
 const ControlFlowContext *
 DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {
   // Canonicalize the key:
   F = F->getDefinition();
   if (F == nullptr)
if (Stmt *Body = F->getBody()) {
     return &Result.first->second;
   }
 
   return nullptr;
 }
 
 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-
   // based tools.
   if (Opts.Log == nullptr) {
     if (DataflowLog.getNumOccurrences() > 0) {
       LogOwner = Logger::textual(llvm::errs());
       this->Opts.Log = LogOwner.get();

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

for (const VarDecl *D : Vars) {
     auto &Loc = createStorageLocation(*D);
     setStorageLocation(*D, Loc);
     if (auto *Val = createValue(D->getType()))
       setValue(Loc, *Val);
   }
 }
 
 Environment::Environment(DataflowAnalysisContext &DACtx)
-    : DACtx(&DACtx), FlowConditionToken(&DACtx.makeFlowConditionToken()) {}
+    : DACtx(&DACtx),
+      FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
 
 Environment::Environment(const Environment &Other)
     : DACtx(Other.DACtx), CallStack(Other.CallStack),
       ReturnLoc(Other.ReturnLoc), ThisPointeeLoc(Other.ThisPointeeLoc),
       DeclToLoc(Other.DeclToLoc), ExprToLoc(Other.ExprToLoc),
       LocToVal(Other.LocToVal), MemberLocToStruct(Other.MemberLocToStruct),
       FlowConditionToken(&DACtx->forkFlowCondition(*Other.FlowConditionToken)) {
 }
if (ArgLoc == nullptr)
       continue;
 
     const VarDecl *Param = *ParamIt;
     auto &Loc = createStorageLocation(*Param);
     setStorageLocation(*Param, Loc);
 
     QualType ParamType = Param->getType();
     if (ParamType->isReferenceType()) {
-      auto &Val = create<ReferenceValue>(*ArgLoc);
+      auto &Val = arena().create<ReferenceValue>(*ArgLoc);
       setValue(Loc, Val);
     } else if (auto *ArgVal = getValue(*ArgLoc)) {
       setValue(Loc, *ArgVal);
     } else if (Value *Val = createValue(ParamType)) {
       setValue(Loc, *Val);
     }
   }
 }
if (Type->isBooleanType()) {
     return &makeAtomicBoolValue();
   }
 
   if (Type->isIntegerType()) {
     // FIXME: consider instead `return nullptr`, given that we do nothing useful
     // with integers, and so distinguishing them serves no purpose, but could
     // prevent convergence.
     CreatedValuesCount++;
-    return &create<IntegerValue>();
+    return &arena().create<IntegerValue>();
   }
 
   if (Type->isReferenceType() || Type->isPointerType()) {
     CreatedValuesCount++;
     QualType PointeeType = Type->getPointeeType();
     auto &PointeeLoc = createStorageLocation(PointeeType);
 
     if (Visited.insert(PointeeType.getCanonicalType()).second) {
       Value *PointeeVal = createValueUnlessSelfReferential(
           PointeeType, Visited, Depth, CreatedValuesCount);
       Visited.erase(PointeeType.getCanonicalType());
 
       if (PointeeVal != nullptr)
         setValue(PointeeLoc, *PointeeVal);
     }
 
     if (Type->isReferenceType())
-      return &create<ReferenceValue>(PointeeLoc);
+      return &arena().create<ReferenceValue>(PointeeLoc);
     else
-      return &create<PointerValue>(PointeeLoc);
+      return &arena().create<PointerValue>(PointeeLoc);
   }
 
   if (Type->isRecordType()) {
     CreatedValuesCount++;
     llvm::DenseMap<const ValueDecl *, Value *> FieldValues;
     for (const FieldDecl *Field : DACtx->getReferencedFields(Type)) {
       assert(Field != nullptr);
 
       QualType FieldType = Field->getType();
       if (Visited.contains(FieldType.getCanonicalType()))
         continue;
 
       Visited.insert(FieldType.getCanonicalType());
       if (auto *FieldValue = createValueUnlessSelfReferential(
               FieldType, Visited, Depth + 1, CreatedValuesCount))
         FieldValues.insert({Field, FieldValue});
       Visited.erase(FieldType.getCanonicalType());
     }
 
-    return &create<StructValue>(std::move(FieldValues));
+    return &arena().create<StructValue>(std::move(FieldValues));
   }
 
   return nullptr;
 }
 
 StorageLocation &Environment::skip(StorageLocation &Loc, SkipPast SP) const {
   switch (SP) {
   case SkipPast::None:

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

+//===- ArenaTest.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 "clang/Analysis/FlowSensitive/Arena.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+
+namespace clang::dataflow {
+namespace {
+
+class ArenaTest : public ::testing::Test {
+protected:
+  Arena A;
+};
+
+TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
+  auto &X = A.create<TopBoolValue>();
+  auto &Y = A.create<TopBoolValue>();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &XAndX = A.makeAnd(X, X);
+  EXPECT_EQ(&XAndX, &X);
+}
+
+TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  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.create<AtomicBoolValue>();
+  auto &XAndZ = A.makeAnd(X, Z);
+  EXPECT_NE(&XAndY1, &XAndZ);
+}
+
+TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &XOrX = A.makeOr(X, X);
+  EXPECT_EQ(&XOrX, &X);
+}
+
+TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &XOrY1 = A.makeOr(X, Y);
+  auto &XOrY2 = A.makeOr(X, Y);
+  EXPECT_EQ(&XOrY1, &XOrY2);
+
+  auto &YOrX = A.makeOr(Y, X);
+  EXPECT_EQ(&XOrY1, &YOrX);
+
+  auto &Z = A.create<AtomicBoolValue>();
+  auto &XOrZ = A.makeOr(X, Z);
+  EXPECT_NE(&XOrY1, &XOrZ);
+}
+
+TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &NotX1 = A.makeNot(X);
+  auto &NotX2 = A.makeNot(X);
+  EXPECT_EQ(&NotX1, &NotX2);
+
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &NotY = A.makeNot(Y);
+  EXPECT_NE(&NotX1, &NotY);
+}
+
+TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &XImpliesX = A.makeImplies(X, X);
+  EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
+}
+
+TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  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.create<AtomicBoolValue>();
+  auto &XImpliesZ = A.makeImplies(X, Z);
+  EXPECT_NE(&XImpliesY1, &XImpliesZ);
+}
+
+TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &XIffX = A.makeEquals(X, X);
+  EXPECT_EQ(&XIffX, &A.makeLiteral(true));
+}
+
+TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &XIffY1 = A.makeEquals(X, Y);
+  auto &XIffY2 = A.makeEquals(X, Y);
+  EXPECT_EQ(&XIffY1, &XIffY2);
+
+  auto &YIffX = A.makeEquals(Y, X);
+  EXPECT_EQ(&XIffY1, &YIffX);
+
+  auto &Z = A.create<AtomicBoolValue>();
+  auto &XIffZ = A.makeEquals(X, Z);
+  EXPECT_NE(&XIffY1, &XIffZ);
+}
+
+} // namespace
+} // namespace clang::dataflow

clang/unittests/Analysis/FlowSensitive/CMakeLists.txt

 set(LLVM_LINK_COMPONENTS
   FrontendOpenMP
   Support
   )
 
 add_clang_unittest(ClangAnalysisFlowSensitiveTests
+  ArenaTest.cpp
   CFGMatchSwitchTest.cpp
   ChromiumCheckModelTest.cpp
   DataflowAnalysisContextTest.cpp
   DataflowEnvironmentTest.cpp
   DebugSupportTest.cpp
   LoggerTest.cpp
   MapLatticeTest.cpp
   MatchSwitchTest.cpp

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

 namespace {
 
 using namespace clang;
 using namespace dataflow;
 
 class DataflowAnalysisContextTest : public ::testing::Test {
 protected:
   DataflowAnalysisContextTest()
-      : Context(std::make_unique<WatchedLiteralsSolver>()) {}
+      : Context(std::make_unique<WatchedLiteralsSolver>()), A(Context.arena()) {
+  }
 
   DataflowAnalysisContext Context;
+  Arena &A;
 };
 
-TEST_F(DataflowAnalysisContextTest,
-       CreateAtomicBoolValueReturnsDistinctValues) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  EXPECT_NE(&X, &Y);
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       CreateTopBoolValueReturnsDistinctValues) {
-  auto &X = Context.create<TopBoolValue>();
-  auto &Y = Context.create<TopBoolValue>();
-  EXPECT_NE(&X, &Y);
-}
-
 TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
-  auto &X = Context.create<TopBoolValue>();
-  auto &Y = Context.create<TopBoolValue>();
+  auto &X = A.create<TopBoolValue>();
+  auto &Y = A.create<TopBoolValue>();
   EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
 }
 
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &XAndX = Context.getOrCreateConjunction(X, X);
-  EXPECT_EQ(&XAndX, &X);
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &XAndY1 = Context.getOrCreateConjunction(X, Y);
-  auto &XAndY2 = Context.getOrCreateConjunction(X, Y);
-  EXPECT_EQ(&XAndY1, &XAndY2);
-
-  auto &YAndX = Context.getOrCreateConjunction(Y, X);
-  EXPECT_EQ(&XAndY1, &YAndX);
-
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &XAndZ = Context.getOrCreateConjunction(X, Z);
-  EXPECT_NE(&XAndY1, &XAndZ);
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &XOrX = Context.getOrCreateDisjunction(X, X);
-  EXPECT_EQ(&XOrX, &X);
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &XOrY1 = Context.getOrCreateDisjunction(X, Y);
-  auto &XOrY2 = Context.getOrCreateDisjunction(X, Y);
-  EXPECT_EQ(&XOrY1, &XOrY2);
-
-  auto &YOrX = Context.getOrCreateDisjunction(Y, X);
-  EXPECT_EQ(&XOrY1, &YOrX);
-
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &XOrZ = Context.getOrCreateDisjunction(X, Z);
-  EXPECT_NE(&XOrY1, &XOrZ);
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &NotX1 = Context.getOrCreateNegation(X);
-  auto &NotX2 = Context.getOrCreateNegation(X);
-  EXPECT_EQ(&NotX1, &NotX2);
-
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &NotY = Context.getOrCreateNegation(Y);
-  EXPECT_NE(&NotX1, &NotY);
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateImplicationReturnsTrueGivenSameArgs) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &XImpliesX = Context.getOrCreateImplication(X, X);
-  EXPECT_EQ(&XImpliesX, &Context.getBoolLiteralValue(true));
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &XImpliesY1 = Context.getOrCreateImplication(X, Y);
-  auto &XImpliesY2 = Context.getOrCreateImplication(X, Y);
-  EXPECT_EQ(&XImpliesY1, &XImpliesY2);
-
-  auto &YImpliesX = Context.getOrCreateImplication(Y, X);
-  EXPECT_NE(&XImpliesY1, &YImpliesX);
-
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &XImpliesZ = Context.getOrCreateImplication(X, Z);
-  EXPECT_NE(&XImpliesY1, &XImpliesZ);
-}
-
-TEST_F(DataflowAnalysisContextTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &XIffX = Context.getOrCreateIff(X, X);
-  EXPECT_EQ(&XIffX, &Context.getBoolLiteralValue(true));
-}
-
-TEST_F(DataflowAnalysisContextTest,
-       GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &XIffY1 = Context.getOrCreateIff(X, Y);
-  auto &XIffY2 = Context.getOrCreateIff(X, Y);
-  EXPECT_EQ(&XIffY1, &XIffY2);
-
-  auto &YIffX = Context.getOrCreateIff(Y, X);
-  EXPECT_EQ(&XIffY1, &YIffX);
-
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &XIffZ = Context.getOrCreateIff(X, Z);
-  EXPECT_NE(&XIffY1, &XIffZ);
-}
-
 TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
-  auto &FC = Context.makeFlowConditionToken();
-  auto &C = Context.create<AtomicBoolValue>();
+  auto &FC = A.makeFlowConditionToken();
+  auto &C = A.create<AtomicBoolValue>();
   EXPECT_FALSE(Context.flowConditionImplies(FC, C));
 }
 
 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
-  auto &FC = Context.makeFlowConditionToken();
-  auto &C = Context.create<AtomicBoolValue>();
+  auto &FC = A.makeFlowConditionToken();
+  auto &C = A.create<AtomicBoolValue>();
   Context.addFlowConditionConstraint(FC, C);
   EXPECT_TRUE(Context.flowConditionImplies(FC, C));
 }
 
 TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
-  auto &FC1 = Context.makeFlowConditionToken();
-  auto &C1 = Context.create<AtomicBoolValue>();
+  auto &FC1 = A.makeFlowConditionToken();
+  auto &C1 = A.create<AtomicBoolValue>();
   Context.addFlowConditionConstraint(FC1, C1);
 
   // Forked flow condition inherits the constraints of its parent flow
   // condition.
   auto &FC2 = Context.forkFlowCondition(FC1);
   EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
 
   // Adding a new constraint to the forked flow condition does not affect its
   // parent flow condition.
-  auto &C2 = Context.create<AtomicBoolValue>();
+  auto &C2 = A.create<AtomicBoolValue>();
   Context.addFlowConditionConstraint(FC2, C2);
   EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
   EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
 }
 
 TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
-  auto &C1 = Context.create<AtomicBoolValue>();
-  auto &C2 = Context.create<AtomicBoolValue>();
-  auto &C3 = Context.create<AtomicBoolValue>();
+  auto &C1 = A.create<AtomicBoolValue>();
+  auto &C2 = A.create<AtomicBoolValue>();
+  auto &C3 = A.create<AtomicBoolValue>();
 
-  auto &FC1 = Context.makeFlowConditionToken();
+  auto &FC1 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC1, C1);
   Context.addFlowConditionConstraint(FC1, C3);
 
-  auto &FC2 = Context.makeFlowConditionToken();
+  auto &FC2 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, C2);
   Context.addFlowConditionConstraint(FC2, C3);
 
   auto &FC3 = Context.joinFlowConditions(FC1, FC2);
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
 }
 
 TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
   // Fresh flow condition with empty/no constraints is always true.
-  auto &FC1 = Context.makeFlowConditionToken();
+  auto &FC1 = A.makeFlowConditionToken();
   EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
 
   // Literal `true` is always true.
-  auto &FC2 = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true));
+  auto &FC2 = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
 
   // Literal `false` is never true.
-  auto &FC3 = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false));
+  auto &FC3 = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC3, A.makeLiteral(false));
   EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
 
   // We can't prove that an arbitrary bool A is always true...
-  auto &C1 = Context.create<AtomicBoolValue>();
-  auto &FC4 = Context.makeFlowConditionToken();
+  auto &C1 = A.create<AtomicBoolValue>();
+  auto &FC4 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC4, C1);
   EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
 
   // ... but we can prove A || !A is true.
-  auto &FC5 = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(
-      FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1)));
+  auto &FC5 = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
 }
 
 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &Z = A.create<AtomicBoolValue>();
+  auto &True = A.makeLiteral(true);
+  auto &False = A.makeLiteral(false);
 
   // X == X
   EXPECT_TRUE(Context.equivalentBoolValues(X, X));
   // X != Y
   EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
 
   // !X != X
-  EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));
+  EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
   // !(!X) = X
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
 
   // (X || X) == X
-  EXPECT_TRUE(
-      Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
   // (X || Y) != X
-  EXPECT_FALSE(
-      Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));
+  EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
   // (X || True) == True
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      Context.getOrCreateDisjunction(X, True), True));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
   // (X || False) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      Context.getOrCreateDisjunction(X, False), X));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
 
   // (X && X) == X
-  EXPECT_TRUE(
-      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
   // (X && Y) != X
-  EXPECT_FALSE(
-      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X));
+  EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
   // (X && True) == X
-  EXPECT_TRUE(
-      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
   // (X && False) == False
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      Context.getOrCreateConjunction(X, False), False));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
 
   // (X || Y) == (Y || X)
-  EXPECT_TRUE(
-      Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y),
-                                   Context.getOrCreateDisjunction(Y, X)));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
   // (X && Y) == (Y && X)
-  EXPECT_TRUE(
-      Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y),
-                                   Context.getOrCreateConjunction(Y, X)));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
 
   // ((X || Y) || Z) == (X || (Y || Z))
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),
-      Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
+                                           A.makeOr(X, A.makeOr(Y, Z))));
   // ((X && Y) && Z) == (X && (Y && Z))
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),
-      Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
-}
-
-#if !defined(NDEBUG) && GTEST_HAS_DEATH_TEST
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsTrueUnchanged) {
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &Other = Context.create<AtomicBoolValue>();
-
-  // FC = True
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, True);
-
-  // `True` should never be substituted
-  EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&True, &Other}}),
-               "Do not substitute true/false boolean literals");
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsFalseUnchanged) {
-  auto &False = Context.getBoolLiteralValue(false);
-  auto &Other = Context.create<AtomicBoolValue>();
-
-  // FC = False
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, False);
-
-  // `False` should never be substituted
-  EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&False, &Other}}),
-               "Do not substitute true/false boolean literals");
-}
-#endif
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = X
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, X);
-
-  // If X is true, FC is true
-  auto &FCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
-
-  // If X is false, FC is false
-  auto &FC1WithXFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingNegation) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = !X
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));
-
-  // If X is true, FC is false
-  auto &FCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
-
-  // If X is false, FC is true
-  auto &FC1WithXFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingDisjunction) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = X || Y
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
-
-  // If X is true, FC is true
-  auto &FCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
-
-  // If X is false, FC is equivalent to Y
-  auto &FC1WithXFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingConjunction) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = X && Y
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
-
-  // If X is true, FC is equivalent to Y
-  auto &FCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
-
-  // If X is false, FC is false
-  auto &FCWithXFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingImplication) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = (X => Y)
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, Context.getOrCreateImplication(X, Y));
-
-  // If X is true, FC is equivalent to Y
-  auto &FCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
-
-  // If X is false, FC is true
-  auto &FC1WithXFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
-
-  // If Y is true, FC is true
-  auto &FCWithYTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, True));
-
-  // If Y is false, FC is equivalent to !X
-  auto &FCWithYFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,
-                                           Context.getOrCreateNegation(X)));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingBiconditional) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = (X <=> Y)
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, Context.getOrCreateIff(X, Y));
-
-  // If X is true, FC is equivalent to Y
-  auto &FCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
-
-  // If X is false, FC is equivalent to !Y
-  auto &FC1WithXFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse,
-                                           Context.getOrCreateNegation(Y)));
-
-  // If Y is true, FC is equivalent to X
-  auto &FCWithYTrue =
-      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, X));
-
-  // If Y is false, FC is equivalent to !X
-  auto &FCWithYFalse =
-      Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse,
-                                           Context.getOrCreateNegation(X)));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC = X && Y
-  auto &FC = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
-  // ForkedFC = FC && Z = X && Y && Z
-  auto &ForkedFC = Context.forkFlowCondition(FC);
-  Context.addFlowConditionConstraint(ForkedFC, Z);
-
-  // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
-  // to evaluating the conjunction of the remaining values
-  auto &ForkedFCWithZTrue =
-      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
-  auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
-      ForkedFC, {{&Y, &True}, {&Z, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
-
-  // If any of X,Y,Z is false, ForkedFC is false
-  auto &ForkedFCWithXFalse =
-      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
-  auto &ForkedFCWithYFalse =
-      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
-  auto &ForkedFCWithZFalse =
-      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
-  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
-  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
-}
-
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
-  auto &X = Context.create<AtomicBoolValue>();
-  auto &Y = Context.create<AtomicBoolValue>();
-  auto &Z = Context.create<AtomicBoolValue>();
-  auto &True = Context.getBoolLiteralValue(true);
-  auto &False = Context.getBoolLiteralValue(false);
-
-  // FC1 = X
-  auto &FC1 = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC1, X);
-  // FC2 = Y
-  auto &FC2 = Context.makeFlowConditionToken();
-  Context.addFlowConditionConstraint(FC2, Y);
-  // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
-  auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
-  Context.addFlowConditionConstraint(JoinedFC, Z);
-
-  // If any of X, Y is true, JoinedFC is equivalent to Z
-  auto &JoinedFCWithXTrue =
-      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
-  auto &JoinedFCWithYTrue =
-      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
-  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
-
-  // If Z is true, JoinedFC is equivalent to (X || Y)
-  auto &JoinedFCWithZTrue =
-      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
-
-  // If any of X, Y is false, JoinedFC is equivalent to the conjunction of the
-  // other value and Z
-  auto &JoinedFCWithXFalse =
-      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
-  auto &JoinedFCWithYFalse =
-      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
-  EXPECT_TRUE(Context.equivalentBoolValues(
-      JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
-
-  // If Z is false, JoinedFC is false
-  auto &JoinedFCWithZFalse =
-      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
-  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
+  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z),
+                                           A.makeAnd(X, A.makeAnd(Y, Z))));
 }
 
 } // namespace