[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)

[sammccall]

Summary

This properly frees the Value hierarchy from managing boolean formulas.

We still distinguish AtomicBoolValue; this type is used in client code.
However we expect to convert such uses to BoolValue (where the
distinction is not needed) or Atom (where atomic identity is intended),
and then fold AtomicBoolValue into FormulaBoolValue.

We also distinguish TopBoolValue; this has distinct rules for
widen/join/equivalence, and top-ness is not represented in Formula.
It'd be nice to find a cleaner representation (e.g. the absence of a
formula), but no immediate plans.

For now, BoolValues with the same Formula are deduplicated. This doesn't
seem desirable, as Values are mutable by their creators (properties).
We can probably drop this for FormulaBoolValue immediately (not in this
patch, to isolate changes). For AtomicBoolValue we first need to update
clients to stop using value pointers for atom identity.

The data structures around flow conditions are updated:

• flow condition tokens are Atom, rather than AtomicBoolValue*
• conditions are Formula, rather than BoolValue

Most APIs were changed directly, some with many clients had a
new version added and the existing one deprecated.

The factories for BoolValues in Environment keep their existing
signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue)
and are not deprecated. These have very many clients and finding the
most ergonomic API & migration path still needs some thought.

[sammccall]

Here we start to see benefits: Value becomes less reliant on inheritance, flow conditions are no longer Values that can uselessly bear properties, atomic variables are numbered in order of creation, we'll soon be able to have distinct BoolValues with the same formula (but different properties).

I think I could separate the Value/Arena changes from the ones to use Atom/Formula in DAContext if you think it's useful (the drawback is some risk of ending up in merge hell...)

[mboehme]

Just some top-level comments to begin with.

In D153469#4439770, @sammccall wrote:

Here we start to see benefits: Value becomes less reliant on inheritance, flow conditions are no longer Values that can uselessly bear properties, atomic variables are numbered in order of creation, we'll soon be able to have distinct BoolValues with the same formula (but different properties).

I like where this is going. Specifically, I like that we will soon no longer be relying in BoolValue object identity and will be able to have different BoolValues with the same formula. I'm working on a similar change for StructValue, so I'm well aware of how problematic it is to share the same Value but then modify properties on it -- it seems like a potential source of really puzzling bugs.

I think I could separate the Value/Arena changes from the ones to use Atom/Formula in DAContext if you think it's useful (the drawback is some risk of ending up in merge hell...)

I don't think that's necessary -- this patch is large in terms of numbers of lines changed, but when you eliminate the mechanical changes, there's not too much going on.

[gribozavr2]

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

61

Per our offline conversation, do you still believe in this fixme?

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

132

146

[sammccall]

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

61

No, I'm no longer convinced "unsound" is true.

However, I do think there's something to be fixed: if we really believe in it, we should be interning other types of values too (or have a clear idea about why bools are special).

And I think I still lean towards removing it: it looks like a power-vs-complexity tradeoff in the Value concept, and I suspect the historical reason to intern values was to intern formulas, not because we needed the power.

Reworded the fixme to say we should decide and be more consistent - text doesn't take a position on which way we should decide.

[uabelho]

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

521

There are still uses of this method in-tree. I get the following error (and many more) when I compile trunk now with -Werror:

../../clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp:148:9: error: 'addToFlowCondition' is deprecated: Use Formula version instead [-Werror,-Wdeprecated-declarations]
    Env.addToFlowCondition(*Val);
        ^
../../clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h:532:3: note: 'addToFlowCondition' has been explicitly marked deprecated here
  LLVM_DEPRECATED("Use Formula version instead", "")
  ^
../include/llvm/Support/Compiler.h:155:50: note: expanded from macro 'LLVM_DEPRECATED'
#define LLVM_DEPRECATED(MSG, FIX) __attribute__((deprecated(MSG, FIX)))
                                                 ^
1 error generated.

[sammccall]

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

521

Sure, I plan to clean these up once this change sticks.

Do you think -Wdeprecated -Werror is a build config we should keep working at all times?
This would mean you we can't use deprecation to migrate internal callers over multiple patches, essentially

So building with -Wno-error=deprecated-declarations or so seems to make more sense to me, but I can't see anything written either way. (Nor buildbot mail)

[uabelho]

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

521

There are bots failing now at least:
https://lab.llvm.org/buildbot/#/builders/57
https://lab.llvm.org/buildbot/#/builders/214

I *think* deprecation is mainly used to let downstream adapt? And when deprecating stuff in-tree code is usually fixed at once?

[sammccall]

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

521

Fair enough, thanks for the bot links

I don't think expanding the scope of the change for now is a good idea.
9d5cfed2443aa294e67bea694d5aab02c40fa278 replaces [[deprecated]] with a comment.

[uabelho]

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

521

Thank you!

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

 #include "clang/Analysis/FlowSensitive/Formula.h"
 #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`.
+/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
 class Arena {
 public:
-  Arena()
-      : TrueVal(create<AtomicBoolValue>()),
-        FalseVal(create<AtomicBoolValue>()) {}
+  Arena() : True(makeAtom()), False(makeAtom()) {}
   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.
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);
+  /// Creates a BoolValue wrapping a particular formula.
+  ///
+  /// Passing in the same formula will result in the same BoolValue.
+  /// FIXME: This canonicalization isn't sound e.g. if we create two BoolValues
+  ///        with the same formula but attach different properties.
+  ///        Stop relying on pointer identity of BoolValues and remove it.
+  BoolValue &makeBoolValue(const Formula &);
+
+  /// Creates a fresh atom and wraps in in an AtomicBoolValue.
+  /// FIXME: For now, identical-address AtomicBoolValue <=> identical atom.
+  ///        Stop relying on pointer identity and remove this guarantee.
+  AtomicBoolValue &makeAtomValue() {
+    return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom())));
+  }
+
+  /// Creates a fresh Top boolean value.
+  TopBoolValue &makeTopValue() {
+    // No need for deduplicating: there's no way to create aliasing Tops.
+    return create<TopBoolValue>(makeAtomRef(makeAtom()));
+  }
 
   /// Returns a symbolic integer value that models an integer literal equal to
   /// `Value`. These literals are the same every time.
   /// Integer literals are not typed; the type is determined by the `Expr` that
   /// an integer literal is associated with.
   IntegerValue &makeIntLiteral(llvm::APInt Value);
 
