[clang][dataflow] Add support for serialization and deserialization. (#152487)

Adds support for compact serialization of Formulas, and a corresponding
parse function. Extends Environment and AnalysisContext with necessary
functions for serializing and deserializing all formula-related parts of
the environment.

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

@@ -42,6 +42,18 @@ struct ContextSensitiveOptions {
   unsigned Depth = 2;
 };
 
+/// A simple representation of essential elements of the logical context used in
+/// environments. Designed for import/export for applications requiring
+/// serialization support.
+struct SimpleLogicalContext {
+  // Global invariant that applies for all definitions in the context.
+  const Formula *Invariant;
+  // Flow-condition tokens in the context.
+  llvm::DenseMap<Atom, const Formula *> TokenDefs;
+  // Dependencies between flow-condition definitions.
+  llvm::DenseMap<Atom, llvm::DenseSet<Atom>> TokenDeps;
+};
+
 /// Owns objects that encompass the state of a program and stores context that
 /// is used during dataflow analysis.
 class DataflowAnalysisContext {
@@ -140,6 +152,15 @@ public:
   /// Adds `Constraint` to the flow condition identified by `Token`.
   void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
 
+  /// Adds `Deps` to the dependencies of the flow condition identified by
+  /// `Token`. Intended for use in deserializing contexts. The formula alone
+  /// doesn't have enough information to indicate its deps.
+  void addFlowConditionDeps(Atom Token, const llvm::DenseSet<Atom> &Deps) {
+    // Avoid creating an entry for `Token` with an empty set.
+    if (!Deps.empty())
+      FlowConditionDeps[Token].insert(Deps.begin(), Deps.end());
+  }
+
   /// Creates a new flow condition with the same constraints as the flow
   /// condition identified by `Token` and returns its token.
   Atom forkFlowCondition(Atom Token);
@@ -207,6 +228,14 @@ public:
     return {};
   }
 
+  /// Export the logical-context portions of `AC`, limited to the given target
+  /// flow-condition tokens.
+  SimpleLogicalContext
+  exportLogicalContext(llvm::DenseSet<dataflow::Atom> TargetTokens) const;
+
+  /// Initializes this context's "logical" components with `LC`.
+  void initLogicalContext(SimpleLogicalContext LC);
+
 private:
   friend class Environment;
 
@@ -228,6 +257,11 @@ private:
   DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver,
                           Options Opts);
 
+  /// Computes the transitive closure of dependencies of (flow-condition)
+  /// `Tokens`. That is, the set of flow-condition tokens reachable from
+  /// `Tokens` in the dependency graph.
+  llvm::DenseSet<Atom> collectDependencies(llvm::DenseSet<Atom> Tokens) const;
+
   // Extends the set of modeled field declarations.
   void addModeledFields(const FieldSet &Fields);
 

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

@@ -157,10 +157,18 @@ public:
   };
 
   /// Creates an environment that uses `DACtx` to store objects that encompass
-  /// the state of a program.
+  /// the state of a program. `FlowConditionToken` sets the flow condition
+  /// associated with the environment. Generally, new environments should be
+  /// initialized with a fresh token, by using one of the other
+  /// constructors. This constructor is for specialized use, including
+  /// deserialization and delegation from other constructors.
+  Environment(DataflowAnalysisContext &DACtx, Atom FlowConditionToken)
+      : DACtx(&DACtx), FlowConditionToken(FlowConditionToken) {}
+
+  /// Creates an environment that uses `DACtx` to store objects that encompass
+  /// the state of a program. Populates a fresh atom as flow condition token.
   explicit Environment(DataflowAnalysisContext &DACtx)
-      : DACtx(&DACtx),
-        FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
+      : Environment(DACtx, DACtx.arena().makeFlowConditionToken()) {}
 
   /// Creates an environment that uses `DACtx` to store objects that encompass
   /// the state of a program, with `S` as the statement to analyze.

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

@@ -85,21 +85,17 @@ public:
   }
 
   using AtomNames = llvm::DenseMap<Atom, std::string>;
