Refactor compiler to allow loading backends from separate DLLs #1708

cpitclaudel · 2022-01-13T16:44:59Z

This is the first step towards making it easier to plug in compiler backends.

To minimize code churn I didn't move each existing backend to a separate DLL. Should I?
I'm not a huge fan of the two-layered structure (factory + actual prover), but IIUC that's needed to load a DLL (since types are not first-class values in C#)
There are surprising dependencies between DafnyAST.cs and the compiler (the AST depended on some values from the compiler); I tagged the corresponding commit with NEEDS REVIEW.

With this PR the /compileTarget flag can take a path to a DLL.

The Csharp and Go compilers were using a separate FreshIdGenerator for a few variables. Why?

MikaelMayer · 2022-01-13T20:00:26Z

This is the first step towards making it easier to plug in compiler backends.

To minimize code churn I didn't move each existing backend to a separate DLL. Should I?

I'm not a huge fan of the two-layered structure (factory + actual prover), but IIUC that's needed to load a DLL (since types are not first-class values in C#)

There are surprising dependencies between DafnyAST.cs and the compiler (the AST depended on some values from the compiler); I tagged the corresponding commit with NEEDS REVIEW.

With this PR the /compileTarget flag can take a path to a DLL.

For the moment, I would advise to not move each existing backend to a separate DLL because it makes development easier. I'm working on refactoring the compiler itself so that it's more modular (e.g. no call to a single CreateForEachLoop that is responsible of subtype checking). Hence I not only need to modify the base compiler, but also the different instances, and I run a test for all of them at the same time.

Source/Dafny/Compilers/Compiler-Csharp.cs

keyboardDrummer · 2022-01-17T12:38:25Z

Source/Dafny/Compilers/Compiler-go.cs

- var okVar = FreshId("_ok");
- var iterVar = FreshId("_iter");
+ var okVar = idGenerator.FreshId("_ok");
+ var iterVar = idGenerator.FreshId("_iter");


Where does this _ok => _iter rename come from?

I don't think there's a rename here?

Source/Dafny/Compilers/Compiler-Csharp.cs

Source/Dafny/Compilers/SinglePassCompiler.cs

Source/Dafny/DafnyOptions.cs

Source/Dafny/Resolver.cs

Source/DafnyDriver/DafnyDriver.cs

Test/SelfHosting/Main.cs

cpitclaudel · 2022-01-18T16:47:20Z

For the moment, I would advise to not move each existing backend to a separate DLL because it makes development easier.

👍, although it might be nice to split off the Java compiler, because compiling the runtime every time is a pain.

MikaelMayer · 2022-01-18T17:14:45Z

compiling

I investigated more why I believed we should hold off splitting the compilers into different projects. It turns out I had some instability with some versions of Newtonsoft.Json.dll (DafnyDriver requires 9.0.0.0, DafnyLanguageServer requires 11.0.0.0, so if I compile DafnyDriver, the language server does not work).
So I don't have any more strong argument of not splitting the compilers.

Source/Dafny/AST/ASTExport/Program.cs

keyboardDrummer · 2022-01-19T11:29:48Z

For the moment, I would advise to not move each existing backend to a separate DLL because it makes development easier.

👍, although it might be nice to split off the Java compiler, because compiling the runtime every time is a pain.

What do we mean by splitting off the compilers? We'd move the compiler file to a new .NET project, sure, but where do we leave that project?

If we keep that project in the Dafny solution then it wouldn't impact development, right? It just means that Rider can build DafnyPipeline without building the Java compiler.

cpitclaudel · 2022-01-19T16:42:50Z

It just means that Rider can build DafnyPipeline without building the Java compiler.

That was my hope, yes.

robin-aws · 2022-01-19T17:53:09Z

Source/Dafny/Compilers/ICompiler.cs

+
+namespace Microsoft.Dafny;
+
+public interface ICompiler {


This interface is so much nicer. :)

Here's an idea to consider for the very next PR (since it's not necessary here and the PR is already large): could we add a method to be invoked earlier in the pipeline, before verification, that can produce compiler-specific errors? Something like CheckCompatibility.

The use case would be a codebase using a specific compiler, especially one of the more incomplete ones like C++, where it's currently pretty frustrating to spend a ton of time getting your code to verify successfully only to then find out "oh wait, my compiler doesn't support unbounded ints" and have to start over. This is particularly easy for newer Dafny programmers to hit, since the documentation on which features are supported by which compilers is something you have to think to look up, and isn't that obvious for newcomers.

Here's an idea to consider for the very next PR (since it's not necessary here and the PR is already large): could we add a method to be invoked earlier in the pipeline, before verification, that can produce compiler-specific errors? Something like CheckCompatibility.