-  /// 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;
+  // Factories for boolean formulas.
+  // Formulas are interned: passing the same arguments return the same result.
+  // For commutative operations like And/Or, interning ignores order.
+  // Simplifications are applied: makeOr(X, X) => X, etc.
+
+  /// Returns a formula for the conjunction of `LHS` and `RHS`.
+  const Formula &makeAnd(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for the disjunction of `LHS` and `RHS`.
+  const Formula &makeOr(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for the negation of `Val`.
+  const Formula &makeNot(const Formula &Val);
+
+  /// Returns a formula for `LHS => RHS`.
+  const Formula &makeImplies(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for `LHS <=> RHS`.
+  const Formula &makeEquals(const Formula &LHS, const Formula &RHS);
+
+  /// Returns a formula for the variable A.
+  const Formula &makeAtomRef(Atom A);
+
+  /// Returns a formula for a literal true/false.
+  const Formula &makeLiteral(bool Value) {
+    return makeAtomRef(Value ? True : False);
   }
 
+  /// Returns a new atomic boolean variable, distinct from any other.
+  Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
   /// Creates a fresh flow condition and returns a token that identifies it. The
   /// token can be used to perform various operations on the flow condition such
   /// as adding constraints to it, forking it, joining it with another flow
   /// condition, or checking implications.
-  AtomicBoolValue &makeFlowConditionToken() {
-    return create<AtomicBoolValue>();
-  }
-
-  /// Gets the boolean formula equivalent of a BoolValue.
-  /// Each unique Top values is translated to an Atom.
-  /// TODO: migrate to storing Formula directly in Values instead.
-  const Formula &getFormula(const BoolValue &);
-
-  /// Returns a new atomic boolean variable, distinct from any other.
-  Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+  Atom makeFlowConditionToken() { return makeAtom(); }
 
 private:
   llvm::BumpPtrAllocator Alloc;
 
   // 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 integer literals and
   // composite boolean values.
   llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
-  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;
+  using FormulaPair = std::pair<const Formula *, const Formula *>;
+  llvm::DenseMap<FormulaPair, const Formula *> Ands;
+  llvm::DenseMap<FormulaPair, const Formula *> Ors;
+  llvm::DenseMap<const Formula *, const Formula *> Nots;
+  llvm::DenseMap<FormulaPair, const Formula *> Implies;
+  llvm::DenseMap<FormulaPair, const Formula *> Equals;
+  llvm::DenseMap<Atom, const Formula *> AtomRefs;
 
-  llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+  llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
   unsigned NextAtom = 0;
 
-  AtomicBoolValue &TrueVal;
-  AtomicBoolValue &FalseVal;
+  Atom True, False;
 };
 
 } // namespace clang::dataflow
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H

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

public:
   }
 
   /// 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);
 
   /// Adds `Constraint` to the flow condition identified by `Token`.
-  void addFlowConditionConstraint(AtomicBoolValue &Token,
-                                  BoolValue &Constraint);
+  void addFlowConditionConstraint(Atom Token, const Formula &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);
+  Atom forkFlowCondition(Atom 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);
+  Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
 
   /// 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);
+  bool flowConditionImplies(Atom Token, const Formula &);
 
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` are always true.
-  bool flowConditionIsTautology(AtomicBoolValue &Token);
+  bool flowConditionIsTautology(Atom 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);
+  bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
 
-  LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
+  LLVM_DUMP_METHOD void dumpFlowCondition(Atom 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; }
 
private:
   /// context.
   llvm::DenseSet<const FieldDecl *> getReferencedFields(QualType Type);
 
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
-      AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
-      llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+      Atom Token, llvm::DenseSet<const Formula *> &Constraints,
+      llvm::DenseSet<Atom> &VisitedTokens);
 
   /// Returns the outcome of satisfiability checking on `Constraints`.
   /// Possible outcomes are:
   /// - `Satisfiable`: A satisfying assignment exists and is returned.
   /// - `Unsatisfiable`: A satisfying assignment does not exist.
   /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+  Solver::Result querySolver(llvm::DenseSet<const Formula *> Constraints);
 
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
-  bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
+  bool isUnsatisfiable(llvm::DenseSet<const Formula *> Constraints) {
     return querySolver(std::move(Constraints)).getStatus() ==
            Solver::Result::Status::Unsatisfiable;
   }
 
   std::unique_ptr<Solver> S;
   std::unique_ptr<Arena> A;
 
   // Maps from program declarations and statements to storage locations that are
private:
   // 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.
   //
   // Flow conditions depend on other flow conditions if they are created using
   // `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
   // dependencies is stored in the `FlowConditionDeps` map.
-  llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
-      FlowConditionDeps;
-  llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
+  llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
+  llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
 
   llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts;
 
   // Fields modeled by environments covered by this context.
   llvm::DenseSet<const FieldDecl *> ModeledFields;
 
   std::unique_ptr<Logger> LogOwner; // If created via flags.
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H

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

public:
   /// 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->arena().create<T>(std::forward<Args>(args)...);