-  // Produce a stable human-readable representation of this formula.
-  // For example: (V3 | !(V1 & V2))
-  // If AtomNames is provided, these override the default V0, V1... names.
+  /// Produces a stable human-readable representation of this formula.
+  /// For example: (V3 | !(V1 & V2))
+  /// If AtomNames is provided, these override the default V0, V1... names.
   void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
 
-  // Allocate Formulas using Arena rather than calling this function directly.
+  /// Allocates Formulas using Arena rather than calling this function directly.
   static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
                                ArrayRef<const Formula *> Operands,
                                unsigned Value = 0);
 
-private:
-  Formula() = default;
-  Formula(const Formula &) = delete;
-  Formula &operator=(const Formula &) = delete;
-
+  /// Count of operands (sub-formulas) associated with Formulas of kind `K`.
   static unsigned numOperands(Kind K) {
     switch (K) {
     case AtomRef:
@@ -116,6 +112,11 @@ private:
     llvm_unreachable("Unhandled Formula::Kind enum");
   }
 
+private:
+  Formula() = default;
+  Formula(const Formula &) = delete;
+  Formula &operator=(const Formula &) = delete;
+
   Kind FormulaKind;
   // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
   unsigned Value;

clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h

@@ -0,0 +1,40 @@
+//=== FormulaSerialization.h - Formula De/Serialization support -*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_SERIALIZATION_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_SERIALIZATION_H
+
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseMapInfo.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <string>
+
+namespace clang::dataflow {
+
+/// Prints `F` to `OS` in a compact format, optimized for easy parsing
+/// (deserialization) rather than human use.
+void serializeFormula(const Formula &F, llvm::raw_ostream &OS);
+
+/// Parses `Str` to build a serialized Formula.
+/// @returns error on parse failure or if parsing does not fully consume `Str`.
+/// @param A used to construct the formula components.
+/// @param AtomMap maps serialized Atom identifiers (unsigned ints) to Atoms.
+///        This map is provided by the caller to enable consistency across
+///        multiple formulas in a single file.
+llvm::Expected<const Formula *>
+parseFormula(llvm::StringRef Str, Arena &A,
+             llvm::DenseMap<unsigned, Atom> &AtomMap);
+
+} // namespace clang::dataflow
+#endif

clang/lib/Analysis/FlowSensitive/CMakeLists.txt

@@ -6,6 +6,7 @@ add_clang_library(clangAnalysisFlowSensitive
   DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
   Formula.cpp
+  FormulaSerialization.cpp
   HTMLLogger.cpp
   Logger.cpp
   RecordOps.cpp

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

@@ -208,6 +208,24 @@ bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
   return isUnsatisfiable(std::move(Constraints));
 }
 
+llvm::DenseSet<Atom> DataflowAnalysisContext::collectDependencies(
+    llvm::DenseSet<Atom> Tokens) const {
+  // Use a worklist algorithm, with `Remaining` holding the worklist and
+  // `Tokens` tracking which atoms have already been added to the worklist.
+  std::vector<Atom> Remaining(Tokens.begin(), Tokens.end());
+  while (!Remaining.empty()) {
+    Atom CurrentToken = Remaining.back();
+    Remaining.pop_back();
+    if (auto DepsIt = FlowConditionDeps.find(CurrentToken);
+        DepsIt != FlowConditionDeps.end())
+      for (Atom A : DepsIt->second)
+        if (Tokens.insert(A).second)
+          Remaining.push_back(A);
+  }
+
+  return Tokens;
+}
+
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     Atom Token, llvm::SetVector<const Formula *> &Constraints) {
   llvm::DenseSet<Atom> AddedTokens;
@@ -224,6 +242,8 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
 
     auto ConstraintsIt = FlowConditionConstraints.find(Token);
     if (ConstraintsIt == FlowConditionConstraints.end()) {
+      // The flow condition is unconstrained. Just add the atom directly, which
+      // is equivalent to asserting it is true.
       Constraints.insert(&arena().makeAtomRef(Token));
     } else {
       // Bind flow condition token via `iff` to its set of constraints:
@@ -239,6 +259,65 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   }
 }
 
