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(Plugin.Load(pluginPath, arguments));
+ }
+ }
+
+ 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.Plugins.PluginConfiguration 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,86 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Reflection;
+using Microsoft.Dafny.Plugins;
+
+namespace Microsoft.Dafny;
+
+/// <summary>
+/// This class 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 PluginConfiguration PluginConfiguration;
+
+ private readonly string pluginPath;
+ private readonly Assembly assembly;
+ private System.Type[] rewriterTypes;
+
+ private Plugin(string path, string[] args) {
+ pluginPath = path;
+ assembly = Assembly.LoadFrom(pluginPath);
+ rewriterTypes = CheckPluginForRewriters(assembly);
+ PluginConfiguration = LoadConfiguration(assembly, args, rewriterTypes);
+ }
+
+ public static Plugin Load(string pluginPath, string[] args) {
+ return new Plugin(pluginPath, args);
+ }
+
+ class AutomaticPluginConfiguration : PluginConfiguration {
+ private Func<ErrorReporter, Rewriter>[] rewriters;
+ public AutomaticPluginConfiguration(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(PluginConfiguration)));
+ }
+
+ private static System.Type[] CheckPluginForRewriters(Assembly assembly) {
+ 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 {assembly.Location} does not contain any Microsoft.Dafny.Plugins.Rewriter");
+ }
+
+ return rewriterTpes;
+ }
+
+ private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] args, System.Type[] rewriterTypes) {
+ PluginConfiguration pluginConfiguration = null;
+ foreach (var configurationType in GetConfigurationsTypes(assembly)) {
+ if (pluginConfiguration != null) {
+ throw new Exception(
+ $"Only one class should extend Microsoft.Dafny.Plugins.PluginConfiguration from {assembly.Location}. Please remove {configurationType}.");
+ }
+
+ pluginConfiguration = (PluginConfiguration)Activator.CreateInstance(configurationType);
+
+ if (pluginConfiguration == null) {
+ throw new Exception($"Could not instantiate a {configurationType} from {assembly.Location}");
+ }
+
+ pluginConfiguration.ParseArguments(args);
+ }
+
+ pluginConfiguration ??= new AutomaticPluginConfiguration(
+ rewriterTypes.Select<System.Type, Func<ErrorReporter, Rewriter>>((System.Type rewriterType) =>
+ (ErrorReporter errorReporter) =>
+ Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray());
+ return pluginConfiguration;
+ }
+
+ public IEnumerable<IRewriter> GetRewriters(ErrorReporter reporter) {
+ return PluginConfiguration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter));
+ }
+}

Source/Dafny/Plugins/PluginConfiguration.cs

@@ -0,0 +1,31 @@
+using System;
+using System.Collections.Generic;
+
+namespace Microsoft.Dafny.Plugins;
+
+/// <summary>
+/// Plugins should define a class that extends PluginConfiguration,
+/// 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 PluginConfiguration, 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 PluginConfiguration {
+ /// <summary>
+ /// A Microsoft.Dafny.Plugins.PluginConfiguration 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 PluginConfiguration, 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 PluginConfiguration class, and override the method GetRewriters(), whose first argument is an ErrorReporter
+ /// * Have no PluginConfiguration 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);
+ }
+ }
+}