+    return arena().create<T>(std::forward<Args>(args)...);
   }
 
   /// Returns a symbolic integer value that models an integer literal equal to
   /// `Value`
   IntegerValue &getIntLiteralValue(llvm::APInt Value) const {
-    return DACtx->arena().makeIntLiteral(Value);
+    return arena().makeIntLiteral(Value);
   }
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`
   AtomicBoolValue &getBoolLiteralValue(bool Value) const {
-    return DACtx->arena().makeLiteral(Value);
+    return cast<AtomicBoolValue>(
+        arena().makeBoolValue(arena().makeLiteral(Value)));
   }
 
   /// Returns an atomic boolean value.
   BoolValue &makeAtomicBoolValue() const {
-    return DACtx->arena().create<AtomicBoolValue>();
+    return arena().makeAtomValue();
   }
 
   /// Returns a unique instance of boolean Top.
   BoolValue &makeTopBoolValue() const {
-    return DACtx->arena().create<TopBoolValue>();
+    return arena().makeTopValue();
   }
 
   /// 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->arena().makeAnd(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeAnd(LHS.formula(), RHS.formula()));
   }
 
   /// 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->arena().makeOr(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeOr(LHS.formula(), RHS.formula()));
   }
 
   /// 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->arena().makeNot(Val);
+    return arena().makeBoolValue(arena().makeNot(Val.formula()));
   }
 
   /// 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->arena().makeImplies(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeImplies(LHS.formula(), RHS.formula()));
   }
 
   /// 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->arena().makeEquals(LHS, RHS);
+    return arena().makeBoolValue(
+        arena().makeEquals(LHS.formula(), RHS.formula()));
   }
 
   /// Returns the token that identifies the flow condition of the environment.
-  AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
+  Atom getFlowConditionToken() const { return FlowConditionToken; }
 
   /// Adds `Val` to the set of clauses that constitute the flow condition.
+  void addToFlowCondition(const Formula &);
+  LLVM_DEPRECATED("Use Formula version instead", "")
   void addToFlowCondition(BoolValue &Val);
 
   /// Returns true if and only if the clauses that constitute the flow condition
   /// imply that `Val` is true.
+  bool flowConditionImplies(const Formula &) const;
+  LLVM_DEPRECATED("Use Formula version instead", "")
   bool flowConditionImplies(BoolValue &Val) const;
 
   /// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
   /// returns null.
   const DeclContext *getDeclCtx() const { return CallStack.back(); }
 
   /// Returns the function currently being analyzed, or null if the code being
   /// analyzed isn't part of a function.
   const FunctionDecl *getCurrentFunc() const {
     return dyn_cast<FunctionDecl>(getDeclCtx());
   }
 
   /// Returns whether this `Environment` can be extended to analyze the given
   /// `Callee` (i.e. if `pushCall` can be used), with recursion disallowed and a
   /// given `MaxDepth`.
   bool canDescend(unsigned MaxDepth, const DeclContext *Callee) const;
 
   /// Returns the `DataflowAnalysisContext` used by the environment.
   DataflowAnalysisContext &getDataflowAnalysisContext() const { return *DACtx; }
 
+  Arena &arena() const { return DACtx->arena(); }
+
   LLVM_DUMP_METHOD void dump() const;
   LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;
 
 private:
   /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
   /// return null.
   ///
   /// Recursively initializes storage locations and values until it sees a
private:
   llvm::DenseMap<const StorageLocation *, Value *> LocToVal;
 
   // Maps locations of struct members to symbolic values of the structs that own
   // them and the decls of the struct members.
   llvm::DenseMap<const StorageLocation *,
                  std::pair<StructValue *, const ValueDecl *>>
       MemberLocToStruct;
 
-  AtomicBoolValue *FlowConditionToken;
+  Atom FlowConditionToken;
 };
 
 /// Returns the storage location for the implicit object of a
 /// `CXXMemberCallExpr`, or null if none is defined in the environment.
 /// Dereferences the pointer if the member call expression was written using
 /// `->`.
 AggregateStorageLocation *
 getImplicitObjectLocation(const CXXMemberCallExpr &MCE, const Environment &Env);

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

 // during dataflow analysis.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H
 
 #include "clang/AST/Decl.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringMap.h"
 #include "llvm/ADT/StringRef.h"
-#include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <utility>
 
 namespace clang {
 namespace dataflow {
 
 /// Base class for all values computed by abstract interpretation.
 ///
 /// Don't use `Value` instances by value. All `Value` instances are allocated
 /// and owned by `DataflowAnalysisContext`.
 class Value {
 public:
   enum class Kind {
     Integer,
     Reference,
     Pointer,
     Struct,
 
-    // Synthetic boolean values are either atomic values or logical connectives.
+    // TODO: Top values should not be need to be type-specific.
     TopBool,
     AtomicBool,
-    Conjunction,
-    Disjunction,
-    Negation,
-    Implication,
-    Biconditional,
+    FormulaBool,
   };
 
   explicit Value(Kind ValKind) : ValKind(ValKind) {}
 
   // Non-copyable because addresses of values are used as their identities
   // throughout framework and user code. The framework is responsible for
   // construction and destruction of values.
   Value(const Value &) = delete;

 ///   compute deep equality of `Value` at said location.
 /// * TopBoolValue -- both are `TopBoolValue`s.
 ///
 /// Otherwise, falls back to pointer equality.
 bool areEquivalentValues(const Value &Val1, const Value &Val2);
 
 /// Models a boolean.
 class BoolValue : public Value {
+  const Formula *F;
+
 public:
-  explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
+  explicit BoolValue(Kind ValueKind, const Formula &F)
+      : Value(ValueKind), F(&F) {}
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::TopBool ||
            Val->getKind() == Kind::AtomicBool ||
-           Val->getKind() == Kind::Conjunction ||
-           Val->getKind() == Kind::Disjunction ||
-           Val->getKind() == Kind::Negation ||
-           Val->getKind() == Kind::Implication ||
-           Val->getKind() == Kind::Biconditional;
+           Val->getKind() == Kind::FormulaBool;
   }
+
+  const Formula &formula() const { return *F; }
 };
 
-/// Models the trivially true formula, which is Top in the lattice of boolean
-/// formulas.
+/// A TopBoolValue represents a boolean that is explicitly unconstrained.
+///
+/// This is equivalent to an AtomicBoolValue that does not appear anywhere
+/// else in a system of formula.
+/// Knowing the value is unconstrained is useful when e.g. reasoning about
+/// convergence.
 class TopBoolValue final : public BoolValue {
 public:
-  TopBoolValue() : BoolValue(Kind::TopBool) {}
+  TopBoolValue(const Formula &F) : BoolValue(Kind::TopBool, F) {
+    assert(F.kind() == Formula::AtomRef);
+  }
 
   static bool classof(const Value *Val) {
     return Val->getKind() == Kind::TopBool;
   }
+
+  Atom atom() const { return formula().atom(); }
 };
 
 /// Models an atomic boolean.
+///
+/// FIXME: Merge this class into FormulaBoolValue.
+///        When we want to specify atom identity, use Atom.
 class AtomicBoolValue : public BoolValue {
 public:
-  explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::AtomicBool;
-  }
-};
-
-/// Models a boolean conjunction.
-// FIXME: Consider representing binary and unary boolean operations similar
-// to how they are represented in the AST. This might become more pressing
-// when such operations need to be added for other data types.
-class ConjunctionValue : public BoolValue {
-public:
-  explicit ConjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Conjunction), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Conjunction;
-  }
-
-  /// Returns the left sub-value of the conjunction.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the conjunction.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
-};
-
-/// Models a boolean disjunction.
-class DisjunctionValue : public BoolValue {
-public:
-  explicit DisjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Disjunction), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Disjunction;
+  explicit AtomicBoolValue(const Formula &F) : BoolValue(Kind::AtomicBool, F) {
+    assert(F.kind() == Formula::AtomRef);
   }
 
-  /// Returns the left sub-value of the disjunction.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the disjunction.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
-};
-
-/// Models a boolean negation.
-class NegationValue : public BoolValue {
-public:
-  explicit NegationValue(BoolValue &SubVal)
-      : BoolValue(Kind::Negation), SubVal(SubVal) {}
-
   static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Negation;
+    return Val->getKind() == Kind::AtomicBool;
   }
 
-  /// Returns the sub-value of the negation.
-  BoolValue &getSubVal() const { return SubVal; }
-
-private:
-  BoolValue &SubVal;
+  Atom atom() const { return formula().atom(); }
 };
 
-/// Models a boolean implication.
-///
-/// Equivalent to `!LHS v RHS`.
-class ImplicationValue : public BoolValue {
+/// Models a compound boolean formula.
+class FormulaBoolValue : public BoolValue {
 public:
-  explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
-  static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Implication;
+  explicit FormulaBoolValue(const Formula &F)
+      : BoolValue(Kind::FormulaBool, F) {
+    assert(F.kind() != Formula::AtomRef && "For now, use AtomicBoolValue");
   }
 
-  /// Returns the left sub-value of the implication.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the implication.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
-};
-
-/// Models a boolean biconditional.
-///
-/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`.
-class BiconditionalValue : public BoolValue {
-public:
-  explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
-      : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal),
-        RightSubVal(RightSubVal) {}
-
   static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::Biconditional;
+    return Val->getKind() == Kind::FormulaBool;
   }
