[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.

Author: ymand

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 @@ class DataflowAnalysisContext {
   /// 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 @@ class DataflowAnalysisContext {
     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 @@ class DataflowAnalysisContext {
   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 @@ class Environment {
   };
 
   /// 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 @@ class alignas(const Formula *) Formula {
   }
 
   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 @@ class alignas(const Formula *) Formula {
     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 << "(";