The compiler is fast and verification errors lead to runtime (not compile-time) errors, so we could just run the compiler first or in parallel with verification instead of running verification first and only then running the compiler. So instead of resolve → verify → translate → compile we could just run

resolve → verify → translate → compile

Or even resolve → translate → verify → compile if we don't want concurrency.

Probably a good entry for your compiler planning doc!

Yup, you're absolutely right that there's other ways to get the same result (and it would be better to not have another method to implement if possible). I'm not sure I believe "verification errors lead to runtime (not compile-time) errors" is always true, or that we want to ensure it is always true in the future, but we can work that into the design. :)

Our compilers are actually "translators", the two are synonyms. When you say "compiler", do you mean the actual language-to-bytecode compiler?

keyboardDrummer · 2022-01-20T11:44:36Z

It just means that Rider can build DafnyPipeline without building the Java compiler.

That was my hope, yes.

Sounds great, but let's do it in a separate PR

MikaelMayer

Also, how will it work to provide new compiler assemblies? Are you reusing the same compileTarget option?

MikaelMayer · 2022-01-19T19:52:32Z

Source/Dafny/Compilers/ICompiler.cs

+
+namespace Microsoft.Dafny;
+
+public interface ICompiler {


Our compilers are actually "translators", the two are synonyms. When you say "compiler", do you mean the actual language-to-bytecode compiler?

MikaelMayer · 2022-01-21T15:17:37Z

Source/Dafny/DafnyOptions.cs

- }
-
- public CompilationTarget CompileTarget = CompilationTarget.Csharp;
+ public CompilerFactory CompilerFactoryInstance;


With flags it was obvious we could run multiple compilers at the same time.
How are you going to do it with this? I suggest you use a comma-separated list of compilers

With flags it was obvious we could run multiple compilers at the same time.

I don't think we ever could actually run multiple compilers at the same time, could we?

keyboardDrummer · 2022-01-21T15:31:23Z

Source/Dafny/Compilers/ICompiler.cs