-
-  /// Returns the left sub-value of the biconditional.
-  BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
-  /// Returns the right sub-value of the biconditional.
-  BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
-  BoolValue &LeftSubVal;
-  BoolValue &RightSubVal;
 };
 
 /// Models an integer.
 class IntegerValue : public Value {
 public:
   explicit IntegerValue() : Value(Kind::Integer) {}
 
   static bool classof(const Value *Val) {

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"
+#include "clang/Analysis/FlowSensitive/Value.h"
 
 namespace clang::dataflow {
 
-static std::pair<BoolValue *, BoolValue *>
-makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+static std::pair<const Formula *, const Formula *>
+canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
-  if (&RHS < &LHS)
+  if (&RHS < &LHS) // FIXME: use a deterministic order instead
     std::swap(Res.first, Res.second);
   return Res;
 }
 
-BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeAtomRef(Atom A) {
+  auto [It, Inserted] = AtomRefs.try_emplace(A);
+  if (Inserted)
+    It->second =
+        &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+  return *It->second;
+}
+
+const Formula &Arena::makeAnd(const Formula &LHS, const Formula &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;
+  auto [It, Inserted] =
+      Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+  return *It->second;
 }
 
-BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeOr(const Formula &LHS, const Formula &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;
+  auto [It, Inserted] =
+      Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+  return *It->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;
+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;
 }
 
-BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeImplies(const Formula &LHS, const Formula &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;
+  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;
 }
 
-BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeEquals(const Formula &LHS, const Formula &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;
+  auto [It, Inserted] =
+      Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+  if (Inserted)
+    It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+  return *It->second;
 }
 
 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
   auto [It, Inserted] = IntegerLiterals.try_emplace(Value, nullptr);
 
   if (Inserted)
     It->second = &create<IntegerValue>();
   return *It->second;
 }
 
-const Formula &Arena::getFormula(const BoolValue &B) {
-  auto It = ValToFormula.find(&B);
-  if (It != ValToFormula.end())
-    return *It->second;
-  Formula &F = [&]() -> Formula & {
-    switch (B.getKind()) {
-    case Value::Kind::Integer:
-    case Value::Kind::Reference:
-    case Value::Kind::Pointer:
-    case Value::Kind::Struct:
-      llvm_unreachable("not a boolean");
-    case Value::Kind::TopBool:
-    case Value::Kind::AtomicBool:
-      // TODO: assign atom numbers on creation rather than in getFormula(), so
-      // they will be deterministic and maybe even meaningful.
-      return Formula::create(Alloc, Formula::AtomRef, {},
-                             static_cast<unsigned>(makeAtom()));
-    case Value::Kind::Conjunction:
-      return Formula::create(
-          Alloc, Formula::And,
-          {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
-           &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
-    case Value::Kind::Disjunction:
-      return Formula::create(
-          Alloc, Formula::Or,
-          {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
-           &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
-    case Value::Kind::Negation:
-      return Formula::create(Alloc, Formula::Not,
-                             {&getFormula(cast<NegationValue>(B).getSubVal())});
-    case Value::Kind::Implication:
-      return Formula::create(
-          Alloc, Formula::Implies,
-          {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
-           &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
-    case Value::Kind::Biconditional:
-      return Formula::create(
-          Alloc, Formula::Equal,
-          {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
-           &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
-    }
-  }();
-  ValToFormula.try_emplace(&B, &F);
-  return F;
+BoolValue &Arena::makeBoolValue(const Formula &F) {
+  auto [It, Inserted] = FormulaValues.try_emplace(&F);
+  if (Inserted)
+    It->second = (F.kind() == Formula::AtomRef)
+                     ? (BoolValue *)&create<AtomicBoolValue>(F)
+                     : &create<FormulaBoolValue>(F);
+  return *It->second;
 }
 
 } // namespace clang::dataflow

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
   if (Res.second) {
     auto &PointeeLoc = createStorageLocation(CanonicalPointeeType);
     Res.first->second = &arena().create<PointerValue>(PointeeLoc);
   }
   return *Res.first->second;
 }
 
 void DataflowAnalysisContext::addFlowConditionConstraint(
-    AtomicBoolValue &Token, BoolValue &Constraint) {
-  auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
+    Atom Token, const Formula &Constraint) {
+  auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
   if (!Res.second) {
     Res.first->second =
         &arena().makeAnd(*Res.first->second, Constraint);
   }
 }
 
-AtomicBoolValue &
-DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
-  auto &ForkToken = arena().makeFlowConditionToken();
-  FlowConditionDeps[&ForkToken].insert(&Token);
-  addFlowConditionConstraint(ForkToken, Token);
+Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) {
+  Atom ForkToken = arena().makeFlowConditionToken();
+  FlowConditionDeps[ForkToken].insert(Token);
+  addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
   return ForkToken;
 }
 
-AtomicBoolValue &
-DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
-                                            AtomicBoolValue &SecondToken) {
-  auto &Token = arena().makeFlowConditionToken();
-  FlowConditionDeps[&Token].insert(&FirstToken);
-  FlowConditionDeps[&Token].insert(&SecondToken);
-  addFlowConditionConstraint(
-      Token, arena().makeOr(FirstToken, SecondToken));
+Atom 
+DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
+                                            Atom SecondToken) {
+  Atom Token = arena().makeFlowConditionToken();
+  FlowConditionDeps[Token].insert(FirstToken);
+  FlowConditionDeps[Token].insert(SecondToken);
+  addFlowConditionConstraint(Token,
+                             arena().makeOr(arena().makeAtomRef(FirstToken),
+                                            arena().makeAtomRef(SecondToken)));
   return Token;
 }
 
-Solver::Result
-DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
+Solver::Result DataflowAnalysisContext::querySolver(
+    llvm::DenseSet<const Formula *> Constraints) {
   Constraints.insert(&arena().makeLiteral(true));
-  Constraints.insert(
-      &arena().makeNot(arena().makeLiteral(false)));
-  llvm::DenseSet<const Formula *> Formulas;
-  for (const BoolValue * Constraint : Constraints)
-    Formulas.insert(&arena().getFormula(*Constraint));
-  return S->solve(Formulas);
+  Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
+  return S->solve(Constraints);
 }
 
-bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
-                                                   BoolValue &Val) {
+bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
+                                                   const Formula &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
-  llvm::DenseSet<BoolValue *> Constraints = {&Token,
+  llvm::DenseSet<const Formula *> Constraints = {&arena().makeAtomRef(Token),
                                                  &arena().makeNot(Val)};
-  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
+bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
-  llvm::DenseSet<BoolValue *> Constraints = {
-      &arena().makeNot(Token)};
-  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  llvm::DenseSet<const Formula *> Constraints = {
+      &arena().makeNot(arena().makeAtomRef(Token))};
+  llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
-                                                   BoolValue &Val2) {
-  llvm::DenseSet<BoolValue *> Constraints = {
+bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
+                                                 const Formula &Val2) {
+  llvm::DenseSet<const Formula *> Constraints = {
       &arena().makeNot(arena().makeEquals(Val1, Val2))};
-  return isUnsatisfiable(Constraints);
+  return isUnsatisfiable(std::move(Constraints));
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
-    AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
-    llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
-  auto Res = VisitedTokens.insert(&Token);
+    Atom Token, llvm::DenseSet<const Formula *> &Constraints,
+    llvm::DenseSet<Atom> &VisitedTokens) {
+  auto Res = VisitedTokens.insert(Token);
   if (!Res.second)
     return;
 
-  auto ConstraintsIt = FlowConditionConstraints.find(&Token);
+  auto ConstraintsIt = FlowConditionConstraints.find(Token);
   if (ConstraintsIt == FlowConditionConstraints.end()) {
-    Constraints.insert(&Token);
+    Constraints.insert(&arena().makeAtomRef(Token));
   } else {
     // Bind flow condition token via `iff` to its set of constraints:
     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
-    Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
+    Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
+                                           *ConstraintsIt->second));
   }
 
-  auto DepsIt = FlowConditionDeps.find(&Token);
+  auto DepsIt = FlowConditionDeps.find(Token);
   if (DepsIt != FlowConditionDeps.end()) {
-    for (AtomicBoolValue *DepToken : DepsIt->second) {
-      addTransitiveFlowConditionConstraints(*DepToken, Constraints,
+    for (Atom DepToken : DepsIt->second) {
+      addTransitiveFlowConditionConstraints(DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
-void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
+void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
                                                 llvm::raw_ostream &OS) {
-  // TODO: accumulate formulas directly instead
-  llvm::DenseSet<BoolValue *> Constraints = {&Token};
-  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+  llvm::DenseSet<const Formula *> Constraints = {&arena().makeAtomRef(Token)};
+  llvm::DenseSet<Atom> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
   // TODO: have formulas know about true/false directly instead
-  auto &True = arena().getFormula(arena().makeLiteral(true));
-  auto &False = arena().getFormula(arena().makeLiteral(false));
+  auto &True = arena().makeLiteral(true);
+  auto &False = arena().makeLiteral(false);
   auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
     if (&F == &True) {
       OS << "True";
       return true;
     }
     if (&F == &False) {
       OS << "False";
       return true;
     }
     return false;
   };
 
   std::vector<std::string> Lines;
   for (const auto *Constraint : Constraints) {
     Lines.emplace_back();
     llvm::raw_string_ostream LineOS(Lines.back());
-    arena().getFormula(*Constraint).print(LineOS, Delegate);
+    Constraint->print(LineOS, Delegate);
   }
   llvm::sort(Lines);
   for (const auto &Line : Lines)
     OS << Line << "\n";
 }
 
 const ControlFlowContext *
 DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

if (isa<BoolValue>(&Val1) && isa<BoolValue>(&Val2)) {
     // bool in the other.
     // For example:
     // ```
     // std::optional<bool> o;
     // int x;
     // if (o.has_value())
     //   x = o.value();
     // ```
-    auto *Expr1 = cast<BoolValue>(&Val1);
-    auto *Expr2 = cast<BoolValue>(&Val2);
-    auto &MergedVal = MergedEnv.makeAtomicBoolValue();
-    MergedEnv.addToFlowCondition(MergedEnv.makeOr(
-        MergedEnv.makeAnd(Env1.getFlowConditionToken(),
-                          MergedEnv.makeIff(MergedVal, *Expr1)),
-        MergedEnv.makeAnd(Env2.getFlowConditionToken(),
-                          MergedEnv.makeIff(MergedVal, *Expr2))));
-    return &MergedVal;
+    auto &Expr1 = cast<BoolValue>(Val1).formula();
+    auto &Expr2 = cast<BoolValue>(Val2).formula();
+    auto &A = MergedEnv.arena();
+    auto &MergedVal = A.makeAtomRef(A.makeAtom());
+    MergedEnv.addToFlowCondition(
+        A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
+                           A.makeEquals(MergedVal, Expr1)),
+                 A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
+                           A.makeEquals(MergedVal, Expr2))));
+    return &A.makeBoolValue(MergedVal);
   }
 
   // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
   // returns false to avoid storing unneeded values in `DACtx`.
   // FIXME: Creating the value based on the type alone creates misshapen values
   // for lvalues, since the type does not reflect the need for `ReferenceValue`.
   if (Value *MergedVal = MergedEnv.createValue(Type))
     if (Model.merge(Type, Val1, Env1, Val2, Env2, *MergedVal, MergedEnv))
if (getStorageLocation(*FD) != nullptr)
       continue;
     auto &Loc = createStorageLocation(FD->getType());
     setStorageLocation(*FD, Loc);
   }
 }
 
 Environment::Environment(DataflowAnalysisContext &DACtx)
     : DACtx(&DACtx),
-      FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
+      FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
 
 Environment::Environment(const Environment &Other)
     : DACtx(Other.DACtx), CallStack(Other.CallStack),
       ReturnVal(Other.ReturnVal), ReturnLoc(Other.ReturnLoc),
       ThisPointeeLoc(Other.ThisPointeeLoc), DeclToLoc(Other.DeclToLoc),
       ExprToLoc(Other.ExprToLoc), LocToVal(Other.LocToVal),
       MemberLocToStruct(Other.MemberLocToStruct),
-      FlowConditionToken(&DACtx->forkFlowCondition(*Other.FlowConditionToken)) {
-}
+      FlowConditionToken(DACtx->forkFlowCondition(Other.FlowConditionToken)) {}
 
 Environment &Environment::operator=(const Environment &Other) {
   Environment Copy(Other);
   *this = std::move(Copy);
   return *this;
 }
 
 Environment::Environment(DataflowAnalysisContext &DACtx,
LatticeJoinEffect Environment::join(const Environment &Other,
   JoinedEnv.MemberLocToStruct =
       intersectDenseMaps(MemberLocToStruct, Other.MemberLocToStruct);
   if (MemberLocToStruct.size() != JoinedEnv.MemberLocToStruct.size())
     Effect = LatticeJoinEffect::Changed;
 
   // FIXME: set `Effect` as needed.
   // FIXME: update join to detect backedges and simplify the flow condition
   // accordingly.
-  JoinedEnv.FlowConditionToken = &DACtx->joinFlowConditions(
-      *FlowConditionToken, *Other.FlowConditionToken);
+  JoinedEnv.FlowConditionToken =
+      DACtx->joinFlowConditions(FlowConditionToken, Other.FlowConditionToken);
 
   for (auto &Entry : LocToVal) {
     const StorageLocation *Loc = Entry.first;
     assert(Loc != nullptr);
 
     Value *Val = Entry.second;
     assert(Val != nullptr);
 
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 &DACtx->arena().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 &DACtx->arena().create<ReferenceValue>(PointeeLoc);
+      return &arena().create<ReferenceValue>(PointeeLoc);
     else
-      return &DACtx->arena().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 &DACtx->arena().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:
     return Loc;
   case SkipPast::Reference:
     // References cannot be chained so we only need to skip past one level of
     // indirection.
     if (auto *Val = dyn_cast_or_null<ReferenceValue>(getValue(Loc)))
       return Val->getReferentLoc();
     return Loc;
   }
   llvm_unreachable("bad SkipPast kind");
 }
 
 const StorageLocation &Environment::skip(const StorageLocation &Loc,
                                          SkipPast SP) const {
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
+void Environment::addToFlowCondition(const Formula &Val) {
+  DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
+}
 void Environment::addToFlowCondition(BoolValue &Val) {
-  DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
+  addToFlowCondition(Val.formula());
 }
 
+bool Environment::flowConditionImplies(const Formula &Val) const {
+  return DACtx->flowConditionImplies(FlowConditionToken, Val);
+}
 bool Environment::flowConditionImplies(BoolValue &Val) const {
-  return DACtx->flowConditionImplies(*FlowConditionToken, Val);
+  return flowConditionImplies(Val.formula());
 }
 
 void Environment::dump(raw_ostream &OS) const {
   // FIXME: add printing for remaining fields and allow caller to decide what
   // fields are printed.
   OS << "DeclToLoc:\n";
   for (auto [D, L] : DeclToLoc)
     OS << "  [" << D->getNameAsString() << ", " << L << "]\n";
 
   OS << "ExprToLoc:\n";
   for (auto [E, L] : ExprToLoc)
     OS << "  [" << E << ", " << L << "]\n";
 
   OS << "LocToVal:\n";
   for (auto [L, V] : LocToVal) {
     OS << "  [" << L << ", " << V << ": " << *V << "]\n";
   }
 
   OS << "FlowConditionToken:\n";
-  DACtx->dumpFlowCondition(*FlowConditionToken, OS);
+  DACtx->dumpFlowCondition(FlowConditionToken, OS);
 }
 
 void Environment::dump() const {
   dump(llvm::dbgs());
 }
 
 AggregateStorageLocation *
 getImplicitObjectLocation(const CXXMemberCallExpr &MCE,

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

llvm::StringRef debugString(Value::Kind Kind) {
   case Value::Kind::Pointer:
     return "Pointer";
   case Value::Kind::Struct:
     return "Struct";
   case Value::Kind::AtomicBool:
     return "AtomicBool";
   case Value::Kind::TopBool:
     return "TopBool";
-  case Value::Kind::Conjunction:
-    return "Conjunction";
-  case Value::Kind::Disjunction:
-    return "Disjunction";
-  case Value::Kind::Negation:
-    return "Negation";
-  case Value::Kind::Implication:
-    return "Implication";
-  case Value::Kind::Biconditional:
-    return "Biconditional";
+  case Value::Kind::FormulaBool:
+    return "FormulaBool";
   }
   llvm_unreachable("Unhandled value kind");
 }
 
 llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
                               Solver::Result::Assignment Assignment) {
   switch (Assignment) {
   case Solver::Result::Assignment::AssignedFalse:

clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp

case Value::Kind::Pointer:
       JOS.attributeObject(
           "pointee", [&] { dump(cast<PointerValue>(V).getPointeeLoc()); });
       break;
     case Value::Kind::Struct:
       for (const auto &Child : cast<StructValue>(V).children())
         JOS.attributeObject("f:" + Child.first->getNameAsString(),
                             [&] { dump(*Child.second); });
       break;
-    case Value::Kind::Disjunction: {
-      auto &VV = cast<DisjunctionValue>(V);
-      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
-      break;
-    }
-    case Value::Kind::Conjunction: {
-      auto &VV = cast<ConjunctionValue>(V);
-      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
-      break;
-    }
-    case Value::Kind::Negation: {
-      auto &VV = cast<NegationValue>(V);
-      JOS.attributeObject("not", [&] { dump(VV.getSubVal()); });
-      break;
-    }
-    case Value::Kind::Implication: {
-      auto &VV = cast<ImplicationValue>(V);
-      JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); });
-      break;
-    }
-    case Value::Kind::Biconditional: {
-      auto &VV = cast<BiconditionalValue>(V);
-      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
-      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+    case Value::Kind::FormulaBool: {
+      auto &VV = cast<FormulaBoolValue>(V);
+      JOS.attribute("formula", llvm::to_string(VV.formula()));
       break;
     }
     }
 
     for (const auto& Prop : V.properties())
       JOS.attributeObject(("p:" + Prop.first()).str(),
                           [&] { dump(*Prop.second); });
 
     // Running the SAT solver is expensive, but knowing which booleans are
     // guaranteed true/false here is valuable and hard to determine by hand.
     if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
-      JOS.attribute("truth", Env.flowConditionImplies(*B) ? "true"
-                             : Env.flowConditionImplies(Env.makeNot(*B))
-                                 ? "false"
-                                 : "unknown");
+      JOS.attribute(
+          "truth", Env.flowConditionImplies(B->formula()) ? "true"
+                   : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
     }
   }
   void dump(const StorageLocation &L) {
     JOS.attribute("location", llvm::to_string(&L));
     if (!Visited.insert(&L).second)
       return;
 
     JOS.attribute("type", L.getType().getAsString());

clang/lib/Analysis/FlowSensitive/Transfer.cpp

static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
 
   if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
     if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
       return Env.makeIff(*LHSBool, *RHSBool);
 
   return Env.makeAtomicBoolValue();
 }
 
-// Functionally updates `V` such that any instances of `TopBool` are replaced
-// with fresh atomic bools. Note: This implementation assumes that `B` is a
-// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
-// present in the original .
-static BoolValue &unpackValue(BoolValue &V, Environment &Env);
-
-template <typename Derived, typename M>
-BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
-  auto &V = *cast<Derived>(&B);
-  BoolValue &Left = V.getLeftSubValue();
-  BoolValue &Right = V.getRightSubValue();
-  BoolValue &ULeft = unpackValue(Left, Env);
-  BoolValue &URight = unpackValue(Right, Env);
-
-  if (&ULeft == &Left && &URight == &Right)
-    return V;
-
-  return (Env.*build)(ULeft, URight);
-}
-
 static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
-  switch (V.getKind()) {
-  case Value::Kind::Integer:
-  case Value::Kind::Reference:
-  case Value::Kind::Pointer:
-  case Value::Kind::Struct:
-    llvm_unreachable("BoolValue cannot have any of these kinds.");
-
-  case Value::Kind::AtomicBool:
-    return V;
-
-  case Value::Kind::TopBool:
-    // Unpack `TopBool` into a fresh atomic bool.
-    return Env.makeAtomicBoolValue();
-
-  case Value::Kind::Negation: {
-    auto &N = *cast<NegationValue>(&V);
-    BoolValue &Sub = N.getSubVal();
-    BoolValue &USub = unpackValue(Sub, Env);
-
-    if (&USub == &Sub)
-      return V;
-    return Env.makeNot(USub);
-  }
-  case Value::Kind::Conjunction:
-    return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
-                                                   &Environment::makeAnd);
-  case Value::Kind::Disjunction:
-    return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
-                                                   &Environment::makeOr);
-  case Value::Kind::Implication:
-    return unpackBinaryBoolValue<ImplicationValue>(
-        Env, V, &Environment::makeImplication);
-  case Value::Kind::Biconditional:
-    return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
-                                                     &Environment::makeIff);
+  if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
+    auto &A = Env.getDataflowAnalysisContext().arena();
+    return A.makeBoolValue(A.makeAtomRef(Top->atom()));
   }
