feat: Plugin support

Source/Dafny/AST/DafnyAst.cs

@@ -75,6 +75,10 @@ public string Name {
  }
  }
  }
+
+ public IToken GetFirstTopLevelToken() {
+ return DefaultModuleDef.GetFirstTopLevelToken();
+ }
  }
 
  public class Include : IComparable {
@@ -4223,6 +4227,17 @@ public bool IsEssentiallyEmptyModuleBody() {
  }
  return true;
  }
+
+ public IToken GetFirstTopLevelToken() {
+ return TopLevelDecls.OfType<ClassDecl>()
+ .SelectMany(classDecl => classDecl.Members)
+ .Where(member => member.tok.line > 0)
+ .Select(member => member.tok)
+ .Concat(TopLevelDecls.OfType<LiteralModuleDecl>()
+ .Select(moduleDecl => moduleDecl.ModuleDef.GetFirstTopLevelToken())
+ .Where(tok => tok.line > 0)
+ ).FirstOrDefault(Token.NoToken);
+ }
  }
 
  public class DefaultModuleDecl : ModuleDefinition {

Source/Dafny/DafnyOptions.cs

@@ -7,7 +7,10 @@
 using System.Text;
 using System.Diagnostics.Contracts;
 using System.IO;
+using System.Reflection;
+using System.Text.RegularExpressions;
 using JetBrains.Annotations;
+using Microsoft.Dafny.Plugins;
 using Bpl = Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
@@ -135,12 +138,13 @@ public enum IncludesModes {
  // Working around the fact that xmlFilename is private
  public string BoogieXmlFilename = null;
 
+ public List<Plugin> 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)) {
@@ -230,6 +234,41 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
  return true;
  }
 
