Merge pull request #41 from cvc5/cppCompilerPlugin

Note that the C++ compiler in its current state generates valid C++ code, but suffers crashes when executed.

This won't be actively maintained in the short term, as it only gave a 15% or so boost in performance anyways.

plugins/cpp_compiler/README.md

@@ -0,0 +1,26 @@
+# Compiling ALF signatures to C++
+
+For the purposes of optimizing proof checking times, the ALF checker supports compiling user signatures to C++, which can subsequently by compiled as part of the ALF checker.
+When invoked with the option `--gen-compile`, the ALF checker will generate C++ code corresponding to type checking, evaluation of terms and matching for programs for all definitions it reads.
+After incorporating this code by recompiling the checker, this code can be run via the command line option `--run-compile`.
+
+In detail, the recommended steps for compiling an ALF signature are:
+1. Run `alfc --gen-compile <signature>`. This will generate `compiled.out.cpp` in the current directory.
+2. Replacing the file `./src/compiled.cpp` with this file and recompile `alfc`.
+3. Run `alfc --run-compile <proof>`, where `<proof>` includes `<signature>`.
+
+Running with `--run-compile` leads to performance gains that depend on the signature, but are typically up to 50% faster.
+
+# Appendix
+
+## Command line options of alfc
+
+The ALF command line interface can be invoked by `alfc <option>* <file>` where `<option>` is one of the following:
+- `--gen-compile`: output the C++ code for all included signatures from the input file.
+- `--run-compile`: use the compiled C++ signatures whenever available.
+
+
+## Notes to get compiling
+
+- Add Compiler as a friend class of TypeChecker.
+- Add Executor as a friend class of State.

src/compiler.cpp → plugins/cpp_compiler/compiler.cpp

@@ -203,8 +203,12 @@ void Compiler::setLiteralTypeRule(Kind k, const Expr& t)
   d_init << "  d_tc.setLiteralTypeRule(Kind::" << k << ", _e" << id << ");" << std::endl;
 }
 