-  llvm_unreachable("All reachable cases in switch return");
+  return V;
 }
 
 // Unpacks the value (if any) associated with `E` and updates `E` to the new
 // value, if any unpacking occured. Also, does the lvalue-to-rvalue conversion,
 // by skipping past the reference.
 static Value *maybeUnpackLValueExpr(const Expr &E, Environment &Env) {
   auto *Loc = Env.getStorageLocationStrict(E);
   if (Loc == nullptr)

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

 namespace {
 
 class ArenaTest : public ::testing::Test {
 protected:
   Arena A;
 };
 
 TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomValue();
+  auto &Y = A.makeAtomValue();
   EXPECT_NE(&X, &Y);
 }
 
 TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
-  auto &X = A.create<TopBoolValue>();
-  auto &Y = A.create<TopBoolValue>();
+  auto &X = A.makeTopValue();
+  auto &Y = A.makeTopValue();
   EXPECT_NE(&X, &Y);
 }
 
 TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   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 &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XAndY1 = A.makeAnd(X, Y);
   auto &XAndY2 = A.makeAnd(X, Y);
   EXPECT_EQ(&XAndY1, &XAndY2);
 
   auto &YAndX = A.makeAnd(Y, X);
   EXPECT_EQ(&XAndY1, &YAndX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XAndZ = A.makeAnd(X, Z);
   EXPECT_NE(&XAndY1, &XAndZ);
 }
 
 TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   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 &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XOrY1 = A.makeOr(X, Y);
   auto &XOrY2 = A.makeOr(X, Y);
   EXPECT_EQ(&XOrY1, &XOrY2);
 
   auto &YOrX = A.makeOr(Y, X);
   EXPECT_EQ(&XOrY1, &YOrX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XOrZ = A.makeOr(X, Z);
   EXPECT_NE(&XOrY1, &XOrZ);
 }
 
 TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &NotX1 = A.makeNot(X);
   auto &NotX2 = A.makeNot(X);
   EXPECT_EQ(&NotX1, &NotX2);
