From 7abd76085a3ec623215033cb6eb44ffa313da225 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 09:57:45 -0600 Subject: [PATCH 01/47] Removed internal --- Source/Dafny/Rewriter.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index b4ead9aa257..2571baa5a00 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -16,11 +16,11 @@ public IRewriter(ErrorReporter reporter) { this.reporter = reporter; } - internal virtual void PreResolve(ModuleDefinition m) { + virtual void PreResolve(ModuleDefinition m) { Contract.Requires(m != null); } - internal virtual void PostResolve(ModuleDefinition m) { + virtual void PostResolve(ModuleDefinition m) { Contract.Requires(m != null); } From daa54eea67c0379a1a11ed33e7287292cd8bd6f2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 11:03:33 -0600 Subject: [PATCH 02/47] Fixed error --- Source/Dafny/Rewriter.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 2571baa5a00..1523716a59d 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -16,11 +16,11 @@ public IRewriter(ErrorReporter reporter) { this.reporter = reporter; } - virtual void PreResolve(ModuleDefinition m) { + public virtual void PreResolve(ModuleDefinition m) { Contract.Requires(m != null); } - virtual void PostResolve(ModuleDefinition m) { + public virtual void PostResolve(ModuleDefinition m) { Contract.Requires(m != null); } From 867015b5a0133527362115e597372cc93bfbe460 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 11:07:45 -0600 Subject: [PATCH 03/47] Fixed all dependencies errors --- Source/Dafny/RefinementTransformer.cs | 4 ++-- Source/Dafny/Rewriter.cs | 18 +++++++++--------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 0567c07e0df..27554f4e53e 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -164,7 +164,7 @@ public RefinementTransformer(Program p) public ModuleSignature RefinedSig; // the intention is to use this field only after a successful PreResolve private ModuleSignature refinedSigOpened; - internal override void PreResolve(ModuleDefinition m) { + public override void PreResolve(ModuleDefinition m) { if (m.RefinementQId?.Decl != null) { // There is a refinement parent and it resolved OK RefinedSig = m.RefinementQId.Sig; @@ -485,7 +485,7 @@ public bool ResolvedTypesAreTheSame(Type prev, Type next) { } } - internal override void PostResolve(ModuleDefinition m) { + public override void PostResolve(ModuleDefinition m) { if (m == moduleUnderConstruction) { while (this.postTasks.Count != 0) { var a = postTasks.Dequeue(); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 1523716a59d..3c23ac15df7 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -67,7 +67,7 @@ internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - internal override void PostResolve(ModuleDefinition m) { + public override void PostResolve(ModuleDefinition m) { var splitter = new Triggers.QuantifierSplitter(); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { splitter.Visit(decl); @@ -82,7 +82,7 @@ public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - internal override void PostResolve(ModuleDefinition m) { + public override void PostResolve(ModuleDefinition m) { var forallvisiter = new ForAllStmtVisitor(reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { forallvisiter.Visit(decl, true); @@ -456,7 +456,7 @@ public AutoContractsRewriter(ErrorReporter reporter, BuiltIns builtIns) this.builtIns = builtIns; } - internal override void PreResolve(ModuleDefinition m) { + public override void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { @@ -543,7 +543,7 @@ void ProcessClassPreResolve(ClassDecl cl) { } } - internal override void PostResolve(ModuleDefinition m) { + public override void PostResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { @@ -910,7 +910,7 @@ public OpaqueFunctionRewriter(ErrorReporter reporter) revealOriginal = new Dictionary(); } - internal override void PreResolve(ModuleDefinition m) { + public override void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { if (d is TopLevelDeclWithMembers) { ProcessOpaqueClassFunctions((TopLevelDeclWithMembers)d); @@ -918,7 +918,7 @@ internal override void PreResolve(ModuleDefinition m) { } } - internal override void PostResolve(ModuleDefinition m) { + public override void PostResolve(ModuleDefinition m) { foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { if (decl is Lemma || decl is TwoStateLemma) { var lem = (Method)decl; @@ -1053,7 +1053,7 @@ public AutoReqFunctionRewriter(ErrorReporter reporter) Contract.Requires(reporter != null); } - internal override void PostResolve(ModuleDefinition m) { + public override void PostResolve(ModuleDefinition m) { var components = m.CallGraph.TopologicallySortedComponents(); foreach (var scComponent in components) { // Visit the call graph bottom up, so anything we call already has its prequisites calculated @@ -1416,7 +1416,7 @@ public ProvideRevealAllRewriter(ErrorReporter reporter) Contract.Requires(reporter != null); } - internal override void PreResolve(ModuleDefinition m) { + public override void PreResolve(ModuleDefinition m) { var declarations = m.TopLevelDecls; foreach (var d in declarations) { @@ -1481,7 +1481,7 @@ public TimeLimitRewriter(ErrorReporter reporter) Contract.Requires(reporter != null); } - internal override void PreResolve(ModuleDefinition m) { + public override void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { if (d is TopLevelDeclWithMembers tld) { foreach (MemberDecl member in tld.Members) { From 54218fccb0a2961b616cf0e89928dc0ef1d080c4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 11:37:35 -0600 Subject: [PATCH 04/47] Initial support for /compiler: or -compiler: flag --- Source/Dafny/DafnyOptions.cs | 16 +++++++++++++++ Source/Dafny/Resolver.cs | 38 ++++++++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b8657487ea6..9870af47e36 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -137,6 +137,9 @@ public enum IncludesModes { // Working around the fact that xmlFilename is private public string BoogieXmlFilename = null; + // invariant: All strings of this list are non-empty + public readonly List CompilerBackends = new(); + public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); @@ -232,6 +235,16 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com return true; } + case "compiler": { + if (ps.ConfirmArgumentCount(1)) { + if (args[ps.i].Length > 0) { + CompilerBackends.AddRange(args[ps.i].Split(',').Where(s => s.Length > 0)); + } + } + + return true; + } + case "Main": case "main": { if (ps.ConfirmArgumentCount(1)) { @@ -804,6 +817,9 @@ 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: + (experimental) List of comma-separated DLLs or assemblies that contain at least one + instantiatable class extending Microsoft.Dafny.IRewriter /Main: 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'. diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7660cd57caf..5aba436ada0 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -11,6 +11,8 @@ using System.Linq; using System.Numerics; using System.Diagnostics.Contracts; +using System.IO; +using System.Reflection; using JetBrains.Annotations; using Microsoft.BaseTypes; using Microsoft.Boogie; @@ -436,6 +438,42 @@ public void ResolveProgram(Program prog) { rewriters.Add(new InductionRewriter(reporter)); + if (DafnyOptions.O.CompilerBackends.Count() >= 1) { + foreach (var assemblyPath in DafnyOptions.O.CompilerBackends) { + Assembly compilerBackend; + try { + compilerBackend = Assembly.Load(assemblyPath); + } catch (ArgumentException) { + reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend paths cannot be empty."); + continue; + } catch (FileNotFoundException) { + reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend '{assemblyPath}' could not be found "); + continue; + } catch (FileLoadException e) { + reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend '{assemblyPath}' could not be loaded: {e.Message}"); + continue; + } catch (BadImageFormatException e) { + reporter.Error(MessageSource.Resolver, Token.NoToken, $"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)))) { + var pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter; + if (pluginRewriter == null) { + reporter.Error(MessageSource.Resolver, Token.NoToken, $"[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}'"); + } + } + } + systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); prog.CompileModules.Add(prog.BuiltIns.SystemModule); RevealAllInScope(prog.BuiltIns.SystemModule.TopLevelDecls, systemNameInfo.VisibilityScope); From 8951357c8bcc1ad9b8c660073b400c494a792624 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 13:28:16 -0600 Subject: [PATCH 05/47] Correct way to load an external DLL --- Source/Dafny/Resolver.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5aba436ada0..083351bd3ec 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -442,7 +442,7 @@ public void ResolveProgram(Program prog) { foreach (var assemblyPath in DafnyOptions.O.CompilerBackends) { Assembly compilerBackend; try { - compilerBackend = Assembly.Load(assemblyPath); + compilerBackend = Assembly.LoadFrom(assemblyPath); } catch (ArgumentException) { reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend paths cannot be empty."); continue; From 90d825508b7ce60f0555cf5fbf2e9915e4195b08 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 13:30:08 -0600 Subject: [PATCH 06/47] Better comments --- Source/Dafny/DafnyOptions.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 9870af47e36..e93d0e2e4e9 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -818,7 +818,7 @@ verification outcome This includes lack of support for BigIntegers (aka int), most higher order functions, and advanced features like traits or co-inductive types. /compiler: - (experimental) List of comma-separated DLLs or assemblies that contain at least one + (experimental) List of comma-separated paths to assemblies that contain at least one instantiatable class extending Microsoft.Dafny.IRewriter /Main: The (fully-qualified) name of the method to use as the executable entry point. From 39eca0020a4c95e6138e7e14e160838e6d5b0f0a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 14:15:06 -0600 Subject: [PATCH 07/47] Added a test for the /compiler: option --- Source/Dafny/Reporting.cs | 2 +- .../ExternalResolverTest.cs | 94 +++++++++++++++++++ 2 files changed, 95 insertions(+), 1 deletion(-) create mode 100644 Source/DafnyPipeline.Test/ExternalResolverTest.cs diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 828e3eb2e3a..07f65c674b9 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -153,7 +153,7 @@ public static string TokenToString(IToken tok) { } public abstract class BatchErrorReporter : ErrorReporter { - private readonly Dictionary> allMessages; + protected readonly Dictionary> allMessages; protected BatchErrorReporter() { ErrorsOnly = false; diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs new file mode 100644 index 00000000000..3bf5ef3448e --- /dev/null +++ b/Source/DafnyPipeline.Test/ExternalResolverTest.cs @@ -0,0 +1,94 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using System.Text.Json; +using System.Threading.Tasks; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using Xunit; +using Microsoft.Dafny; + +namespace DafnyPipeline.Test; + +[Collection("External Resolver plug-in tests")] +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. + /// + public async Task GetLibrary(string code) { + var temp = Path.GetTempFileName(); + var compilation = CSharpCompilation.Create("tempAssembly"); + var standardLibraries = new List() + { + "DafnyPipeline", + "System.Runtime", + "Boogie.Core" + }; + compilation = compilation.AddReferences(standardLibraries.Select(fileName => + MetadataReference.CreateFromFile(Assembly.Load(fileName).Location))) + .AddReferences( + MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location)) + .WithOptions( + new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary) + ); + var syntaxTree = CSharpSyntaxTree.ParseText(code); + compilation = compilation.AddSyntaxTrees(syntaxTree); + var assemblyPath = $"{temp}.dll"; + var result = compilation.Emit(assemblyPath); + + var configuration = JsonSerializer.Serialize( + new { + runtimeOptions = new { + tfm = "net6.0", + framework = new { + name = "Microsoft.NETCore.App", + version = "6.0.0", + rollForward = "LatestMinor" + } + } + }, new JsonSerializerOptions() { WriteIndented = true }); + await File.WriteAllTextAsync(temp + ".runtimeconfig.json", configuration + Environment.NewLine); + + Assert.True(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); + return assemblyPath; + } + + class CollectionErrorReporter : BatchErrorReporter { + public string GetLastErrorMessage() { + return allMessages[ErrorLevel.Error][0].message; + } + } + + [Fact] + public async void EnsureItIsPossibleToPluginIRewriter() { + var library = await GetLibrary(@" + using Microsoft.Dafny; + public class ErrorRewriter: IRewriter { + public ErrorRewriter(ErrorReporter reporter) : base(reporter) + {} + + public override void PostResolve(ModuleDefinition m) { + reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); + } + }"); + + var reporter = new CollectionErrorReporter(); + var options = new DafnyOptions(reporter); + options.CompilerBackends.Add(library); + DafnyOptions.Install(options); + + var programString = "function test(): int { 1 }"; + ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDecl(), null); + Microsoft.Dafny.Type.ResetScopes(); + BuiltIns builtIns = new BuiltIns(); + Parser.Parse(programString, "virtual", "virtual", module, builtIns, reporter); + var dafnyProgram = new Program("programName", module, builtIns, reporter); + Main.Resolve(dafnyProgram, reporter); + + Assert.Equal(1, reporter.Count(ErrorLevel.Error)); + Assert.Equal("Impossible to continue", reporter.GetLastErrorMessage()); + } +} \ No newline at end of file From 4b8db033dbbe463a05b4d5e3413d2b54b2f1b4b3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 20 Jan 2022 16:14:39 -0600 Subject: [PATCH 08/47] Support for compiler options in DafnyLanguageServer Display the error on the first token of any program. --- Source/Dafny/DafnyOptions.cs | 2 +- Source/Dafny/Resolver.cs | 18 +++++++++++++----- .../Unit/TextDocumentLoaderTest.cs | 6 +++++- .../Language/CompilerOptions.cs | 16 ++++++++++++++++ .../Language/LanguageServerExtensions.cs | 1 + Source/DafnyLanguageServer/README.md | 9 +++++++++ .../Workspace/LanguageServerExtensions.cs | 4 +++- .../Workspace/TextDocumentLoader.cs | 18 ++++++++++++++---- 8 files changed, 62 insertions(+), 12 deletions(-) create mode 100644 Source/DafnyLanguageServer/Language/CompilerOptions.cs diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index e93d0e2e4e9..ca51d42a9bd 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -138,7 +138,7 @@ public enum IncludesModes { public string BoogieXmlFilename = null; // invariant: All strings of this list are non-empty - public readonly List CompilerBackends = new(); + public List CompilerBackends = new(); public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 083351bd3ec..f4d2c560b4e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -439,21 +439,29 @@ public void ResolveProgram(Program prog) { rewriters.Add(new InductionRewriter(reporter)); if (DafnyOptions.O.CompilerBackends.Count() >= 1) { + IToken GetFirstTopLevelToken() { + return prog.DefaultModuleDef.TopLevelDecls.Select(x => x as ClassDecl) + .Where(x => x != null) + .SelectMany(classDecl => classDecl.Members) + .Where(member => member.tok.line > 0) + .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, Token.NoToken, $"Compiler backend paths cannot be empty."); + reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend paths cannot be empty."); continue; } catch (FileNotFoundException) { - reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend '{assemblyPath}' could not be found "); + reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend '{assemblyPath}' could not be found "); continue; } catch (FileLoadException e) { - reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend '{assemblyPath}' could not be loaded: {e.Message}"); + reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend '{assemblyPath}' could not be loaded: {e.Message}"); continue; } catch (BadImageFormatException e) { - reporter.Error(MessageSource.Resolver, Token.NoToken, $"Compiler backend version of '{assemblyPath}' is incompatible: {e.Message}"); + reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"Compiler backend version of '{assemblyPath}' is incompatible: {e.Message}"); continue; } @@ -461,7 +469,7 @@ public void ResolveProgram(Program prog) { foreach (System.Type type in compilerBackend.GetTypes().Where(t => t.IsAssignableTo(typeof(IRewriter)))) { var pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter; if (pluginRewriter == null) { - reporter.Error(MessageSource.Resolver, Token.NoToken, $"[Internal error] '{type.FullName}' could not be created as an IRewriter"); + reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"[Internal error] '{type.FullName}' could not be created as an IRewriter"); } else { rewriters.Add(pluginRewriter); oneRewriterInstantiated = true; diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index e4f777498dc..3094eb9ad56 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -8,6 +8,7 @@ using System.Threading; using System.Threading.Tasks; using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Options; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit { [TestClass] @@ -20,6 +21,7 @@ public class TextDocumentLoaderTest { private Mock notificationPublisher; private TextDocumentLoader textDocumentLoader; private Mock logger; + private Mock> compilerOptions; [TestInitialize] public void SetUp() { @@ -30,6 +32,7 @@ public void SetUp() { ghostStateDiagnosticCollector = new(); notificationPublisher = new(); logger = new Mock(); + compilerOptions = new Mock>(); textDocumentLoader = TextDocumentLoader.Create( parser.Object, symbolResolver.Object, @@ -37,7 +40,8 @@ public void SetUp() { symbolTableFactory.Object, ghostStateDiagnosticCollector.Object, notificationPublisher.Object, - logger.Object + logger.Object, + compilerOptions.Object ); } diff --git a/Source/DafnyLanguageServer/Language/CompilerOptions.cs b/Source/DafnyLanguageServer/Language/CompilerOptions.cs new file mode 100644 index 00000000000..3b27d252769 --- /dev/null +++ b/Source/DafnyLanguageServer/Language/CompilerOptions.cs @@ -0,0 +1,16 @@ +namespace Microsoft.Dafny.LanguageServer.Language { + /// + /// Options for the resolution and compilation pipeline + /// + public class CompilerOptions { + /// + /// The IConfiguration section of the compiler options. + /// + public const string Section = "Compiler"; + + /// + /// Gets or sets which backends will be targeted so that their resolver can run before verification. + /// + public string Backends { get; set; } = ""; + } +} diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs index 749e74ddc53..0e25f567593 100644 --- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs @@ -25,6 +25,7 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv return services .Configure(configuration.GetSection(VerifierOptions.Section)) .Configure(configuration.GetSection(GhostOptions.Section)) + .Configure(configuration.GetSection(CompilerOptions.Section)) .AddSingleton(serviceProvider => DafnyLangParser.Create(serviceProvider.GetRequiredService>())) .AddSingleton() .AddSingleton(CreateVerifier) diff --git a/Source/DafnyLanguageServer/README.md b/Source/DafnyLanguageServer/README.md index 636c54e42d5..4fab247221b 100644 --- a/Source/DafnyLanguageServer/README.md +++ b/Source/DafnyLanguageServer/README.md @@ -75,3 +75,12 @@ Options provided through the command line have higher priority than the options # Default: true (mark the statements) --ghost:markStatements=true ``` + +### Compilation Backends + +```sh +# Provides a comma-separated list of paths to assemblies +# that contain an instantiatable IRewrite that is used during resolution +# Default: "" (nothing extra is loaded) +--compiler:backends= +``` diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs index 462c56e3159..e0b1d9c7438 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs @@ -6,6 +6,7 @@ using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Server; using System; +using Microsoft.Extensions.Options; namespace Microsoft.Dafny.LanguageServer.Workspace { /// @@ -44,7 +45,8 @@ private static TextDocumentLoader CreateTextDocumentLoader(IServiceProvider serv services.GetRequiredService(), services.GetRequiredService(), services.GetRequiredService(), - services.GetRequiredService() + services.GetRequiredService(), + services.GetRequiredService>() ); } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index c07eee6dcd0..f5ccc073d64 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -10,6 +10,7 @@ using System.Threading; using System.Threading.Tasks; using Microsoft.Extensions.Logging; +using Microsoft.Extensions.Options; namespace Microsoft.Dafny.LanguageServer.Workspace { /// @@ -32,6 +33,7 @@ public class TextDocumentLoader : ITextDocumentLoader { private readonly ICompilationStatusNotificationPublisher notificationPublisher; private readonly ILoggerFactory loggerFactory; private readonly BlockingCollection requestQueue = new(); + private readonly IOptions compilerOptions; private TextDocumentLoader( ILoggerFactory loggerFactory, @@ -40,7 +42,8 @@ private TextDocumentLoader( IProgramVerifier verifier, ISymbolTableFactory symbolTableFactory, IGhostStateDiagnosticCollector ghostStateDiagnosticCollector, - ICompilationStatusNotificationPublisher notificationPublisher) { + ICompilationStatusNotificationPublisher notificationPublisher, + IOptions compilerOptions) { this.parser = parser; this.symbolResolver = symbolResolver; this.verifier = verifier; @@ -48,6 +51,7 @@ private TextDocumentLoader( this.ghostStateDiagnosticCollector = ghostStateDiagnosticCollector; this.notificationPublisher = notificationPublisher; this.loggerFactory = loggerFactory; + this.compilerOptions = compilerOptions; } public static TextDocumentLoader Create( @@ -57,9 +61,10 @@ public static TextDocumentLoader Create( ISymbolTableFactory symbolTableFactory, IGhostStateDiagnosticCollector ghostStateDiagnosticCollector, ICompilationStatusNotificationPublisher notificationPublisher, - ILoggerFactory loggerFactory - ) { - var loader = new TextDocumentLoader(loggerFactory, parser, symbolResolver, verifier, symbolTableFactory, ghostStateDiagnosticCollector, notificationPublisher); + ILoggerFactory loggerFactory, + IOptions compilerOptions + ) { + var loader = new TextDocumentLoader(loggerFactory, parser, symbolResolver, verifier, symbolTableFactory, ghostStateDiagnosticCollector, notificationPublisher, compilerOptions); var loadThread = new Thread(loader.Run, MaxStackSize) { IsBackground = true }; loadThread.Start(); return loader; @@ -111,6 +116,11 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { notificationPublisher.SendStatusNotification(textDocument, CompilationStatus.ParsingFailed); return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger(), textDocument, errorReporter, program, loadCanceled: false); } + + if (compilerOptions.Value.Backends.Length > 0) { + DafnyOptions.O.CompilerBackends = compilerOptions.Value.Backends.Split(",").Where(x => x.Length > 0).ToList(); + } + var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, cancellationToken); var symbolTable = symbolTableFactory.CreateFrom(program, compilationUnit, cancellationToken); if (errorReporter.HasErrors) { From 3d9553c753e6a570120ebd246c62418075cd24c1 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 21 Jan 2022 11:31:33 -0600 Subject: [PATCH 09/47] Plugin for everything instead of just resolution. --- Source/Dafny/DafnyOptions.cs | 20 +++++++++---- Source/Dafny/Resolver.cs | 29 ++----------------- .../Unit/TextDocumentLoaderTest.cs | 6 ++-- .../{CompilerOptions.cs => DafnyOptions.cs} | 6 ++-- .../Language/LanguageServerExtensions.cs | 2 +- Source/DafnyLanguageServer/README.md | 6 ++-- .../Workspace/LanguageServerExtensions.cs | 2 +- .../Workspace/TextDocumentLoader.cs | 12 ++++---- .../ExternalResolverTest.cs | 6 ++-- 9 files changed, 37 insertions(+), 52 deletions(-) rename Source/DafnyLanguageServer/Language/{CompilerOptions.cs => DafnyOptions.cs} (75%) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index ca51d42a9bd..b11043520a4 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/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 CompilerBackends = new(); + public List 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: +/plugins: (experimental) List of comma-separated paths to assemblies that contain at least one instantiatable class extending Microsoft.Dafny.IRewriter /Main: diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f4d2c560b4e..6ad6542269e 100644 --- a/Source/Dafny/Resolver.cs +++ b/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}'"); - } } } diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 3094eb9ad56..92c8f7e1fd2 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -21,7 +21,7 @@ public class TextDocumentLoaderTest { private Mock notificationPublisher; private TextDocumentLoader textDocumentLoader; private Mock logger; - private Mock> compilerOptions; + private Mock> dafnyPluginOptions; [TestInitialize] public void SetUp() { @@ -32,7 +32,7 @@ public void SetUp() { ghostStateDiagnosticCollector = new(); notificationPublisher = new(); logger = new Mock(); - compilerOptions = new Mock>(); + dafnyPluginOptions = new Mock>(); textDocumentLoader = TextDocumentLoader.Create( parser.Object, symbolResolver.Object, @@ -41,7 +41,7 @@ public void SetUp() { ghostStateDiagnosticCollector.Object, notificationPublisher.Object, logger.Object, - compilerOptions.Object + dafnyPluginOptions.Object ); } diff --git a/Source/DafnyLanguageServer/Language/CompilerOptions.cs b/Source/DafnyLanguageServer/Language/DafnyOptions.cs similarity index 75% rename from Source/DafnyLanguageServer/Language/CompilerOptions.cs rename to Source/DafnyLanguageServer/Language/DafnyOptions.cs index 3b27d252769..f9575cb8537 100644 --- a/Source/DafnyLanguageServer/Language/CompilerOptions.cs +++ b/Source/DafnyLanguageServer/Language/DafnyOptions.cs @@ -2,15 +2,15 @@ /// /// Options for the resolution and compilation pipeline /// - public class CompilerOptions { + public class DafnyPluginsOptions { /// /// The IConfiguration section of the compiler options. /// - public const string Section = "Compiler"; + public const string Section = "Dafny"; /// /// Gets or sets which backends will be targeted so that their resolver can run before verification. /// - public string Backends { get; set; } = ""; + public string Plugins { get; set; } = ""; } } diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs index 0e25f567593..7db8c81b07f 100644 --- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs @@ -25,7 +25,7 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv return services .Configure(configuration.GetSection(VerifierOptions.Section)) .Configure(configuration.GetSection(GhostOptions.Section)) - .Configure(configuration.GetSection(CompilerOptions.Section)) + .Configure(configuration.GetSection(DafnyPluginsOptions.Section)) .AddSingleton(serviceProvider => DafnyLangParser.Create(serviceProvider.GetRequiredService>())) .AddSingleton() .AddSingleton(CreateVerifier) diff --git a/Source/DafnyLanguageServer/README.md b/Source/DafnyLanguageServer/README.md index 4fab247221b..842226b76d5 100644 --- a/Source/DafnyLanguageServer/README.md +++ b/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= ``` diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs index e0b1d9c7438..9663600480c 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs @@ -46,7 +46,7 @@ private static TextDocumentLoader CreateTextDocumentLoader(IServiceProvider serv services.GetRequiredService(), services.GetRequiredService(), services.GetRequiredService(), - services.GetRequiredService>() + services.GetRequiredService>() ); } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index f5ccc073d64..6762609c9f2 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -33,7 +33,7 @@ public class TextDocumentLoader : ITextDocumentLoader { private readonly ICompilationStatusNotificationPublisher notificationPublisher; private readonly ILoggerFactory loggerFactory; private readonly BlockingCollection requestQueue = new(); - private readonly IOptions compilerOptions; + private readonly IOptions dafnyPluginsOptions; private TextDocumentLoader( ILoggerFactory loggerFactory, @@ -43,7 +43,7 @@ private TextDocumentLoader( ISymbolTableFactory symbolTableFactory, IGhostStateDiagnosticCollector ghostStateDiagnosticCollector, ICompilationStatusNotificationPublisher notificationPublisher, - IOptions compilerOptions) { + IOptions dafnyPluginsOptions) { this.parser = parser; this.symbolResolver = symbolResolver; this.verifier = verifier; @@ -51,7 +51,7 @@ private TextDocumentLoader( 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 + IOptions 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(), 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); diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs index 3bf5ef3448e..9ca4cb20d7a 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/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. /// - public async Task GetLibrary(string code) { + public async Task GetLibrary(string code) { var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create("tempAssembly"); var standardLibraries = new List() @@ -53,7 +53,7 @@ public async Task 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 }"; From 36645266377b8dc97c80d26230a32fca6cab08ef Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 21 Jan 2022 12:03:25 -0600 Subject: [PATCH 10/47] Fixed multiple loading of the option --- Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 6762609c9f2..52dea01ca8b 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -117,7 +117,7 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger(), textDocument, errorReporter, program, loadCanceled: false); } - if (dafnyPluginsOptions.Value.Plugins.Length > 0) { + if (dafnyPluginsOptions.Value.Plugins.Length > 0 && DafnyOptions.O.Plugins.Count == 0) { DafnyOptions.O.Parse(new[] { "-plugins:" + dafnyPluginsOptions.Value.Plugins }); } From 453942497790c459d938d4da0479d41aae614524 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 21 Jan 2022 12:35:57 -0600 Subject: [PATCH 11/47] Better error reporting --- Source/Dafny/AST/DafnyAst.cs | 8 ++++++++ Source/Dafny/Resolver.cs | 18 ++++++++---------- .../Workspace/TextDocumentLoader.cs | 6 +++++- 3 files changed, 21 insertions(+), 11 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index a47e8f3734a..752af5acc45 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -75,6 +75,14 @@ public string Name { } } } + + public IToken GetFirstTopLevelToken() { + return DefaultModuleDef.TopLevelDecls.Select(x => x as ClassDecl) + .Where(x => x != null) + .SelectMany(classDecl => classDecl.Members) + .Where(member => member.tok.line > 0) + .Select(member => member.tok).FirstOrDefault(Token.NoToken); + } } public class Include : IComparable { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6ad6542269e..ce120f23c2c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -439,19 +439,17 @@ public void ResolveProgram(Program prog) { rewriters.Add(new InductionRewriter(reporter)); if (DafnyOptions.O.Plugins.Count() >= 1) { - IToken GetFirstTopLevelToken() { - return prog.DefaultModuleDef.TopLevelDecls.Select(x => x as ClassDecl) - .Where(x => x != null) - .SelectMany(classDecl => classDecl.Members) - .Where(member => member.tok.line > 0) - .Select(member => member.tok).FirstOrDefault(Token.NoToken); - } - 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; + IRewriter pluginRewriter = null; + Exception e = null; + try { + pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter; + } catch (Exception _e) { + e = _e; + } if (pluginRewriter == null) { - reporter.Error(MessageSource.Resolver, GetFirstTopLevelToken(), $"[Internal error] '{type.FullName}' could not be created as an IRewriter"); + reporter.Error(MessageSource.Resolver, prog.GetFirstTopLevelToken(), $"[Internal error] '{type.FullName}' could not be created as an IRewriter" + (e != null ? ":" + e.ToString() : "")); } else { rewriters.Add(pluginRewriter); } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 52dea01ca8b..d53db7dc520 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -118,7 +118,11 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { } if (dafnyPluginsOptions.Value.Plugins.Length > 0 && DafnyOptions.O.Plugins.Count == 0) { - DafnyOptions.O.Parse(new[] { "-plugins:" + dafnyPluginsOptions.Value.Plugins }); + try { + DafnyOptions.O.Parse(new[] { "-plugins:" + dafnyPluginsOptions.Value.Plugins }); + } catch (Exception e) { + errorReporter.Error(MessageSource.Parser, program.GetFirstTopLevelToken(), "Error while instantiating the plugins:" + e.ToString()); + } } var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, cancellationToken); From 27bd135344515a0f4f9d132904940665d8204092 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 21 Jan 2022 14:14:42 -0600 Subject: [PATCH 12/47] Removed useless code. --- Source/DafnyPipeline.Test/ExternalResolverTest.cs | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs index 9ca4cb20d7a..4fde1e80c0f 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/Source/DafnyPipeline.Test/ExternalResolverTest.cs @@ -39,19 +39,6 @@ public async Task GetLibrary(string code) { var assemblyPath = $"{temp}.dll"; var result = compilation.Emit(assemblyPath); - var configuration = JsonSerializer.Serialize( - new { - runtimeOptions = new { - tfm = "net6.0", - framework = new { - name = "Microsoft.NETCore.App", - version = "6.0.0", - rollForward = "LatestMinor" - } - } - }, new JsonSerializerOptions() { WriteIndented = true }); - await File.WriteAllTextAsync(temp + ".runtimeconfig.json", configuration + Environment.NewLine); - Assert.True(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); return Assembly.LoadFrom(assemblyPath); } From 2b87a903dc303e69f677c76fefdce585b1f4cc01 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 21 Jan 2022 14:27:19 -0600 Subject: [PATCH 13/47] More debugging code (revert this commit) --- Source/Dafny/DafnyOptions.cs | 3 +++ Source/Dafny/Resolver.cs | 2 ++ 2 files changed, 5 insertions(+) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b11043520a4..dc1c6af710a 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -240,11 +240,14 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com var pluginsList = args[ps.i]; if (pluginsList.Length > 0) { foreach (var pluginPath in pluginsList.Split(',').Where(s => s.Length > 0)) { + Console.WriteLine($"Loading {pluginPath}..."); var pluginAssembly = Assembly.LoadFrom(pluginPath); + Console.WriteLine($"Loaded {pluginPath}..."); if (!pluginAssembly.GetTypes().Any(t => t.IsAssignableTo(typeof(IRewriter)))) { throw new Exception($"Plugin {pluginPath} does not contain any Microsoft.Dafny.IRewriter"); } + Console.WriteLine($"At least one IRewriter in {pluginPath}..."); Plugins.Add(pluginAssembly); } } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index ce120f23c2c..d704e22bf18 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -444,7 +444,9 @@ public void ResolveProgram(Program prog) { IRewriter pluginRewriter = null; Exception e = null; try { + Console.WriteLine($"Creating instance..."); pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter; + Console.WriteLine($"Created instance..."); } catch (Exception _e) { e = _e; } From 98b6d97a5492fe8d46f9b5b25a967dd484ee8dc8 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 21 Jan 2022 15:13:19 -0600 Subject: [PATCH 14/47] Revert "More debugging code (revert this commit)" This reverts commit 2b87a903dc303e69f677c76fefdce585b1f4cc01. --- Source/Dafny/DafnyOptions.cs | 3 --- Source/Dafny/Resolver.cs | 2 -- 2 files changed, 5 deletions(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index dc1c6af710a..b11043520a4 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -240,14 +240,11 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com var pluginsList = args[ps.i]; if (pluginsList.Length > 0) { foreach (var pluginPath in pluginsList.Split(',').Where(s => s.Length > 0)) { - Console.WriteLine($"Loading {pluginPath}..."); var pluginAssembly = Assembly.LoadFrom(pluginPath); - Console.WriteLine($"Loaded {pluginPath}..."); if (!pluginAssembly.GetTypes().Any(t => t.IsAssignableTo(typeof(IRewriter)))) { throw new Exception($"Plugin {pluginPath} does not contain any Microsoft.Dafny.IRewriter"); } - Console.WriteLine($"At least one IRewriter in {pluginPath}..."); Plugins.Add(pluginAssembly); } } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d704e22bf18..ce120f23c2c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -444,9 +444,7 @@ public void ResolveProgram(Program prog) { IRewriter pluginRewriter = null; Exception e = null; try { - Console.WriteLine($"Creating instance..."); pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter; - Console.WriteLine($"Created instance..."); } catch (Exception _e) { e = _e; } From 93a170cb8bd3fdd076c60581e1c8915b417f82f6 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 25 Jan 2022 15:27:07 -0600 Subject: [PATCH 15/47] WIP: adding a new test --- Source/Dafny/Rewriter.cs | 3 + .../Various/ExternalResolverTest.cs | 96 +++++++++++++++++++ 2 files changed, 99 insertions(+) create mode 100644 Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 3c23ac15df7..de189a50f44 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -8,6 +8,9 @@ using IToken = Microsoft.Boogie.IToken; namespace Microsoft.Dafny { + /// + /// Class that plugins should extend, in order to provide an extra IRewriter to the pipeline. + /// public abstract class IRewriter { protected readonly ErrorReporter reporter; diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs new file mode 100644 index 00000000000..cb30b74c8fe --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs @@ -0,0 +1,96 @@ +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using System.Threading.Tasks; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using System; +using Microsoft.Dafny.LanguageServer.Language; +using Microsoft.VisualStudio.TestTools.UnitTesting; +using System.Collections.Generic; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.Boogie; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Microsoft.Extensions.Configuration; +using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Protocol; +using OmniSharp.Extensions.LanguageServer.Protocol.Client; +using OmniSharp.Extensions.LanguageServer.Protocol.Document; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; + +[TestClass] +public class ExternalResolverTest : DafnyLanguageServerTestBase { + private ILanguageClient client; + protected DiagnosticsReceiver diagnosticReceiver; + private Assembly library, + + + [TestInitialize] + public async Task SetUp() { + diagnosticReceiver = new(); + library = await GetLibrary(@" + using Microsoft.Dafny; + public class ErrorRewriter: IRewriter { + public ErrorRewriter(ErrorReporter reporter) : base(reporter) + {} + + public override void PostResolve(ModuleDefinition m) { + reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); + } + }"); + this.configuration = await CreateConfiguration() + client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); + } + + protected override IConfiguration CreateConfiguration() { + return new ConfigurationBuilder().AddCommandLine( + new string[] { "--dafny:plugins:" + this.library.Location }).Build(); + } + + /// + /// 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. + /// + public async Task GetLibrary(string code) { + var temp = Path.GetTempFileName(); + var compilation = CSharpCompilation.Create("tempAssembly"); + var standardLibraries = new List() + { + "DafnyPipeline", + "System.Runtime", + "Boogie.Core" + }; + compilation = compilation.AddReferences(standardLibraries.Select(fileName => + MetadataReference.CreateFromFile(Assembly.Load(fileName).Location))) + .AddReferences( + MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location)) + .WithOptions( + new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary) + ); + var syntaxTree = CSharpSyntaxTree.ParseText(code); + compilation = compilation.AddSyntaxTrees(syntaxTree); + var assemblyPath = $"{temp}.dll"; + var result = compilation.Emit(assemblyPath); + + Assert.IsTrue(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); + return Assembly.LoadFrom(assemblyPath); + } + + [TestMethod] + public async Task EnsureItIsPossibleToPluginIRewriter() { + var documentItem = CreateTestDocument("function test(): int { 1 }"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var resolutionReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); + Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); + var diagnostics = resolutionReport.Diagnostics.ToArray(); + Assert.AreEqual(1, diagnostics.Length); + Assert.AreEqual("Impossible to continue", diagnostics[0].Message); + Assert.AreEqual(new Range((7, 4), (7, 15)), diagnostics[0].Range); + } +} \ No newline at end of file From 31578e82fb2477f4bbc9e9f42d22156f599bc4cd Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 25 Jan 2022 15:52:37 -0600 Subject: [PATCH 16/47] Fixed the test of DafnyLanguageServer to prove plugins work. --- .../Various/ExternalResolverTest.cs | 10 ++++------ .../Workspace/LanguageServerExtensions.cs | 1 + 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs index cb30b74c8fe..57f06daa6bc 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs @@ -27,9 +27,8 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; [TestClass] public class ExternalResolverTest : DafnyLanguageServerTestBase { private ILanguageClient client; - protected DiagnosticsReceiver diagnosticReceiver; - private Assembly library, - + private DiagnosticsReceiver diagnosticReceiver; + private Assembly library; [TestInitialize] public async Task SetUp() { @@ -44,13 +43,12 @@ public override void PostResolve(ModuleDefinition m) { reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); } }"); - this.configuration = await CreateConfiguration() client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); } protected override IConfiguration CreateConfiguration() { return new ConfigurationBuilder().AddCommandLine( - new string[] { "--dafny:plugins:" + this.library.Location }).Build(); + new[] { "--dafny:plugins=" + this.library.Location }).Build(); } /// @@ -91,6 +89,6 @@ public async Task EnsureItIsPossibleToPluginIRewriter() { var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Impossible to continue", diagnostics[0].Message); - Assert.AreEqual(new Range((7, 4), (7, 15)), diagnostics[0].Range); + Assert.AreEqual(new Range((-1, -1), (-1, 29)), diagnostics[0].Range); } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs index 9663600480c..a5694c2a2b7 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs @@ -26,6 +26,7 @@ public static LanguageServerOptions WithDafnyWorkspace(this LanguageServerOption private static IServiceCollection WithDafnyWorkspace(this IServiceCollection services, IConfiguration configuration) { return services .Configure(configuration.GetSection(DocumentOptions.Section)) + .Configure(configuration.GetSection(DafnyPluginsOptions.Section)) .AddSingleton() .AddSingleton(serviceProvider => DafnyLangParser.Create(serviceProvider.GetRequiredService>())) .AddSingleton(CreateTextDocumentLoader) From 3b82af73ce396c2ef8d45660b5b429ea606fe6b2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 25 Jan 2022 16:41:29 -0600 Subject: [PATCH 17/47] Crystal clear API documentation for Resolver plugins --- Source/Dafny/AST/DafnyAst.cs | 14 +- Source/Dafny/DafnyOptions.cs | 1 - Source/Dafny/RefinementTransformer.cs | 222 +++++++++++++------------- Source/Dafny/Resolver.cs | 8 +- Source/Dafny/Rewriter.cs | 114 +++++++++---- 5 files changed, 211 insertions(+), 148 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 752af5acc45..065630de1ba 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -77,11 +77,7 @@ public string Name { } public IToken GetFirstTopLevelToken() { - return DefaultModuleDef.TopLevelDecls.Select(x => x as ClassDecl) - .Where(x => x != null) - .SelectMany(classDecl => classDecl.Members) - .Where(member => member.tok.line > 0) - .Select(member => member.tok).FirstOrDefault(Token.NoToken); + return DefaultModuleDef.GetFirstTopLevelToken(); } } @@ -4231,6 +4227,14 @@ public bool IsEssentiallyEmptyModuleBody() { } return true; } + + public IToken GetFirstTopLevelToken() { + return TopLevelDecls.Select(x => x as ClassDecl) + .Where(x => x != null) + .SelectMany(classDecl => classDecl.Members) + .Where(member => member.tok.line > 0) + .Select(member => member.tok).FirstOrDefault(Token.NoToken); + } } public class DefaultModuleDecl : ModuleDefinition { diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index faf5d6eaa5f..63916bc4cf6 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -136,7 +136,6 @@ public enum IncludesModes { // Working around the fact that xmlFilename is private public string BoogieXmlFilename = null; - // invariant: All strings of this list are non-empty public List Plugins = new(); public virtual TestGenerationOptions TestGenOptions => diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 27554f4e53e..240a20249f6 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -183,7 +183,7 @@ public override void PreResolve(ModuleDefinition m) { string message = mdecl.Opened ? "{0} in {1} cannot be imported with \"opened\" because it does not match the corresponding import in the refinement base {2}." : "{0} in {1} must be imported with \"opened\" to match the corresponding import in its refinement base {2}."; - reporter.Error(MessageSource.RefinementTransformer, m.tok, message, im.Name, m.Name, + Reporter.Error(MessageSource.RefinementTransformer, m.tok, message, im.Name, m.Name, m.RefinementQId.ToString()); } } @@ -235,9 +235,9 @@ void PreResolveWorker(ModuleDefinition m) { MergeTopLevelDecls(m, nw, d, index); } else if (nw is TypeSynonymDecl) { var msg = $"a type synonym ({nw.Name}) is not allowed to replace a {d.WhatKind} from the refined module ({m.RefinementQId}), even if it denotes the same type"; - reporter.Error(MessageSource.RefinementTransformer, nw.tok, msg); + Reporter.Error(MessageSource.RefinementTransformer, nw.tok, msg); } else if (!(d is AbstractModuleDecl)) { - reporter.Error(MessageSource.RefinementTransformer, nw.tok, $"to redeclare and refine declaration '{d.Name}' from module '{m.RefinementQId}', you must use the refining (`...`) notation"); + Reporter.Error(MessageSource.RefinementTransformer, nw.tok, $"to redeclare and refine declaration '{d.Name}' from module '{m.RefinementQId}', you must use the refining (`...`) notation"); } } } @@ -263,14 +263,14 @@ private void CheckSuperflousRefiningMarks(List topLevelDecls, List Contract.Requires(excludeList != null); foreach (var d in topLevelDecls) { if (d.IsRefining && !excludeList.Contains(d.Name)) { - reporter.Error(MessageSource.RefinementTransformer, d.tok, $"declaration '{d.Name}' indicates refining (notation `...`), but does not refine anything"); + Reporter.Error(MessageSource.RefinementTransformer, d.tok, $"declaration '{d.Name}' indicates refining (notation `...`), but does not refine anything"); } } } private void MergeModuleExports(ModuleExportDecl nw, ModuleExportDecl d) { if (nw.IsDefault != d.IsDefault) { - reporter.Error(MessageSource.RefinementTransformer, nw, "can't change if a module export is default ({0})", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "can't change if a module export is default ({0})", nw.Name); } nw.Exports.AddRange(d.Exports); @@ -282,69 +282,69 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec if (d is ModuleDecl) { if (!(nw is ModuleDecl)) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); } else if (d is ModuleExportDecl) { if (!(nw is ModuleExportDecl)) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module export ({0}) must refine another export", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "a module export ({0}) must refine another export", nw.Name); } else { MergeModuleExports((ModuleExportDecl)nw, (ModuleExportDecl)d); } } else if (!(d is AbstractModuleDecl)) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name); } else { // check that the new module refines the previous declaration if (!CheckIsRefinement((ModuleDecl)nw, (AbstractModuleDecl)d)) { - reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name); } } } else if (d is OpaqueTypeDecl) { if (nw is ModuleDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); } else { var od = (OpaqueTypeDecl)d; if (nw is OpaqueTypeDecl) { if (od.SupportsEquality != ((OpaqueTypeDecl)nw).SupportsEquality) { - reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name); } if (od.Characteristics.HasCompiledValue != ((OpaqueTypeDecl)nw).Characteristics.HasCompiledValue) { - reporter.Error(MessageSource.RefinementTransformer, nw.tok, "type declaration '{0}' is not allowed to change the requirement of supporting auto-initialization", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw.tok, "type declaration '{0}' is not allowed to change the requirement of supporting auto-initialization", nw.Name); } else if (od.Characteristics.IsNonempty != ((OpaqueTypeDecl)nw).Characteristics.IsNonempty) { - reporter.Error(MessageSource.RefinementTransformer, nw.tok, "type declaration '{0}' is not allowed to change the requirement of being nonempty", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw.tok, "type declaration '{0}' is not allowed to change the requirement of being nonempty", nw.Name); } } else { if (od.SupportsEquality) { if (nw is ClassDecl || nw is NewtypeDecl) { // fine } else if (nw is CoDatatypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype"); + Reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype"); } else { Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl); // Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has - // taken place, so we defer it until the PostResolve phase. + // taken place, so we defer it until the PostResolveIntermediate phase. var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); postTasks.Enqueue(() => { if (!udt.SupportsEquality) { - reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support equality, is used to refine an opaque type with equality support", udt.Name); + Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support equality, is used to refine an opaque type with equality support", udt.Name); } }); } } if (od.Characteristics.HasCompiledValue) { // We need to figure out if the new type supports auto-initialization. But we won't know about that until resolution has - // taken place, so we defer it until the PostResolve phase. + // taken place, so we defer it until the PostResolveIntermediate phase. var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); postTasks.Enqueue(() => { if (!udt.HasCompilableValue) { - reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support auto-initialization, is used to refine an opaque type that expects auto-initialization", udt.Name); + Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which does not support auto-initialization, is used to refine an opaque type that expects auto-initialization", udt.Name); } }); } else if (od.Characteristics.IsNonempty) { // We need to figure out if the new type is nonempty. But we won't know about that until resolution has - // taken place, so we defer it until the PostResolve phase. + // taken place, so we defer it until the PostResolveIntermediate phase. var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); postTasks.Enqueue(() => { if (!udt.IsNonempty) { - reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which may be empty, is used to refine an opaque type expected to be nonempty", udt.Name); + Reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}', which may be empty, is used to refine an opaque type expected to be nonempty", udt.Name); } }); } @@ -352,7 +352,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec if (nw is TopLevelDeclWithMembers) { m.TopLevelDecls[index] = MergeClass((TopLevelDeclWithMembers)nw, od); } else if (od.Members.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw, + Reporter.Error(MessageSource.RefinementTransformer, nw, "a {0} ({1}) cannot declare members, so it cannot refine an opaque type with members", nw.WhatKind, nw.Name); } else { @@ -360,36 +360,36 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec } } } else if (nw is OpaqueTypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, + Reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); } else if ((d is IndDatatypeDecl && nw is IndDatatypeDecl) || (d is CoDatatypeDecl && nw is CoDatatypeDecl)) { m.TopLevelDecls[index] = MergeClass((DatatypeDecl)nw, (DatatypeDecl)d); } else if (nw is DatatypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (d is NewtypeDecl && nw is NewtypeDecl) { m.TopLevelDecls[index] = MergeClass((NewtypeDecl)nw, (NewtypeDecl)d); } else if (nw is NewtypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (nw is IteratorDecl) { if (d is IteratorDecl) { m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); } else { - reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); } } else if (nw is TraitDecl) { if (d is TraitDecl) { m.TopLevelDecls[index] = MergeClass((TraitDecl)nw, (TraitDecl)d); } else { - reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is ClassDecl) { if (d is ClassDecl && !(d is TraitDecl)) { m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); } else { - reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is TypeSynonymDecl && d is TypeSynonymDecl && ((TypeSynonymDecl)nw).Rhs != null && ((TypeSynonymDecl)d).Rhs != null) { - reporter.Error(MessageSource.RefinementTransformer, d, + Reporter.Error(MessageSource.RefinementTransformer, d, "a type ({0}) in a refining module may not replace an already defined type (even with the same value)", d.Name); } else { @@ -409,7 +409,7 @@ public bool CheckIsRefinement(ModuleDecl derived, AbstractModuleDecl original) { } else if (derived is AbstractModuleDecl) { exports = new HashSet(((AbstractModuleDecl)derived).Exports.ConvertAll(t => t.val)); } else { - reporter.Error(MessageSource.RefinementTransformer, derived, "a module ({0}) can only be refined by an alias module or a module facade", original.Name); + Reporter.Error(MessageSource.RefinementTransformer, derived, "a module ({0}) can only be refined by an alias module or a module facade", original.Name); return false; } var oexports = new HashSet(original.Exports.ConvertAll(t => t.val)); @@ -485,7 +485,7 @@ public bool ResolvedTypesAreTheSame(Type prev, Type next) { } } - public override void PostResolve(ModuleDefinition m) { + public override void PostResolveIntermediate(ModuleDefinition m) { if (m == moduleUnderConstruction) { while (this.postTasks.Count != 0) { var a = postTasks.Dequeue(); @@ -621,25 +621,25 @@ IteratorDecl MergeIterator(IteratorDecl nw, IteratorDecl prev) { Contract.Requires(prev != null); if (nw.Requires.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw.Requires[0].E.tok, "a refining iterator is not allowed to add preconditions"); + Reporter.Error(MessageSource.RefinementTransformer, nw.Requires[0].E.tok, "a refining iterator is not allowed to add preconditions"); } if (nw.YieldRequires.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw.YieldRequires[0].E.tok, "a refining iterator is not allowed to add yield preconditions"); + Reporter.Error(MessageSource.RefinementTransformer, nw.YieldRequires[0].E.tok, "a refining iterator is not allowed to add yield preconditions"); } if (nw.Reads.Expressions.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw.Reads.Expressions[0].E.tok, "a refining iterator is not allowed to extend the reads clause"); + Reporter.Error(MessageSource.RefinementTransformer, nw.Reads.Expressions[0].E.tok, "a refining iterator is not allowed to extend the reads clause"); } if (nw.Modifies.Expressions.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw.Modifies.Expressions[0].E.tok, "a refining iterator is not allowed to extend the modifies clause"); + Reporter.Error(MessageSource.RefinementTransformer, nw.Modifies.Expressions[0].E.tok, "a refining iterator is not allowed to extend the modifies clause"); } if (nw.Decreases.Expressions.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw.Decreases.Expressions[0].tok, "a refining iterator is not allowed to extend the decreases clause"); + Reporter.Error(MessageSource.RefinementTransformer, nw.Decreases.Expressions[0].tok, "a refining iterator is not allowed to extend the decreases clause"); } if (nw.SignatureIsOmitted) { Contract.Assert(nw.Ins.Count == 0); Contract.Assert(nw.Outs.Count == 0); - reporter.Info(MessageSource.RefinementTransformer, nw.SignatureEllipsis, Printer.IteratorSignatureToString(prev)); + Reporter.Info(MessageSource.RefinementTransformer, nw.SignatureEllipsis, Printer.IteratorSignatureToString(prev)); } else { CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "iterator"); CheckAgreement_Parameters(nw.tok, prev.Ins, nw.Ins, nw.Name, "iterator", "in-parameter"); @@ -705,17 +705,17 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM var newConst = (ConstantField)nwMember; var origConst = member as ConstantField; if (origConst == null) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const declaration ({0}) in a refining class ({1}) must replace a const in the refinement base", nwMember.Name, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const declaration ({0}) in a refining class ({1}) must replace a const in the refinement base", nwMember.Name, nw.Name); } else if (!(newConst.Type is InferredTypeProxy) && !TypesAreSyntacticallyEqual(newConst.Type, origConst.Type)) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "the type of a const declaration ({0}) in a refining class ({1}) must be syntactically the same as for the const being refined", nwMember.Name, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "the type of a const declaration ({0}) in a refining class ({1}) must be syntactically the same as for the const being refined", nwMember.Name, nw.Name); } else if (newConst.Rhs != null && origConst.Rhs != null) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const re-declaration ({0}) can give an initializing expression only if the const in the refinement base does not", nwMember.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const re-declaration ({0}) can give an initializing expression only if the const in the refinement base does not", nwMember.Name); } else if (newConst.HasStaticKeyword != origConst.HasStaticKeyword) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const in a refining module cannot be changed from static to non-static or vice versa: {0}", nwMember.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const in a refining module cannot be changed from static to non-static or vice versa: {0}", nwMember.Name); } else if (origConst.IsGhost && !newConst.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const re-declaration ({0}) is not allowed to un-ghostify the const", nwMember.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const re-declaration ({0}) is not allowed to un-ghostify the const", nwMember.Name); } else if (newConst.Rhs == null && origConst.IsGhost == newConst.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const re-declaration ({0}) must be to ghostify the const{1}", nwMember.Name, origConst.Rhs == null ? " or to provide an initializing expression" : ""); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a const re-declaration ({0}) must be to ghostify the const{1}", nwMember.Name, origConst.Rhs == null ? " or to provide an initializing expression" : ""); } nwMember.RefinementBase = member; // we may need to clone the given const declaration if either its type or initializing expression was omitted @@ -729,11 +729,11 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM } else if (nwMember is Field) { if (!(member is Field) || member is ConstantField) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a field declaration ({0}) in a refining class ({1}) must replace a field in the refinement base", nwMember.Name, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a field declaration ({0}) in a refining class ({1}) must replace a field in the refinement base", nwMember.Name, nw.Name); } else if (!TypesAreSyntacticallyEqual(((Field)nwMember).Type, ((Field)member).Type)) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a field declaration ({0}) in a refining class ({1}) must repeat the syntactically same type as the field has in the refinement base", nwMember.Name, nw.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a field declaration ({0}) in a refining class ({1}) must repeat the syntactically same type as the field has in the refinement base", nwMember.Name, nw.Name); } else if (member.IsGhost || !nwMember.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a field re-declaration ({0}) must be to ghostify the field", nwMember.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a field re-declaration ({0}) must be to ghostify the field", nwMember.Name); } nwMember.RefinementBase = member; @@ -748,39 +748,39 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM (f is GreatestPredicate) != (member is GreatestPredicate) || (f is TwoStatePredicate) != (member is TwoStatePredicate) || (f is TwoStateFunction) != (member is TwoStateFunction)) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a {0} declaration ({1}) can only refine a {0}", f.WhatKind, nwMember.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a {0} declaration ({1}) can only refine a {0}", f.WhatKind, nwMember.Name); } else { var prevFunction = (Function)member; if (f.Req.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, f.Req[0].E.tok, "a refining {0} is not allowed to add preconditions", f.WhatKind); + Reporter.Error(MessageSource.RefinementTransformer, f.Req[0].E.tok, "a refining {0} is not allowed to add preconditions", f.WhatKind); } if (f.Reads.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", f.WhatKind); + Reporter.Error(MessageSource.RefinementTransformer, f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", f.WhatKind); } if (f.Decreases.Expressions.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", f.WhatKind); + Reporter.Error(MessageSource.RefinementTransformer, f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", f.WhatKind); } if (prevFunction.HasStaticKeyword != f.HasStaticKeyword) { - reporter.Error(MessageSource.RefinementTransformer, f, "a function in a refining module cannot be changed from static to non-static or vice versa: {0}", f.Name); + Reporter.Error(MessageSource.RefinementTransformer, f, "a function in a refining module cannot be changed from static to non-static or vice versa: {0}", f.Name); } if (!prevFunction.IsGhost && f.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, f, "a function method cannot be changed into a (ghost) function in a refining module: {0}", f.Name); + Reporter.Error(MessageSource.RefinementTransformer, f, "a function method cannot be changed into a (ghost) function in a refining module: {0}", f.Name); } else if (prevFunction.IsGhost && !f.IsGhost && prevFunction.Body != null) { - reporter.Error(MessageSource.RefinementTransformer, f, "a function can be changed into a function method in a refining module only if the function has not yet been given a body: {0}", f.Name); + Reporter.Error(MessageSource.RefinementTransformer, f, "a function can be changed into a function method in a refining module only if the function has not yet been given a body: {0}", f.Name); } if (f.SignatureIsOmitted) { Contract.Assert(f.TypeArgs.Count == 0); Contract.Assert(f.Formals.Count == 0); - reporter.Info(MessageSource.RefinementTransformer, f.SignatureEllipsis, Printer.FunctionSignatureToString(prevFunction)); + Reporter.Info(MessageSource.RefinementTransformer, f.SignatureEllipsis, Printer.FunctionSignatureToString(prevFunction)); } else { CheckAgreement_TypeParameters(f.tok, prevFunction.TypeArgs, f.TypeArgs, f.Name, "function"); CheckAgreement_Parameters(f.tok, prevFunction.Formals, f.Formals, f.Name, "function", "parameter"); if (prevFunction.Result != null && f.Result != null && prevFunction.Result.Name != f.Result.Name) { - reporter.Error(MessageSource.RefinementTransformer, f, "the name of function return value '{0}'({1}) differs from the name of corresponding function return value in the module it refines ({2})", f.Name, f.Result.Name, prevFunction.Result.Name); + Reporter.Error(MessageSource.RefinementTransformer, f, "the name of function return value '{0}'({1}) differs from the name of corresponding function return value in the module it refines ({2})", f.Name, f.Result.Name, prevFunction.Result.Name); } if (!TypesAreSyntacticallyEqual(prevFunction.ResultType, f.ResultType)) { - reporter.Error(MessageSource.RefinementTransformer, f, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it refines ({2})", f.Name, f.ResultType, prevFunction.ResultType); + Reporter.Error(MessageSource.RefinementTransformer, f, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it refines ({2})", f.Name, f.ResultType, prevFunction.ResultType); } } @@ -789,7 +789,7 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM if (prevFunction.Body == null) { replacementBody = f.Body; } else if (f.Body != null) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, $"a refining {f.WhatKind} is not allowed to extend/change the body"); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, $"a refining {f.WhatKind} is not allowed to extend/change the body"); } var newF = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, f.Result, moreBody, replacementBody, prevFunction.Body == null, f.Attributes); newF.RefinementBase = member; @@ -799,14 +799,14 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM } else { var m = (Method)nwMember; if (!(member is Method)) { - reporter.Error(MessageSource.RefinementTransformer, nwMember, "a method declaration ({0}) can only refine a method", nwMember.Name); + Reporter.Error(MessageSource.RefinementTransformer, nwMember, "a method declaration ({0}) can only refine a method", nwMember.Name); } else { var prevMethod = (Method)member; if (m.Req.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, m.Req[0].E.tok, "a refining method is not allowed to add preconditions"); + Reporter.Error(MessageSource.RefinementTransformer, m.Req[0].E.tok, "a refining method is not allowed to add preconditions"); } if (m.Mod.Expressions.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause"); + Reporter.Error(MessageSource.RefinementTransformer, m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause"); } // If the previous method was not specified with "decreases *", then the new method is not allowed to provide any "decreases" clause. // Any "decreases *" clause is not inherited, so if the previous method was specified with "decreases *", then the new method needs @@ -819,23 +819,23 @@ TopLevelDeclWithMembers MergeClass(TopLevelDeclWithMembers nw, TopLevelDeclWithM } else { if (!Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) { // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause. - reporter.Error(MessageSource.RefinementTransformer, m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'"); + Reporter.Error(MessageSource.RefinementTransformer, m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'"); } decreases = m.Decreases; } if (prevMethod.HasStaticKeyword != m.HasStaticKeyword) { - reporter.Error(MessageSource.RefinementTransformer, m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name); + Reporter.Error(MessageSource.RefinementTransformer, m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name); } if (prevMethod.IsGhost && !m.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, m, "a method cannot be changed into a ghost method in a refining module: {0}", m.Name); + Reporter.Error(MessageSource.RefinementTransformer, m, "a method cannot be changed into a ghost method in a refining module: {0}", m.Name); } else if (!prevMethod.IsGhost && m.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, m, "a ghost method cannot be changed into a non-ghost method in a refining module: {0}", m.Name); + Reporter.Error(MessageSource.RefinementTransformer, m, "a ghost method cannot be changed into a non-ghost method in a refining module: {0}", m.Name); } if (m.SignatureIsOmitted) { Contract.Assert(m.TypeArgs.Count == 0); Contract.Assert(m.Ins.Count == 0); Contract.Assert(m.Outs.Count == 0); - reporter.Info(MessageSource.RefinementTransformer, m.SignatureEllipsis, Printer.MethodSignatureToString(prevMethod)); + Reporter.Info(MessageSource.RefinementTransformer, m.SignatureEllipsis, Printer.MethodSignatureToString(prevMethod)); } else { CheckAgreement_TypeParameters(m.tok, prevMethod.TypeArgs, m.TypeArgs, m.Name, "method"); CheckAgreement_Parameters(m.tok, prevMethod.Ins, m.Ins, m.Name, "method", "in-parameter"); @@ -867,13 +867,13 @@ void CheckAgreement_TypeParameters(IToken tok, List old, List old, List old, List nw, st Contract.Requires(thing != null); Contract.Requires(parameterKind != null); if (old.Count != nw.Count) { - reporter.Error(MessageSource.RefinementTransformer, tok, "{0} '{1}' is declared with a different number of {2} ({3} instead of {4}) than the corresponding {0} in the module it refines", thing, name, parameterKind, nw.Count, old.Count); + Reporter.Error(MessageSource.RefinementTransformer, tok, "{0} '{1}' is declared with a different number of {2} ({3} instead of {4}) than the corresponding {0} in the module it refines", thing, name, parameterKind, nw.Count, old.Count); } else { for (int i = 0; i < old.Count; i++) { var o = old[i]; var n = nw[i]; if (o.Name != n.Name) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "there is a difference in name of {0} {1} ('{2}' versus '{3}') of {4} {5} compared to corresponding {4} in the module it refines", parameterKind, i, n.Name, o.Name, thing, name); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "there is a difference in name of {0} {1} ('{2}' versus '{3}') of {4} {5} compared to corresponding {4} in the module it refines", parameterKind, i, n.Name, o.Name, thing, name); } else if (!o.IsGhost && n.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-ghost to ghost", parameterKind, n.Name, thing, name); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-ghost to ghost", parameterKind, n.Name, thing, name); } else if (o.IsGhost && !n.IsGhost) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from ghost to non-ghost", parameterKind, n.Name, thing, name); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from ghost to non-ghost", parameterKind, n.Name, thing, name); } else if (!o.IsOld && n.IsOld) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-new to new", parameterKind, n.Name, thing, name); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-new to new", parameterKind, n.Name, thing, name); } else if (o.IsOld && !n.IsOld) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from new to non-new", parameterKind, n.Name, thing, name); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from new to non-new", parameterKind, n.Name, thing, name); } else if (!TypesAreSyntacticallyEqual(o.Type, n.Type)) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it refines ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it refines ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type); } else if (n.DefaultValue != null) { - reporter.Error(MessageSource.RefinementTransformer, n.tok, "a refining formal parameter ('{0}') in a refinement module is not allowed to give a default-value expression", n.Name); + Reporter.Error(MessageSource.RefinementTransformer, n.tok, "a refining formal parameter ('{0}') in a refinement module is not allowed to give a default-value expression", n.Name); } } } @@ -965,18 +965,18 @@ BlockStmt MergeBlockStmt(BlockStmt skeleton, BlockStmt oldStmt) { string hoverText; var bodyInit = MergeStmtList(sbsSkeleton.BodyInit, sbsOldStmt.BodyInit, out hoverText); if (hoverText.Length != 0) { - reporter.Info(MessageSource.RefinementTransformer, sbsSkeleton.SeparatorTok ?? sbsSkeleton.Tok, hoverText); + Reporter.Info(MessageSource.RefinementTransformer, sbsSkeleton.SeparatorTok ?? sbsSkeleton.Tok, hoverText); } var bodyProper = MergeStmtList(sbsSkeleton.BodyProper, sbsOldStmt.BodyProper, out hoverText); if (hoverText.Length != 0) { - reporter.Info(MessageSource.RefinementTransformer, sbsSkeleton.EndTok, hoverText); + Reporter.Info(MessageSource.RefinementTransformer, sbsSkeleton.EndTok, hoverText); } return new DividedBlockStmt(sbsSkeleton.Tok, sbsSkeleton.EndTok, bodyInit, sbsSkeleton.SeparatorTok, bodyProper); } else { string hoverText; var body = MergeStmtList(skeleton.Body, oldStmt.Body, out hoverText); if (hoverText.Length != 0) { - reporter.Info(MessageSource.RefinementTransformer, skeleton.EndTok, hoverText); + Reporter.Info(MessageSource.RefinementTransformer, skeleton.EndTok, hoverText); } return new BlockStmt(skeleton.Tok, skeleton.EndTok, body); } @@ -999,7 +999,7 @@ List MergeStmtList(List skeleton, List oldStmt, } else if (((SkeletonStatement)cur).S == null) { // the "..." matches the empty statement sequence } else { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "skeleton statement does not match old statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "skeleton statement does not match old statement"); } i++; } else { @@ -1061,7 +1061,7 @@ List MergeStmtList(List skeleton, List oldStmt, oldS = oldStmt[j]; } if (hoverTextA.Length != 0) { - reporter.Info(MessageSource.RefinementTransformer, c.Tok, hoverTextA); + Reporter.Info(MessageSource.RefinementTransformer, c.Tok, hoverTextA); } } i++; @@ -1071,7 +1071,7 @@ List MergeStmtList(List skeleton, List oldStmt, Contract.Assert(c.ConditionOmitted); var oldAssume = oldS as PredicateStmt; if (oldAssume == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "assert template does not match inherited statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "assert template does not match inherited statement"); i++; } else { // Clone the expression, but among the new assert's attributes, indicate @@ -1082,7 +1082,7 @@ List MergeStmtList(List skeleton, List oldStmt, var attrs = refinementCloner.MergeAttributes(oldAssume.Attributes, skel.Attributes); body.Add(new AssertStmt(new Translator.ForceCheckToken(skel.Tok), new Translator.ForceCheckToken(skel.EndTok), e, skel.Proof, skel.Label, new Attributes("_prependAssertToken", new List(), attrs))); - reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, "assume->assert: " + Printer.ExprToString(e)); + Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, "assume->assert: " + Printer.ExprToString(e)); i++; j++; } @@ -1091,14 +1091,14 @@ List MergeStmtList(List skeleton, List oldStmt, Contract.Assert(c.ConditionOmitted); var oldExpect = oldS as ExpectStmt; if (oldExpect == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "expect template does not match inherited statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "expect template does not match inherited statement"); i++; } else { var e = refinementCloner.CloneExpr(oldExpect.Expr); var message = refinementCloner.CloneExpr(oldExpect.Message); var attrs = refinementCloner.MergeAttributes(oldExpect.Attributes, skel.Attributes); body.Add(new ExpectStmt(skel.Tok, skel.EndTok, e, message, attrs)); - reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.ExprToString(e)); + Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.ExprToString(e)); i++; j++; } @@ -1107,13 +1107,13 @@ List MergeStmtList(List skeleton, List oldStmt, Contract.Assert(c.ConditionOmitted); var oldAssume = oldS as AssumeStmt; if (oldAssume == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "assume template does not match inherited statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "assume template does not match inherited statement"); i++; } else { var e = refinementCloner.CloneExpr(oldAssume.Expr); var attrs = refinementCloner.MergeAttributes(oldAssume.Attributes, skel.Attributes); body.Add(new AssumeStmt(skel.Tok, skel.EndTok, e, attrs)); - reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.ExprToString(e)); + Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.ExprToString(e)); i++; j++; } @@ -1122,7 +1122,7 @@ List MergeStmtList(List skeleton, List oldStmt, Contract.Assert(c.ConditionOmitted); var oldIf = oldS as IfStmt; if (oldIf == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "if-statement template does not match inherited statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "if-statement template does not match inherited statement"); i++; } else { var resultingThen = MergeBlockStmt(skel.Thn, oldIf.Thn); @@ -1130,7 +1130,7 @@ List MergeStmtList(List skeleton, List oldStmt, var e = refinementCloner.CloneExpr(oldIf.Guard); var r = new IfStmt(skel.Tok, skel.EndTok, oldIf.IsBindingGuard, e, resultingThen, resultingElse); body.Add(r); - reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.GuardToString(oldIf.IsBindingGuard, e)); + Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.GuardToString(oldIf.IsBindingGuard, e)); i++; j++; } @@ -1138,16 +1138,16 @@ List MergeStmtList(List skeleton, List oldStmt, var skel = (WhileStmt)S; var oldWhile = oldS as WhileStmt; if (oldWhile == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "while-statement template does not match inherited statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "while-statement template does not match inherited statement"); i++; } else { Expression guard; if (c.ConditionOmitted) { guard = refinementCloner.CloneExpr(oldWhile.Guard); - reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.GuardToString(false, oldWhile.Guard)); + Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.GuardToString(false, oldWhile.Guard)); } else { if (oldWhile.Guard != null) { - reporter.Error(MessageSource.RefinementTransformer, skel.Guard.tok, "a skeleton while statement with a guard can only replace a while statement with a non-deterministic guard"); + Reporter.Error(MessageSource.RefinementTransformer, skel.Guard.tok, "a skeleton while statement with a guard can only replace a while statement with a non-deterministic guard"); } guard = skel.Guard; } @@ -1163,7 +1163,7 @@ List MergeStmtList(List skeleton, List oldStmt, Contract.Assert(c.ConditionOmitted); var oldModifyStmt = oldS as ModifyStmt; if (oldModifyStmt == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "modify template does not match inherited statement"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "modify template does not match inherited statement"); i++; } else { var mod = refinementCloner.CloneSpecFrameExpr(oldModifyStmt.Mod); @@ -1176,13 +1176,13 @@ List MergeStmtList(List skeleton, List oldStmt, // also sets ".ReverifyPost" to "true" for any "return" statements. mbody = MergeBlockStmt(skel.Body, new BlockStmt(oldModifyStmt.Tok, oldModifyStmt.EndTok, new List())); } else if (skel.Body == null) { - reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "modify template must have a body if the inherited modify statement does"); + Reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "modify template must have a body if the inherited modify statement does"); mbody = null; } else { mbody = MergeBlockStmt(skel.Body, oldModifyStmt.Body); } body.Add(new ModifyStmt(skel.Tok, skel.EndTok, mod.Expressions, mod.Attributes, mbody)); - reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.FrameExprListToString(mod.Expressions)); + Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, Printer.FrameExprListToString(mod.Expressions)); i++; j++; } @@ -1456,7 +1456,7 @@ WhileStmt MergeWhileStmt(WhileStmt cNew, WhileStmt cOld, Expression guard) { } else { if (!Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) { // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause. - reporter.Error(MessageSource.RefinementTransformer, cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'"); + Reporter.Error(MessageSource.RefinementTransformer, cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'"); } decr = cNew.Decreases; } @@ -1469,7 +1469,7 @@ WhileStmt MergeWhileStmt(WhileStmt cNew, WhileStmt cOld, Expression guard) { } else if (cOld.Body == null) { newBody = MergeBlockStmt(cNew.Body, new BlockStmt(cOld.Tok, cOld.EndTok, new List())); } else if (cNew.Body == null) { - reporter.Error(MessageSource.RefinementTransformer, cNew.Tok, "while template must have a body if the inherited while statement does"); + Reporter.Error(MessageSource.RefinementTransformer, cNew.Tok, "while template must have a body if the inherited while statement does"); newBody = null; } else { newBody = MergeBlockStmt(cNew.Body, cOld.Body); @@ -1508,9 +1508,9 @@ Statement MergeElse(Statement skeleton, Statement oldStmt) { void MergeAddStatement(Statement s, List stmtList) { Contract.Requires(s != null); Contract.Requires(stmtList != null); - var prevErrorCount = reporter.Count(ErrorLevel.Error); + var prevErrorCount = Reporter.Count(ErrorLevel.Error); CheckIsOkayNewStatement(s, new Stack(), 0); - if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { + if (Reporter.Count(ErrorLevel.Error) == prevErrorCount) { stmtList.Add(s); } } @@ -1527,29 +1527,29 @@ void CheckIsOkayNewStatement(Statement s, Stack labels, int loopLevels) labels.Push(n.Data.Name); } if (s is SkeletonStatement) { - reporter.Error(MessageSource.RefinementTransformer, s, "skeleton statement may not be used here; it does not have a matching statement in what is being replaced"); + Reporter.Error(MessageSource.RefinementTransformer, s, "skeleton statement may not be used here; it does not have a matching statement in what is being replaced"); } else if (s is ReturnStmt) { // allow return statements, but make note of that this requires verifying the postcondition ((ReturnStmt)s).ReverifyPost = true; } else if (s is YieldStmt) { - reporter.Error(MessageSource.RefinementTransformer, s, "yield statements are not allowed in skeletons"); + Reporter.Error(MessageSource.RefinementTransformer, s, "yield statements are not allowed in skeletons"); } else if (s is BreakStmt) { var b = (BreakStmt)s; if (b.TargetLabel != null ? !labels.Contains(b.TargetLabel.val) : loopLevels < b.BreakCount) { - reporter.Error(MessageSource.RefinementTransformer, s, "break statement in skeleton is not allowed to break outside the skeleton fragment"); + Reporter.Error(MessageSource.RefinementTransformer, s, "break statement in skeleton is not allowed to break outside the skeleton fragment"); } } else if (s is AssignStmt) { // TODO: To be a refinement automatically (that is, without any further verification), only variables and fields defined // in this module are allowed. This needs to be checked. If the LHS refers to an l-value that was not declared within // this module, then either an error should be reported or the Translator needs to know to translate new proof obligations. var a = (AssignStmt)s; - reporter.Error(MessageSource.RefinementTransformer, a.Tok, "cannot have assignment statement"); + Reporter.Error(MessageSource.RefinementTransformer, a.Tok, "cannot have assignment statement"); } else if (s is ConcreteUpdateStatement) { postTasks.Enqueue(() => { CheckIsOkayUpdateStmt((ConcreteUpdateStatement)s, moduleUnderConstruction); }); } else if (s is CallStmt) { - reporter.Error(MessageSource.RefinementTransformer, s.Tok, "cannot have call statement"); + Reporter.Error(MessageSource.RefinementTransformer, s.Tok, "cannot have call statement"); } else { if (s is WhileStmt || s is AlternativeLoopStmt) { loopLevels++; @@ -1573,23 +1573,23 @@ void CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m) { Contract.Assert(ident.Var is LocalVariable || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals) if ((ident.Var is LocalVariable && RefinementToken.IsInherited(((LocalVariable)ident.Var).Tok, m)) || ident.Var is Formal) { // for some reason, formals are not considered to be inherited. - reporter.Error(MessageSource.RefinementTransformer, l.tok, "refinement method cannot assign to variable defined in parent module ('{0}')", ident.Var.Name); + Reporter.Error(MessageSource.RefinementTransformer, l.tok, "refinement method cannot assign to variable defined in parent module ('{0}')", ident.Var.Name); } } else if (l is MemberSelectExpr) { var member = ((MemberSelectExpr)l).Member; if (RefinementToken.IsInherited(member.tok, m)) { - reporter.Error(MessageSource.RefinementTransformer, l.tok, "refinement method cannot assign to a field defined in parent module ('{0}')", member.Name); + Reporter.Error(MessageSource.RefinementTransformer, l.tok, "refinement method cannot assign to a field defined in parent module ('{0}')", member.Name); } } else { // must be an array element - reporter.Error(MessageSource.RefinementTransformer, l.tok, "new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)"); + Reporter.Error(MessageSource.RefinementTransformer, l.tok, "new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)"); } } if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; foreach (var rhs in s.Rhss) { if (rhs.CanAffectPreviouslyKnownExpressions) { - reporter.Error(MessageSource.RefinementTransformer, rhs.Tok, "assignment RHS in refinement method is not allowed to affect previously defined state"); + Reporter.Error(MessageSource.RefinementTransformer, rhs.Tok, "assignment RHS in refinement method is not allowed to affect previously defined state"); } } } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index ce120f23c2c..74fe461896a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -525,7 +525,7 @@ public void ResolveProgram(Program prog) { if (!good || reporter.Count(ErrorLevel.Error) != preResolveErrorCount) { break; } - r.PostResolve(m); + r.PostResolveIntermediate(m); } if (good && reporter.Count(ErrorLevel.Error) == errorCount) { m.SuccessfullyResolved = true; @@ -708,6 +708,12 @@ public void ResolveProgram(Program prog) { Type.DisableScopes(); CheckDupModuleNames(prog); + + foreach (var module in prog.Modules()) { + foreach (var r in rewriters) { + r.PostResolve(module); + } + } } void FillInDefaultDecreasesClauses(Program prog) { diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index de189a50f44..210d330033f 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -12,29 +12,83 @@ namespace Microsoft.Dafny { /// Class that plugins should extend, in order to provide an extra IRewriter to the pipeline. /// public abstract class IRewriter { - protected readonly ErrorReporter reporter; + /// + /// Used to report errors and warnings, with positional information. + /// + protected readonly ErrorReporter Reporter; + /// + /// Make sure, when you extends an IRewriter in a plugin, that + /// 1. You accept an ErrorReporter as the first argument of your constructor + /// 2. All other arguments, if any, should have default values + /// 3. You provide this ErrorReporter to the base class + /// Then you can use the protected field "reporter" like the following: + /// + /// reporter.Error(MessageSource.Compiler, token, "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() + /// + /// public IRewriter(ErrorReporter reporter) { Contract.Requires(reporter != null); - this.reporter = reporter; + this.Reporter = reporter; + } + + /// + /// Phase 1/5 + /// Override this method to obtain a module definition after parsing and built-in pre-resolvers, + /// You can then report errors using reporter.Error(MessageSource.Resolver, token, "message") (see above) + /// This is a good place to perform AST rewritings, if necessary + /// + /// A module definition before is resolved + public virtual void PreResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); } - public virtual void PreResolve(ModuleDefinition m) { - Contract.Requires(m != null); + /// + /// Phase 2/5 + /// Override this method to obtain a module definition after bare resolution, if no error were thrown, + /// You can then report errors using reporter.Error (see above) + /// We heavily discourage AST rewriting after this stage, as automatic type checking will not take place anymore. + /// + /// A module definition after it is resolved and type-checked + public virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); } - public virtual void PostResolve(ModuleDefinition m) { - Contract.Requires(m != null); + /// + /// Phase 3/5 + /// Override this method to obtain the module definition after resolution and + /// SCC/Cyclicity/Recursivity analysis. + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed + public virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); } - // After SCC/Cyclicity/Recursivity analysis: - internal virtual void PostCyclicityResolve(ModuleDefinition m) { - Contract.Requires(m != null); + /// + /// Phase 4/5 + /// Override this method to obtain the module definition after resolving decreasesResolve + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity and decreasesResolve checks have been performed + public virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); } - // After SCC/Cyclicity/Recursivity analysis and after application of default decreases: - internal virtual void PostDecreasesResolve(ModuleDefinition m) { - Contract.Requires(m != null); + /// + /// Phase 5/5 + /// Override this method to obtain a module definition after the entire resolution pipeline + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed + public virtual void PostResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); } } @@ -50,8 +104,8 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - internal override void PostCyclicityResolve(ModuleDefinition m) { - var finder = new Triggers.QuantifierCollector(reporter); + public override void PostCyclicityResolve(ModuleDefinition m) { + var finder = new Triggers.QuantifierCollector(Reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { finder.Visit(decl, null); @@ -70,7 +124,7 @@ internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PostResolve(ModuleDefinition m) { + public override void PostResolveIntermediate(ModuleDefinition m) { var splitter = new Triggers.QuantifierSplitter(); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { splitter.Visit(decl); @@ -85,8 +139,8 @@ public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PostResolve(ModuleDefinition m) { - var forallvisiter = new ForAllStmtVisitor(reporter); + public override void PostResolveIntermediate(ModuleDefinition m) { + var forallvisiter = new ForAllStmtVisitor(Reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { forallvisiter.Visit(decl, true); if (decl is ExtremeLemma) { @@ -546,7 +600,7 @@ void ProcessClassPreResolve(ClassDecl cl) { } } - public override void PostResolve(ModuleDefinition m) { + public override void PostResolveIntermediate(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { @@ -888,7 +942,7 @@ void AddHoverText(IToken tok, string format, params object[] args) { } } var s = "autocontracts:\n" + string.Format(format, args); - reporter.Info(MessageSource.Rewriter, tok, s.Replace("\n", "\n ")); + Reporter.Info(MessageSource.Rewriter, tok, s.Replace("\n", "\n ")); } } @@ -921,7 +975,7 @@ public override void PreResolve(ModuleDefinition m) { } } - public override void PostResolve(ModuleDefinition m) { + public override void PostResolveIntermediate(ModuleDefinition m) { foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { if (decl is Lemma || decl is TwoStateLemma) { var lem = (Method)decl; @@ -1056,7 +1110,7 @@ public AutoReqFunctionRewriter(ErrorReporter reporter) Contract.Requires(reporter != null); } - public override void PostResolve(ModuleDefinition m) { + public override void PostResolveIntermediate(ModuleDefinition m) { var components = m.CallGraph.TopologicallySortedComponents(); foreach (var scComponent in components) { // Visit the call graph bottom up, so anything we call already has its prequisites calculated @@ -1137,7 +1191,7 @@ public void addAutoReqToolTipInfoToFunction(string label, Function f, List generateAutoReqs(Expression expr) { Expression allReqsSatisfied = andify(e.Term.tok, auto_reqs); Expression allReqsSatisfiedAndTerm = Expression.CreateAnd(allReqsSatisfied, e.Term); e.UpdateTerm(allReqsSatisfiedAndTerm); - reporter.Info(MessageSource.Rewriter, e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&"); + Reporter.Info(MessageSource.Rewriter, e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&"); } } else if (expr is SetComprehension) { var e = (SetComprehension)expr; @@ -1512,7 +1566,7 @@ public override void PreResolve(ModuleDefinition m) { Expression newArg = new LiteralExpr(attr.Args[0].tok, value * current_limit); member.Attributes = new Attributes("_" + name, new List() { newArg }, attrs); if (Attributes.Contains(attrs, name)) { - reporter.Warning(MessageSource.Rewriter, member.tok, "timeLimitMultiplier annotation overrides " + name + " annotation"); + Reporter.Warning(MessageSource.Rewriter, member.tok, "timeLimitMultiplier annotation overrides " + name + " annotation"); } } } @@ -1653,7 +1707,7 @@ internal InductionRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - internal override void PostDecreasesResolve(ModuleDefinition m) { + public override void PostDecreasesResolve(ModuleDefinition m) { if (DafnyOptions.O.Induction == 0) { // Don't bother inferring :induction attributes. This will also have the effect of not warning about malformed :induction attributes } else { @@ -1768,7 +1822,7 @@ void ComputeInductionVariables(IToken tok, List boundVars, Lis continue; } if (0 <= j) { - reporter.Warning(MessageSource.Rewriter, arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute", + Reporter.Warning(MessageSource.Rewriter, arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute", lemma != null ? "lemma parameter" : "bound variable", lemma != null ? "lemma" : "quantifier"); return; } @@ -1779,10 +1833,10 @@ void ComputeInductionVariables(IToken tok, List boundVars, Lis i = 0; continue; } - reporter.Warning(MessageSource.Rewriter, arg.tok, "lemma parameters given as :induction arguments must be given in the same order as in the lemma; ignoring attribute"); + Reporter.Warning(MessageSource.Rewriter, arg.tok, "lemma parameters given as :induction arguments must be given in the same order as in the lemma; ignoring attribute"); return; } - reporter.Warning(MessageSource.Rewriter, arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute", + Reporter.Warning(MessageSource.Rewriter, arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute", i == 0 ? "'false' or 'true' or " : "", lemma != null ? "lemma parameter" : "bound variable"); return; @@ -1812,7 +1866,7 @@ void ComputeInductionVariables(IToken tok, List boundVars, Lis if (lemma is PrefixLemma) { s = lemma.Name + " " + s; } - reporter.Info(MessageSource.Rewriter, tok, s); + Reporter.Info(MessageSource.Rewriter, tok, s); } } class Induction_Visitor : BottomUpVisitor { From ed409745d41b4df50b5e3228976bc49c9e29badb Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 25 Jan 2022 16:44:58 -0600 Subject: [PATCH 18/47] Added missing two newlines --- Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs | 2 +- Source/DafnyPipeline.Test/ExternalResolverTest.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs index 57f06daa6bc..9acf9c95ae0 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs @@ -91,4 +91,4 @@ public async Task EnsureItIsPossibleToPluginIRewriter() { Assert.AreEqual("Impossible to continue", diagnostics[0].Message); Assert.AreEqual(new Range((-1, -1), (-1, 29)), diagnostics[0].Range); } -} \ No newline at end of file +} diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs index 4fde1e80c0f..ae0817ae730 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/Source/DafnyPipeline.Test/ExternalResolverTest.cs @@ -78,4 +78,4 @@ public override void PostResolve(ModuleDefinition m) { Assert.Equal(1, reporter.Count(ErrorLevel.Error)); Assert.Equal("Impossible to continue", reporter.GetLastErrorMessage()); } -} \ No newline at end of file +} From d40790b977218564e8005a0cc58e7cdccf83aba0 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Jan 2022 13:16:00 -0600 Subject: [PATCH 19/47] Fixed XUnit tests --- Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs | 2 +- Source/DafnyPipeline.Test/ExternalResolverTest.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs index 9acf9c95ae0..e0b7d6fecb1 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs @@ -40,7 +40,7 @@ public ErrorRewriter(ErrorReporter reporter) : base(reporter) {} public override void PostResolve(ModuleDefinition m) { - reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); + Reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); } }"); client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs index ae0817ae730..e34e7fdf9cf 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/Source/DafnyPipeline.Test/ExternalResolverTest.cs @@ -58,7 +58,7 @@ public ErrorRewriter(ErrorReporter reporter) : base(reporter) {} public override void PostResolve(ModuleDefinition m) { - reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); + Reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); } }"); From b3d96834a219443daa64ced4e47f93d892af11fd Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Jan 2022 13:18:00 -0600 Subject: [PATCH 20/47] Better names --- .../DafnyLanguageServer.Test/Various/ExternalResolverTest.cs | 4 ++-- Source/DafnyPipeline.Test/ExternalResolverTest.cs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs index e0b7d6fecb1..6b2bab18819 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs @@ -39,8 +39,8 @@ public class ErrorRewriter: IRewriter { public ErrorRewriter(ErrorReporter reporter) : base(reporter) {} - public override void PostResolve(ModuleDefinition m) { - Reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); } }"); client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs index e34e7fdf9cf..561c1713349 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/Source/DafnyPipeline.Test/ExternalResolverTest.cs @@ -57,8 +57,8 @@ public class ErrorRewriter: IRewriter { public ErrorRewriter(ErrorReporter reporter) : base(reporter) {} - public override void PostResolve(ModuleDefinition m) { - Reporter.Error(MessageSource.Compiler, m.tok, ""Impossible to continue""); + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); } }"); From 2516be6d50f33a307d6f9014c1d5406301feb14d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Jan 2022 16:40:38 -0600 Subject: [PATCH 21/47] Proper Configuration for plugins to extend IRewriter is now Plugin.Rewriter Proper internal Plugin class to handle the assembly --- Source/Dafny/DafnyOptions.cs | 45 +++++--- Source/Dafny/Plugins/Configuration.cs | 25 +++++ Source/Dafny/Plugins/Rewriter.cs | 87 +++++++++++++++ Source/Dafny/RefinementTransformer.cs | 3 +- Source/Dafny/Resolver.cs | 22 +--- Source/Dafny/Rewriter.cs | 103 ++---------------- .../Various/ExternalResolverTest.cs | 43 +++++--- ...DafnyOptions.cs => DafnyPluginsOptions.cs} | 4 +- .../Language/LanguageServerExtensions.cs | 1 - .../Workspace/TextDocumentLoader.cs | 4 +- .../ExternalResolverTest.cs | 39 +++++-- 11 files changed, 223 insertions(+), 153 deletions(-) create mode 100644 Source/Dafny/Plugins/Configuration.cs create mode 100644 Source/Dafny/Plugins/Rewriter.cs rename Source/DafnyLanguageServer/Language/{DafnyOptions.cs => DafnyPluginsOptions.cs} (69%) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 63916bc4cf6..7b04ac8a2c4 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -8,7 +8,9 @@ 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 { @@ -136,7 +138,7 @@ public enum IncludesModes { // Working around the fact that xmlFilename is private public string BoogieXmlFilename = null; - public List Plugins = new(); + public List Plugins = new(); public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); @@ -232,17 +234,33 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com return true; } - case "plugins": { + case "Plugin": + case "plugin": { if (ps.ConfirmArgumentCount(1)) { - 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"); + var pluginAndArgument = args[ps.i]; + if (pluginAndArgument.Length > 0 && + pluginAndArgument[0] == '"' && + pluginAndArgument[^1] == '"' + ) { + pluginAndArgument = pluginAndArgument.Substring(1, pluginAndArgument.Length - 2); + } + if (pluginAndArgument.Length > 0) { + var pluginArray = pluginAndArgument.Split(','); + var pluginPath = pluginArray[0]; + var arguments = Array.Empty(); + if (pluginArray.Length > 2) { + ps.Error("\"plugin\" cannot have more than one comma separating the DLL from the arguments"); + } else { + if (pluginArray.Length == 2) { + // Parse arguments, accepting and remove double quotes that isolate long arguments + var splitter = new Regex(@"""((?:[^""]|\\"")*)""|([^ ]+)"); + arguments = splitter.Matches(pluginArray[1]).Select( + matchResult => matchResult.Groups[1].Success ? + matchResult.Groups[1].Value.Replace(@"\""", @"""") : + matchResult.Groups[2].Value + ).ToArray(); } - Plugins.Add(pluginAssembly); + Plugins.Add(new Plugin(pluginPath, arguments, errorReporter)); } } } @@ -826,9 +844,10 @@ 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. -/plugins: - (experimental) List of comma-separated paths to assemblies that contain at least one - instantiatable class extending Microsoft.Dafny.IRewriter +/plugin:[:] + (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.Initializer to receive arguments /Main: 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'. diff --git a/Source/Dafny/Plugins/Configuration.cs b/Source/Dafny/Plugins/Configuration.cs new file mode 100644 index 00000000000..be1acd58a91 --- /dev/null +++ b/Source/Dafny/Plugins/Configuration.cs @@ -0,0 +1,25 @@ +using System; +using System.Collections.Generic; + +namespace Microsoft.Dafny.Plugins; + +/// +/// A class that plugins should extend, in order to receive plugin-specific command-line arguments +/// +public abstract class Configuration { + /// + /// A Microsoft.Dafny.Plugins.Configuration will be automatically instantiated an arguments + /// will be provided to the plugin by the method `ParseArguments``; + /// + /// The arguments passed to the plugin + public virtual void ParseArguments(string[] args) { + } + + /// + /// Override this method to provide specific rewriters to Dafny + /// + /// a list of Rewriter that are going to be used in the resolution pipeline + public virtual Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return Array.Empty(); + } +} \ No newline at end of file diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs new file mode 100644 index 00000000000..dfa557353bc --- /dev/null +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -0,0 +1,87 @@ +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny.Plugins { + /// + /// A class that plugins should extend, in order to provide an extra Rewriter to the pipeline. + /// + public abstract class Rewriter { + /// + /// Used to report errors and warnings, with positional information. + /// + protected readonly ErrorReporter Reporter; + + /// + /// Make sure, when you extends an Rewriter in a plugin, that + /// 1. You accept an ErrorReporter as the first argument of your constructor + /// 2. All other arguments, if any, should have default values + /// 3. You provide this ErrorReporter to the base class + /// Then you can use the protected field "reporter" like the following: + /// + /// reporter.Error(MessageSource.Compiler, token, "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() + /// + /// + public Rewriter(ErrorReporter reporter) { + Contract.Requires(reporter != null); + this.Reporter = reporter; + } + + /// + /// Phase 1/5 + /// Override this method to obtain a module definition after parsing and built-in pre-resolvers, + /// You can then report errors using reporter.Error(MessageSource.Resolver, token, "message") (see above) + /// This is a good place to perform AST rewritings, if necessary + /// + /// A module definition before is resolved + public virtual void PreResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 2/5 + /// Override this method to obtain a module definition after bare resolution, if no error were thrown, + /// You can then report errors using reporter.Error (see above) + /// We heavily discourage AST rewriting after this stage, as automatic type checking will not take place anymore. + /// + /// A module definition after it is resolved and type-checked + public virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 3/5 + /// Override this method to obtain the module definition after resolution and + /// SCC/Cyclicity/Recursivity analysis. + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed + public virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 4/5 + /// Override this method to obtain the module definition after resolving decreasesResolve + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity and decreasesResolve checks have been performed + public virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 5/5 + /// Override this method to obtain a module definition after the entire resolution pipeline + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed + public virtual void PostResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + } +} \ No newline at end of file diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 240a20249f6..1c74cc7b905 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -19,6 +19,7 @@ using System.Numerics; using System.Diagnostics.Contracts; using System.Linq; +using Microsoft.Dafny.Plugins; using IToken = Microsoft.Boogie.IToken; namespace Microsoft.Dafny { @@ -140,7 +141,7 @@ public override string filename { /// Jason Koenig and K. Rustan M. Leino. /// In EPTCS, 2016. (Post-workshop proceedings of REFINE 2015.) /// - public class RefinementTransformer : IRewriter { + public class RefinementTransformer : Rewriter { Cloner rawCloner; // This cloner just gives exactly the same thing back. RefinementCloner refinementCloner; // This cloner wraps things in a RefinementToken diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 74fe461896a..db863b80f17 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -17,6 +17,7 @@ using Microsoft.BaseTypes; using Microsoft.Boogie; using Microsoft.CodeAnalysis.CSharp.Syntax; +using Microsoft.Dafny.Plugins; namespace Microsoft.Dafny { public class Resolver { @@ -240,7 +241,7 @@ enum ValuetypeVariety { private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; - private List rewriters; + private List rewriters; private RefinementTransformer refinementTransformer; public Resolver(Program prog) { @@ -421,7 +422,7 @@ public void ResolveProgram(Program prog) { h++; } - rewriters = new List(); + rewriters = new List(); refinementTransformer = new RefinementTransformer(prog); rewriters.Add(refinementTransformer); rewriters.Add(new AutoContractsRewriter(reporter, builtIns)); @@ -439,20 +440,9 @@ public void ResolveProgram(Program prog) { rewriters.Add(new InductionRewriter(reporter)); if (DafnyOptions.O.Plugins.Count() >= 1) { - foreach (var assembly in DafnyOptions.O.Plugins) { - foreach (System.Type type in assembly.GetTypes().Where(t => t.IsAssignableTo(typeof(IRewriter)))) { - IRewriter pluginRewriter = null; - Exception e = null; - try { - pluginRewriter = Activator.CreateInstance(type, reporter) as IRewriter; - } catch (Exception _e) { - e = _e; - } - if (pluginRewriter == null) { - reporter.Error(MessageSource.Resolver, prog.GetFirstTopLevelToken(), $"[Internal error] '{type.FullName}' could not be created as an IRewriter" + (e != null ? ":" + e.ToString() : "")); - } else { - rewriters.Add(pluginRewriter); - } + foreach (var plugin in DafnyOptions.O.Plugins) { + foreach (var rewriter in plugin.Configuration.GetRewriters(reporter)) { + rewriters.Add(rewriter); } } } diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 210d330033f..2c881859d69 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -4,94 +4,11 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using Microsoft.Dafny.Plugins; using Bpl = Microsoft.Boogie; using IToken = Microsoft.Boogie.IToken; namespace Microsoft.Dafny { - /// - /// Class that plugins should extend, in order to provide an extra IRewriter to the pipeline. - /// - public abstract class IRewriter { - /// - /// Used to report errors and warnings, with positional information. - /// - protected readonly ErrorReporter Reporter; - - /// - /// Make sure, when you extends an IRewriter in a plugin, that - /// 1. You accept an ErrorReporter as the first argument of your constructor - /// 2. All other arguments, if any, should have default values - /// 3. You provide this ErrorReporter to the base class - /// Then you can use the protected field "reporter" like the following: - /// - /// reporter.Error(MessageSource.Compiler, token, "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() - /// - /// - public IRewriter(ErrorReporter reporter) { - Contract.Requires(reporter != null); - this.Reporter = reporter; - } - - /// - /// Phase 1/5 - /// Override this method to obtain a module definition after parsing and built-in pre-resolvers, - /// You can then report errors using reporter.Error(MessageSource.Resolver, token, "message") (see above) - /// This is a good place to perform AST rewritings, if necessary - /// - /// A module definition before is resolved - public virtual void PreResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 2/5 - /// Override this method to obtain a module definition after bare resolution, if no error were thrown, - /// You can then report errors using reporter.Error (see above) - /// We heavily discourage AST rewriting after this stage, as automatic type checking will not take place anymore. - /// - /// A module definition after it is resolved and type-checked - public virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 3/5 - /// Override this method to obtain the module definition after resolution and - /// SCC/Cyclicity/Recursivity analysis. - /// You can then report errors using reporter.Error (see above) - /// - /// A module definition after it - /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed - public virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 4/5 - /// Override this method to obtain the module definition after resolving decreasesResolve - /// You can then report errors using reporter.Error (see above) - /// - /// A module definition after it - /// is resolved, type-checked and SCC/Cyclicity/Recursivity and decreasesResolve checks have been performed - public virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 5/5 - /// Override this method to obtain a module definition after the entire resolution pipeline - /// You can then report errors using reporter.Error (see above) - /// - /// A module definition after it - /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed - public virtual void PostResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - } - public class AutoGeneratedToken : TokenWrapper { public AutoGeneratedToken(Boogie.IToken wrappedToken) : base(wrappedToken) { @@ -99,7 +16,7 @@ public AutoGeneratedToken(Boogie.IToken wrappedToken) } } - public class TriggerGeneratingRewriter : IRewriter { + public class TriggerGeneratingRewriter : Rewriter { internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } @@ -119,7 +36,7 @@ public override void PostCyclicityResolve(ModuleDefinition m) { } } - internal class QuantifierSplittingRewriter : IRewriter { + internal class QuantifierSplittingRewriter : Rewriter { internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } @@ -134,7 +51,7 @@ public override void PostResolveIntermediate(ModuleDefinition m) { } // write out the quantifier for ForallStmt - public class ForallStmtRewriter : IRewriter { + public class ForallStmtRewriter : Rewriter { public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } @@ -504,7 +421,7 @@ Expression Substitute(Expression expr, IVariable v, Expression e) { /// requires Valid() /// reads Repr /// - public class AutoContractsRewriter : IRewriter { + public class AutoContractsRewriter : Rewriter { readonly BuiltIns builtIns; public AutoContractsRewriter(ErrorReporter reporter, BuiltIns builtIns) : base(reporter) { @@ -953,7 +870,7 @@ void AddHoverText(IToken tok, string format, params object[] args) { /// recursive clique (if any), or if the programmer /// specifically asks to see it via the reveal_foo() lemma /// - public class OpaqueFunctionRewriter : IRewriter { + public class OpaqueFunctionRewriter : Rewriter { protected Dictionary fullVersion; // Given an opaque function, retrieve the full protected Dictionary original; // Given a full version of an opaque function, find the original opaque version protected Dictionary revealOriginal; // Map reveal_* lemmas (or two-state lemmas) back to their original functions @@ -1101,7 +1018,7 @@ protected override bool VisitOneExpr(Expression expr, ref bool context) { /// Automatically accumulate requires for function calls within a function body, /// if requested via {:autoreq} /// - public class AutoReqFunctionRewriter : IRewriter { + public class AutoReqFunctionRewriter : Rewriter { Function parentFunction; bool containsMatch; // TODO: Track this per-requirement, rather than per-function @@ -1467,7 +1384,7 @@ List generateAutoReqs(Expression expr) { } } - public class ProvideRevealAllRewriter : IRewriter { + public class ProvideRevealAllRewriter : Rewriter { public ProvideRevealAllRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); @@ -1532,7 +1449,7 @@ public override void PreResolve(ModuleDefinition m) { /// Replace all occurrences of attribute {:timeLimitMultiplier X} with {:timeLimit Y} /// where Y = X*default-time-limit or Y = X*command-line-time-limit /// - public class TimeLimitRewriter : IRewriter { + public class TimeLimitRewriter : Rewriter { public TimeLimitRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); @@ -1702,7 +1619,7 @@ public override IToken Tok(IToken tok) { // =========================================================================================== - public class InductionRewriter : IRewriter { + public class InductionRewriter : Rewriter { internal InductionRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs index 6b2bab18819..d2c37296b9b 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs @@ -28,34 +28,49 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; public class ExternalResolverTest : DafnyLanguageServerTestBase { private ILanguageClient client; private DiagnosticsReceiver diagnosticReceiver; - private Assembly library; + private string libraryPath; [TestInitialize] public async Task SetUp() { diagnosticReceiver = new(); - library = await GetLibrary(@" - using Microsoft.Dafny; - public class ErrorRewriter: IRewriter { - public ErrorRewriter(ErrorReporter reporter) : base(reporter) - {} + libraryPath = await GetLibrary(@" +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); - } - }"); +public class TestConfiguration: Configuration { + public string Argument = """"; + public override void ParseArguments(string[] args) { + Argument = args[0]; + } + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return new Rewriter[]{new ErrorRewriter(errorReporter, this)}; + } +} + +public class ErrorRewriter: Rewriter { + private readonly TestConfiguration configuration; + + public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): base(reporter) { + this.configuration = configuration; + } + + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue ""+configuration.Argument); + } +}"); client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); } protected override IConfiguration CreateConfiguration() { return new ConfigurationBuilder().AddCommandLine( - new[] { "--dafny:plugins=" + this.library.Location }).Build(); + new[] { "--dafny:plugins:0=" + libraryPath + ",\"because whatever\"" }).Build(); } /// /// 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. /// - public async Task GetLibrary(string code) { + public async Task GetLibrary(string code) { var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create("tempAssembly"); var standardLibraries = new List() @@ -77,7 +92,7 @@ public async Task GetLibrary(string code) { var result = compilation.Emit(assemblyPath); Assert.IsTrue(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); - return Assembly.LoadFrom(assemblyPath); + return assemblyPath; } [TestMethod] @@ -88,7 +103,7 @@ public async Task EnsureItIsPossibleToPluginIRewriter() { Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); - Assert.AreEqual("Impossible to continue", diagnostics[0].Message); + Assert.AreEqual("Impossible to continue because whatever", diagnostics[0].Message); Assert.AreEqual(new Range((-1, -1), (-1, 29)), diagnostics[0].Range); } } diff --git a/Source/DafnyLanguageServer/Language/DafnyOptions.cs b/Source/DafnyLanguageServer/Language/DafnyPluginsOptions.cs similarity index 69% rename from Source/DafnyLanguageServer/Language/DafnyOptions.cs rename to Source/DafnyLanguageServer/Language/DafnyPluginsOptions.cs index f9575cb8537..bb89769df51 100644 --- a/Source/DafnyLanguageServer/Language/DafnyOptions.cs +++ b/Source/DafnyLanguageServer/Language/DafnyPluginsOptions.cs @@ -9,8 +9,8 @@ public class DafnyPluginsOptions { public const string Section = "Dafny"; /// - /// Gets or sets which backends will be targeted so that their resolver can run before verification. + /// Gets or sets which plugins to use in Dafny (e.g. for resolution or compilation) /// - public string Plugins { get; set; } = ""; + public string[] Plugins { get; set; } = System.Array.Empty(); } } diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs index 7db8c81b07f..749e74ddc53 100644 --- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs @@ -25,7 +25,6 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv return services .Configure(configuration.GetSection(VerifierOptions.Section)) .Configure(configuration.GetSection(GhostOptions.Section)) - .Configure(configuration.GetSection(DafnyPluginsOptions.Section)) .AddSingleton(serviceProvider => DafnyLangParser.Create(serviceProvider.GetRequiredService>())) .AddSingleton() .AddSingleton(CreateVerifier) diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index d53db7dc520..7a4bcadbd3e 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -119,7 +119,9 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { if (dafnyPluginsOptions.Value.Plugins.Length > 0 && DafnyOptions.O.Plugins.Count == 0) { try { - DafnyOptions.O.Parse(new[] { "-plugins:" + dafnyPluginsOptions.Value.Plugins }); + foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { + DafnyOptions.O.Parse(new[] { "-plugin:" + pluginPathArgument }); + } } catch (Exception e) { errorReporter.Error(MessageSource.Parser, program.GetFirstTopLevelToken(), "Error while instantiating the plugins:" + e.ToString()); } diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/ExternalResolverTest.cs index 561c1713349..94aabb2460e 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/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. /// - public async Task GetLibrary(string code) { + public async Task GetLibrary(string code) { var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create("tempAssembly"); var standardLibraries = new List() @@ -40,7 +40,7 @@ public async Task GetLibrary(string code) { var result = compilation.Emit(assemblyPath); Assert.True(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); - return Assembly.LoadFrom(assemblyPath); + return assemblyPath; } class CollectionErrorReporter : BatchErrorReporter { @@ -52,19 +52,34 @@ public string GetLastErrorMessage() { [Fact] public async void EnsureItIsPossibleToPluginIRewriter() { var library = await GetLibrary(@" - using Microsoft.Dafny; - public class ErrorRewriter: IRewriter { - public ErrorRewriter(ErrorReporter reporter) : base(reporter) - {} +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; + +public class TestConfiguration: Configuration { + public string Argument = """"; + public override void ParseArguments(string[] args) { + Argument = args[0]; + } + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return new Rewriter[]{new ErrorRewriter(errorReporter, this)}; + } +} - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); - } - }"); +public class ErrorRewriter: Rewriter { + private readonly TestConfiguration configuration; + + public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): base(reporter) { + this.configuration = configuration; + } + + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue ""+configuration.Argument); + } +}"); var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); - options.Plugins.Add(library); + options.Plugins.Add(new Microsoft.Dafny.Plugin(library, new string[] { "because whatever" }, reporter)); DafnyOptions.Install(options); var programString = "function test(): int { 1 }"; @@ -76,6 +91,6 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { Main.Resolve(dafnyProgram, reporter); Assert.Equal(1, reporter.Count(ErrorLevel.Error)); - Assert.Equal("Impossible to continue", reporter.GetLastErrorMessage()); + Assert.Equal("Impossible to continue because whatever", reporter.GetLastErrorMessage()); } } From 0b104e49f7edc7127942c5b0ffcf887c65b30a89 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Jan 2022 16:48:22 -0600 Subject: [PATCH 22/47] Updated README --- Source/DafnyLanguageServer/README.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Source/DafnyLanguageServer/README.md b/Source/DafnyLanguageServer/README.md index 842226b76d5..17514b07937 100644 --- a/Source/DafnyLanguageServer/README.md +++ b/Source/DafnyLanguageServer/README.md @@ -79,8 +79,9 @@ Options provided through the command line have higher priority than the options ### Plugins ```sh -# Provides a comma-separated list of paths to assemblies -# that contain an instantiatable IRewrite to use during resolution +# Provides a path to assemblies +# that contain an instantiatable Microsoft.Dafny.Plugins.Configuration to use during resolution +# Optionally, after a comma, provide an extra list of space-separated arguments. # Default: "" (nothing extra is loaded) ---dafny:plugins= +--dafny:plugins:0= ``` From b99acbdff15825b7a4443dbfb3a7fb1993e8d77a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Jan 2022 16:50:31 -0600 Subject: [PATCH 23/47] Updated documentation --- Source/Dafny/Plugins/Rewriter.cs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs index dfa557353bc..8c0350952b0 100644 --- a/Source/Dafny/Plugins/Rewriter.cs +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -12,9 +12,7 @@ public abstract class Rewriter { /// /// Make sure, when you extends an Rewriter in a plugin, that - /// 1. You accept an ErrorReporter as the first argument of your constructor - /// 2. All other arguments, if any, should have default values - /// 3. You provide this ErrorReporter to the base class + /// you provide an ErrorReporter to the base class (you can obtain one in Configuration.GetRewriters()) /// Then you can use the protected field "reporter" like the following: /// /// reporter.Error(MessageSource.Compiler, token, "Your error message here"); From 9b405dea34ce673983d9fcdaa10201f7c3135f71 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 09:43:22 -0600 Subject: [PATCH 24/47] Ensure it works even without Configuration. Better documentation --- Source/Dafny/Plugin.cs | 56 +++++++++++++++++++ Source/Dafny/Plugins/Configuration.cs | 4 ++ Source/Dafny/Plugins/Rewriter.cs | 14 +++-- ...ExternalResolverTest.cs => PluginsTest.cs} | 6 +- ...ExternalResolverTest.cs => PluginsTest.cs} | 39 +++++++++++-- 5 files changed, 108 insertions(+), 11 deletions(-) create mode 100644 Source/Dafny/Plugin.cs rename Source/DafnyLanguageServer.Test/Various/{ExternalResolverTest.cs => PluginsTest.cs} (94%) rename Source/DafnyPipeline.Test/{ExternalResolverTest.cs => PluginsTest.cs} (68%) diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs new file mode 100644 index 00000000000..e9a0410608d --- /dev/null +++ b/Source/Dafny/Plugin.cs @@ -0,0 +1,56 @@ +using System; +using System.Linq; +using System.Reflection; +using Microsoft.Dafny.Plugins; + +namespace Microsoft.Dafny; + +/// +/// 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 +/// +public class Plugin { + private readonly Assembly assembly; + public readonly Configuration Configuration; + + class AutomaticConfiguration : Configuration { + private Func[] rewriters; + public AutomaticConfiguration(Func[] rewriters) { + this.rewriters = rewriters; + } + + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return rewriters.Select(funcErrorReporterRewriter => + funcErrorReporterRewriter(errorReporter)).ToArray(); + } + } + + public Plugin(string pluginPath, string[] args, ErrorReporter reporter) { + assembly = Assembly.LoadFrom(pluginPath); + + System.Type[] rewriterTypes = assembly.GetTypes().Where(t => + t.IsAssignableTo(typeof(Rewriter))).ToArray(); + // Checks about the plugin to be well-behaved. + if (!rewriterTypes.Any()) { + throw new Exception($"Plugin {pluginPath} does not contain any Microsoft.Dafny.Plugins.Rewriter"); + } + + foreach (var configurationType in assembly.GetTypes() + .Where(t => t.IsAssignableTo(typeof(Configuration)))) { + if (Configuration != null) { + throw new Exception($"Only one class should extend Microsoft.Dafny.Plugins.Configuration from {pluginPath}. Please remove {configurationType}."); + } + Configuration = Activator.CreateInstance(configurationType) as Configuration; + + if (Configuration == null) { + throw new Exception($"Could not instantiate a {configurationType} from {pluginPath}"); + } + Configuration.ParseArguments(args); + } + + Configuration ??= new AutomaticConfiguration( + rewriterTypes.Select>((System.Type rewriterType) => + (ErrorReporter errorReporter) => + Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray()); + } +} \ No newline at end of file diff --git a/Source/Dafny/Plugins/Configuration.cs b/Source/Dafny/Plugins/Configuration.cs index be1acd58a91..532675b7fcf 100644 --- a/Source/Dafny/Plugins/Configuration.cs +++ b/Source/Dafny/Plugins/Configuration.cs @@ -5,6 +5,10 @@ namespace Microsoft.Dafny.Plugins; /// /// A class that plugins should extend, in order to receive plugin-specific command-line arguments +/// +/// If no class extending Microsoft.Dafny.Plugins.Configuration is defined in the assembly plugin, +/// Dafny will implicitly load all classes extending Rewriter +/// providing them with an ErrorReporter as the first and only argument /// public abstract class Configuration { /// diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs index 8c0350952b0..9969adba162 100644 --- a/Source/Dafny/Plugins/Rewriter.cs +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -3,6 +3,9 @@ namespace Microsoft.Dafny.Plugins { /// /// 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 as the first and only argument. /// public abstract class Rewriter { /// @@ -11,16 +14,19 @@ public abstract class Rewriter { protected readonly ErrorReporter Reporter; /// - /// Make sure, when you extends an Rewriter in a plugin, that - /// you provide an ErrorReporter to the base class (you can obtain one in Configuration.GetRewriters()) + /// 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 error message here"); + /// 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() /// - /// + /// The error reporter. Usually outputs automatically to IDE or command-line public Rewriter(ErrorReporter reporter) { Contract.Requires(reporter != null); this.Reporter = reporter; diff --git a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs similarity index 94% rename from Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs rename to Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index d2c37296b9b..e5368e89115 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExternalResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -25,7 +25,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; [TestClass] -public class ExternalResolverTest : DafnyLanguageServerTestBase { +public class PluginsTest : DafnyLanguageServerTestBase { private ILanguageClient client; private DiagnosticsReceiver diagnosticReceiver; private string libraryPath; @@ -68,7 +68,7 @@ protected override IConfiguration CreateConfiguration() { /// /// 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. + /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// public async Task GetLibrary(string code) { var temp = Path.GetTempFileName(); @@ -96,7 +96,7 @@ public async Task GetLibrary(string code) { } [TestMethod] - public async Task EnsureItIsPossibleToPluginIRewriter() { + public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { var documentItem = CreateTestDocument("function test(): int { 1 }"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var resolutionReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); diff --git a/Source/DafnyPipeline.Test/ExternalResolverTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs similarity index 68% rename from Source/DafnyPipeline.Test/ExternalResolverTest.cs rename to Source/DafnyPipeline.Test/PluginsTest.cs index 94aabb2460e..f4cc9ec0074 100644 --- a/Source/DafnyPipeline.Test/ExternalResolverTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -12,11 +12,11 @@ namespace DafnyPipeline.Test; -[Collection("External Resolver plug-in tests")] -public class ExternalResolverTest { +[Collection("Dafny plug-ins tests")] +public class PluginsTest { /// /// 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. + /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// public async Task GetLibrary(string code) { var temp = Path.GetTempFileName(); @@ -50,7 +50,7 @@ public string GetLastErrorMessage() { } [Fact] - public async void EnsureItIsPossibleToPluginIRewriter() { + public async void EnsurePluginIsExecuted() { var library = await GetLibrary(@" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; @@ -93,4 +93,35 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { Assert.Equal(1, reporter.Count(ErrorLevel.Error)); Assert.Equal("Impossible to continue because whatever", reporter.GetLastErrorMessage()); } + + [Fact] + public async void EnsurePluginIsExecutedEvenWithoutConfiguration() { + var library = await GetLibrary(@" +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; + +public class ErrorRewriter: Rewriter { + public ErrorRewriter(ErrorReporter reporter): base(reporter) {} + + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); + } +}"); + + var reporter = new CollectionErrorReporter(); + var options = new DafnyOptions(reporter); + options.Plugins.Add(new Microsoft.Dafny.Plugin(library, new string[] { "ignored arguments" }, reporter)); + DafnyOptions.Install(options); + + var programString = "function test(): int { 1 }"; + ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDecl(), null); + Microsoft.Dafny.Type.ResetScopes(); + BuiltIns builtIns = new BuiltIns(); + Parser.Parse(programString, "virtual", "virtual", module, builtIns, reporter); + var dafnyProgram = new Program("programName", module, builtIns, reporter); + Main.Resolve(dafnyProgram, reporter); + + Assert.Equal(1, reporter.Count(ErrorLevel.Error)); + Assert.Equal("Impossible to continue", reporter.GetLastErrorMessage()); + } } From 62ad0ed550aaa43a41ffbc1270d7b63c92ea3cde Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 10:01:12 -0600 Subject: [PATCH 25/47] support for commas in arguments. --- Source/Dafny/DafnyOptions.cs | 24 +++++++++---------- .../Various/PluginsTest.cs | 4 ++-- 2 files changed, 13 insertions(+), 15 deletions(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 7b04ac8a2c4..51b38b93177 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -248,20 +248,18 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com var pluginArray = pluginAndArgument.Split(','); var pluginPath = pluginArray[0]; var arguments = Array.Empty(); - if (pluginArray.Length > 2) { - ps.Error("\"plugin\" cannot have more than one comma separating the DLL from the arguments"); - } else { - if (pluginArray.Length == 2) { - // Parse arguments, accepting and remove double quotes that isolate long arguments - var splitter = new Regex(@"""((?:[^""]|\\"")*)""|([^ ]+)"); - arguments = splitter.Matches(pluginArray[1]).Select( - matchResult => matchResult.Groups[1].Success ? - matchResult.Groups[1].Value.Replace(@"\""", @"""") : - matchResult.Groups[2].Value - ).ToArray(); - } - Plugins.Add(new Plugin(pluginPath, arguments, errorReporter)); + 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)); } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index e5368e89115..17b407a3327 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -63,7 +63,7 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { protected override IConfiguration CreateConfiguration() { return new ConfigurationBuilder().AddCommandLine( - new[] { "--dafny:plugins:0=" + libraryPath + ",\"because whatever\"" }).Build(); + new[] { "--dafny:plugins:0=" + libraryPath + ",\"because, whatever\"" }).Build(); } /// @@ -103,7 +103,7 @@ public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); - Assert.AreEqual("Impossible to continue because whatever", diagnostics[0].Message); + Assert.AreEqual("Impossible to continue because, whatever", diagnostics[0].Message); Assert.AreEqual(new Range((-1, -1), (-1, 29)), diagnostics[0].Range); } } From 647b2334cf39593304f849d66c701544568f2be2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 11:13:43 -0600 Subject: [PATCH 26/47] Plugin test should use the module's first positional token. --- Source/DafnyLanguageServer.Test/Various/PluginsTest.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index 17b407a3327..a82441b091a 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -40,7 +40,7 @@ public async Task SetUp() { public class TestConfiguration: Configuration { public string Argument = """"; public override void ParseArguments(string[] args) { - Argument = args[0]; + Argument = args.Length > 0 ? args[0] : ""[no argument]""; } public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { return new Rewriter[]{new ErrorRewriter(errorReporter, this)}; @@ -55,7 +55,7 @@ public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): b } public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue ""+configuration.Argument); + Reporter.Error(MessageSource.Compiler, moduleDefinition.GetFirstTopLevelToken(), ""Impossible to continue ""+configuration.Argument); } }"); client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); @@ -104,6 +104,6 @@ public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); Assert.AreEqual("Impossible to continue because, whatever", diagnostics[0].Message); - Assert.AreEqual(new Range((-1, -1), (-1, 29)), diagnostics[0].Range); + Assert.AreEqual(new Range((0, 9), (0, 13)), diagnostics[0].Range); } } From 7698e7c5b1a0c75e8d3e1fdabfa440adb5ae225d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 12:54:04 -0600 Subject: [PATCH 27/47] * Ensure even the default module's default token is not empty even if it has no declaration * Correct support for long arguments --- Source/Dafny/AST/DafnyAst.cs | 7 ++++++- Source/Dafny/DafnyOptions.cs | 5 ++++- Source/DafnyLanguageServer.Test/Various/PluginsTest.cs | 4 ++-- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 065630de1ba..d514b34a541 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -4233,7 +4233,12 @@ public IToken GetFirstTopLevelToken() { .Where(x => x != null) .SelectMany(classDecl => classDecl.Members) .Where(member => member.tok.line > 0) - .Select(member => member.tok).FirstOrDefault(Token.NoToken); + .Select(member => member.tok) + .Concat(TopLevelDecls.Select(x => x as LiteralModuleDecl) + .Where(x => x != null) + .Select((moduleDecl => moduleDecl.ModuleDef.GetFirstTopLevelToken())) + .Where(tok => tok.line > 0) + ).FirstOrDefault(Token.NoToken); } } diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 51b38b93177..14f1659c04c 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -242,7 +242,10 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com pluginAndArgument[0] == '"' && pluginAndArgument[^1] == '"' ) { - pluginAndArgument = pluginAndArgument.Substring(1, pluginAndArgument.Length - 2); + 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(','); diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index a82441b091a..01a631b6aa7 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -63,7 +63,7 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { protected override IConfiguration CreateConfiguration() { return new ConfigurationBuilder().AddCommandLine( - new[] { "--dafny:plugins:0=" + libraryPath + ",\"because, whatever\"" }).Build(); + new[] { $@"--dafny:plugins:0=""{libraryPath},\""because\\ whatever\""""" }).Build(); } /// @@ -103,7 +103,7 @@ public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); - Assert.AreEqual("Impossible to continue because, whatever", diagnostics[0].Message); + Assert.AreEqual("Impossible to continue because\\ whatever", diagnostics[0].Message); Assert.AreEqual(new Range((0, 9), (0, 13)), diagnostics[0].Range); } } From eeb264b829776e190857358bf372c6970a03d914 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 14:53:54 -0600 Subject: [PATCH 28/47] PostResolve also for the entire program. Another test to exemplify the plugin mechanism --- Source/Dafny/Plugins/Rewriter.cs | 11 ++ Source/Dafny/Resolver.cs | 12 +- .../Various/PluginsAdvancedTest.cs | 168 ++++++++++++++++++ 3 files changed, 186 insertions(+), 5 deletions(-) create mode 100644 Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs index 9969adba162..28c91e1e6ed 100644 --- a/Source/Dafny/Plugins/Rewriter.cs +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -87,5 +87,16 @@ public virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) { public virtual void PostResolve(ModuleDefinition moduleDefinition) { Contract.Requires(moduleDefinition != null); } + + /// + /// Phase 5/5 + /// 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) + /// + /// The entire program after it is fully resolved + public virtual void PostResolve(Program program) { + Contract.Requires(program != null); + } } } \ No newline at end of file diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index db863b80f17..f14ad26dfca 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -439,11 +439,9 @@ public void ResolveProgram(Program prog) { rewriters.Add(new InductionRewriter(reporter)); - if (DafnyOptions.O.Plugins.Count() >= 1) { - foreach (var plugin in DafnyOptions.O.Plugins) { - foreach (var rewriter in plugin.Configuration.GetRewriters(reporter)) { - rewriters.Add(rewriter); - } + foreach (var plugin in DafnyOptions.O.Plugins) { + foreach (var rewriter in plugin.Configuration.GetRewriters(reporter)) { + rewriters.Add(rewriter); } } @@ -704,6 +702,10 @@ public void ResolveProgram(Program prog) { r.PostResolve(module); } } + + foreach (var r in rewriters) { + r.PostResolve(prog); + } } void FillInDefaultDecreasesClauses(Program prog) { diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs new file mode 100644 index 00000000000..f5a4dd27b40 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -0,0 +1,168 @@ +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using System.Threading.Tasks; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using System; +using Microsoft.Dafny.LanguageServer.Language; +using Microsoft.VisualStudio.TestTools.UnitTesting; +using System.Collections.Generic; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.Boogie; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Microsoft.Extensions.Configuration; +using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Protocol; +using OmniSharp.Extensions.LanguageServer.Protocol.Client; +using OmniSharp.Extensions.LanguageServer.Protocol.Document; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; + +[TestClass] +public class PluginsAdvancedTest : DafnyLanguageServerTestBase { + private ILanguageClient client; + private DiagnosticsReceiver diagnosticReceiver; + private string libraryPath; + + [TestInitialize] + public async Task SetUp() { + diagnosticReceiver = new(); + libraryPath = await GetLibrary(@" +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; +using System.Collections; +/// +/// Small plugin that detect all extern method and verify that there are test methods that actually invoke them. +/// +public class TestConfiguration: Configuration { + public string PluginUser = """"; + public bool ForceName = false; + public override void ParseArguments(string[] args) { + ForceName = args.Length > 0 && args[0] == ""force""; + PluginUser = args.Length > 1 ? "", "" + args[1] : """"; + } + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return new Rewriter[]{new ExternCheckRewriter(errorReporter, this)}; + } +} + +public class ExternCheckRewriter: Rewriter { + private readonly TestConfiguration configuration; + + public ExternCheckRewriter(ErrorReporter reporter, TestConfiguration configuration): base(reporter) { + this.configuration = configuration; + } + + public override void PostResolve(Program program) { + foreach (var moduleDefinition in program.Modules()) { + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls) { + if (topLevelDecl is ClassDecl cd) { + foreach (var member in cd.Members) { + if (member is Method methodExtern) { + if (Attributes.Contains(member.Attributes, ""extern"")) { + // Verify that there exists a test method which references this extern method. + var tested = false; + Method candidate = null; + foreach (var member2 in cd.Members) { + if (member2 == member || !(member2 is Method methodTest)) { + continue; + } + if (!Attributes.Contains(methodTest.Attributes, ""test"")) { + continue; + } + if (!moduleDefinition.CallGraph.Reaches(methodTest, methodExtern)) { + continue; + } + candidate = methodTest; + + if (configuration.ForceName && candidate.Name != methodExtern.Name + ""_test"") { + continue; + } + tested = true; + break; + } + + if (!tested) { + var forceMessage = configuration.ForceName ? $"" named {methodExtern.Name}_test"" : """"; + var token = configuration.ForceName && candidate != null + ? new NestedToken(methodExtern.tok, candidate.tok, ""You might want to just rename this method"") + : methodExtern.tok; + Reporter.Error(MessageSource.Resolver, token, + $""Please declare a method {{:test}}{forceMessage} that will call {methodExtern.Name}{configuration.PluginUser}""); + } + } + } + } + } + } + } + } +}"); + client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); + } + + protected override IConfiguration CreateConfiguration() { + return new ConfigurationBuilder().AddCommandLine( + new[] { $@"--dafny:plugins:0=""{libraryPath},force you""" }).Build(); + } + + /// + /// This method creates a library and returns the path to that library. + /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. + /// + public async Task GetLibrary(string code) { + var temp = Path.GetTempFileName(); + var compilation = CSharpCompilation.Create("tempAssembly"); + var standardLibraries = new List() + { + "DafnyPipeline", + "System.Runtime", + "Boogie.Core", + "System.Collections" + }; + compilation = compilation.AddReferences(standardLibraries.Select(fileName => + MetadataReference.CreateFromFile(Assembly.Load(fileName).Location))) + .AddReferences( + MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location)) + .WithOptions( + new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary) + ); + var syntaxTree = CSharpSyntaxTree.ParseText(code); + compilation = compilation.AddSyntaxTrees(syntaxTree); + var assemblyPath = $"{temp}.dll"; + var result = compilation.Emit(assemblyPath); + + Assert.IsTrue(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); + return assemblyPath; + } + + [TestMethod] + public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration() { + var documentItem = CreateTestDocument(@" +method {:extern} myMethod(i: int) returns (j: int) + +method {:test} myMethodWrongName() { + var result := myMethod(0); + expect result == 1; +} +"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var resolutionReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); + Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); + var diagnostics = resolutionReport.Diagnostics.ToArray(); + Assert.AreEqual(1, diagnostics.Length); + Assert.AreEqual("Please declare a method {:test} named myMethod_test that will call myMethod, you", diagnostics[0].Message); + Assert.AreEqual(new Range((1, 17), (1, 25)), diagnostics[0].Range); + var related = diagnostics[0].RelatedInformation?.GetEnumerator(); + Assert.IsTrue(related != null && related.MoveNext()); + Assert.AreEqual("You might want to just rename this method", related.Current.Message); + Assert.AreEqual(new Range((3, 15), (3, 32)), related.Current.Location.Range); + related.Dispose(); + } +} From d5b653fe046f971f255c0cb8f63595ab25db03b6 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 14:54:33 -0600 Subject: [PATCH 29/47] Addressed review comments --- Source/Dafny/Plugin.cs | 50 +++++++++++++------ Source/DafnyLanguageServer/README.md | 11 ++-- .../Workspace/TextDocumentLoader.cs | 2 +- 3 files changed, 45 insertions(+), 18 deletions(-) diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs index e9a0410608d..d0e77aaaf0f 100644 --- a/Source/Dafny/Plugin.cs +++ b/Source/Dafny/Plugin.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Generic; using System.Linq; using System.Reflection; using Microsoft.Dafny.Plugins; @@ -10,8 +11,11 @@ namespace Microsoft.Dafny; /// The configuration provides the methods to parse command-line arguments and obtain Rewriters /// public class Plugin { + public Configuration Configuration; + + private readonly string path; private readonly Assembly assembly; - public readonly Configuration Configuration; + private System.Type[] rewriterTypes; class AutomaticConfiguration : Configuration { private Func[] rewriters; @@ -25,32 +29,50 @@ public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { } } + public static IEnumerable GetConfigurationsTypes(Assembly assembly) { + return assembly.GetTypes() + .Where(t => t.IsAssignableTo(typeof(Configuration))); + } + public Plugin(string pluginPath, string[] args, ErrorReporter reporter) { - assembly = Assembly.LoadFrom(pluginPath); + path = pluginPath; + assembly = Assembly.LoadFrom(path); + rewriterTypes = CheckPluginForRewriters(assembly, path); + Configuration = LoadConfiguration(assembly, args, path, rewriterTypes); + } - System.Type[] rewriterTypes = assembly.GetTypes().Where(t => + 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 (!rewriterTypes.Any()) { - throw new Exception($"Plugin {pluginPath} does not contain any Microsoft.Dafny.Plugins.Rewriter"); + if (!rewriterTpes.Any()) { + throw new Exception($"Plugin {path} does not contain any Microsoft.Dafny.Plugins.Rewriter"); } - foreach (var configurationType in assembly.GetTypes() - .Where(t => t.IsAssignableTo(typeof(Configuration)))) { - if (Configuration != null) { - throw new Exception($"Only one class should extend Microsoft.Dafny.Plugins.Configuration from {pluginPath}. Please remove {configurationType}."); + 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 = Activator.CreateInstance(configurationType) as Configuration; - if (Configuration == null) { - throw new Exception($"Could not instantiate a {configurationType} from {pluginPath}"); + configuration = (Configuration)Activator.CreateInstance(configurationType); + + if (configuration == null) { + throw new Exception($"Could not instantiate a {configurationType} from {path}"); } - Configuration.ParseArguments(args); + + configuration.ParseArguments(args); } - Configuration ??= new AutomaticConfiguration( + configuration ??= new AutomaticConfiguration( rewriterTypes.Select>((System.Type rewriterType) => (ErrorReporter errorReporter) => Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray()); + return configuration; } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer/README.md b/Source/DafnyLanguageServer/README.md index 17514b07937..2701de8d93f 100644 --- a/Source/DafnyLanguageServer/README.md +++ b/Source/DafnyLanguageServer/README.md @@ -79,9 +79,14 @@ Options provided through the command line have higher priority than the options ### Plugins ```sh -# Provides a path to assemblies -# that contain an instantiatable Microsoft.Dafny.Plugins.Configuration to use during resolution +# Provides a path to assemblies that contain +# 1) Either a class extending Microsoft.Dafny.Plugins.Configuration to receive plugin arguments +# and provide classes extending Microsoft.Dafny.Plugins.Rewriter +# 2) Or, if no Configuration is defined, at least one Microsoft.Dafny.Plugins.Rewriter that it will load during resolution # Optionally, after a comma, provide an extra list of space-separated arguments. +# Easier to use via VSCode's Settings interface (no need to escape inner double quotes) # Default: "" (nothing extra is loaded) ---dafny:plugins:0= +--dafny:plugins:0=example.dll +--dafny:plugins:1=example2.dll,oneArgument +"--dafny:plugins:1=\"example2.dll,\\\"firstArgument with space\\\" secondArgument\"" ``` diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 7a4bcadbd3e..b39f0bebf4f 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -117,7 +117,7 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger(), textDocument, errorReporter, program, loadCanceled: false); } - if (dafnyPluginsOptions.Value.Plugins.Length > 0 && DafnyOptions.O.Plugins.Count == 0) { + if (dafnyPluginsOptions.Value.Plugins.Length > 0 && !DafnyOptions.O.Plugins.Any()) { try { foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { DafnyOptions.O.Parse(new[] { "-plugin:" + pluginPathArgument }); From 6e236bdfaada8d267709938498d345ffaa2a00be Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Jan 2022 15:01:16 -0600 Subject: [PATCH 30/47] Fixed typos --- Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index f5a4dd27b40..5ba5e04e6b6 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -38,7 +38,7 @@ public async Task SetUp() { using Microsoft.Dafny.Plugins; using System.Collections; /// -/// Small plugin that detect all extern method and verify that there are test methods that actually invoke them. +/// Small plugin that detects all extern methods and verifies that there are test methods that actually invoke them. /// public class TestConfiguration: Configuration { public string PluginUser = """"; From 9f9e3be42eb6796fdf38df1e74e82f32371cd183 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 31 Jan 2022 16:36:39 -0600 Subject: [PATCH 31/47] Addressed review comments --- Source/Dafny/AST/DafnyAst.cs | 8 +- Source/Dafny/Reporting.cs | 8 +- .../Various/PluginsAdvancedTest.cs | 74 +++---------------- .../Various/PluginsTest.cs | 72 +++--------------- .../Various/PluginsTestBase.cs | 65 ++++++++++++++++ Source/DafnyPipeline.Test/PluginsTest.cs | 17 ++--- 6 files changed, 102 insertions(+), 142 deletions(-) create mode 100644 Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index d514b34a541..63c1a10e819 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -4229,14 +4229,12 @@ public bool IsEssentiallyEmptyModuleBody() { } public IToken GetFirstTopLevelToken() { - return TopLevelDecls.Select(x => x as ClassDecl) - .Where(x => x != null) + return TopLevelDecls.OfType() .SelectMany(classDecl => classDecl.Members) .Where(member => member.tok.line > 0) .Select(member => member.tok) - .Concat(TopLevelDecls.Select(x => x as LiteralModuleDecl) - .Where(x => x != null) - .Select((moduleDecl => moduleDecl.ModuleDef.GetFirstTopLevelToken())) + .Concat(TopLevelDecls.OfType() + .Select(moduleDecl => moduleDecl.ModuleDef.GetFirstTopLevelToken()) .Where(tok => tok.line > 0) ).FirstOrDefault(Token.NoToken); } diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 07f65c674b9..e6104436010 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -153,11 +153,11 @@ public static string TokenToString(IToken tok) { } public abstract class BatchErrorReporter : ErrorReporter { - protected readonly Dictionary> allMessages; + protected readonly Dictionary> AllMessages; protected BatchErrorReporter() { ErrorsOnly = false; - allMessages = new Dictionary> { + AllMessages = new Dictionary> { [ErrorLevel.Error] = new(), [ErrorLevel.Warning] = new(), [ErrorLevel.Info] = new() @@ -169,12 +169,12 @@ public override bool Message(MessageSource source, ErrorLevel level, IToken tok, // discard the message return false; } - allMessages[level].Add(new ErrorMessage { token = tok, message = msg }); + AllMessages[level].Add(new ErrorMessage { token = tok, message = msg }); return true; } public override int Count(ErrorLevel level) { - return allMessages[level].Count; + return AllMessages[level].Count; } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index 5ba5e04e6b6..520e018d22b 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -1,39 +1,21 @@ -using System.Collections.Generic; -using System.IO; -using System.Linq; -using System.Reflection; +using System.Linq; using System.Threading.Tasks; -using Microsoft.CodeAnalysis; -using Microsoft.CodeAnalysis.CSharp; -using System; -using Microsoft.Dafny.LanguageServer.Language; using Microsoft.VisualStudio.TestTools.UnitTesting; -using System.Collections.Generic; using System.Threading; -using System.Threading.Tasks; -using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; -using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; -using Microsoft.Extensions.Configuration; -using Microsoft.Extensions.Logging; -using OmniSharp.Extensions.LanguageServer.Protocol; -using OmniSharp.Extensions.LanguageServer.Protocol.Client; -using OmniSharp.Extensions.LanguageServer.Protocol.Document; -using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; [TestClass] -public class PluginsAdvancedTest : DafnyLanguageServerTestBase { - private ILanguageClient client; - private DiagnosticsReceiver diagnosticReceiver; - private string libraryPath; - +public class PluginsAdvancedTest : PluginsTestBase { [TestInitialize] public async Task SetUp() { - diagnosticReceiver = new(); - libraryPath = await GetLibrary(@" + await SetUpPlugin(); + } + + protected override string GetLibraryCode() { + return @" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; using System.Collections; @@ -103,43 +85,11 @@ public override void PostResolve(Program program) { } } } -}"); - client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); +}"; } - protected override IConfiguration CreateConfiguration() { - return new ConfigurationBuilder().AddCommandLine( - new[] { $@"--dafny:plugins:0=""{libraryPath},force you""" }).Build(); - } - - /// - /// This method creates a library and returns the path to that library. - /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. - /// - public async Task GetLibrary(string code) { - var temp = Path.GetTempFileName(); - var compilation = CSharpCompilation.Create("tempAssembly"); - var standardLibraries = new List() - { - "DafnyPipeline", - "System.Runtime", - "Boogie.Core", - "System.Collections" - }; - compilation = compilation.AddReferences(standardLibraries.Select(fileName => - MetadataReference.CreateFromFile(Assembly.Load(fileName).Location))) - .AddReferences( - MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location)) - .WithOptions( - new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary) - ); - var syntaxTree = CSharpSyntaxTree.ParseText(code); - compilation = compilation.AddSyntaxTrees(syntaxTree); - var assemblyPath = $"{temp}.dll"; - var result = compilation.Emit(assemblyPath); - - Assert.IsTrue(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); - return assemblyPath; + protected override string[] GetCommandLineArgument() { + return new[] { $@"--dafny:plugins:0=""{LibraryPath},force you""" }; } [TestMethod] @@ -152,8 +102,8 @@ public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration( expect result == 1; } "); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var resolutionReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); + await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var resolutionReport = await DiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index 01a631b6aa7..32b832b3ee7 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -1,39 +1,20 @@ -using System.Collections.Generic; -using System.IO; -using System.Linq; -using System.Reflection; +using System.Linq; using System.Threading.Tasks; -using Microsoft.CodeAnalysis; -using Microsoft.CodeAnalysis.CSharp; -using System; -using Microsoft.Dafny.LanguageServer.Language; using Microsoft.VisualStudio.TestTools.UnitTesting; -using System.Collections.Generic; using System.Threading; -using System.Threading.Tasks; -using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; -using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; -using Microsoft.Extensions.Configuration; -using Microsoft.Extensions.Logging; -using OmniSharp.Extensions.LanguageServer.Protocol; -using OmniSharp.Extensions.LanguageServer.Protocol.Client; -using OmniSharp.Extensions.LanguageServer.Protocol.Document; -using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; [TestClass] -public class PluginsTest : DafnyLanguageServerTestBase { - private ILanguageClient client; - private DiagnosticsReceiver diagnosticReceiver; - private string libraryPath; - +public class PluginsTest : PluginsTestBase { [TestInitialize] public async Task SetUp() { - diagnosticReceiver = new(); - libraryPath = await GetLibrary(@" + await SetUpPlugin(); + } + protected override string GetLibraryCode() { + return @" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; @@ -57,49 +38,18 @@ public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): b public override void PostResolve(ModuleDefinition moduleDefinition) { Reporter.Error(MessageSource.Compiler, moduleDefinition.GetFirstTopLevelToken(), ""Impossible to continue ""+configuration.Argument); } -}"); - client = await InitializeClient(options => options.OnPublishDiagnostics(diagnosticReceiver.NotificationReceived)); +}"; } - protected override IConfiguration CreateConfiguration() { - return new ConfigurationBuilder().AddCommandLine( - new[] { $@"--dafny:plugins:0=""{libraryPath},\""because\\ whatever\""""" }).Build(); - } - - /// - /// This method creates a library and returns the path to that library. - /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. - /// - public async Task GetLibrary(string code) { - var temp = Path.GetTempFileName(); - var compilation = CSharpCompilation.Create("tempAssembly"); - var standardLibraries = new List() - { - "DafnyPipeline", - "System.Runtime", - "Boogie.Core" - }; - compilation = compilation.AddReferences(standardLibraries.Select(fileName => - MetadataReference.CreateFromFile(Assembly.Load(fileName).Location))) - .AddReferences( - MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location)) - .WithOptions( - new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary) - ); - var syntaxTree = CSharpSyntaxTree.ParseText(code); - compilation = compilation.AddSyntaxTrees(syntaxTree); - var assemblyPath = $"{temp}.dll"; - var result = compilation.Emit(assemblyPath); - - Assert.IsTrue(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); - return assemblyPath; + protected override string[] GetCommandLineArgument() { + return new[] { $@"--dafny:plugins:0=""{LibraryPath},\""because\\ whatever\""""" }; } [TestMethod] public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { var documentItem = CreateTestDocument("function test(): int { 1 }"); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var resolutionReport = await diagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); + await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var resolutionReport = await DiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); Assert.AreEqual(1, diagnostics.Length); diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs new file mode 100644 index 00000000000..c1f1e9376d8 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -0,0 +1,65 @@ +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reflection; +using System.Threading.Tasks; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Microsoft.Extensions.Configuration; +using Microsoft.VisualStudio.TestTools.UnitTesting; +using OmniSharp.Extensions.LanguageServer.Protocol.Client; +using OmniSharp.Extensions.LanguageServer.Protocol.Document; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; + +public abstract class PluginsTestBase : DafnyLanguageServerTestBase { + protected ILanguageClient Client; + protected DiagnosticsReceiver DiagnosticReceiver; + protected string LibraryPath; + + /// + /// This method creates a library and returns the path to that library. + /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. + /// + private string GetLibrary(string code) { + var temp = Path.GetTempFileName(); + var compilation = CSharpCompilation.Create("tempAssembly"); + var standardLibraries = new List() + { + "DafnyPipeline", + "System.Runtime", + "Boogie.Core", + "System.Collections" + }; + compilation = compilation.AddReferences(standardLibraries.Select(fileName => + MetadataReference.CreateFromFile(Assembly.Load((string)fileName).Location))) + .AddReferences( + MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location)) + .WithOptions( + new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary) + ); + var syntaxTree = CSharpSyntaxTree.ParseText(code); + compilation = compilation.AddSyntaxTrees(syntaxTree); + var assemblyPath = $"{temp}.dll"; + var result = compilation.Emit(assemblyPath); + + Assert.IsTrue(result.Success, string.Join("\n", result.Diagnostics.Select(d => d.ToString()))); + return assemblyPath; + } + + protected abstract string GetLibraryCode(); + + protected abstract string[] GetCommandLineArgument(); + + public async Task SetUpPlugin() { + DiagnosticReceiver = new(); + LibraryPath = GetLibrary(GetLibraryCode()); + Client = await InitializeClient(options => options.OnPublishDiagnostics(DiagnosticReceiver.NotificationReceived)); + } + + + protected override IConfiguration CreateConfiguration() { + return new ConfigurationBuilder().AddCommandLine(GetCommandLineArgument()).Build(); + } +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index f4cc9ec0074..bcef80e132d 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -1,10 +1,7 @@ -using System; -using System.Collections.Generic; +using System.Collections.Generic; using System.IO; using System.Linq; using System.Reflection; -using System.Text.Json; -using System.Threading.Tasks; using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; using Xunit; @@ -18,7 +15,7 @@ public class PluginsTest { /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// - public async Task GetLibrary(string code) { + private string GetLibrary(string code) { var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create("tempAssembly"); var standardLibraries = new List() @@ -45,13 +42,13 @@ public async Task GetLibrary(string code) { class CollectionErrorReporter : BatchErrorReporter { public string GetLastErrorMessage() { - return allMessages[ErrorLevel.Error][0].message; + return AllMessages[ErrorLevel.Error][0].message; } } [Fact] - public async void EnsurePluginIsExecuted() { - var library = await GetLibrary(@" + public void EnsurePluginIsExecuted() { + var library = GetLibrary(@" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; @@ -95,8 +92,8 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { } [Fact] - public async void EnsurePluginIsExecutedEvenWithoutConfiguration() { - var library = await GetLibrary(@" + public void EnsurePluginIsExecutedEvenWithoutConfiguration() { + var library = GetLibrary(@" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; From e8ddf7c0c81e18875bbdf9b1ffc7bc969b6af66c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 1 Feb 2022 14:34:04 -0600 Subject: [PATCH 32/47] Reviews implemented. --- Source/Dafny/DafnyOptions.cs | 6 +++-- Source/Dafny/Plugins/Configuration.cs | 10 ++++--- Source/Dafny/Plugins/Rewriter.cs | 5 ++-- Source/DafnyLanguageServer/README.md | 34 ++++++++++++++++++------ Source/DafnyPipeline.Test/PluginsTest.cs | 14 ++++++---- 5 files changed, 48 insertions(+), 21 deletions(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 14f1659c04c..8e71c1f77bf 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -845,10 +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:[:] +/plugin:[ ] (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.Initializer to receive arguments + 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: 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'. diff --git a/Source/Dafny/Plugins/Configuration.cs b/Source/Dafny/Plugins/Configuration.cs index 532675b7fcf..1bab3ac70e2 100644 --- a/Source/Dafny/Plugins/Configuration.cs +++ b/Source/Dafny/Plugins/Configuration.cs @@ -4,11 +4,13 @@ namespace Microsoft.Dafny.Plugins; /// -/// A class that plugins should extend, in order to receive plugin-specific command-line arguments +/// 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 no class extending Microsoft.Dafny.Plugins.Configuration is defined in the assembly plugin, -/// Dafny will implicitly load all classes extending Rewriter -/// providing them with an ErrorReporter as the first and only argument +/// 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. /// public abstract class Configuration { /// diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs index 28c91e1e6ed..f577caf9076 100644 --- a/Source/Dafny/Plugins/Rewriter.cs +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -5,7 +5,8 @@ namespace Microsoft.Dafny.Plugins { /// 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 as the first and only argument. + /// of Rewriter from the plugin, providing them with an ErrorReporter in the constructor + /// as the first and only argument. /// public abstract class Rewriter { /// @@ -68,7 +69,7 @@ public virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) { /// /// Phase 4/5 - /// Override this method to obtain the module definition after resolving decreasesResolve + /// Override this method to obtain the module definition after the phase decreasesResolve /// You can then report errors using reporter.Error (see above) /// /// A module definition after it diff --git a/Source/DafnyLanguageServer/README.md b/Source/DafnyLanguageServer/README.md index 2701de8d93f..c295534908c 100644 --- a/Source/DafnyLanguageServer/README.md +++ b/Source/DafnyLanguageServer/README.md @@ -79,14 +79,32 @@ Options provided through the command line have higher priority than the options ### Plugins ```sh -# Provides a path to assemblies that contain -# 1) Either a class extending Microsoft.Dafny.Plugins.Configuration to receive plugin arguments -# and provide classes extending Microsoft.Dafny.Plugins.Rewriter -# 2) Or, if no Configuration is defined, at least one Microsoft.Dafny.Plugins.Rewriter that it will load during resolution -# Optionally, after a comma, provide an extra list of space-separated arguments. +# Provides a path to assemblies and optional space-separated command-line arguments after a commo. # Easier to use via VSCode's Settings interface (no need to escape inner double quotes) -# Default: "" (nothing extra is loaded) +# Repeat with --dafny:plugins:0=... --dafny:plugins:1=... for multiple plugins. --dafny:plugins:0=example.dll ---dafny:plugins:1=example2.dll,oneArgument -"--dafny:plugins:1=\"example2.dll,\\\"firstArgument with space\\\" secondArgument\"" +--dafny:plugins:0=example2.dll,oneArgument +"--dafny:plugins:0=\"example2.dll,\\\"firstArgument with space\\\" secondArgument\"" ``` + +#### About plugins +Plugins are libraries linked to a `Dafny.dll` of the same version than the language server. +A plugin typically defines: + +* Zero or one class extending `Microsoft.Dafny.Plugins.Configuration` which receives plugins arguments in their method `ParseArguments`, + and returns a list of `Microsoft.Dafny.Plugins.Rewriter` when their method `GetRewriters()` is called by Dafny. +* Zero or more classes extending `Microsoft.Dafny.Plugins.Rewriter`. + If a configuration class is provided, it is responsible for instantiating them and returning them in `GetRewriters()`. + If no configuration class is provided, an automatic configuration will load every defined `Rewriter`s automatically. + +The most important methods of the class `Rewriter` that plugins override are +* (experimental) `PreResolve(ModuleDefinition)`: Here you can optionally modify the AST before it is resolved. +* `PostResolve(ModuleDefinition)`: This method is repeatedly called with every resolved and type-checked module, before verification. + Plugins override this method typically to report additional diagnostics. +* `PostResolve(Program)`: This method is called once after all `PostResolve(ModuleDefinition)` have been called. + +Plugins are typically used to report additional diagnostics such as unsupported constructs for specific compilers (through the methods `Èrror(...)` and `Warning(...)` of the field `Reporter` of the class `Rewriter`) + +Note that all plugin errors should use the original program's expressions' token and NOT `Token.NoToken`, else no error will be displayed in the IDE. + +Morover, plugins should not write anything to `stdout` as it interferes with the communication protocol with the IDE. \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index bcef80e132d..1884d21e57f 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -111,14 +111,18 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { DafnyOptions.Install(options); var programString = "function test(): int { 1 }"; + var dafnyProgram = CreateProgram(programString, reporter); + Main.Resolve(dafnyProgram, reporter); + Assert.Equal(1, reporter.Count(ErrorLevel.Error)); + Assert.Equal("Impossible to continue", reporter.GetLastErrorMessage()); + } + + private static Program CreateProgram(string programString, CollectionErrorReporter reporter) { ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDecl(), null); - Microsoft.Dafny.Type.ResetScopes(); + Type.ResetScopes(); BuiltIns builtIns = new BuiltIns(); Parser.Parse(programString, "virtual", "virtual", module, builtIns, reporter); var dafnyProgram = new Program("programName", module, builtIns, reporter); - Main.Resolve(dafnyProgram, reporter); - - Assert.Equal(1, reporter.Count(ErrorLevel.Error)); - Assert.Equal("Impossible to continue", reporter.GetLastErrorMessage()); + return dafnyProgram; } } From a27836ef79c68934d328fcd954a06727d646af3d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 2 Feb 2022 16:33:11 -0600 Subject: [PATCH 33/47] Fixed the synchronicity problem between two different plugin tests. --- .../Various/PluginsAdvancedTest.cs | 18 +++++++++++++++++- .../Various/PluginsTest.cs | 18 +++++++++++++++++- .../Various/PluginsTestBase.cs | 16 +++++++++++++--- .../Various/ShutdownTest.cs | 2 +- .../Workspace/TextDocumentLoader.cs | 1 + 5 files changed, 49 insertions(+), 6 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index 520e018d22b..272d3d89a34 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -3,6 +3,7 @@ using Microsoft.VisualStudio.TestTools.UnitTesting; using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Microsoft.Extensions.DependencyModel; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -19,6 +20,9 @@ protected override string GetLibraryCode() { using Microsoft.Dafny; using Microsoft.Dafny.Plugins; using System.Collections; + +namespace PluginsAdvancedTest { + /// /// Small plugin that detects all extern methods and verifies that there are test methods that actually invoke them. /// @@ -85,9 +89,15 @@ public override void PostResolve(Program program) { } } } +} + }"; } + protected override string GetLibraryName() { + return "PluginsAdvancedTest"; + } + protected override string[] GetCommandLineArgument() { return new[] { $@"--dafny:plugins:0=""{LibraryPath},force you""" }; } @@ -106,7 +116,8 @@ public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration( var resolutionReport = await DiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); - Assert.AreEqual(1, diagnostics.Length); + Assert.AreEqual(1, DafnyOptions.O.Plugins.Count, "Too many plugins loaded"); + Assert.AreEqual(1, diagnostics.Length, LibraryPath + " did not raise an error."); Assert.AreEqual("Please declare a method {:test} named myMethod_test that will call myMethod, you", diagnostics[0].Message); Assert.AreEqual(new Range((1, 17), (1, 25)), diagnostics[0].Range); var related = diagnostics[0].RelatedInformation?.GetEnumerator(); @@ -115,4 +126,9 @@ public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration( Assert.AreEqual(new Range((3, 15), (3, 32)), related.Current.Location.Range); related.Dispose(); } + + [TestCleanup] + public void DoCleanup() { + CleanupPlugin(); + } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index 32b832b3ee7..95004bb9a39 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -18,6 +18,8 @@ protected override string GetLibraryCode() { using Microsoft.Dafny; using Microsoft.Dafny.Plugins; +namespace PluginsTest { + public class TestConfiguration: Configuration { public string Argument = """"; public override void ParseArguments(string[] args) { @@ -38,22 +40,36 @@ public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): b public override void PostResolve(ModuleDefinition moduleDefinition) { Reporter.Error(MessageSource.Compiler, moduleDefinition.GetFirstTopLevelToken(), ""Impossible to continue ""+configuration.Argument); } +} + }"; } + protected override string GetLibraryName() { + return "PluginsTest"; + } + protected override string[] GetCommandLineArgument() { return new[] { $@"--dafny:plugins:0=""{LibraryPath},\""because\\ whatever\""""" }; } [TestMethod] public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { + // TODO: Need to clean up the plugins from the options after they are set. + // This code will run with the plugin from PluginsAdvancedTest, but that plugin won't throw an exception on the code below. var documentItem = CreateTestDocument("function test(): int { 1 }"); await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var resolutionReport = await DiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None); Assert.AreEqual(documentItem.Uri, resolutionReport.Uri); var diagnostics = resolutionReport.Diagnostics.ToArray(); - Assert.AreEqual(1, diagnostics.Length); + Assert.AreEqual(DafnyOptions.O.Plugins.Count, 1, "Too many plugins loaded"); + Assert.AreEqual(1, diagnostics.Length, LibraryPath + " did not raise an error."); Assert.AreEqual("Impossible to continue because\\ whatever", diagnostics[0].Message); Assert.AreEqual(new Range((0, 9), (0, 13)), diagnostics[0].Range); } + + [TestCleanup] + public void DoCleanup() { + CleanupPlugin(); + } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index c1f1e9376d8..2a69166eea6 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -2,6 +2,7 @@ using System.IO; using System.Linq; using System.Reflection; +using System.Threading; using System.Threading.Tasks; using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; @@ -18,13 +19,15 @@ public abstract class PluginsTestBase : DafnyLanguageServerTestBase { protected DiagnosticsReceiver DiagnosticReceiver; protected string LibraryPath; + private static readonly object PluginSync = new { }; + /// /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// - private string GetLibrary(string code) { + private string GetLibrary(string code, string assemblyName) { var temp = Path.GetTempFileName(); - var compilation = CSharpCompilation.Create("tempAssembly"); + var compilation = CSharpCompilation.Create(assemblyName); var standardLibraries = new List() { "DafnyPipeline", @@ -50,14 +53,21 @@ private string GetLibrary(string code) { protected abstract string GetLibraryCode(); + protected abstract string GetLibraryName(); + protected abstract string[] GetCommandLineArgument(); public async Task SetUpPlugin() { DiagnosticReceiver = new(); - LibraryPath = GetLibrary(GetLibraryCode()); + LibraryPath = GetLibrary(GetLibraryCode(), GetLibraryName()); + Monitor.Enter(PluginSync); Client = await InitializeClient(options => options.OnPublishDiagnostics(DiagnosticReceiver.NotificationReceived)); } + protected void CleanupPlugin() { + DafnyOptions.O.Plugins.RemoveAt(0); + Monitor.Exit(PluginSync); + } protected override IConfiguration CreateConfiguration() { return new ConfigurationBuilder().AddCommandLine(GetCommandLineArgument()).Build(); diff --git a/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs b/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs index 6edbd325d1c..47f43ef4f36 100644 --- a/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs @@ -71,7 +71,7 @@ public async Task LanguageServerShutsDownIfParentDies() { // Wait for the language server to kill itself by waiting until it closes the output stream. await process.StandardOutput.ReadToEndAsync(); - Thread.Sleep(300); // Give the process some time to die + Thread.Sleep(400); // Give the process some time to die Assert.ThrowsException(() => { var languageServer = Process.GetProcessById(int.Parse(languageServerProcessId)); diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index b39f0bebf4f..7e541bb4c2b 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -117,6 +117,7 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger(), textDocument, errorReporter, program, loadCanceled: false); } + // We load plugins at most once. if (dafnyPluginsOptions.Value.Plugins.Length > 0 && !DafnyOptions.O.Plugins.Any()) { try { foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { From b09f5d5c174ddba8a35c3ac4e3d0c79188aaf948 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 3 Feb 2022 09:28:26 -0600 Subject: [PATCH 34/47] Separated Rewriter from plugins from internal rewriters. Use of Internal back like before Fixed the tests of DafnyPipeline --- Source/Dafny/{Rewriter.cs => IRewriter.cs} | 157 ++++++++++++++++++--- Source/Dafny/Plugin.cs | 4 + Source/Dafny/Plugins/Rewriter.cs | 50 +------ Source/Dafny/RefinementTransformer.cs | 6 +- Source/Dafny/Resolver.cs | 8 +- Source/DafnyPipeline.Test/PluginsTest.cs | 8 +- 6 files changed, 151 insertions(+), 82 deletions(-) rename Source/Dafny/{Rewriter.cs => IRewriter.cs} (93%) diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/IRewriter.cs similarity index 93% rename from Source/Dafny/Rewriter.cs rename to Source/Dafny/IRewriter.cs index 2c881859d69..6812333e810 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/IRewriter.cs @@ -4,11 +4,110 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; -using Microsoft.Dafny.Plugins; using Bpl = Microsoft.Boogie; using IToken = Microsoft.Boogie.IToken; namespace Microsoft.Dafny { + /// + /// 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. + /// + public abstract class IRewriter { + /// + /// Used to report errors and warnings, with positional information. + /// + protected readonly ErrorReporter Reporter; + + /// + /// 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() + /// + /// The error reporter. Usually outputs automatically to IDE or command-line + internal IRewriter(ErrorReporter reporter) { + Contract.Requires(reporter != null); + this.Reporter = reporter; + } + + /// + /// Phase 1/5 + /// Override this method to obtain a module definition after parsing and built-in pre-resolvers, + /// You can then report errors using reporter.Error(MessageSource.Resolver, token, "message") (see above) + /// This is a good place to perform AST rewritings, if necessary + /// + /// A module definition before is resolved + internal virtual void PreResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 2/5 + /// Override this method to obtain a module definition after bare resolution, if no error were thrown, + /// You can then report errors using reporter.Error (see above) + /// We heavily discourage AST rewriting after this stage, as automatic type checking will not take place anymore. + /// + /// A module definition after it is resolved and type-checked + internal virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 3/5 + /// Override this method to obtain the module definition after resolution and + /// SCC/Cyclicity/Recursivity analysis. + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed + internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 4/5 + /// Override this method to obtain the module definition after the phase decreasesResolve + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity and decreasesResolve checks have been performed + internal virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 5/5 + /// Override this method to obtain a module definition after the entire resolution pipeline + /// You can then report errors using reporter.Error (see above) + /// + /// A module definition after it + /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed + internal virtual void PostResolve(ModuleDefinition moduleDefinition) { + Contract.Requires(moduleDefinition != null); + } + + /// + /// Phase 5/5 + /// 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) + /// + /// The entire program after it is fully resolved + internal virtual void PostResolve(Program program) { + Contract.Requires(program != null); + } + } + public class AutoGeneratedToken : TokenWrapper { public AutoGeneratedToken(Boogie.IToken wrappedToken) : base(wrappedToken) { @@ -16,12 +115,12 @@ public AutoGeneratedToken(Boogie.IToken wrappedToken) } } - public class TriggerGeneratingRewriter : Rewriter { + public class TriggerGeneratingRewriter : IRewriter { internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PostCyclicityResolve(ModuleDefinition m) { + internal override void PostCyclicityResolve(ModuleDefinition m) { var finder = new Triggers.QuantifierCollector(Reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { @@ -36,12 +135,12 @@ public override void PostCyclicityResolve(ModuleDefinition m) { } } - internal class QuantifierSplittingRewriter : Rewriter { + internal class QuantifierSplittingRewriter : IRewriter { internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PostResolveIntermediate(ModuleDefinition m) { + internal override void PostResolveIntermediate(ModuleDefinition m) { var splitter = new Triggers.QuantifierSplitter(); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { splitter.Visit(decl); @@ -51,12 +150,12 @@ public override void PostResolveIntermediate(ModuleDefinition m) { } // write out the quantifier for ForallStmt - public class ForallStmtRewriter : Rewriter { + public class ForallStmtRewriter : IRewriter { public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PostResolveIntermediate(ModuleDefinition m) { + internal override void PostResolveIntermediate(ModuleDefinition m) { var forallvisiter = new ForAllStmtVisitor(Reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { forallvisiter.Visit(decl, true); @@ -421,7 +520,7 @@ Expression Substitute(Expression expr, IVariable v, Expression e) { /// requires Valid() /// reads Repr /// - public class AutoContractsRewriter : Rewriter { + public class AutoContractsRewriter : IRewriter { readonly BuiltIns builtIns; public AutoContractsRewriter(ErrorReporter reporter, BuiltIns builtIns) : base(reporter) { @@ -430,7 +529,7 @@ public AutoContractsRewriter(ErrorReporter reporter, BuiltIns builtIns) this.builtIns = builtIns; } - public override void PreResolve(ModuleDefinition m) { + internal override void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { @@ -517,7 +616,7 @@ void ProcessClassPreResolve(ClassDecl cl) { } } - public override void PostResolveIntermediate(ModuleDefinition m) { + internal override void PostResolveIntermediate(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { @@ -870,7 +969,7 @@ void AddHoverText(IToken tok, string format, params object[] args) { /// recursive clique (if any), or if the programmer /// specifically asks to see it via the reveal_foo() lemma /// - public class OpaqueFunctionRewriter : Rewriter { + public class OpaqueFunctionRewriter : IRewriter { protected Dictionary fullVersion; // Given an opaque function, retrieve the full protected Dictionary original; // Given a full version of an opaque function, find the original opaque version protected Dictionary revealOriginal; // Map reveal_* lemmas (or two-state lemmas) back to their original functions @@ -884,7 +983,7 @@ public OpaqueFunctionRewriter(ErrorReporter reporter) revealOriginal = new Dictionary(); } - public override void PreResolve(ModuleDefinition m) { + internal override void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { if (d is TopLevelDeclWithMembers) { ProcessOpaqueClassFunctions((TopLevelDeclWithMembers)d); @@ -892,7 +991,7 @@ public override void PreResolve(ModuleDefinition m) { } } - public override void PostResolveIntermediate(ModuleDefinition m) { + internal override void PostResolveIntermediate(ModuleDefinition m) { foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { if (decl is Lemma || decl is TwoStateLemma) { var lem = (Method)decl; @@ -1018,7 +1117,7 @@ protected override bool VisitOneExpr(Expression expr, ref bool context) { /// Automatically accumulate requires for function calls within a function body, /// if requested via {:autoreq} /// - public class AutoReqFunctionRewriter : Rewriter { + public class AutoReqFunctionRewriter : IRewriter { Function parentFunction; bool containsMatch; // TODO: Track this per-requirement, rather than per-function @@ -1027,7 +1126,7 @@ public AutoReqFunctionRewriter(ErrorReporter reporter) Contract.Requires(reporter != null); } - public override void PostResolveIntermediate(ModuleDefinition m) { + internal override void PostResolveIntermediate(ModuleDefinition m) { var components = m.CallGraph.TopologicallySortedComponents(); foreach (var scComponent in components) { // Visit the call graph bottom up, so anything we call already has its prequisites calculated @@ -1384,13 +1483,13 @@ List generateAutoReqs(Expression expr) { } } - public class ProvideRevealAllRewriter : Rewriter { + public class ProvideRevealAllRewriter : IRewriter { public ProvideRevealAllRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PreResolve(ModuleDefinition m) { + internal override void PreResolve(ModuleDefinition m) { var declarations = m.TopLevelDecls; foreach (var d in declarations) { @@ -1449,13 +1548,13 @@ public override void PreResolve(ModuleDefinition m) { /// Replace all occurrences of attribute {:timeLimitMultiplier X} with {:timeLimit Y} /// where Y = X*default-time-limit or Y = X*command-line-time-limit /// - public class TimeLimitRewriter : Rewriter { + public class TimeLimitRewriter : IRewriter { public TimeLimitRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PreResolve(ModuleDefinition m) { + internal override void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { if (d is TopLevelDeclWithMembers tld) { foreach (MemberDecl member in tld.Members) { @@ -1619,12 +1718,12 @@ public override IToken Tok(IToken tok) { // =========================================================================================== - public class InductionRewriter : Rewriter { + public class InductionRewriter : IRewriter { internal InductionRewriter(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } - public override void PostDecreasesResolve(ModuleDefinition m) { + internal override void PostDecreasesResolve(ModuleDefinition m) { if (DafnyOptions.O.Induction == 0) { // Don't bother inferring :induction attributes. This will also have the effect of not warning about malformed :induction attributes } else { @@ -1981,6 +2080,22 @@ expr is BoxingCastExpr || } } } + + class PluginRewriter : IRewriter { + private Plugins.Rewriter internalRewriter; + + public PluginRewriter(ErrorReporter reporter, Plugins.Rewriter internalRewriter) : base(reporter) { + this.internalRewriter = internalRewriter; + } + + internal override void PostResolve(ModuleDefinition moduleDefinition) { + internalRewriter.PostResolve(moduleDefinition); + } + + internal override void PostResolve(Program program) { + internalRewriter.PostResolve(program); + } + } } diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs index d0e77aaaf0f..12e3bf8ff79 100644 --- a/Source/Dafny/Plugin.cs +++ b/Source/Dafny/Plugin.cs @@ -75,4 +75,8 @@ private static Configuration LoadConfiguration(Assembly assembly, string[] args, Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray()); return configuration; } + + public IEnumerable GetRewriters(ErrorReporter reporter) { + return Configuration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter)); + } } \ No newline at end of file diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs index f577caf9076..778f54dea44 100644 --- a/Source/Dafny/Plugins/Rewriter.cs +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -30,56 +30,9 @@ public abstract class Rewriter { /// The error reporter. Usually outputs automatically to IDE or command-line public Rewriter(ErrorReporter reporter) { Contract.Requires(reporter != null); - this.Reporter = reporter; + Reporter = reporter; } - - /// - /// Phase 1/5 - /// Override this method to obtain a module definition after parsing and built-in pre-resolvers, - /// You can then report errors using reporter.Error(MessageSource.Resolver, token, "message") (see above) - /// This is a good place to perform AST rewritings, if necessary - /// - /// A module definition before is resolved - public virtual void PreResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 2/5 - /// Override this method to obtain a module definition after bare resolution, if no error were thrown, - /// You can then report errors using reporter.Error (see above) - /// We heavily discourage AST rewriting after this stage, as automatic type checking will not take place anymore. - /// - /// A module definition after it is resolved and type-checked - public virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 3/5 - /// Override this method to obtain the module definition after resolution and - /// SCC/Cyclicity/Recursivity analysis. - /// You can then report errors using reporter.Error (see above) - /// - /// A module definition after it - /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed - public virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - - /// - /// Phase 4/5 - /// Override this method to obtain the module definition after the phase decreasesResolve - /// You can then report errors using reporter.Error (see above) - /// - /// A module definition after it - /// is resolved, type-checked and SCC/Cyclicity/Recursivity and decreasesResolve checks have been performed - public virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) { - Contract.Requires(moduleDefinition != null); - } - /// - /// Phase 5/5 /// Override this method to obtain a module definition after the entire resolution pipeline /// You can then report errors using reporter.Error (see above) /// @@ -90,7 +43,6 @@ public virtual void PostResolve(ModuleDefinition moduleDefinition) { } /// - /// Phase 5/5 /// 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) diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 1c74cc7b905..67caa778fb8 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -141,7 +141,7 @@ public override string filename { /// Jason Koenig and K. Rustan M. Leino. /// In EPTCS, 2016. (Post-workshop proceedings of REFINE 2015.) /// - public class RefinementTransformer : Rewriter { + public class RefinementTransformer : IRewriter { Cloner rawCloner; // This cloner just gives exactly the same thing back. RefinementCloner refinementCloner; // This cloner wraps things in a RefinementToken @@ -165,7 +165,7 @@ public RefinementTransformer(Program p) public ModuleSignature RefinedSig; // the intention is to use this field only after a successful PreResolve private ModuleSignature refinedSigOpened; - public override void PreResolve(ModuleDefinition m) { + internal override void PreResolve(ModuleDefinition m) { if (m.RefinementQId?.Decl != null) { // There is a refinement parent and it resolved OK RefinedSig = m.RefinementQId.Sig; @@ -486,7 +486,7 @@ public bool ResolvedTypesAreTheSame(Type prev, Type next) { } } - public override void PostResolveIntermediate(ModuleDefinition m) { + internal override void PostResolveIntermediate(ModuleDefinition m) { if (m == moduleUnderConstruction) { while (this.postTasks.Count != 0) { var a = postTasks.Dequeue(); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f14ad26dfca..6e5611b3628 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -241,7 +241,7 @@ enum ValuetypeVariety { private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; - private List rewriters; + private List rewriters; private RefinementTransformer refinementTransformer; public Resolver(Program prog) { @@ -422,7 +422,7 @@ public void ResolveProgram(Program prog) { h++; } - rewriters = new List(); + rewriters = new List(); refinementTransformer = new RefinementTransformer(prog); rewriters.Add(refinementTransformer); rewriters.Add(new AutoContractsRewriter(reporter, builtIns)); @@ -440,9 +440,7 @@ public void ResolveProgram(Program prog) { rewriters.Add(new InductionRewriter(reporter)); foreach (var plugin in DafnyOptions.O.Plugins) { - foreach (var rewriter in plugin.Configuration.GetRewriters(reporter)) { - rewriters.Add(rewriter); - } + rewriters.AddRange(plugin.GetRewriters(reporter)); } systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index 1884d21e57f..c20d18a99c2 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -15,9 +15,9 @@ public class PluginsTest { /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// - private string GetLibrary(string code) { + private string GetLibrary(string code, string name) { var temp = Path.GetTempFileName(); - var compilation = CSharpCompilation.Create("tempAssembly"); + var compilation = CSharpCompilation.Create(name); var standardLibraries = new List() { "DafnyPipeline", @@ -72,7 +72,7 @@ public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): b public override void PostResolve(ModuleDefinition moduleDefinition) { Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue ""+configuration.Argument); } -}"); +}", "simplePlugin"); var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); @@ -103,7 +103,7 @@ public ErrorRewriter(ErrorReporter reporter): base(reporter) {} public override void PostResolve(ModuleDefinition moduleDefinition) { Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); } -}"); +}", "secondPlugin"); var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); From e4c58e56fef8b368f32d70955228a380e84756fe Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 3 Feb 2022 09:29:44 -0600 Subject: [PATCH 35/47] Rewriter --- Source/Dafny/{IRewriter.cs => Rewriter.cs} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename Source/Dafny/{IRewriter.cs => Rewriter.cs} (100%) diff --git a/Source/Dafny/IRewriter.cs b/Source/Dafny/Rewriter.cs similarity index 100% rename from Source/Dafny/IRewriter.cs rename to Source/Dafny/Rewriter.cs From 57f7589f12bb2eff141b89d4e0cb00d40d2c812a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 3 Feb 2022 09:36:03 -0600 Subject: [PATCH 36/47] Note about the experimental feature of plugins --- Source/DafnyLanguageServer/README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Source/DafnyLanguageServer/README.md b/Source/DafnyLanguageServer/README.md index c295534908c..7995c33c3e7 100644 --- a/Source/DafnyLanguageServer/README.md +++ b/Source/DafnyLanguageServer/README.md @@ -88,6 +88,11 @@ Options provided through the command line have higher priority than the options ``` #### About plugins + +*Plugins are experimental. +The plugin API directly exposes the Dafny AST, which is constantly evolving. +Hence, always recompile your plugin against the binary of Dafny that will be importing your plugin.* + Plugins are libraries linked to a `Dafny.dll` of the same version than the language server. A plugin typically defines: From 4e52ba60365d54b1e20dc82815f1cf6809990113 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 4 Feb 2022 10:57:17 -0600 Subject: [PATCH 37/47] Cleanup plugin + moved initialization earlier so that it's run only once. --- .../DafnyLanguageServer.Test/Various/PluginsTest.cs | 1 - .../Various/PluginsTestBase.cs | 2 -- .../DafnyLanguageServer.Test/Various/ShutdownTest.cs | 2 +- Source/DafnyLanguageServer/DafnyLanguageServer.cs | 10 ++++++++++ .../Workspace/TextDocumentLoader.cs | 11 ----------- 5 files changed, 11 insertions(+), 15 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index 95004bb9a39..a3ba63df57a 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -55,7 +55,6 @@ protected override string[] GetCommandLineArgument() { [TestMethod] public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { - // TODO: Need to clean up the plugins from the options after they are set. // This code will run with the plugin from PluginsAdvancedTest, but that plugin won't throw an exception on the code below. var documentItem = CreateTestDocument("function test(): int { 1 }"); await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index 2a69166eea6..394b8510c3d 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -60,13 +60,11 @@ private string GetLibrary(string code, string assemblyName) { public async Task SetUpPlugin() { DiagnosticReceiver = new(); LibraryPath = GetLibrary(GetLibraryCode(), GetLibraryName()); - Monitor.Enter(PluginSync); Client = await InitializeClient(options => options.OnPublishDiagnostics(DiagnosticReceiver.NotificationReceived)); } protected void CleanupPlugin() { DafnyOptions.O.Plugins.RemoveAt(0); - Monitor.Exit(PluginSync); } protected override IConfiguration CreateConfiguration() { diff --git a/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs b/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs index 47f43ef4f36..b79c3bd27b9 100644 --- a/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ShutdownTest.cs @@ -71,7 +71,7 @@ public async Task LanguageServerShutsDownIfParentDies() { // Wait for the language server to kill itself by waiting until it closes the output stream. await process.StandardOutput.ReadToEndAsync(); - Thread.Sleep(400); // Give the process some time to die + await Task.Delay(400); // Give the process some time to die Assert.ThrowsException(() => { var languageServer = Process.GetProcessById(int.Parse(languageServerProcessId)); diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index cac97bc501c..fb4de74352a 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -11,6 +11,7 @@ using OmniSharp.Extensions.LanguageServer.Server; using System.Threading; using System.Threading.Tasks; +using Microsoft.Extensions.Options; namespace Microsoft.Dafny.LanguageServer { public static class DafnyLanguageServer { @@ -35,6 +36,15 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req Action killLanguageServer) { var logger = server.GetRequiredService>(); logger.LogTrace("initializing service"); + var dafnyPluginsOptions = server.GetRequiredService>(); + + try { + foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { + DafnyOptions.O.Parse(new[] { "-plugin:" + pluginPathArgument }); + } + } catch (Exception e) { + logger.LogError(e, "Error while instantiating the plugins:"); + } KillLanguageServerIfParentDies(logger, request, killLanguageServer); diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 7e541bb4c2b..c19c81df605 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -117,17 +117,6 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger(), textDocument, errorReporter, program, loadCanceled: false); } - // We load plugins at most once. - if (dafnyPluginsOptions.Value.Plugins.Length > 0 && !DafnyOptions.O.Plugins.Any()) { - try { - foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { - DafnyOptions.O.Parse(new[] { "-plugin:" + pluginPathArgument }); - } - } catch (Exception e) { - errorReporter.Error(MessageSource.Parser, program.GetFirstTopLevelToken(), "Error while instantiating the plugins:" + e.ToString()); - } - } - var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, cancellationToken); var symbolTable = symbolTableFactory.CreateFrom(program, compilationUnit, cancellationToken); if (errorReporter.HasErrors) { From f9c3a173f8d3368198f692f7bf6551bc183ea2b1 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 4 Feb 2022 13:52:36 -0600 Subject: [PATCH 38/47] Better syntax --- .../Various/PluginsAdvancedTest.cs | 10 ++++------ Source/DafnyLanguageServer.Test/Various/PluginsTest.cs | 10 ++++------ .../Various/PluginsTestBase.cs | 6 +++--- 3 files changed, 11 insertions(+), 15 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index 272d3d89a34..ef685ed5f72 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -15,8 +15,8 @@ public async Task SetUp() { await SetUpPlugin(); } - protected override string GetLibraryCode() { - return @" + protected override string LibraryCode => + @" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; using System.Collections; @@ -92,11 +92,9 @@ public override void PostResolve(Program program) { } }"; - } - protected override string GetLibraryName() { - return "PluginsAdvancedTest"; - } + protected override string LibraryName => + "PluginsAdvancedTest"; protected override string[] GetCommandLineArgument() { return new[] { $@"--dafny:plugins:0=""{LibraryPath},force you""" }; diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index a3ba63df57a..dbb0458094a 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -13,8 +13,8 @@ public class PluginsTest : PluginsTestBase { public async Task SetUp() { await SetUpPlugin(); } - protected override string GetLibraryCode() { - return @" + protected override string LibraryCode => + @" using Microsoft.Dafny; using Microsoft.Dafny.Plugins; @@ -43,11 +43,9 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { } }"; - } - protected override string GetLibraryName() { - return "PluginsTest"; - } + protected override string LibraryName => + "PluginsTest"; protected override string[] GetCommandLineArgument() { return new[] { $@"--dafny:plugins:0=""{LibraryPath},\""because\\ whatever\""""" }; diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index 394b8510c3d..2606b9276ed 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -51,15 +51,15 @@ private string GetLibrary(string code, string assemblyName) { return assemblyPath; } - protected abstract string GetLibraryCode(); + protected abstract string LibraryCode { get; } - protected abstract string GetLibraryName(); + protected abstract string LibraryName { get; } protected abstract string[] GetCommandLineArgument(); public async Task SetUpPlugin() { DiagnosticReceiver = new(); - LibraryPath = GetLibrary(GetLibraryCode(), GetLibraryName()); + LibraryPath = GetLibrary(LibraryCode, LibraryName); Client = await InitializeClient(options => options.OnPublishDiagnostics(DiagnosticReceiver.NotificationReceived)); } From 1d349319751ffb476b1bb0eada2ea22e6546c13c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 4 Feb 2022 13:57:34 -0600 Subject: [PATCH 39/47] Property again --- .../DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs | 5 ++--- Source/DafnyLanguageServer.Test/Various/PluginsTest.cs | 5 ++--- Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs | 6 +++--- 3 files changed, 7 insertions(+), 9 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index ef685ed5f72..e342ca43c32 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -96,9 +96,8 @@ public override void PostResolve(Program program) { protected override string LibraryName => "PluginsAdvancedTest"; - protected override string[] GetCommandLineArgument() { - return new[] { $@"--dafny:plugins:0=""{LibraryPath},force you""" }; - } + protected override string[] CommandLineArgument => + new[] { $@"--dafny:plugins:0=""{LibraryPath},force you""" }; [TestMethod] public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration() { diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index dbb0458094a..b65f7f46755 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -47,9 +47,8 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { protected override string LibraryName => "PluginsTest"; - protected override string[] GetCommandLineArgument() { - return new[] { $@"--dafny:plugins:0=""{LibraryPath},\""because\\ whatever\""""" }; - } + protected override string[] CommandLineArgument => + new[] { $@"--dafny:plugins:0=""{LibraryPath},\""because\\ whatever\""""" }; [TestMethod] public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index 2606b9276ed..b078d8d81a2 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -25,7 +25,7 @@ public abstract class PluginsTestBase : DafnyLanguageServerTestBase { /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// - private string GetLibrary(string code, string assemblyName) { + private static string GetLibrary(string code, string assemblyName) { var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create(assemblyName); var standardLibraries = new List() @@ -55,7 +55,7 @@ private string GetLibrary(string code, string assemblyName) { protected abstract string LibraryName { get; } - protected abstract string[] GetCommandLineArgument(); + protected abstract string[] CommandLineArgument { get; } public async Task SetUpPlugin() { DiagnosticReceiver = new(); @@ -68,6 +68,6 @@ protected void CleanupPlugin() { } protected override IConfiguration CreateConfiguration() { - return new ConfigurationBuilder().AddCommandLine(GetCommandLineArgument()).Build(); + return new ConfigurationBuilder().AddCommandLine(CommandLineArgument).Build(); } } \ No newline at end of file From 8f8a135de6751eee7d971fe3a410aa33d0865e7b Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 4 Feb 2022 14:01:16 -0600 Subject: [PATCH 40/47] Extracted a method to load the plugins --- .../DafnyLanguageServer/DafnyLanguageServer.cs | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index fb4de74352a..c9eec0d873c 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -36,8 +36,19 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req Action killLanguageServer) { var logger = server.GetRequiredService>(); logger.LogTrace("initializing service"); - var dafnyPluginsOptions = server.GetRequiredService>(); + LoadPlugins(logger, server); + + KillLanguageServerIfParentDies(logger, request, killLanguageServer); + + return Task.CompletedTask; + } + + /// + /// Load the plugins for the Dafny pipeline + /// + private static void LoadPlugins(ILogger logger, ILanguageServer server) { + var dafnyPluginsOptions = server.GetRequiredService>(); try { foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { DafnyOptions.O.Parse(new[] { "-plugin:" + pluginPathArgument }); @@ -45,10 +56,6 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req } catch (Exception e) { logger.LogError(e, "Error while instantiating the plugins:"); } - - KillLanguageServerIfParentDies(logger, request, killLanguageServer); - - return Task.CompletedTask; } /// From 749c3f0c897a75d81158eb2428548251ecbc41ab Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 4 Feb 2022 14:25:44 -0600 Subject: [PATCH 41/47] Display plugin loading errors as part of the diagnostics. --- Source/DafnyLanguageServer/DafnyLanguageServer.cs | 7 ++++++- Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs | 7 +++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index c9eec0d873c..bf15f7baab1 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Generic; using System.Diagnostics; using Microsoft.Dafny.LanguageServer.Handlers; using Microsoft.Dafny.LanguageServer.Language; @@ -15,6 +16,7 @@ namespace Microsoft.Dafny.LanguageServer { public static class DafnyLanguageServer { + public static List LoadErrors = new(); private static string DafnyVersion { get { var version = typeof(DafnyLanguageServer).Assembly.GetName().Version!; @@ -49,12 +51,15 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req /// private static void LoadPlugins(ILogger logger, ILanguageServer server) { var dafnyPluginsOptions = server.GetRequiredService>(); + var lastPlugin = ""; try { foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { + lastPlugin = pluginPathArgument; DafnyOptions.O.Parse(new[] { "-plugin:" + pluginPathArgument }); } } catch (Exception e) { - logger.LogError(e, "Error while instantiating the plugins:"); + logger.LogError(e, $"Error while instantiating plugin {lastPlugin}"); + LoadErrors.Add($"Error while instantiating plugin {lastPlugin}. Please restart the server.\n" + e); } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index c19c81df605..1a303633899 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -112,6 +112,7 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { var (textDocument, cancellationToken) = loadRequest; var errorReporter = new DiagnosticErrorReporter(textDocument.Uri); var program = parser.Parse(textDocument, errorReporter, cancellationToken); + PublishDafnyLanguageServerLoadErrors(errorReporter, program); if (errorReporter.HasErrors) { notificationPublisher.SendStatusNotification(textDocument, CompilationStatus.ParsingFailed); return CreateDocumentWithEmptySymbolTable(loggerFactory.CreateLogger(), textDocument, errorReporter, program, loadCanceled: false); @@ -128,6 +129,12 @@ private DafnyDocument LoadInternal(LoadRequest loadRequest) { return new DafnyDocument(textDocument, errorReporter, new List(), ghostDiagnostics, program, symbolTable); } + private static void PublishDafnyLanguageServerLoadErrors(DiagnosticErrorReporter errorReporter, Dafny.Program program) { + foreach (var error in DafnyLanguageServer.LoadErrors) { + errorReporter.Error(MessageSource.Compiler, program.GetFirstTopLevelToken(), error); + } + } + private static DafnyDocument CreateDocumentWithEmptySymbolTable( ILogger logger, TextDocumentItem textDocument, From c42d10c1e211b1e2e0d69f6388c3fb914daea48f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 7 Feb 2022 14:48:48 -0600 Subject: [PATCH 42/47] Adressed review comments --- Source/Dafny/DafnyOptions.cs | 4 +- Source/Dafny/Plugin.cs | 56 ++++++++++--------- ...onfiguration.cs => PluginConfiguration.cs} | 10 ++-- Source/Dafny/Plugins/Rewriter.cs | 6 +- Source/Dafny/Resolver.cs | 24 ++++---- Source/Dafny/Rewriter.cs | 6 +- .../Various/PluginsAdvancedTest.cs | 2 +- .../Various/PluginsTest.cs | 2 +- Source/DafnyPipeline.Test/PluginsTest.cs | 6 +- 9 files changed, 60 insertions(+), 56 deletions(-) rename Source/Dafny/Plugins/{Configuration.cs => PluginConfiguration.cs} (76%) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 8e71c1f77bf..0d7075ccc9d 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -262,7 +262,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com matchResult.Groups[2].Value ).ToArray(); } - Plugins.Add(new Plugin(pluginPath, arguments, errorReporter)); + Plugins.Add(Plugin.Load(pluginPath, arguments)); } } @@ -848,7 +848,7 @@ verification outcome /plugin:[ ] (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 + 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: diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs index 12e3bf8ff79..d48827d715e 100644 --- a/Source/Dafny/Plugin.cs +++ b/Source/Dafny/Plugin.cs @@ -7,19 +7,30 @@ namespace Microsoft.Dafny; /// -/// This class is internal to Dafny. It wraps an assembly and an extracted configuration from this assembly, +/// 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 /// public class Plugin { - public Configuration Configuration; + public PluginConfiguration PluginConfiguration; - private readonly string path; + private readonly string pluginPath; private readonly Assembly assembly; private System.Type[] rewriterTypes; - class AutomaticConfiguration : Configuration { + 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[] rewriters; - public AutomaticConfiguration(Func[] rewriters) { + public AutomaticPluginConfiguration(Func[] rewriters) { this.rewriters = rewriters; } @@ -31,52 +42,45 @@ public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { public static IEnumerable 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); + .Where(t => t.IsAssignableTo(typeof(PluginConfiguration))); } - private static System.Type[] CheckPluginForRewriters(Assembly assembly, string path) { + 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 {path} does not contain any Microsoft.Dafny.Plugins.Rewriter"); + throw new Exception($"Plugin {assembly.Location} 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; + private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] args, System.Type[] rewriterTypes) { + PluginConfiguration pluginConfiguration = null; foreach (var configurationType in GetConfigurationsTypes(assembly)) { - if (configuration != null) { + if (pluginConfiguration != null) { throw new Exception( - $"Only one class should extend Microsoft.Dafny.Plugins.Configuration from {path}. Please remove {configurationType}."); + $"Only one class should extend Microsoft.Dafny.Plugins.PluginConfiguration from {assembly.Location}. Please remove {configurationType}."); } - configuration = (Configuration)Activator.CreateInstance(configurationType); + pluginConfiguration = (PluginConfiguration)Activator.CreateInstance(configurationType); - if (configuration == null) { - throw new Exception($"Could not instantiate a {configurationType} from {path}"); + if (pluginConfiguration == null) { + throw new Exception($"Could not instantiate a {configurationType} from {assembly.Location}"); } - configuration.ParseArguments(args); + pluginConfiguration.ParseArguments(args); } - configuration ??= new AutomaticConfiguration( + pluginConfiguration ??= new AutomaticPluginConfiguration( rewriterTypes.Select>((System.Type rewriterType) => (ErrorReporter errorReporter) => Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray()); - return configuration; + return pluginConfiguration; } public IEnumerable GetRewriters(ErrorReporter reporter) { - return Configuration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter)); + return PluginConfiguration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter)); } } \ No newline at end of file diff --git a/Source/Dafny/Plugins/Configuration.cs b/Source/Dafny/Plugins/PluginConfiguration.cs similarity index 76% rename from Source/Dafny/Plugins/Configuration.cs rename to Source/Dafny/Plugins/PluginConfiguration.cs index 1bab3ac70e2..df53f2ed08a 100644 --- a/Source/Dafny/Plugins/Configuration.cs +++ b/Source/Dafny/Plugins/PluginConfiguration.cs @@ -4,17 +4,17 @@ namespace Microsoft.Dafny.Plugins; /// -/// Plugins should define a class that extends Configuration, +/// 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 Configuration, then Dafny will instantiate every sub-class +/// 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. /// -public abstract class Configuration { +public abstract class PluginConfiguration { /// - /// A Microsoft.Dafny.Plugins.Configuration will be automatically instantiated an arguments + /// A Microsoft.Dafny.Plugins.PluginConfiguration will be automatically instantiated an arguments /// will be provided to the plugin by the method `ParseArguments``; /// /// The arguments passed to the plugin @@ -28,4 +28,4 @@ public virtual void ParseArguments(string[] args) { public virtual Rewriter[] GetRewriters(ErrorReporter errorReporter) { return Array.Empty(); } -} \ No newline at end of file +} diff --git a/Source/Dafny/Plugins/Rewriter.cs b/Source/Dafny/Plugins/Rewriter.cs index 778f54dea44..c1dc0f3b79d 100644 --- a/Source/Dafny/Plugins/Rewriter.cs +++ b/Source/Dafny/Plugins/Rewriter.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny.Plugins { /// /// 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 + /// 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. /// @@ -17,8 +17,8 @@ public abstract class Rewriter { /// /// 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. + /// * 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: /// diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6e5611b3628..fcecb574b88 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -481,8 +481,8 @@ public void ResolveProgram(Program prog) { m.RefinementQId.Set(md); // If module is not found, md is null and an error message has been emitted } - foreach (var r in rewriters) { - r.PreResolve(m); + foreach (var rewriter in rewriters) { + rewriter.PreResolve(m); } literalDecl.Signature = RegisterTopLevelDecls(m, true); @@ -507,11 +507,11 @@ public void ResolveProgram(Program prog) { prog.ModuleSigs[m] = sig; - foreach (var r in rewriters) { + foreach (var rewriter in rewriters) { if (!good || reporter.Count(ErrorLevel.Error) != preResolveErrorCount) { break; } - r.PostResolveIntermediate(m); + rewriter.PostResolveIntermediate(m); } if (good && reporter.Count(ErrorLevel.Error) == errorCount) { m.SuccessfullyResolved = true; @@ -611,8 +611,8 @@ public void ResolveProgram(Program prog) { } } - foreach (var r in rewriters) { - r.PostCyclicityResolve(module); + foreach (var rewriter in rewriters) { + rewriter.PostCyclicityResolve(module); } } @@ -641,8 +641,8 @@ public void ResolveProgram(Program prog) { } foreach (var module in prog.Modules()) { - foreach (var r in rewriters) { - r.PostDecreasesResolve(module); + foreach (var rewriter in rewriters) { + rewriter.PostDecreasesResolve(module); } } @@ -696,13 +696,13 @@ public void ResolveProgram(Program prog) { CheckDupModuleNames(prog); foreach (var module in prog.Modules()) { - foreach (var r in rewriters) { - r.PostResolve(module); + foreach (var rewriter in rewriters) { + rewriter.PostResolve(module); } } - foreach (var r in rewriters) { - r.PostResolve(prog); + foreach (var rewriter in rewriters) { + rewriter.PostResolve(prog); } } diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 6812333e810..123a87a0052 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -11,7 +11,7 @@ namespace Microsoft.Dafny { /// /// 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 + /// 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. /// @@ -24,8 +24,8 @@ public abstract class IRewriter { /// /// 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. + /// * 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: /// diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index e342ca43c32..ef6a4b08bff 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -26,7 +26,7 @@ namespace PluginsAdvancedTest { /// /// Small plugin that detects all extern methods and verifies that there are test methods that actually invoke them. /// -public class TestConfiguration: Configuration { +public class TestConfiguration: PluginConfiguration { public string PluginUser = """"; public bool ForceName = false; public override void ParseArguments(string[] args) { diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index b65f7f46755..6fdcf05d276 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -20,7 +20,7 @@ public async Task SetUp() { namespace PluginsTest { -public class TestConfiguration: Configuration { +public class TestConfiguration: PluginConfiguration { public string Argument = """"; public override void ParseArguments(string[] args) { Argument = args.Length > 0 ? args[0] : ""[no argument]""; diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index c20d18a99c2..be9ef0cdc65 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -52,7 +52,7 @@ public void EnsurePluginIsExecuted() { using Microsoft.Dafny; using Microsoft.Dafny.Plugins; -public class TestConfiguration: Configuration { +public class TestConfiguration: PluginConfiguration { public string Argument = """"; public override void ParseArguments(string[] args) { Argument = args[0]; @@ -76,7 +76,7 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); - options.Plugins.Add(new Microsoft.Dafny.Plugin(library, new string[] { "because whatever" }, reporter)); + options.Plugins.Add(Plugin.Load(library, new string[] { "because whatever" })); DafnyOptions.Install(options); var programString = "function test(): int { 1 }"; @@ -107,7 +107,7 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); - options.Plugins.Add(new Microsoft.Dafny.Plugin(library, new string[] { "ignored arguments" }, reporter)); + options.Plugins.Add(Plugin.Load(library, new string[] { "ignored arguments" })); DafnyOptions.Install(options); var programString = "function test(): int { 1 }"; From b6fcbd8c5cd72121b9df513f6c53020f5744adfd Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 8 Feb 2022 12:39:36 -0600 Subject: [PATCH 43/47] Plugins as separate CS files --- .../DafnyLanguageServer.Test.csproj | 6 ++ .../Various/PluginsAdvancedTest.cs | 78 ------------------- .../Various/PluginsTest.cs | 30 ------- .../Various/PluginsTestBase.cs | 12 ++- .../_plugins/PluginsAdvancedTest.cs | 75 ++++++++++++++++++ .../_plugins/PluginsTest.cs | 28 +++++++ .../DafnyPipeline.Test.csproj | 7 +- Source/DafnyPipeline.Test/PluginsTest.cs | 46 +++-------- .../_plugins/secondPlugin.cs | 10 +++ .../_plugins/simplePlugin.cs | 24 ++++++ 10 files changed, 166 insertions(+), 150 deletions(-) create mode 100644 Source/DafnyLanguageServer.Test/_plugins/PluginsAdvancedTest.cs create mode 100644 Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs create mode 100644 Source/DafnyPipeline.Test/_plugins/secondPlugin.cs create mode 100644 Source/DafnyPipeline.Test/_plugins/simplePlugin.cs diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index 7ff5cdf8843..9fb0811efbd 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -54,5 +54,11 @@ PreserveNewest + + + + + + diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index ef6a4b08bff..bf48448a5f4 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -15,84 +15,6 @@ public async Task SetUp() { await SetUpPlugin(); } - protected override string LibraryCode => - @" -using Microsoft.Dafny; -using Microsoft.Dafny.Plugins; -using System.Collections; - -namespace PluginsAdvancedTest { - -/// -/// Small plugin that detects all extern methods and verifies that there are test methods that actually invoke them. -/// -public class TestConfiguration: PluginConfiguration { - public string PluginUser = """"; - public bool ForceName = false; - public override void ParseArguments(string[] args) { - ForceName = args.Length > 0 && args[0] == ""force""; - PluginUser = args.Length > 1 ? "", "" + args[1] : """"; - } - public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { - return new Rewriter[]{new ExternCheckRewriter(errorReporter, this)}; - } -} - -public class ExternCheckRewriter: Rewriter { - private readonly TestConfiguration configuration; - - public ExternCheckRewriter(ErrorReporter reporter, TestConfiguration configuration): base(reporter) { - this.configuration = configuration; - } - - public override void PostResolve(Program program) { - foreach (var moduleDefinition in program.Modules()) { - foreach (var topLevelDecl in moduleDefinition.TopLevelDecls) { - if (topLevelDecl is ClassDecl cd) { - foreach (var member in cd.Members) { - if (member is Method methodExtern) { - if (Attributes.Contains(member.Attributes, ""extern"")) { - // Verify that there exists a test method which references this extern method. - var tested = false; - Method candidate = null; - foreach (var member2 in cd.Members) { - if (member2 == member || !(member2 is Method methodTest)) { - continue; - } - if (!Attributes.Contains(methodTest.Attributes, ""test"")) { - continue; - } - if (!moduleDefinition.CallGraph.Reaches(methodTest, methodExtern)) { - continue; - } - candidate = methodTest; - - if (configuration.ForceName && candidate.Name != methodExtern.Name + ""_test"") { - continue; - } - tested = true; - break; - } - - if (!tested) { - var forceMessage = configuration.ForceName ? $"" named {methodExtern.Name}_test"" : """"; - var token = configuration.ForceName && candidate != null - ? new NestedToken(methodExtern.tok, candidate.tok, ""You might want to just rename this method"") - : methodExtern.tok; - Reporter.Error(MessageSource.Resolver, token, - $""Please declare a method {{:test}}{forceMessage} that will call {methodExtern.Name}{configuration.PluginUser}""); - } - } - } - } - } - } - } - } -} - -}"; - protected override string LibraryName => "PluginsAdvancedTest"; diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index 6fdcf05d276..ce159695bb1 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -13,36 +13,6 @@ public class PluginsTest : PluginsTestBase { public async Task SetUp() { await SetUpPlugin(); } - protected override string LibraryCode => - @" -using Microsoft.Dafny; -using Microsoft.Dafny.Plugins; - -namespace PluginsTest { - -public class TestConfiguration: PluginConfiguration { - public string Argument = """"; - public override void ParseArguments(string[] args) { - Argument = args.Length > 0 ? args[0] : ""[no argument]""; - } - public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { - return new Rewriter[]{new ErrorRewriter(errorReporter, this)}; - } -} - -public class ErrorRewriter: Rewriter { - private readonly TestConfiguration configuration; - - public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): base(reporter) { - this.configuration = configuration; - } - - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Compiler, moduleDefinition.GetFirstTopLevelToken(), ""Impossible to continue ""+configuration.Argument); - } -} - -}"; protected override string LibraryName => "PluginsTest"; diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index b078d8d81a2..8cf0d529235 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -25,7 +25,13 @@ public abstract class PluginsTestBase : DafnyLanguageServerTestBase { /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// - private static string GetLibrary(string code, string assemblyName) { + private static string GetLibrary(string assemblyName) { + var assembly = Assembly.GetExecutingAssembly(); + string[] names = assembly.GetManifestResourceNames(); + Stream codeStream = assembly.GetManifestResourceStream($"Microsoft.Dafny.LanguageServer.IntegrationTest._plugins.{assemblyName}.cs"); + Assert.IsNotNull(codeStream); + string code = new StreamReader(codeStream).ReadToEnd(); + var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create(assemblyName); var standardLibraries = new List() @@ -51,15 +57,13 @@ private static string GetLibrary(string code, string assemblyName) { return assemblyPath; } - protected abstract string LibraryCode { get; } - protected abstract string LibraryName { get; } protected abstract string[] CommandLineArgument { get; } public async Task SetUpPlugin() { DiagnosticReceiver = new(); - LibraryPath = GetLibrary(LibraryCode, LibraryName); + LibraryPath = GetLibrary(LibraryName); Client = await InitializeClient(options => options.OnPublishDiagnostics(DiagnosticReceiver.NotificationReceived)); } diff --git a/Source/DafnyLanguageServer.Test/_plugins/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/_plugins/PluginsAdvancedTest.cs new file mode 100644 index 00000000000..06b5dd35baa --- /dev/null +++ b/Source/DafnyLanguageServer.Test/_plugins/PluginsAdvancedTest.cs @@ -0,0 +1,75 @@ +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; +using System.Collections; + +namespace PluginsAdvancedTest { + + /// + /// Small plugin that detects all extern methods and verifies that there are test methods that actually invoke them. + /// + public class TestConfiguration : PluginConfiguration { + public string PluginUser = ""; + public bool ForceName = false; + public override void ParseArguments(string[] args) { + ForceName = args.Length > 0 && args[0] == "force"; + PluginUser = args.Length > 1 ? ", " + args[1] : ""; + } + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return new Rewriter[] { new ExternCheckRewriter(errorReporter, this) }; + } + } + + public class ExternCheckRewriter : Rewriter { + private readonly TestConfiguration configuration; + + public ExternCheckRewriter(ErrorReporter reporter, TestConfiguration configuration) : base(reporter) { + this.configuration = configuration; + } + + public override void PostResolve(Program program) { + foreach (var moduleDefinition in program.Modules()) { + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls) { + if (topLevelDecl is ClassDecl cd) { + foreach (var member in cd.Members) { + if (member is Method methodExtern) { + if (Attributes.Contains(member.Attributes, "extern")) { + // Verify that there exists a test method which references this extern method. + var tested = false; + Method candidate = null; + foreach (var member2 in cd.Members) { + if (member2 == member || !(member2 is Method methodTest)) { + continue; + } + if (!Attributes.Contains(methodTest.Attributes, "test")) { + continue; + } + if (!moduleDefinition.CallGraph.Reaches(methodTest, methodExtern)) { + continue; + } + candidate = methodTest; + + if (configuration.ForceName && candidate.Name != methodExtern.Name + "_test") { + continue; + } + tested = true; + break; + } + + if (!tested) { + var forceMessage = configuration.ForceName ? $" named {methodExtern.Name}_test" : ""; + var token = configuration.ForceName && candidate != null + ? new NestedToken(methodExtern.tok, candidate.tok, "You might want to just rename this method") + : methodExtern.tok; + Reporter.Error(MessageSource.Resolver, token, + $"Please declare a method {{:test}}{forceMessage} that will call {methodExtern.Name}{configuration.PluginUser}"); + } + } + } + } + } + } + } + } + } + +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs b/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs new file mode 100644 index 00000000000..75e66ec78c1 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs @@ -0,0 +1,28 @@ +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; + +namespace PluginsTest { + + public class TestConfiguration : PluginConfiguration { + public string Argument = ""; + public override void ParseArguments(string[] args) { + Argument = args.Length > 0 ? args[0] : "[no argument]"; + } + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return new Rewriter[] { new ErrorRewriter(errorReporter, this) }; + } + } + + public class ErrorRewriter : Rewriter { + private readonly TestConfiguration configuration; + + public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration) : base(reporter) { + this.configuration = configuration; + } + + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.GetFirstTopLevelToken(), "Impossible to continue " + configuration.Argument); + } + } + +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index 4ac17b6c8d2..238b7c392f6 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -32,5 +32,10 @@ PreserveNewest - + + + + + + diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index be9ef0cdc65..37035363be6 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -2,6 +2,7 @@ using System.IO; using System.Linq; using System.Reflection; +using System.Resources; using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; using Xunit; @@ -15,7 +16,12 @@ public class PluginsTest { /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. /// - private string GetLibrary(string code, string name) { + private string GetLibrary(string name) { + var assembly = Assembly.GetExecutingAssembly(); + Stream codeStream = assembly.GetManifestResourceStream($"DafnyPipeline.Test._plugins.{name}.cs"); + Assert.NotNull(codeStream); + string code = new StreamReader(codeStream).ReadToEnd(); + var temp = Path.GetTempFileName(); var compilation = CSharpCompilation.Create(name); var standardLibraries = new List() @@ -48,31 +54,7 @@ public string GetLastErrorMessage() { [Fact] public void EnsurePluginIsExecuted() { - var library = GetLibrary(@" -using Microsoft.Dafny; -using Microsoft.Dafny.Plugins; - -public class TestConfiguration: PluginConfiguration { - public string Argument = """"; - public override void ParseArguments(string[] args) { - Argument = args[0]; - } - public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { - return new Rewriter[]{new ErrorRewriter(errorReporter, this)}; - } -} - -public class ErrorRewriter: Rewriter { - private readonly TestConfiguration configuration; - - public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration): base(reporter) { - this.configuration = configuration; - } - - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue ""+configuration.Argument); - } -}", "simplePlugin"); + var library = GetLibrary("simplePlugin"); var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); @@ -93,17 +75,7 @@ public override void PostResolve(ModuleDefinition moduleDefinition) { [Fact] public void EnsurePluginIsExecutedEvenWithoutConfiguration() { - var library = GetLibrary(@" -using Microsoft.Dafny; -using Microsoft.Dafny.Plugins; - -public class ErrorRewriter: Rewriter { - public ErrorRewriter(ErrorReporter reporter): base(reporter) {} - - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, ""Impossible to continue""); - } -}", "secondPlugin"); + var library = GetLibrary("secondPlugin"); var reporter = new CollectionErrorReporter(); var options = new DafnyOptions(reporter); diff --git a/Source/DafnyPipeline.Test/_plugins/secondPlugin.cs b/Source/DafnyPipeline.Test/_plugins/secondPlugin.cs new file mode 100644 index 00000000000..cb54597f5b6 --- /dev/null +++ b/Source/DafnyPipeline.Test/_plugins/secondPlugin.cs @@ -0,0 +1,10 @@ +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; + +public class ErrorRewriter : Rewriter { + public ErrorRewriter(ErrorReporter reporter) : base(reporter) { } + + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, "Impossible to continue"); + } +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/_plugins/simplePlugin.cs b/Source/DafnyPipeline.Test/_plugins/simplePlugin.cs new file mode 100644 index 00000000000..7cad925dabf --- /dev/null +++ b/Source/DafnyPipeline.Test/_plugins/simplePlugin.cs @@ -0,0 +1,24 @@ +using Microsoft.Dafny; +using Microsoft.Dafny.Plugins; + +public class TestConfiguration : PluginConfiguration { + public string Argument = ""; + public override void ParseArguments(string[] args) { + Argument = args[0]; + } + public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { + return new Rewriter[] { new ErrorRewriter(errorReporter, this) }; + } +} + +public class ErrorRewriter : Rewriter { + private readonly TestConfiguration configuration; + + public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration) : base(reporter) { + this.configuration = configuration; + } + + public override void PostResolve(ModuleDefinition moduleDefinition) { + Reporter.Error(MessageSource.Compiler, moduleDefinition.tok, "Impossible to continue " + configuration.Argument); + } +} \ No newline at end of file From 1fd20d453b290030b74530db32f0f12adca7b56c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 8 Feb 2022 12:40:34 -0600 Subject: [PATCH 44/47] Removed unused static variable --- Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs | 2 -- 1 file changed, 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index 8cf0d529235..5c038843ff8 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -19,8 +19,6 @@ public abstract class PluginsTestBase : DafnyLanguageServerTestBase { protected DiagnosticsReceiver DiagnosticReceiver; protected string LibraryPath; - private static readonly object PluginSync = new { }; - /// /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. From e17738b9fef67886fe29c45ca9123446c420ca96 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 8 Feb 2022 13:47:33 -0600 Subject: [PATCH 45/47] plugin as a record --- Source/Dafny/Plugin.cs | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs index d48827d715e..0e45662f434 100644 --- a/Source/Dafny/Plugin.cs +++ b/Source/Dafny/Plugin.cs @@ -10,22 +10,11 @@ namespace Microsoft.Dafny; /// 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 /// -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 record Plugin(Assembly Assembly, string[] Args) { + public PluginConfiguration PluginConfiguration { get; init; } = LoadConfiguration(Assembly, Args); public static Plugin Load(string pluginPath, string[] args) { - return new Plugin(pluginPath, args); + return new Plugin(Assembly.LoadFrom(pluginPath), args); } class AutomaticPluginConfiguration : PluginConfiguration { @@ -56,7 +45,8 @@ private static System.Type[] CheckPluginForRewriters(Assembly assembly) { return rewriterTpes; } - private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] args, System.Type[] rewriterTypes) { + private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] args) { + var rewriterTypes = CheckPluginForRewriters(assembly); PluginConfiguration pluginConfiguration = null; foreach (var configurationType in GetConfigurationsTypes(assembly)) { if (pluginConfiguration != null) { From 568f1a59244ef8310d572e73b81bcaf65698ccbb Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 9 Feb 2022 10:45:41 -0600 Subject: [PATCH 46/47] Implemented review comments --- Source/Dafny/Plugin.cs | 26 +++++++++---------- .../DafnyLanguageServer.cs | 7 +++-- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs index 0e45662f434..180e60a0b70 100644 --- a/Source/Dafny/Plugin.cs +++ b/Source/Dafny/Plugin.cs @@ -11,38 +11,34 @@ namespace Microsoft.Dafny; /// The configuration provides the methods to parse command-line arguments and obtain Rewriters /// public record Plugin(Assembly Assembly, string[] Args) { - public PluginConfiguration PluginConfiguration { get; init; } = LoadConfiguration(Assembly, Args); + public PluginConfiguration PluginConfiguration { get; } = LoadConfiguration(Assembly, Args); public static Plugin Load(string pluginPath, string[] args) { return new Plugin(Assembly.LoadFrom(pluginPath), args); } class AutomaticPluginConfiguration : PluginConfiguration { - private Func[] rewriters; - public AutomaticPluginConfiguration(Func[] rewriters) { - this.rewriters = rewriters; - } - + public Func[] Rewriters { get; init; } public override Rewriter[] GetRewriters(ErrorReporter errorReporter) { - return rewriters.Select(funcErrorReporterRewriter => + return Rewriters.Select(funcErrorReporterRewriter => funcErrorReporterRewriter(errorReporter)).ToArray(); } } public static IEnumerable GetConfigurationsTypes(Assembly assembly) { return assembly.GetTypes() - .Where(t => t.IsAssignableTo(typeof(PluginConfiguration))); + .Where(type => type.IsAssignableTo(typeof(PluginConfiguration))); } private static System.Type[] CheckPluginForRewriters(Assembly assembly) { - System.Type[] rewriterTpes = assembly.GetTypes().Where(t => - t.IsAssignableTo(typeof(Rewriter))).ToArray(); + var rewriterTypes = assembly.GetTypes().Where(type => + type.IsAssignableTo(typeof(Rewriter))).ToArray(); // Checks about the plugin to be well-behaved. - if (!rewriterTpes.Any()) { + if (!rewriterTypes.Any()) { throw new Exception($"Plugin {assembly.Location} does not contain any Microsoft.Dafny.Plugins.Rewriter"); } - return rewriterTpes; + return rewriterTypes; } private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] args) { @@ -63,10 +59,12 @@ private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] pluginConfiguration.ParseArguments(args); } - pluginConfiguration ??= new AutomaticPluginConfiguration( + pluginConfiguration ??= new AutomaticPluginConfiguration { + Rewriters = rewriterTypes.Select>((System.Type rewriterType) => (ErrorReporter errorReporter) => - Activator.CreateInstance(rewriterType, new object[] { errorReporter }) as Rewriter).ToArray()); + (Rewriter)Activator.CreateInstance(rewriterType, new object[] { errorReporter })).ToArray() + }; return pluginConfiguration; } diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index bf15f7baab1..5493d7263d3 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -16,7 +16,7 @@ namespace Microsoft.Dafny.LanguageServer { public static class DafnyLanguageServer { - public static List LoadErrors = new(); + public static IReadOnlyList LoadErrors = new List(); private static string DafnyVersion { get { var version = typeof(DafnyLanguageServer).Assembly.GetName().Version!; @@ -52,6 +52,7 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req private static void LoadPlugins(ILogger logger, ILanguageServer server) { var dafnyPluginsOptions = server.GetRequiredService>(); var lastPlugin = ""; + var loadErrors = new List(); try { foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { lastPlugin = pluginPathArgument; @@ -59,8 +60,10 @@ private static void LoadPlugins(ILogger logger, ILanguageServer server) } } catch (Exception e) { logger.LogError(e, $"Error while instantiating plugin {lastPlugin}"); - LoadErrors.Add($"Error while instantiating plugin {lastPlugin}. Please restart the server.\n" + e); + loadErrors.Add($"Error while instantiating plugin {lastPlugin}. Please restart the server.\n" + e); } + + LoadErrors = loadErrors; } /// From eb35472cb2a05d4a585b7fc4b57121ca12ae74a9 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 10 Feb 2022 12:37:39 -0600 Subject: [PATCH 47/47] Refactored a factory + made static variable readonly --- Source/Dafny/Plugin.cs | 9 +++++---- Source/DafnyLanguageServer/DafnyLanguageServer.cs | 6 ++---- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/Source/Dafny/Plugin.cs b/Source/Dafny/Plugin.cs index 180e60a0b70..b80ad2356df 100644 --- a/Source/Dafny/Plugin.cs +++ b/Source/Dafny/Plugin.cs @@ -60,14 +60,15 @@ private static PluginConfiguration LoadConfiguration(Assembly assembly, string[] } pluginConfiguration ??= new AutomaticPluginConfiguration { - Rewriters = - rewriterTypes.Select>((System.Type rewriterType) => - (ErrorReporter errorReporter) => - (Rewriter)Activator.CreateInstance(rewriterType, new object[] { errorReporter })).ToArray() + Rewriters = rewriterTypes.Select(CreateRewriterFactory).ToArray() }; return pluginConfiguration; } + private static Func CreateRewriterFactory(System.Type rewriterType) { + return errorReporter => (Rewriter)Activator.CreateInstance(rewriterType, new object[] { errorReporter }); + } + public IEnumerable GetRewriters(ErrorReporter reporter) { return PluginConfiguration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter)); } diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 5493d7263d3..b64f3b76d55 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -16,7 +16,8 @@ namespace Microsoft.Dafny.LanguageServer { public static class DafnyLanguageServer { - public static IReadOnlyList LoadErrors = new List(); + private static List loadErrors = new List(); + public static IReadOnlyList LoadErrors => loadErrors; private static string DafnyVersion { get { var version = typeof(DafnyLanguageServer).Assembly.GetName().Version!; @@ -52,7 +53,6 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req private static void LoadPlugins(ILogger logger, ILanguageServer server) { var dafnyPluginsOptions = server.GetRequiredService>(); var lastPlugin = ""; - var loadErrors = new List(); try { foreach (var pluginPathArgument in dafnyPluginsOptions.Value.Plugins) { lastPlugin = pluginPathArgument; @@ -62,8 +62,6 @@ private static void LoadPlugins(ILogger logger, ILanguageServer server) logger.LogError(e, $"Error while instantiating plugin {lastPlugin}"); loadErrors.Add($"Error while instantiating plugin {lastPlugin}. Please restart the server.\n" + e); } - - LoadErrors = loadErrors; } ///