-void Compiler::includeFile(const Filepath& s)
+void Compiler::includeFile(const Filepath& s, bool isReference, const Expr& referenceNf)
 {
+  if (isReference)
+  {
+    ALFC_FATAL() << "Compiler::includeFile: cannot use reference when compiling";
+  }
   Assert (d_nscopes==0);
   d_init << "  d_state.markIncluded(\"" << s.getRawPath() << "\");" << std::endl;
   d_config << "  ss << std::setw(15) << \" \" << \"" << s.getRawPath()

src/compiler.h → plugins/cpp_compiler/compiler.h

@@ -146,7 +146,7 @@ class Compiler : public Plugin
   /** Pop scope */
   void popScope() override;
   /** include file, if not already done */
-  void includeFile(const Filepath& s) override;
+  void includeFile(const Filepath& s, bool isReference, const Expr& referenceNf) override;
   /** Set type rule for literal kind k to t */
   void setLiteralTypeRule(Kind k, const Expr& t) override;
   /** */

src/cmd_parser.cpp

@@ -568,10 +568,6 @@ bool CmdParser::parseNextCommand()
         {
           d_lex.parseError("Cannot use more than one reference");
         }
-        if (d_state.getOptions().d_compile)
-        {
-          d_lex.parseError("Cannot use reference when compiling");
-        }
       }
       if (d_state.getAssumptionLevel()>0)
       {

src/expr.h

@@ -17,7 +17,6 @@
 
 namespace alfc {
 
-class Compiler;
 class State;
 class ExprValue;
 class TypeChecker;

src/main.cpp

@@ -15,8 +15,6 @@
 #include "base/output.h"
 #include "parser.h"
 #include "state.h"
-#include "compiler.h"
-#include "executor.h"
 
 using namespace alfc;
 
@@ -37,15 +35,6 @@ int main( int argc, char* argv[] )
     {
       opts.d_binderFresh = true;
     }
-    else if (arg=="--gen-compile")
-    {
-      opts.d_compile = true;
-    }
-    else if (arg=="--run-compile")
-    {
-      opts.d_runCompile = true;
-      // TODO: warn if not compiled?
-    }
     else if (arg=="--no-parse-let")
     {
       opts.d_parseLet = false;
@@ -74,13 +63,12 @@ int main( int argc, char* argv[] )
     {
       std::stringstream out;
       out << "     --binder-fresh: binders generate fresh variables when parsed in proof files." << std::endl;
-      out << "      --gen-compile: output the C++ code for all included signatures from the input file." << std::endl;
       out << "             --help: displays this message." << std::endl;
       out << " --no-normalize-dec: do not treat decimal literals as syntax sugar for rational literals." << std::endl;
       out << " --no-normalize-hex: do not treat hexadecimal literals as syntax sugar for binary literals." << std::endl;
+      out << "     --no-parse-let: do not treat let as a builtin symbol for specifying terms having shared subterms." << std::endl;
       out << "     --no-print-let: do not letify the output of terms in error messages and trace messages." << std::endl;
       out << "--no-rule-sym-table: do not use a separate symbol table for proof rules and declared terms." << std::endl;
-      out << "      --run-compile: use the compiled C++ signatures whenever available." << std::endl;
       out << "      --show-config: displays the build information for this binary." << std::endl;
       out << "            --stats: enables detailed statistics." << std::endl;
       out << "           -t <tag>: enables the given trace tag (requires debug build)." << std::endl;
@@ -101,17 +89,6 @@ int main( int argc, char* argv[] )
       out << "no";
 #endif
       out << std::endl;
-      out << std::setw(w) << "compiled : ";
-      std::string cfiles = Executor::showCompiledFiles();
-      if (!cfiles.empty())
-      {
-        out << "yes" << std::endl;
-        out << cfiles;
-      }
-      else
-      {
-        out << "no" << std::endl;
-      }
       std::cout << out.str();
       return 0;
     }
@@ -159,17 +136,11 @@ int main( int argc, char* argv[] )
     }
   }
   State s(opts, stats);
-  std::unique_ptr<Compiler> d_compiler;
-  std::unique_ptr<Executor> d_executor;
-  if (opts.d_compile)
-  {
-    d_compiler.reset(new Compiler(s));
-    s.setPlugin(d_compiler.get());
-  }
-  else if (opts.d_runCompile)
+  Plugin * plugin = nullptr;
+  // NOTE: initialization of plugin goes here
+  if (plugin!=nullptr)
   {
-    d_executor.reset(new Executor(s));
-    s.setPlugin(d_executor.get());
+    s.setPlugin(plugin);
   }
   if (!readFile)
   {
@@ -195,10 +166,9 @@ int main( int argc, char* argv[] )
     }
   }
   std::cout << "success" << std::endl;