-
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &NotY = A.makeNot(Y);
   EXPECT_NE(&NotX1, &NotY);
 }
 
 TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &XImpliesX = A.makeImplies(X, X);
   EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
 }
 
 TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XImpliesY1 = A.makeImplies(X, Y);
   auto &XImpliesY2 = A.makeImplies(X, Y);
   EXPECT_EQ(&XImpliesY1, &XImpliesY2);
 
   auto &YImpliesX = A.makeImplies(Y, X);
   EXPECT_NE(&XImpliesY1, &YImpliesX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XImpliesZ = A.makeImplies(X, Z);
   EXPECT_NE(&XImpliesY1, &XImpliesZ);
 }
 
 TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
-  auto &X = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
   auto &XIffX = A.makeEquals(X, X);
   EXPECT_EQ(&XIffX, &A.makeLiteral(true));
 }
 
 TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
   auto &XIffY1 = A.makeEquals(X, Y);
   auto &XIffY2 = A.makeEquals(X, Y);
   EXPECT_EQ(&XIffY1, &XIffY2);
 
   auto &YIffX = A.makeEquals(Y, X);
   EXPECT_EQ(&XIffY1, &YIffX);
 
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &XIffZ = A.makeEquals(X, Z);
   EXPECT_NE(&XIffY1, &XIffZ);
 }
 