+static void getReferencedAtoms(const Formula &F,
+                               llvm::DenseSet<dataflow::Atom> &Refs) {
+  switch (F.kind()) {
+  case Formula::AtomRef:
+    Refs.insert(F.getAtom());
+    break;
+  case Formula::Literal:
+    break;
+  case Formula::Not:
+    getReferencedAtoms(*F.operands()[0], Refs);
+    break;
+  case Formula::And:
+  case Formula::Or:
+  case Formula::Implies:
+  case Formula::Equal:
+    ArrayRef<const Formula *> Operands = F.operands();
+    getReferencedAtoms(*Operands[0], Refs);
+    getReferencedAtoms(*Operands[1], Refs);
+    break;
+  }
+}
+
+SimpleLogicalContext DataflowAnalysisContext::exportLogicalContext(
+    llvm::DenseSet<dataflow::Atom> TargetTokens) const {
+  SimpleLogicalContext LC;
+
+  if (Invariant != nullptr) {
+    LC.Invariant = Invariant;
+    getReferencedAtoms(*Invariant, TargetTokens);
+  }
+
+  llvm::DenseSet<dataflow::Atom> Dependencies =
+      collectDependencies(std::move(TargetTokens));
+
+  for (dataflow::Atom Token : Dependencies) {
+    // Only process the token if it is constrained. Unconstrained tokens don't
+    // have dependencies.
+    const Formula *Constraints = FlowConditionConstraints.lookup(Token);
+    if (Constraints == nullptr)
+      continue;
+    LC.TokenDefs[Token] = Constraints;
+
+    if (auto DepsIt = FlowConditionDeps.find(Token);
+        DepsIt != FlowConditionDeps.end())
+      LC.TokenDeps[Token] = DepsIt->second;
+  }
+
+  return LC;
+}
+
+void DataflowAnalysisContext::initLogicalContext(SimpleLogicalContext LC) {
+  Invariant = LC.Invariant;
+  FlowConditionConstraints = std::move(LC.TokenDefs);
+  // TODO: The dependencies in `LC.TokenDeps` can be reconstructed from
+  // `LC.TokenDefs`. Give the caller the option to reconstruct, rather than
+  // providing them directly, to save caller space (memory/disk).
+  FlowConditionDeps = std::move(LC.TokenDeps);
+}
+
 static void printAtomList(const llvm::SmallVector<Atom> &Atoms,
                           llvm::raw_ostream &OS) {
   OS << "(";

clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp

@@ -0,0 +1,153 @@
+//===- FormulaSerialization.cpp ---------------------------------*- 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/FormulaSerialization.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/Error.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <cassert>
+
+namespace clang::dataflow {
+
+// Returns the leading indicator of operation formulas. `AtomRef` and `Literal`
+// are handled differently.
+static char compactSigil(Formula::Kind K) {
+  switch (K) {
+  case Formula::AtomRef:
+  case Formula::Literal:
+    // No sigil.
+    return '\0';
+  case Formula::Not:
+    return '!';
+  case Formula::And:
+    return '&';
+  case Formula::Or:
+    return '|';
+  case Formula::Implies:
+    return '>';
+  case Formula::Equal:
+    return '=';
+  }
+  llvm_unreachable("unhandled formula kind");
+}
+
+void serializeFormula(const Formula &F, llvm::raw_ostream &OS) {
+  switch (Formula::numOperands(F.kind())) {
+  case 0:
+    switch (F.kind()) {
+    case Formula::AtomRef:
+      OS << F.getAtom();
+      break;
+    case Formula::Literal:
+      OS << (F.literal() ? 'T' : 'F');
+      break;
+    default:
+      llvm_unreachable("unhandled formula kind");
+    }
+    break;
+  case 1:
+    OS << compactSigil(F.kind());
+    serializeFormula(*F.operands()[0], OS);
+    break;
+  case 2:
+    OS << compactSigil(F.kind());
+    serializeFormula(*F.operands()[0], OS);
+    serializeFormula(*F.operands()[1], OS);
+    break;
+  default:
+    llvm_unreachable("unhandled formula arity");
+  }
+}
+
+static llvm::Expected<const Formula *>
+parsePrefix(llvm::StringRef &Str, Arena &A,
+            llvm::DenseMap<unsigned, Atom> &AtomMap) {
+  if (Str.empty())
+    return llvm::createStringError(llvm::inconvertibleErrorCode(),
+                                   "unexpected end of input");
+
+  char Prefix = Str[0];
+  Str = Str.drop_front();
+
+  switch (Prefix) {
+  case 'T':
+    return &A.makeLiteral(true);
+  case 'F':
+    return &A.makeLiteral(false);
+  case 'V': {
+    unsigned AtomID;
+    if (Str.consumeInteger(10, AtomID))
+      return llvm::createStringError(llvm::inconvertibleErrorCode(),
+                                     "expected atom id");
+    auto [It, Inserted] = AtomMap.try_emplace(AtomID, Atom());
+    if (Inserted)
+      It->second = A.makeAtom();
+    return &A.makeAtomRef(It->second);
+  }
+  case '!': {
+    auto OperandOrErr = parsePrefix(Str, A, AtomMap);
+    if (!OperandOrErr)
+      return OperandOrErr.takeError();
+    return &A.makeNot(**OperandOrErr);
+  }
+  case '&':
+  case '|':
+  case '>':
+  case '=': {
+    auto LeftOrErr = parsePrefix(Str, A, AtomMap);
+    if (!LeftOrErr)
+      return LeftOrErr.takeError();
+
+    auto RightOrErr = parsePrefix(Str, A, AtomMap);
+    if (!RightOrErr)
+      return RightOrErr.takeError();
+
+    const Formula &LHS = **LeftOrErr;
+    const Formula &RHS = **RightOrErr;
+
+    switch (Prefix) {
+    case '&':
+      return &A.makeAnd(LHS, RHS);
+    case '|':
+      return &A.makeOr(LHS, RHS);
+    case '>':
+      return &A.makeImplies(LHS, RHS);
+    case '=':
+      return &A.makeEquals(LHS, RHS);
+    default:
+      llvm_unreachable("unexpected binary op");
+    }
+  }
+  default:
+    return llvm::createStringError(llvm::inconvertibleErrorCode(),
+                                   "unexpected prefix character: %c", Prefix);
+  }
+}
+
+llvm::Expected<const Formula *>
+parseFormula(llvm::StringRef Str, Arena &A,
+             llvm::DenseMap<unsigned, Atom> &AtomMap) {
+  size_t OriginalSize = Str.size();
+  llvm::Expected<const Formula *> F = parsePrefix(Str, A, AtomMap);
+  if (!F)
+    return F.takeError();
+  if (!Str.empty())
+    return llvm::createStringError(llvm::inconvertibleErrorCode(),
+                                   ("unexpected suffix of length: " +
+                                    llvm::Twine(Str.size() - OriginalSize))
+                                       .str());
+  return F;
+}
+
+} // namespace clang::dataflow

clang/unittests/Analysis/FlowSensitive/CMakeLists.txt

@@ -8,6 +8,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
   DataflowEnvironmentTest.cpp
   DebugSupportTest.cpp
   DeterminismTest.cpp
+  FormulaTest.cpp
   LoggerTest.cpp
   MapLatticeTest.cpp
   MatchSwitchTest.cpp

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

@@ -17,6 +17,9 @@ namespace {
 using namespace clang;
 using namespace dataflow;
 
+using ::testing::IsEmpty;
+using ::testing::UnorderedElementsAre;
+
 class DataflowAnalysisContextTest : public ::testing::Test {
 protected:
   DataflowAnalysisContextTest()
@@ -171,4 +174,97 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
                                          A.makeAnd(X, A.makeAnd(Y, Z))));
 }
 