+
+namespace Microsoft.Dafny;
+
+public interface ICompiler {


Consider renaming ICompiler to ICodeGenerator. "Compiler" is generally used to refer to an entire compilation pipeline, including parsing source code, right?

cpitclaudel · 2022-01-21T16:13:33Z

Also, how will it work to provide new compiler assemblies? Are you reusing the same compileTarget option?

That's right, you just pass /compileTarget:path/to/a/library.dll

cpitclaudel · 2022-01-21T16:49:51Z

@MikaelMayer and I disucssed this today. We think it's better if instead of reusing the compileTarget flag to give a DLL we instead make a new flag plugins that takes a list of DLLs, each of which exposes an ICompiler. Then we can resolve the value of compileTarget by looking for an ICompiler with the appropriate SupportedLanguage. So you'd write /plugin:XYZCompiler.dll /compileTarget:xyz.

This same plugin flag can be used for other kinds of plugins, and @MikaelMayer will implement it as part of #1739 . Then I will rebase this PR on top of that.

Finally we decided it would be simpler to get rid of the factory and instantiate an ICompiler instance (renamed to ICodeGenerator) with no arguments right from the beginning of the process, (and later on pass the reporter). I will make these changes after @MikaelMayer completes his.

keyboardDrummer · 2022-01-25T10:28:10Z

This same plugin flag can be used for other kinds of plugins, and @MikaelMayer will implement it as part of #1739 . Then I will rebase this PR on top of that.

Why don't we merge this PR first, since this is already approved?

MikaelMayer · 2022-01-26T17:02:49Z

Why don't we merge this PR first, since this is already approved?

Maybe because 1) the tests are not working yet, and 2) offering an API to implement a factory and then immediately switching to a plugin strategy would be not backward compatible with the factory (for example, /compilationTarget won't accept a DLL anymore once we switch to the plugin system). and 3) it makes sense to accept DLLs as a separate argument rather than changing the CompilationTarget.

MikaelMayer · 2022-01-26T17:03:58Z

I'm voluntarily not writing "changes requested" because I don't want to block this PR, but we are still in discussion about the plugins system which would make this PR easier to implement.

cpitclaudel · 2022-01-26T17:21:30Z

Why don't we merge this PR first, since this is already approved?

The only client of this PR is my compiler work, which can happen in a branch. The plugin API is the result of discussing with @MikaelMayer how to unify his resolver plugins and my compiler plugins, so I don't think we should merge this until the plugin work is done :)

cpitclaudel · 2022-03-30T17:05:50Z

Closing this, since it was superseded by my later PR on top of Mikael's one

cpitclaudel added 5 commits January 6, 2022 16:49

feat: Refactor compiler to make it easier to plug in backends

3a9bc60

docs: Replace reference to php with entry for Python

afdca9f

NEEDS REVIEW: Remove dependency from DafnyAst to SinglePassCompiler

67905af

The Csharp and Go compilers were using a separate FreshIdGenerator for a few variables. Why?

Reformat

95a01a8

Don't check in the self-hosting compiler yet

157774b

cpitclaudel added part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag misc: cleanup Cleanups in the implementation or in corners of the language labels Jan 13, 2022

cpitclaudel self-assigned this Jan 13, 2022

cpitclaudel force-pushed the compiler branch 3 times, most recently from 07cd7c4 to a59a9ef Compare January 16, 2022 23:08

keyboardDrummer reviewed Jan 17, 2022

View reviewed changes

robin-aws mentioned this pull request Jan 19, 2022

Add CSV logger for test results and timing #1712

Merged

keyboardDrummer reviewed Jan 19, 2022

View reviewed changes

Source/Dafny/AST/ASTExport/Program.cs Outdated Show resolved Hide resolved

cpitclaudel force-pushed the compiler branch from 135ae5d to 157774b Compare January 19, 2022 16:44

Rename compiler classes

44f4ecd

cpitclaudel mentioned this pull request Jan 19, 2022

Compiler.ReportError uses hardcoded comment syntax #1729

Open

cpitclaudel added 2 commits January 19, 2022 12:16

Remove FIXME

5e6c10c

Fixes suggested by Remy

4b8b60e

robin-aws reviewed Jan 19, 2022

View reviewed changes

Remove one more FIXME

bc6d44d

cpitclaudel requested a review from keyboardDrummer January 19, 2022 18:15

cpitclaudel added 2 commits January 19, 2022 13:16

Merge branch 'master' into compiler

77ee7c0

Remove more FIXMEs

3c9b777

keyboardDrummer previously approved these changes Jan 20, 2022

View reviewed changes

Format

a3772ac

cpitclaudel dismissed keyboardDrummer’s stale review via a3772ac January 20, 2022 15:32

keyboardDrummer approved these changes Jan 20, 2022

View reviewed changes

cpitclaudel mentioned this pull request Jan 20, 2022

feat: Plugin support #1739

Merged

MikaelMayer reviewed Jan 21, 2022

View reviewed changes

keyboardDrummer reviewed Jan 21, 2022

View reviewed changes

cpitclaudel mentioned this pull request Mar 9, 2022

Allow users to plug in custom compilers #1894

Merged

cpitclaudel closed this Mar 30, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor compiler to allow loading backends from separate DLLs #1708

Refactor compiler to allow loading backends from separate DLLs #1708

cpitclaudel commented Jan 13, 2022 •

edited

Loading

MikaelMayer commented Jan 13, 2022

keyboardDrummer Jan 17, 2022 •

edited

Loading

cpitclaudel Jan 19, 2022

cpitclaudel commented Jan 18, 2022

MikaelMayer commented Jan 18, 2022

keyboardDrummer commented Jan 19, 2022

cpitclaudel commented Jan 19, 2022

robin-aws Jan 19, 2022

cpitclaudel Jan 19, 2022

cpitclaudel Jan 19, 2022

robin-aws Jan 19, 2022

MikaelMayer Jan 19, 2022

keyboardDrummer commented Jan 20, 2022

MikaelMayer left a comment

MikaelMayer Jan 19, 2022

MikaelMayer Jan 21, 2022

cpitclaudel Jan 21, 2022

keyboardDrummer Jan 21, 2022

cpitclaudel commented Jan 21, 2022

cpitclaudel commented Jan 21, 2022

keyboardDrummer commented Jan 25, 2022

MikaelMayer commented Jan 26, 2022

MikaelMayer commented Jan 26, 2022

cpitclaudel commented Jan 26, 2022

cpitclaudel commented Mar 30, 2022

Refactor compiler to allow loading backends from separate DLLs #1708

Refactor compiler to allow loading backends from separate DLLs #1708

Conversation

cpitclaudel commented Jan 13, 2022 • edited Loading

MikaelMayer commented Jan 13, 2022

keyboardDrummer Jan 17, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel commented Jan 18, 2022

MikaelMayer commented Jan 18, 2022

keyboardDrummer commented Jan 19, 2022

cpitclaudel commented Jan 19, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Jan 20, 2022

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel commented Jan 21, 2022

cpitclaudel commented Jan 21, 2022

keyboardDrummer commented Jan 25, 2022

MikaelMayer commented Jan 26, 2022

MikaelMayer commented Jan 26, 2022

cpitclaudel commented Jan 26, 2022

cpitclaudel commented Mar 30, 2022

cpitclaudel commented Jan 13, 2022 •

edited

Loading

keyboardDrummer Jan 17, 2022 •

edited

Loading