-TEST_F(ArenaTest, ValueToFormula) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
-  auto &XIffY = A.makeEquals(X, Y);
-  auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
-  auto &Implies = A.makeImplies(XIffY, XOrNotY);
-
-  EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
-            "((V0 = V1) => (V0 | !V1))");
-}
-
-TEST_F(ArenaTest, ValueToFormulaCached) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
-  auto &XIffY = A.makeEquals(X, Y);
-
-  auto &Formula1 = A.getFormula(XIffY);
-  auto &Formula2 = A.getFormula(XIffY);
-  EXPECT_EQ(&Formula1, &Formula2);
+TEST_F(ArenaTest, Interning) {
+  Atom X = A.makeAtom();
+  Atom Y = A.makeAtom();
+  const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));
+  const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
+  EXPECT_EQ(&F1, &F2);
+  BoolValue &B1 = A.makeBoolValue(F1);
+  BoolValue &B2 = A.makeBoolValue(F2);
+  EXPECT_EQ(&B1, &B2);
+  EXPECT_EQ(&B1.formula(), &F1);
 }
 
 } // namespace
 } // namespace clang::dataflow

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

DataflowAnalysisContextTest()
       : Context(std::make_unique<WatchedLiteralsSolver>()), A(Context.arena()) {
   }
 
   DataflowAnalysisContext Context;
   Arena &A;
 };
 
 TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
-  auto &X = A.create<TopBoolValue>();
-  auto &Y = A.create<TopBoolValue>();
-  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+  auto &X = A.makeTopValue();
+  auto &Y = A.makeTopValue();
+  EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
 }
 
 TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
-  auto &FC = A.makeFlowConditionToken();
-  auto &C = A.create<AtomicBoolValue>();
+  Atom FC = A.makeFlowConditionToken();
+  auto &C = A.makeAtomRef(A.makeAtom());
   EXPECT_FALSE(Context.flowConditionImplies(FC, C));
 }
 
 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
-  auto &FC = A.makeFlowConditionToken();
-  auto &C = A.create<AtomicBoolValue>();
+  Atom FC = A.makeFlowConditionToken();
+  auto &C = A.makeAtomRef(A.makeAtom());
   Context.addFlowConditionConstraint(FC, C);
   EXPECT_TRUE(Context.flowConditionImplies(FC, C));
 }
 
 TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
-  auto &FC1 = A.makeFlowConditionToken();
-  auto &C1 = A.create<AtomicBoolValue>();
+  Atom FC1 = A.makeFlowConditionToken();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
   Context.addFlowConditionConstraint(FC1, C1);
 
   // Forked flow condition inherits the constraints of its parent flow
   // condition.
-  auto &FC2 = Context.forkFlowCondition(FC1);
+  Atom 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 = A.create<AtomicBoolValue>();
+  auto &C2 = A.makeAtomRef(A.makeAtom());
   Context.addFlowConditionConstraint(FC2, C2);
   EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
   EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
 }
 
 TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
-  auto &C1 = A.create<AtomicBoolValue>();
-  auto &C2 = A.create<AtomicBoolValue>();
-  auto &C3 = A.create<AtomicBoolValue>();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
+  auto &C2 = A.makeAtomRef(A.makeAtom());
+  auto &C3 = A.makeAtomRef(A.makeAtom());
 
-  auto &FC1 = A.makeFlowConditionToken();
+  Atom FC1 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC1, C1);
   Context.addFlowConditionConstraint(FC1, C3);
 
-  auto &FC2 = A.makeFlowConditionToken();
+  Atom FC2 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, C2);
   Context.addFlowConditionConstraint(FC2, C3);
 
-  auto &FC3 = Context.joinFlowConditions(FC1, FC2);
+  Atom 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 = A.makeFlowConditionToken();
+  Atom FC1 = A.makeFlowConditionToken();
   EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
 
   // Literal `true` is always true.
-  auto &FC2 = A.makeFlowConditionToken();
+  Atom FC2 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
 
   // Literal `false` is never true.
-  auto &FC3 = A.makeFlowConditionToken();
+  Atom 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 = A.create<AtomicBoolValue>();
-  auto &FC4 = A.makeFlowConditionToken();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
+  Atom FC4 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC4, C1);
   EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
 
   // ... but we can prove A || !A is true.
-  auto &FC5 = A.makeFlowConditionToken();
+  Atom FC5 = A.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
 }
 
 TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
-  auto &X = A.create<AtomicBoolValue>();
-  auto &Y = A.create<AtomicBoolValue>();
-  auto &Z = A.create<AtomicBoolValue>();
+  auto &X = A.makeAtomRef(A.makeAtom());
+  auto &Y = A.makeAtomRef(A.makeAtom());
+  auto &Z = A.makeAtomRef(A.makeAtom());
   auto &True = A.makeLiteral(true);
   auto &False = A.makeLiteral(false);
 
   // X == X
-  EXPECT_TRUE(Context.equivalentBoolValues(X, X));
+  EXPECT_TRUE(Context.equivalentFormulas(X, X));
   // X != Y
-  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+  EXPECT_FALSE(Context.equivalentFormulas(X, Y));
 
   // !X != X
-  EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
+  EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
   // !(!X) = X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
 
   // (X || X) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
   // (X || Y) != X
-  EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
+  EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
   // (X || True) == True
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
   // (X || False) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
 
   // (X && X) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
   // (X && Y) != X
-  EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
+  EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
   // (X && True) == X
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
   // (X && False) == False
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
 
   // (X || Y) == (Y || X)
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
   // (X && Y) == (Y && X)
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
 
   // ((X || Y) || Z) == (X || (Y || Z))
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
-                                           A.makeOr(X, A.makeOr(Y, Z))));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
   // ((X && Y) && Z) == (X && (Y && Z))
