Refactor preprocessing pass registration (#2468)

This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.

As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.

This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.

[0] https://llvm.org/docs/WritingAnLLVMPass.html

1 files changed, 85 insertions, 15 deletions

diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 30a2db579..44e9b4e6e 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -11,9 +11,9 @@
  **
  ** \brief The preprocessing pass registry
  **
- ** The preprocessing pass registry keeps track of all the instances of
- ** preprocessing passes. Upon creation, preprocessing passes are registered in
- ** the registry, which then takes ownership of them.
+ ** This file defines the classes PreprocessingPassRegistry, which keeps track
+ ** of the available preprocessing passes, and RegisterPass, which registers a
+ ** preprocessing pass with the registry.
  **/
 #include "cvc4_private.h"
 
@@ -29,32 +29,102 @@
 namespace CVC4 {
 namespace preprocessing {
 
+class PreprocessingPassContext;
+
+/**
+ * The PreprocessingPassRegistry keeps track of the available preprocessing
+ * passes and how to create instances of those passes. This class is intended
+ * to be used as a singleton and can be shared between threads (assuming that
+ * the memory allocator is thread-safe) as well as different solver instances.
+ */
 class PreprocessingPassRegistry {
  public:
   /**
-   *  Registers a pass with a unique name and takes ownership of it.
+   * Gets the single instance of this class.
    */
-  void registerPass(const std::string& ppName,
-                    std::unique_ptr<PreprocessingPass> preprocessingPass);
+  static PreprocessingPassRegistry& getInstance();
 
   /**
-   * Retrieves a pass with a given name from registry.
+   * Registers a pass. Do not call this directly, use the `RegisterPass` class
+   * instead.
+   *
+   * @param name The name of the preprocessing pass to register
+   * @param ctor A function that creates an instance of the pass given a
+   *             preprocessing pass context
    */
-  PreprocessingPass* getPass(const std::string& ppName);
+  void registerPassInfo(
+      const std::string& name,
+      std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor);
 
   /**
-   Clears all passes from the registry.
+   * Creates an instance of a pass.
+   *
+   * @param ppCtx The preprocessing pass context to pass to the preprocessing
+   *              pass constructor
+   * @param name The name of the pass to create an instance of
    */
-  void unregisterPasses();
+  PreprocessingPass* createPass(PreprocessingPassContext* ppCtx,
+                                const std::string& name);
 
- private:
-  bool hasPass(const std::string& ppName);
+  /**
+   * Returns a sorted list of available preprocessing passes.
+   */
+  std::vector<std::string> getAvailablePasses();
 
-  /* Stores all the registered preprocessing passes. */
-  std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>>
-      d_stringToPreprocessingPass;
+  /**
+   * Checks whether a pass with a given name is available.
+   *
+   * @param name The name of the pass to check for
+   */
+  bool hasPass(const std::string& name);
+
+ private:
+  /**
+   * Map of available preprocessing passes, mapping from preprocessing pass
+   * name to a function that constructs a corresponding instance.
+   */
+  std::unordered_map<
+      std::string,
+      std::function<PreprocessingPass*(PreprocessingPassContext*)> >
+      d_ppInfo;
 };  // class PreprocessingPassRegistry
 
+/**
+ * Class used to register a preprocessing pass. In the source file of a given
+ * pass, create a static instance of this class, e.g.:
+ *
+ * static RegisterPass<MyPass> X("my-pass");
+ *
+ * where `MyPass` is the class of your pass and "my-pass" is its name. This
+ * registers the pass with the `PreprocessingPassRegistry`.
+ */
+template <class T>
+class RegisterPass
+{
+ public:
+  /**
+   * Creates a new preprocessing pass registration.
+   *
+   * @param name The name that should be associated with the preprocessing pass
+   */
+  RegisterPass(const std::string& name)
+  {
+    PreprocessingPassRegistry::getInstance().registerPassInfo(name, callCtor);
+  }
+
+  /**
+   * This method is used by the `PreprocessingPassRegistry` to create a new
+   * instance of the preprocessing pass T.
+   *
+   * @param ppCtx The preprocessing pass context passed to the constructor of
+   *              the preprocessing pass
+   */
+  static PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
+  {
+    return new T(ppCtx);
+  }
+};  // class RegisterPass
+
 }  // namespace preprocessing
 }  // namespace CVC4