-  Plugin * p = s.getPlugin();
-  if (p != nullptr)
+  if (plugin != nullptr)
   {
-    p->finalize();
+    plugin->finalize();
   }
   if (opts.d_stats)
   {

src/plugin.h

@@ -52,8 +52,10 @@ class Plugin
   /**
    * Include file, if not already done so.
    * @param s Specifies the path and name of the file to include.
+   * @param isReference Whether the given file was marked as a reference file.
+   * @param referenceNf The method for normalizing the reference file, if one exists.
    */
-  virtual void includeFile(const Filepath& s) {}
+  virtual void includeFile(const Filepath& s, bool isReference, const Expr& referenceNf) {}
   /**
    * Set type rule for literal kind k to t. This is called when the
    * command declare-consts is executed.

src/state.cpp

@@ -19,8 +19,6 @@ namespace alfc {
 
 Options::Options()
 {
-  d_compile = false;
-  d_runCompile = false;
   d_parseLet = true;
   d_printLet = false;
   d_stats = false;
@@ -217,7 +215,7 @@ bool State::includeFile(const std::string& s, bool isReference, const Expr& refe
   if (d_plugin!=nullptr)
   {
     Assert (!isReference);
-    d_plugin->includeFile(inputPath);
+    d_plugin->includeFile(inputPath, isReference, referenceNf);
   }
   Trace("state") << "Include " << inputPath << std::endl;
   Assert (getAssumptionLevel()==0);

src/state.h

@@ -30,8 +30,6 @@ class Options
 {
  public:
   Options();
-  bool d_compile;
-  bool d_runCompile;
   bool d_printLet;
   /** 'let' is lexed as the SMT-LIB syntax for a dag term specified by a let */
   bool d_parseLet;
@@ -50,7 +48,6 @@ class State
 {
   friend class TypeChecker;
   friend class ExprValue;
-  friend class Executor;
 
  public:
   State(Options& opts, Stats& stats);

src/type_checker.h

@@ -28,7 +28,6 @@ class Plugin;
 class TypeChecker
 {
   friend class State;
-  friend class Compiler;
 
  public:
   TypeChecker(State& s, Options& opts);

user_manual.md

@@ -61,7 +61,6 @@ The ALF checker alfc extends this language with several features:
 - A command `program` for defining side conditions as ordered list of rewrite rules.
 - A command `declare-oracle-fun` for user-provided oracles, that is, functions whose semantics are given by external binaries. Oracles can be used e.g. for modular proof checking.
 - Commands for file inclusion (`include`) and referencing (`reference`). The latter command can be used to specify the name of an `*.smt2` input file that the proof is associated with.
-- Support for compiling ALF signatures to C++ code that can be integrated into `alfc`.
 
 In the following sections, we review these features in more detail. A full syntax for the commands is given at the end of this document.
 
@@ -1514,32 +1513,18 @@ The user is responsible that the input can be properly parsed by the oracle, and
 
 In the above example, a proof rule is then defined that says that if `z` is an integer greater than or equal to `2`, is the product of two integers `x` and `y`, and is prime based on invoking `runIsPrime` in the given requirement, then we can conclude `false`.
 
-# Compiling ALF signatures to C++
-
-For the purposes of optimizing proof checking times, the ALF checker supports compiling user signatures to C++, which can subsequently by compiled as part of the ALF checker.
-When invoked with the option `--gen-compile`, the ALF checker will generate C++ code corresponding to type checking, evaluation of terms and matching for programs for all definitions it reads.
-After incorporating this code by recompiling the checker, this code can be run via the command line option `--run-compile`.
-
-In detail, the recommended steps for compiling an ALF signature are:
-1. Run `alfc --gen-compile <signature>`. This will generate `compiled.out.cpp` in the current directory.
-2. Replacing the file `./src/compiled.cpp` with this file and recompile `alfc`.
-3. Run `alfc --run-compile <proof>`, where `<proof>` includes `<signature>`.
-
-Running with `--run-compile` leads to performance gains that depend on the signature, but are typically up to 50% faster.
-
 # Appendix
 
 ## Command line options of alfc
 
 The ALF command line interface can be invoked by `alfc <option>* <file>` where `<option>` is one of the following:
-- `--gen-compile`: output the C++ code for all included signatures from the input file.
+- `--binder-fresh`: binders generate fresh variables when parsed in proof files.
 - `--help`: displays a help message.
 - `--no-normalize-dec`: do not treat decimal literals as syntax sugar for rational literals.
 - `--no-normalize-hex`: do not treat hexadecimal literals as syntax sugar for binary literals.
 - `--no-parse-let`: do not treat `let` as a builtin symbol for specifying terms having shared subterms.
 - `--no-print-let`: do not letify the output of terms in error messages and trace messages.
 - `--no-rule-sym-table`: do not use a separate symbol table for proof rules and declared terms.
-- `--run-compile`: use the compiled C++ signatures whenever available.
 - `--show-config`: displays the build information for the given binary.
 - `--stats`: enables detailed statistics.
 - `-t <tag>`: enables the given trace tag (for debugging).