-  EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z),
-                                           A.makeAnd(X, A.makeAnd(Y, Z))));
+  EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),
 }
 
 } // namespace

clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

runDataflow(
           const auto *QuxVal =
               dyn_cast_or_null<BoolValue>(Env.getValue(*QuxDecl));
           ASSERT_THAT(QuxVal, NotNull());
 
           const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz");
           ASSERT_THAT(BazDecl, NotNull());
 
           const auto *BazVal =
-              dyn_cast_or_null<ConjunctionValue>(Env.getValue(*BazDecl));
+              dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
           ASSERT_THAT(BazVal, NotNull());
-          EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal);
-
-          const auto *BazRightSubValVal =
-              cast<DisjunctionValue>(&BazVal->getRightSubValue());
-          EXPECT_EQ(&BazRightSubValVal->getLeftSubValue(), BarVal);
-          EXPECT_EQ(&BazRightSubValVal->getRightSubValue(), QuxVal);
+          auto &A = Env.arena();
+          EXPECT_EQ(&BazVal->formula(),
+                    &A.makeAnd(FooVal->formula(),
+                               A.makeOr(BarVal->formula(), QuxVal->formula())));
         });
   }
 
   {
     std::string Code = R"(
     void target(bool Foo, bool Bar, bool Qux) {
       bool Baz = (Foo && Qux) || (Bar);
       // [[p]]
runDataflow(
           const auto *QuxVal =
               dyn_cast_or_null<BoolValue>(Env.getValue(*QuxDecl));
           ASSERT_THAT(QuxVal, NotNull());
 
           const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz");
           ASSERT_THAT(BazDecl, NotNull());
 
           const auto *BazVal =
-              dyn_cast_or_null<DisjunctionValue>(Env.getValue(*BazDecl));
+              dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
           ASSERT_THAT(BazVal, NotNull());
-
-          const auto *BazLeftSubValVal =
-              cast<ConjunctionValue>(&BazVal->getLeftSubValue());
-          EXPECT_EQ(&BazLeftSubValVal->getLeftSubValue(), FooVal);
-          EXPECT_EQ(&BazLeftSubValVal->getRightSubValue(), QuxVal);
-
-          EXPECT_EQ(&BazVal->getRightSubValue(), BarVal);
+          auto &A = Env.arena();
+          EXPECT_EQ(&BazVal->formula(),
+                    &A.makeOr(A.makeAnd(FooVal->formula(), QuxVal->formula()),
+                              BarVal->formula()));
         });
   }
 
   {
     std::string Code = R"(
       void target(bool A, bool B, bool C, bool D) {
         bool Foo = ((A && B) && C) && D;
         // [[p]]
runDataflow(
 
           const auto *DVal = dyn_cast_or_null<BoolValue>(Env.getValue(*DDecl));
           ASSERT_THAT(DVal, NotNull());
 
           const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
           ASSERT_THAT(FooDecl, NotNull());
 
           const auto *FooVal =
-              dyn_cast_or_null<ConjunctionValue>(Env.getValue(*FooDecl));
+              dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
           ASSERT_THAT(FooVal, NotNull());
-
-          const auto &FooLeftSubVal =
-              cast<ConjunctionValue>(FooVal->getLeftSubValue());
-          const auto &FooLeftLeftSubVal =
-              cast<ConjunctionValue>(FooLeftSubVal.getLeftSubValue());
-          EXPECT_EQ(&FooLeftLeftSubVal.getLeftSubValue(), AVal);
-          EXPECT_EQ(&FooLeftLeftSubVal.getRightSubValue(), BVal);
-          EXPECT_EQ(&FooLeftSubVal.getRightSubValue(), CVal);
-          EXPECT_EQ(&FooVal->getRightSubValue(), DVal);
+          auto &A = Env.arena();
+          EXPECT_EQ(
+              &FooVal->formula(),
+              &A.makeAnd(A.makeAnd(A.makeAnd(AVal->formula(), BVal->formula()),
+                                   CVal->formula()),
+                         DVal->formula()));
         });
   }
 }
 
 TEST(TransferTest, AssignFromBoolNegation) {
   std::string Code = R"(
     void target() {
       bool Foo = true;
runDataflow(
         const auto *FooVal =
             dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
         ASSERT_THAT(FooVal, NotNull());
 
         const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
         ASSERT_THAT(BarDecl, NotNull());
 
         const auto *BarVal =
-            dyn_cast_or_null<NegationValue>(Env.getValue(*BarDecl));
+            dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
         ASSERT_THAT(BarVal, NotNull());
-
-        EXPECT_EQ(&BarVal->getSubVal(), FooVal);
+        auto &A = Env.arena();
+        EXPECT_EQ(&BarVal->formula(), &A.makeNot(FooVal->formula()));
       });
 }
 
 TEST(TransferTest, BuiltinExpect) {
   std::string Code = R"(
     void target(long Foo) {
       long Bar = __builtin_expect(Foo, true);
       /*[[p]]*/

clang/unittests/Analysis/FlowSensitive/ValueTest.cpp

 //===- unittests/Analysis/FlowSensitive/ValueTest.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/Value.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 #include <memory>
 
 namespace {
 
 using namespace clang;
TEST(ValueTest, AliasedPointersEquivalent) {
   auto L = ScalarStorageLocation(QualType());
   PointerValue V1(L);
   PointerValue V2(L);
   EXPECT_TRUE(areEquivalentValues(V1, V2));
   EXPECT_TRUE(areEquivalentValues(V2, V1));
 }
 
 TEST(ValueTest, TopsEquivalent) {
-  TopBoolValue V1;
-  TopBoolValue V2;
+  Arena A;
+  TopBoolValue V1(A.makeAtomRef(Atom(0)));
+  TopBoolValue V2(A.makeAtomRef(Atom(1)));
   EXPECT_TRUE(areEquivalentValues(V1, V2));
   EXPECT_TRUE(areEquivalentValues(V2, V1));
 }
 
 TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
-  TopBoolValue Prop1;
-  TopBoolValue Prop2;
-  TopBoolValue V1;
-  TopBoolValue V2;
+  Arena A;
+  TopBoolValue Prop1(A.makeAtomRef(Atom(0)));
+  TopBoolValue Prop2(A.makeAtomRef(Atom(1)));
+  TopBoolValue V1(A.makeAtomRef(Atom(2)));
+  TopBoolValue V2(A.makeAtomRef(Atom(3)));
   V1.setProperty("foo", Prop1);
   V2.setProperty("bar", Prop2);
   EXPECT_TRUE(areEquivalentValues(V1, V2));
   EXPECT_TRUE(areEquivalentValues(V2, V1));
 }
 
 TEST(ValueTest, DifferentKindsNotEquivalent) {
+  Arena A;
   auto L = ScalarStorageLocation(QualType());
   ReferenceValue V1(L);
-  TopBoolValue V2;
+  TopBoolValue V2(A.makeAtomRef(Atom(0)));
   EXPECT_FALSE(areEquivalentValues(V1, V2));
   EXPECT_FALSE(areEquivalentValues(V2, V1));
 }
 
 TEST(ValueTest, NotAliasedReferencesNotEquivalent) {
   auto L1 = ScalarStorageLocation(QualType());
   ReferenceValue V1(L1);
   auto L2 = ScalarStorageLocation(QualType());