feat: Dafny Plugins support (#122)

Author: MikaelMayer

.eslintrc.json

@@ -68,6 +68,7 @@
     "func-call-spacing": "off",
     "@typescript-eslint/func-call-spacing": "warn",
     "keyword-spacing": "off",
+    "curly": "warn",
     "@typescript-eslint/keyword-spacing": [
       "warn",
       {

package.json

@@ -155,6 +155,14 @@
           "default": "true",
           "description": "Mark ghost statements in the code (requires restart and Dafny 3.4.0+)"
         },
+        "dafny.dafnyPlugins": {
+          "type": "array",
+          "items": {
+            "type": "string"
+          },
+          "default": [],
+          "description": "Absolute paths to assemblies to be used as plugins (requires restart and Dafny 3.4.0+).\nExample 1: /user/home/dafnyplugin.dll\nExample 2: /user/home/dafnyplugin.dll,oneArgument\nExample 3: /user/home/dafnyplugin.dll,\"argument with space and \\\" escaped quote\" secondArgument"
+        },
         "dafny.languageServerLaunchArgs": {
           "type": "array",
           "items": {

src/constants.ts

@@ -23,6 +23,7 @@ export namespace ConfigurationConstants {
     export const VerificationVirtualCores = 'verificationVirtualCores';
     export const VerificationCachingPolicy = 'verificationCachingPolicy';
     export const MarkGhostStatements = 'markGhostStatements';
+    export const DafnyPlugins = 'dafnyPlugins';
   }
 
   export namespace Compiler {

src/extension.ts

@@ -58,7 +58,7 @@ class ExtensionRuntime {
 
   private async initializeClient(): Promise<void> {
     this.statusOutput.appendLine(`starting Dafny from ${getLanguageServerRuntimePath(this.context)}`);
-    this.client = await DafnyLanguageClient.create(this.context);
+    this.client = await DafnyLanguageClient.create(this.context, this.statusOutput);
     this.client.start();
     await this.client.onReady();
     this.languageServerVersion = await this.getLanguageServerVersionAfterStartup();

src/language/dafnyLanguageClient.ts

@@ -1,4 +1,4 @@
-import { ExtensionContext, Disposable } from 'vscode';
+import { ExtensionContext, Disposable, OutputChannel } from 'vscode';
 import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node';
 
 import Configuration from '../configuration';
@@ -21,6 +21,7 @@ function getLanguageServerLaunchArgs(): string[] {
     getVerifierCachingPolicy(),
     getVerifierVirtualCoresArgument(),
     getMarkGhostStatementsArgument(),
+    ...getDafnyPluginsArgument(),
     ...launchArgs
   ];
 }
@@ -51,6 +52,18 @@ function getMarkGhostStatementsArgument(): string {
   return `--ghost:markStatements=${Configuration.get<string>(ConfigurationConstants.LanguageServer.MarkGhostStatements)}`;
 }
 
+function getDafnyPluginsArgument(): string[] {
+  const plugins = Configuration.get<string[]>(ConfigurationConstants.LanguageServer.DafnyPlugins);
+  if(plugins === null || !Array.isArray(plugins)) {
+    return [];
+  }
+  return (
+    plugins
+      .filter(plugin => plugin !== null && plugin !== '')
+      .map((plugin, i) => `--dafny:plugins:${i}=${plugin}`)
+  );
+}
+
 export class DafnyLanguageClient extends LanguageClient {
   // eslint-disable-next-line max-params
   private constructor(id: string, name: string, serverOptions: ServerOptions, clientOptions: LanguageClientOptions, forceDebug?: boolean) {
@@ -61,9 +74,18 @@ export class DafnyLanguageClient extends LanguageClient {
     return this.sendRequest<ICounterExampleItem[]>('dafny/counterExample', param);
   }
 
-  public static async create(context: ExtensionContext): Promise<DafnyLanguageClient> {
+  public static argumentsToCommandLine(launchArguments: string[]): string {
+    return launchArguments.map(oneArgument =>
+      (/\s|"|\\/.exec(oneArgument))
+        ? '"' + oneArgument.replace(/\\/g, '\\\\').replace(/"/g, '\\"') + '"'
+        : oneArgument
+    ).join(' ');
+  }
+
+  public static async create(context: ExtensionContext, statusOutput: OutputChannel): Promise<DafnyLanguageClient> {
     const dotnetExecutable = await getDotnetExecutablePath();
     const launchArguments = [ getLanguageServerRuntimePath(context), ...getLanguageServerLaunchArgs() ];
+    statusOutput.appendLine(`Language server arguments: ${DafnyLanguageClient.argumentsToCommandLine(launchArguments)}`);
     const serverOptions: ServerOptions = {
       run: { command: dotnetExecutable, args: launchArguments },
       debug: { command: dotnetExecutable, args: launchArguments }