+using ExportLogicalContextTest = DataflowAnalysisContextTest;
+
+TEST_F(ExportLogicalContextTest, EmptySet) {
+  EXPECT_THAT(Context.exportLogicalContext({}).TokenDefs, IsEmpty());
+}
+
+// Only constrainted tokens are included in the output.
+TEST_F(ExportLogicalContextTest, UnconstrainedIgnored) {
+  Atom FC1 = A.makeFlowConditionToken();
+  EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs, IsEmpty());
+}
+
+TEST_F(ExportLogicalContextTest, SingletonSet) {
+  Atom FC1 = A.makeFlowConditionToken();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
+  Context.addFlowConditionConstraint(FC1, C1);
+  EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(),
+              UnorderedElementsAre(FC1));
+}
+
+TEST_F(ExportLogicalContextTest, NoDependency) {
+  Atom FC1 = A.makeFlowConditionToken();
+  Atom FC2 = A.makeFlowConditionToken();
+  Atom FC3 = A.makeFlowConditionToken();
+  auto &C1 = A.makeAtomRef(A.makeAtom());
+  auto &C2 = A.makeAtomRef(A.makeAtom());
+  auto &C3 = A.makeAtomRef(A.makeAtom());
+
+  Context.addFlowConditionConstraint(FC1, C1);
+  Context.addFlowConditionConstraint(FC2, C2);
+  Context.addFlowConditionConstraint(FC3, C3);
+
+  // FCs are independent.
+  EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(),
+              UnorderedElementsAre(FC1));
+  EXPECT_THAT(Context.exportLogicalContext({FC2}).TokenDefs.keys(),
+              UnorderedElementsAre(FC2));
+  EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(),
+              UnorderedElementsAre(FC3));
+}
+
+TEST_F(ExportLogicalContextTest, SimpleDependencyChain) {
+  Atom FC1 = A.makeFlowConditionToken();
+  const Formula &C = A.makeAtomRef(A.makeAtom());
+  Context.addFlowConditionConstraint(FC1, C);
+  Atom FC2 = Context.forkFlowCondition(FC1);
+  Atom FC3 = Context.forkFlowCondition(FC2);
+
+  EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(),
+              UnorderedElementsAre(FC1, FC2, FC3));
+}
+
+TEST_F(ExportLogicalContextTest, DependencyTree) {
+  Atom FC1 = A.makeFlowConditionToken();
+  const Formula &C = A.makeAtomRef(A.makeAtom());
+  Context.addFlowConditionConstraint(FC1, C);
+  Atom FC2 = Context.forkFlowCondition(FC1);
+  Atom FC3 = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC3, C);
+  Atom FC4 = Context.joinFlowConditions(FC2, FC3);
+
+  EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(),
+              UnorderedElementsAre(FC1, FC2, FC3, FC4));
+}
+
+TEST_F(ExportLogicalContextTest, DependencyDAG) {
+  Atom FC1 = A.makeFlowConditionToken();
+  const Formula &C = A.makeAtomRef(A.makeAtom());
+  Context.addFlowConditionConstraint(FC1, C);
+
+  Atom FC2 = Context.forkFlowCondition(FC1);
+  Atom FC3 = Context.forkFlowCondition(FC1);
+  Atom FC4 = Context.joinFlowConditions(FC2, FC3);
+
+  EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(),
+              UnorderedElementsAre(FC1, FC2, FC3, FC4));
+}
+
+TEST_F(ExportLogicalContextTest, MixedDependencies) {
+  Atom FC1 = A.makeFlowConditionToken();
+  const Formula &C = A.makeAtomRef(A.makeAtom());
+  Context.addFlowConditionConstraint(FC1, C);
+
+  Atom FC2 = Context.forkFlowCondition(FC1);
+  Atom FC3 = Context.forkFlowCondition(FC2);
+  (void)FC3; // unused, and we test below that it is not included.
+
+  Atom FC4 = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC4, C);
+
+  EXPECT_THAT(Context.exportLogicalContext({FC2, FC4}).TokenDefs.keys(),
+              UnorderedElementsAre(FC1, FC2, FC4));
+}
 } // namespace

clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp

@@ -0,0 +1,201 @@
+//===- unittests/Analysis/FlowSensitive/FormulaTest.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/Formula.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/FormulaSerialization.h"
+#include "llvm/Support/raw_ostream.h"
+#include "llvm/Testing/Support/Error.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+using ::llvm::Failed;
+using ::llvm::HasValue;
+using ::llvm::Succeeded;
+using ::testing::ElementsAre;
+using ::testing::IsEmpty;
+
+class SerializeFormulaTest : public ::testing::Test {
+protected:
+  Arena A;
+  std::string Out;
+  llvm::raw_string_ostream OS{Out};
+
+  const Formula &A1 = A.makeAtomRef(A.makeAtom());
+  const Formula &A2 = A.makeAtomRef(A.makeAtom());
+};
+
+TEST_F(SerializeFormulaTest, Atom) {
+  serializeFormula(A1, OS);
+  EXPECT_EQ(Out, "V0");
+  Out = "";
+
+  serializeFormula(A2, OS);
+  EXPECT_EQ(Out, "V1");
+}
+
+TEST_F(SerializeFormulaTest, LiteralTrue) {
+  serializeFormula(A.makeLiteral(true), OS);
+  EXPECT_EQ(Out, "T");
+}
+
+TEST_F(SerializeFormulaTest, LiteralFalse) {
+  serializeFormula(A.makeLiteral(false), OS);
+  EXPECT_EQ(Out, "F");
+}
+
+TEST_F(SerializeFormulaTest, Not) {
+  serializeFormula(A.makeNot(A1), OS);
+  EXPECT_EQ(Out, "!V0");
+}
+
+TEST_F(SerializeFormulaTest, Or) {
+  serializeFormula(A.makeOr(A1, A2), OS);
+  EXPECT_EQ(Out, "|V0V1");
+}
+
+TEST_F(SerializeFormulaTest, And) {
+  serializeFormula(A.makeAnd(A1, A2), OS);
+  EXPECT_EQ(Out, "&V0V1");
+}
+
+TEST_F(SerializeFormulaTest, Implies) {
+  serializeFormula(A.makeImplies(A1, A2), OS);
+  EXPECT_EQ(Out, ">V0V1");
+}
+
+TEST_F(SerializeFormulaTest, Equal) {
+  serializeFormula(A.makeEquals(A1, A2), OS);
+  EXPECT_EQ(Out, "=V0V1");
+}
+
+TEST_F(SerializeFormulaTest, NestedBinaryUnary) {
+  serializeFormula(A.makeEquals(A.makeOr(A1, A2), A2), OS);
+  EXPECT_EQ(Out, "=|V0V1V1");
+}
+
+TEST_F(SerializeFormulaTest, NestedBinaryBinary) {
+  serializeFormula(A.makeEquals(A.makeOr(A1, A2), A.makeAnd(A1, A2)), OS);
+  EXPECT_EQ(Out, "=|V0V1&V0V1");
+}
+
+class ParseFormulaTest : public ::testing::Test {
+protected:
+  void SetUp() override {
+    AtomMap[0] = Atom1;
+    AtomMap[1] = Atom2;
+  }
+
+  // Convenience wrapper for `testParseFormula`.
+  llvm::Expected<const Formula *> testParseFormula(llvm::StringRef Str) {
+    return parseFormula(Str, A, AtomMap);
+  }
+
+  Arena A;
+  std::string Out;
+  llvm::raw_string_ostream OS{Out};
+
+  Atom Atom1 = A.makeAtom();
+  Atom Atom2 = A.makeAtom();
+  const Formula &A1 = A.makeAtomRef(Atom1);
+  const Formula &A2 = A.makeAtomRef(Atom2);
+  llvm::DenseMap<unsigned, Atom> AtomMap;
+};
+
+TEST_F(ParseFormulaTest, Atom) {
+  EXPECT_THAT_EXPECTED(testParseFormula("V0"), HasValue(&A1));
+  EXPECT_THAT_EXPECTED(testParseFormula("V1"), HasValue(&A2));
+}
+
+TEST_F(ParseFormulaTest, LiteralTrue) {
+  EXPECT_THAT_EXPECTED(testParseFormula("T"), HasValue(&A.makeLiteral(true)));
+}
+
+TEST_F(ParseFormulaTest, LiteralFalse) {
+  EXPECT_THAT_EXPECTED(testParseFormula("F"), HasValue(&A.makeLiteral(false)));
+}
+
+TEST_F(ParseFormulaTest, Not) {
+  EXPECT_THAT_EXPECTED(testParseFormula("!V0"), HasValue(&A.makeNot(A1)));
+}
+
+TEST_F(ParseFormulaTest, Or) {
+  EXPECT_THAT_EXPECTED(testParseFormula("|V0V1"), HasValue(&A.makeOr(A1, A2)));
+}
+
+TEST_F(ParseFormulaTest, And) {
+  EXPECT_THAT_EXPECTED(testParseFormula("&V0V1"), HasValue(&A.makeAnd(A1, A2)));
+}
+
+TEST_F(ParseFormulaTest, OutOfNumericOrder) {
+  EXPECT_THAT_EXPECTED(testParseFormula("&V1V0"), HasValue(&A.makeAnd(A2, A1)));
+}
+
+TEST_F(ParseFormulaTest, Implies) {
+  EXPECT_THAT_EXPECTED(testParseFormula(">V0V1"),
+                       HasValue(&A.makeImplies(A1, A2)));
+}
+
+TEST_F(ParseFormulaTest, Equal) {
+  EXPECT_THAT_EXPECTED(testParseFormula("=V0V1"),
+                       HasValue(&A.makeEquals(A1, A2)));
+}
+
+TEST_F(ParseFormulaTest, NestedBinaryUnary) {
+  EXPECT_THAT_EXPECTED(testParseFormula("=|V0V1V1"),
+                       HasValue(&A.makeEquals(A.makeOr(A1, A2), A2)));
+}
+
+TEST_F(ParseFormulaTest, NestedBinaryBinary) {
+  EXPECT_THAT_EXPECTED(
+      testParseFormula("=|V0V1&V0V1"),
+      HasValue(&A.makeEquals(A.makeOr(A1, A2), A.makeAnd(A1, A2))));
+}
+
+// Verifies that parsing generates fresh atoms, if they are not already in the
+// map.
+TEST_F(ParseFormulaTest, GeneratesAtoms) {
+  llvm::DenseMap<unsigned, Atom> FreshAtomMap;
+  ASSERT_THAT_EXPECTED(parseFormula("=V0V1", A, FreshAtomMap), Succeeded());
+  // The map contains two, unique elements.
+  ASSERT_EQ(FreshAtomMap.size(), 2U);
+  EXPECT_NE(FreshAtomMap[0], FreshAtomMap[1]);
+}
+
+TEST_F(ParseFormulaTest, MalformedFormulaFails) {
+  // Arbitrary string.
+  EXPECT_THAT_EXPECTED(testParseFormula("Hello"), Failed());
+  // Empty string.
+  EXPECT_THAT_EXPECTED(testParseFormula(""), Failed());
+  // Malformed atom.
+  EXPECT_THAT_EXPECTED(testParseFormula("Vabc"), Failed());
+  // Irrelevant suffix.
+  EXPECT_THAT_EXPECTED(testParseFormula("V0Hello"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("=V0V1Hello"), Failed());
+  // Sequence without operator.
+  EXPECT_THAT_EXPECTED(testParseFormula("TF"), Failed());
+  // Bad subformula.
+  EXPECT_THAT_EXPECTED(testParseFormula("!G"), Failed());
+  // Incomplete formulas.
+  EXPECT_THAT_EXPECTED(testParseFormula("V"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("&"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("|"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula(">"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("="), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("&V0"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("|V0"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula(">V0"), Failed());
+  EXPECT_THAT_EXPECTED(testParseFormula("=V0"), Failed());
+}
+
+} // namespace