Plugin for everything instead of just resolution.

Source/Dafny/DafnyOptions.cs

@@ -7,6 +7,7 @@
 using System.Text;
 using System.Diagnostics.Contracts;
 using System.IO;
+using System.Reflection;
 using JetBrains.Annotations;
 using Bpl = Microsoft.Boogie;
 
@@ -138,14 +139,13 @@ public enum IncludesModes {
  public string BoogieXmlFilename = null;
 
  // invariant: All strings of this list are non-empty
- public List<string> CompilerBackends = new();
+ public List<Assembly> Plugins = new();
 
  public virtual TestGenerationOptions TestGenOptions =>
  testGenOptions ??= new TestGenerationOptions();
 
  protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
  var args = ps.args; // convenient synonym
-
  switch (name) {
  case "dprelude":
  if (ps.ConfirmArgumentCount(1)) {
@@ -235,10 +235,18 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
  return true;
  }
 
- case "compiler": {
+ case "plugins": {
  if (ps.ConfirmArgumentCount(1)) {
- if (args[ps.i].Length > 0) {
- CompilerBackends.AddRange(args[ps.i].Split(',').Where(s => s.Length > 0));
+ var pluginsList = args[ps.i];
+ if (pluginsList.Length > 0) {
+ foreach (var pluginPath in pluginsList.Split(',').Where(s => s.Length > 0)) {
+ var pluginAssembly = Assembly.LoadFrom(pluginPath);
+ if (!pluginAssembly.GetTypes().Any(t =>
+ t.IsAssignableTo(typeof(IRewriter)))) {
+ throw new Exception($"Plugin {pluginPath} does not contain any Microsoft.Dafny.IRewriter");
+ }
+ Plugins.Add(pluginAssembly);
+ }
  }
  }
 
@@ -817,7 +825,7 @@ verification outcome
  Note that the C++ backend has various limitations (see Docs/Compilation/Cpp.md).
  This includes lack of support for BigIntegers (aka int), most higher order
  functions, and advanced features like traits or co-inductive types.
-/compiler:<assemblies>
+/plugins:<path to assemblies>
  (experimental) List of comma-separated paths to assemblies that contain at least one
  instantiatable class extending Microsoft.Dafny.IRewriter
 /Main:<name>

Source/Dafny/Resolver.cs

@@ -438,7 +438,7 @@ public void ResolveProgram(Program prog) {
 
  rewriters.Add(new InductionRewriter(reporter));
 
- if (DafnyOptions.O.CompilerBackends.Count() >= 1) {
+ if (DafnyOptions.O.Plugins.Count() >= 1) {
  IToken GetFirstTopLevelToken() {
  return prog.DefaultModuleDef.TopLevelDecls.Select(x => x as ClassDecl)
  .Where(x => x != null)
@@ -447,38 +447,15 @@ IToken GetFirstTopLevelToken() {
  .Select(member => member.tok).FirstOrDefault(Token.NoToken);
  }
 
- foreach (var assemblyPath in DafnyOptions.O.CompilerBackends) {
- Assembly compilerBackend;
- try {
- compilerBackend = Assembly.LoadFrom(assemblyPath);
- } catch (ArgumentException) {
- reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend paths cannot be empty.");
- continue;
- } catch (FileNotFoundException) {
- reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend '{assemblyPath}' could not be found ");
- continue;
- } catch (FileLoadException e) {
- reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend '{assemblyPath}' could not be loaded: {e.Message}");
- continue;
- } catch (BadImageFormatException e) {
- reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend version of '{assemblyPath}' is incompatible: {e.Message}");
- continue;
- }
-
- var oneRewriterInstantiated = false;
- foreach (System.Type type in compilerBackend.GetTypes().Where(t => t.IsAssignableTo(typeof(IRewriter)))) {
+ foreach (var assembly in DafnyOptions.O.Plugins) {
+ foreach (System.Type type in assembly.GetTypes().Where(t => t.IsAssignableTo(typeof(IRewriter)))) {
  var pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter;
  if (pluginRewriter == null) {
  reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"[Internal error] '{type.FullName}' could not be created as an IRewriter");
  } else {
  rewriters.Add(pluginRewriter);
- oneRewriterInstantiated = true;
  }
  }
-
- if (!oneRewriterInstantiated) {
- reporter.Error(MessageSource.Resolver, Token.NoToken, $"Could not find an Microsoft.Dafny.IRewriter in '{assemblyPath}'");
- }
  }
  }
 

Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs

@@ -21,7 +21,7 @@ public class TextDocumentLoaderTest {
  private Mock<ICompilationStatusNotificationPublisher> notificationPublisher;
  private TextDocumentLoader textDocumentLoader;
  private Mock<ILoggerFactory> logger;
- private Mock<IOptions<CompilerOptions>> compilerOptions;
+ private Mock<IOptions<DafnyPluginsOptions>> dafnyPluginOptions;
 
  [TestInitialize]
  public void SetUp() {
@@ -32,7 +32,7 @@ public void SetUp() {
  ghostStateDiagnosticCollector = new();
  notificationPublisher = new();
  logger = new Mock<ILoggerFactory>();
- compilerOptions = new Mock<IOptions<CompilerOptions>>();
+ dafnyPluginOptions = new Mock<IOptions<DafnyPluginsOptions>>();
  textDocumentLoader = TextDocumentLoader.Create(
  parser.Object,
  symbolResolver.Object,
@@ -41,7 +41,7 @@ public void SetUp() {
  ghostStateDiagnosticCollector.Object,
  notificationPublisher.Object,
  logger.Object,
- compilerOptions.Object
+ dafnyPluginOptions.Object
  );
  }
 

Source/DafnyLanguageServer/Language/CompilerOptions.cs → Source/DafnyLanguageServer/Language/DafnyOptions.cs

@@ -2,15 +2,15 @@
  /// <summary>
  /// Options for the resolution and compilation pipeline
  /// </summary>
- public class CompilerOptions {
+ public class DafnyPluginsOptions {
  /// <summary>
  /// The IConfiguration section of the compiler options.
  /// </summary>
- public const string Section = "Compiler";
+ public const string Section = "Dafny";
 
  /// <summary>
  /// Gets or sets which backends will be targeted so that their resolver can run before verification.
  /// </summary>
- public string Backends { get; set; } = "";
+ public string Plugins { get; set; } = "";
  }
 }

Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs

@@ -25,7 +25,7 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv
  return services
  .Configure<VerifierOptions>(configuration.GetSection(VerifierOptions.Section))
  .Configure<GhostOptions>(configuration.GetSection(GhostOptions.Section))
- .Configure<CompilerOptions>(configuration.GetSection(CompilerOptions.Section))
+ .Configure<DafnyPluginsOptions>(configuration.GetSection(DafnyPluginsOptions.Section))
  .AddSingleton<IDafnyParser>(serviceProvider => DafnyLangParser.Create(serviceProvider.GetRequiredService<ILogger<DafnyLangParser>>()))
  .AddSingleton<ISymbolResolver, DafnyLangSymbolResolver>()
  .AddSingleton<IProgramVerifier>(CreateVerifier)

Source/DafnyLanguageServer/README.md

@@ -76,11 +76,11 @@ Options provided through the command line have higher priority than the options
 --ghost:markStatements=true
 ```
 
-### Compilation Backends
+### Plugins
 
 ```sh
 # Provides a comma-separated list of paths to assemblies
-# that contain an instantiatable IRewrite that is used during resolution
+# that contain an instantiatable IRewrite to use during resolution
 # Default: "" (nothing extra is loaded)
---compiler:backends=
+--dafny:plugins=
 ```

Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs

@@ -46,7 +46,7 @@ private static TextDocumentLoader CreateTextDocumentLoader(IServiceProvider serv
  services.GetRequiredService<IGhostStateDiagnosticCollector>(),
  services.GetRequiredService<ICompilationStatusNotificationPublisher>(),
  services.GetRequiredService<ILoggerFactory>(),
- services.GetRequiredService<IOptions<CompilerOptions>>()
+ services.GetRequiredService<IOptions<DafnyPluginsOptions>>()
  );
  }
  }

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

@@ -33,7 +33,7 @@ public class TextDocumentLoader : ITextDocumentLoader {
  private readonly ICompilationStatusNotificationPublisher notificationPublisher;
  private readonly ILoggerFactory loggerFactory;
  private readonly BlockingCollection<Request> requestQueue = new();
- private readonly IOptions<CompilerOptions> compilerOptions;
+ private readonly IOptions<DafnyPluginsOptions> dafnyPluginsOptions;
 
  private TextDocumentLoader(
  ILoggerFactory loggerFactory,
@@ -43,15 +43,15 @@ private TextDocumentLoader(
  ISymbolTableFactory symbolTableFactory,
  IGhostStateDiagnosticCollector ghostStateDiagnosticCollector,
  ICompilationStatusNotificationPublisher notificationPublisher,
- IOptions<CompilerOptions> compilerOptions) {
+ IOptions<DafnyPluginsOptions> dafnyPluginsOptions) {
  this.parser = parser;
  this.symbolResolver = symbolResolver;
  this.verifier = verifier;
  this.symbolTableFactory = symbolTableFactory;
  this.ghostStateDiagnosticCollector = ghostStateDiagnosticCollector;
  this.notificationPublisher = notificationPublisher;
  this.loggerFactory = loggerFactory;
- this.compilerOptions = compilerOptions;
+ this.dafnyPluginsOptions = dafnyPluginsOptions;
  }
 
  public static TextDocumentLoader Create(
@@ -62,7 +62,7 @@ public static TextDocumentLoader Create(
  IGhostStateDiagnosticCollector ghostStateDiagnosticCollector,
  ICompilationStatusNotificationPublisher notificationPublisher,
  ILoggerFactory loggerFactory,
- IOptions<CompilerOptions> compilerOptions
+ IOptions<DafnyPluginsOptions> compilerOptions
  ) {
  var loader = new TextDocumentLoader(loggerFactory, parser, symbolResolver, verifier, symbolTableFactory, ghostStateDiagnosticCollector, notificationPublisher, compilerOptions);
  var loadThread = new Thread(loader.Run, MaxStackSize) { IsBackground = true };
@@ -117,8 +117,8 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) {
  return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger<SymbolTable>(), textDocument, errorReporter, program, loadCanceled: false);
  }
 
- if (compilerOptions.Value.Backends.Length > 0) {
- DafnyOptions.O.CompilerBackends = compilerOptions.Value.Backends.Split(",").Where(x => x.Length > 0).ToList();
+ if (dafnyPluginsOptions.Value.Plugins.Length > 0) {
+ DafnyOptions.O.Parse(new[] { "-plugins:" + dafnyPluginsOptions.Value.Plugins });
  }
 
  var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, cancellationToken);

Source/DafnyPipeline.Test/ExternalResolverTest.cs

@@ -18,7 +18,7 @@ public class ExternalResolverTest {
  /// This method creates a library and returns the path to that library.
  /// The library extends an IRewriter so that we can verify that Dafny invokes it if provided in argument.
  /// </summary>
- public async Task<string> GetLibrary(string code) {
+ public async Task<Assembly> GetLibrary(string code) {
  var temp = Path.GetTempFileName();
  var compilation = CSharpCompilation.Create("tempAssembly");
  var standardLibraries = new List<string>()
@@ -53,7 +53,7 @@ public async Task<string> GetLibrary(string code) {
  await File.WriteAllTextAsync(temp + ".runtimeconfig.json", configuration + Environment.NewLine);
 
  Assert.True(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString())));
- return assemblyPath;
+ return Assembly.LoadFrom(assemblyPath);
  }
 
  class CollectionErrorReporter : BatchErrorReporter {
@@ -77,7 +77,7 @@ public override void PostResolve(ModuleDefinition m) {
 
  var reporter = new CollectionErrorReporter();
  var options = new DafnyOptions(reporter);
- options.CompilerBackends.Add(library);
+ options.Plugins.Add(library);
  DafnyOptions.Install(options);
 
  var programString = "function test(): int { 1 }";