+ case "Plugin":
+ case "plugin": {
+ if (ps.ConfirmArgumentCount(1)) {
+ var pluginAndArgument = args[ps.i];
+ if (pluginAndArgument.Length > 0 &&
+ pluginAndArgument[0] == '"' &&
+ pluginAndArgument[^1] == '"'
+ ) {
+ var unescapeRegex = new Regex(@"\\""|\\\\");
+ pluginAndArgument = unescapeRegex.Replace(pluginAndArgument.Substring(1, pluginAndArgument.Length - 2),
+ match => match.Groups[0].Value == @"\""" ? "\"" : @"\"
+ );
+ }
+ if (pluginAndArgument.Length > 0) {
+ var pluginArray = pluginAndArgument.Split(',');
+ var pluginPath = pluginArray[0];
+ var arguments = Array.Empty<string>();
+ if (pluginArray.Length >= 2) {
+ // There are no commas in paths, but there can be in arguments
+ var argumentsString = string.Join(',', pluginArray.Skip(1));
+ // Parse arguments, accepting and remove double quotes that isolate long arguments
+ var splitter = new Regex(@"""((?:[^""]|\\"")*)""|([^ ]+)");
+ arguments = splitter.Matches(argumentsString).Select(
+ matchResult => matchResult.Groups[1].Success ?
+ matchResult.Groups[1].Value.Replace(@"\""", @"""") :
+ matchResult.Groups[2].Value
+ ).ToArray();
+ }
+ Plugins.Add(new Plugin(pluginPath, arguments, errorReporter));
+ }
+ }
+
+ return true;
+ }
+
  case "Main":
  case "main": {
  if (ps.ConfirmArgumentCount(1)) {
@@ -806,6 +845,12 @@ 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.
+/plugin:<path to one assembly>[ <arguments>]
+ (experimental) One path to an assembly that contains at least one
+ instantiatable class extending Microsoft.Dafny.Plugin.Rewriter.
+ It can also extend Microsoft.Dafny.Plugin.Configuration to receive arguments
+ More information about what plugins do and how define them:
+ https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer/README.md#about-plugins
 /Main:<name>
  The (fully-qualified) name of the method to use as the executable entry point.
  Default is the method with the {{:main}} atrribute, or else the method named 'Main'.

Source/Dafny/Plugin.cs

@@ -0,0 +1,82 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Reflection;
+using Microsoft.Dafny.Plugins;
+
+namespace Microsoft.Dafny;
+
+/// <summary>
+/// This class is internal to Dafny. It wraps an assembly and an extracted configuration from this assembly,
+/// The configuration provides the methods to parse command-line arguments and obtain Rewriters 
+/// </summary>
+public class Plugin {
+ public Configuration Configuration;
+
+ private readonly string path;
+ private readonly Assembly assembly;
+ private System.Type[] rewriterTypes;
+
+ class AutomaticConfiguration : Configuration {
+ private Func<ErrorReporter, Rewriter>[] rewriters;
+ public AutomaticConfiguration(Func<ErrorReporter, Rewriter>[] rewriters) {
+ this.rewriters = rewriters;
+ }
+
+ public override Rewriter[] GetRewriters(ErrorReporter errorReporter) {
+ return rewriters.Select(funcErrorReporterRewriter =>
+ funcErrorReporterRewriter(errorReporter)).ToArray();
+ }
+ }
+
+ public static IEnumerable<System.Type> GetConfigurationsTypes(Assembly assembly) {
+ return assembly.GetTypes()
+ .Where(t => t.IsAssignableTo(typeof(Configuration)));
+ }
+
+ public Plugin(string pluginPath, string[] args, ErrorReporter reporter) {
+ path = pluginPath;
+ assembly = Assembly.LoadFrom(path);
+ rewriterTypes = CheckPluginForRewriters(assembly, path);
+ Configuration = LoadConfiguration(assembly, args, path, rewriterTypes);
+ }
+
+ private static System.Type[] CheckPluginForRewriters(Assembly assembly, string path) {
+ System.Type[] rewriterTpes = assembly.GetTypes().Where(t =>
+ t.IsAssignableTo(typeof(Rewriter))).ToArray();
+ // Checks about the plugin to be well-behaved.
+ if (!rewriterTpes.Any()) {
+ throw new Exception($"Plugin {path} does not contain any Microsoft.Dafny.Plugins.Rewriter");
+ }
+
+ return rewriterTpes;
+ }
+
+ private static Configuration LoadConfiguration(Assembly assembly, string[] args, string path, System.Type[] rewriterTypes) {
+ Configuration configuration = null;
+ foreach (var configurationType in GetConfigurationsTypes(assembly)) {
+ if (configuration != null) {
+ throw new Exception(
+ $"Only one class should extend Microsoft.Dafny.Plugins.Configuration from {path}. Please remove {configurationType}.");
+ }
+
+ configuration = (Configuration)Activator.CreateInstance(configurationType);
+
+ if (configuration == null) {
+ throw new Exception($"Could not instantiate a {configurationType} from {path}");
+ }
+
+ configuration.ParseArguments(args);
+ }
+
+ configuration ??= new AutomaticConfiguration(
+ rewriterTypes.Select<System.Type, Func<ErrorReporter, Rewriter>>((System.Type rewriterType) =>
+ (ErrorReporter errorReporter) =>
+ Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray());
+ return configuration;
+ }
+
+ public IEnumerable<IRewriter> GetRewriters(ErrorReporter reporter) {
+ return Configuration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter));
+ }
+}

Source/Dafny/Plugins/Configuration.cs

@@ -0,0 +1,31 @@
+using System;
+using System.Collections.Generic;
+
+namespace Microsoft.Dafny.Plugins;
+
+/// <summary>
+/// Plugins should define a class that extends Configuration,
+/// in order to receive plugin-specific command-line arguments by overwriting the method `ParseArguments`
+/// It is also used to provide to Dafny a list of Rewriter using the method `GetRewriters`
+///
+/// If the plugin defines no Configuration, then Dafny will instantiate every sub-class
+/// of Rewriter from the plugin, providing them with an ErrorReporter in the constructor
+/// as the first and only argument.
+/// </summary>
+public abstract class Configuration {
+ /// <summary>
+ /// A Microsoft.Dafny.Plugins.Configuration will be automatically instantiated an arguments
+ /// will be provided to the plugin by the method `ParseArguments``;
+ /// </summary>
+ /// <param name="args">The arguments passed to the plugin</param>
+ public virtual void ParseArguments(string[] args) {
+ }
+
+ /// <summary>
+ /// Override this method to provide specific rewriters to Dafny
+ /// </summary>
+ /// <returns>a list of Rewriter that are going to be used in the resolution pipeline</returns>
+ public virtual Rewriter[] GetRewriters(ErrorReporter errorReporter) {
+ return Array.Empty<Rewriter>();
+ }
+}

Source/Dafny/Plugins/Rewriter.cs

@@ -0,0 +1,55 @@
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny.Plugins {
+ /// <summary>
+ /// A class that plugins should extend, in order to provide an extra Rewriter to the pipeline.
+ ///
+ /// If the plugin defines no Configuration, then Dafny will instantiate every sub-class
+ /// of Rewriter from the plugin, providing them with an ErrorReporter in the constructor
+ /// as the first and only argument.
+ /// </summary>
+ public abstract class Rewriter {
+ /// <summary>
+ /// Used to report errors and warnings, with positional information.
+ /// </summary>
+ protected readonly ErrorReporter Reporter;
+
+ /// <summary>
+ /// Constructor that accepts an ErrorReporter
+ /// You can obtain an ErrorReporter two following ways:
+ /// * Extend a Configuration class, and override the method GetRewriters(), whose first argument is an ErrorReporter
+ /// * Have no Configuration class, and an ErrorReporter will be provided to your class's constructor.
+ /// 
+ /// Then you can use the protected field "reporter" like the following:
+ /// 
+ /// reporter.Error(MessageSource.Compiler, token, "[Your plugin] Your error message here");
+ ///
+ /// The token is usually obtained on expressions and statements in the field `tok`
+ /// If you do not have access to them, use moduleDefinition.GetFirstTopLevelToken()
+ /// </summary>
+ /// <param name="reporter">The error reporter. Usually outputs automatically to IDE or command-line</param>
+ public Rewriter(ErrorReporter reporter) {
+ Contract.Requires(reporter != null);
+ Reporter = reporter;
+ }
+ /// <summary>
+ /// Override this method to obtain a module definition after the entire resolution pipeline
+ /// You can then report errors using reporter.Error (see above)
+ /// </summary>
+ /// <param name="moduleDefinition">A module definition after it
+ /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed</param>
+ public virtual void PostResolve(ModuleDefinition moduleDefinition) {
+ Contract.Requires(moduleDefinition != null);
+ }
+
+ /// <summary>
+ /// Override this method to obtain the final program after the entire resolution pipeline
+ /// after the individual PostResolve on every module
+ /// You can then report errors using reporter.Error (see above)
+ /// </summary>
+ /// <param name="program">The entire program after it is fully resolved</param>
+ public virtual void PostResolve(Program program) {
+ Contract.Requires(program != null);
+ }
+ }
+}