fix: Fixed the escaper to simplify the plugin syntax (#1817)

* Fixed the escaper to simplify the syntax

* Review comments

Author: MikaelMayer

Source/Dafny/DafnyOptions.cs

@@ -238,15 +238,6 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
         case "plugin": {
             if (ps.ConfirmArgumentCount(1)) {
               var pluginAndArgument = args[ps.i];
-              if (pluginAndArgument.Length > 0 &&
-                  pluginAndArgument[0] == '"' &&
-                  pluginAndArgument[^1] == '"'
-                  ) {
-                var unescapeRegex = new Regex(@"\\""|\\\\");
-                pluginAndArgument = unescapeRegex.Replace(pluginAndArgument.Substring(1, pluginAndArgument.Length - 2),
-                  match => match.Groups[0].Value == @"\""" ? "\"" : @"\"
-                );
-              }
               if (pluginAndArgument.Length > 0) {
                 var pluginArray = pluginAndArgument.Split(',');
                 var pluginPath = pluginArray[0];
@@ -255,12 +246,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
                   // 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();
+                  arguments = ParsePluginArguments(argumentsString);
                 }
                 Plugins.Add(Plugin.Load(pluginPath, arguments));
               }
@@ -546,6 +532,18 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com
       return TestGenOptions.ParseOption(name, ps) || base.ParseOption(name, ps);
     }
 
+    private static string[] ParsePluginArguments(string argumentsString) {
+      var splitter = new Regex(@"""(?<escapedArgument>(?:[^""\\]|\\\\|\\"")*)""|(?<rawArgument>[^ ]+)");
+      var escapedChars = new Regex(@"(?<escapedDoubleQuote>\\"")|\\\\");
+      return splitter.Matches(argumentsString).Select(
+        matchResult =>
+          matchResult.Groups["escapedArgument"].Success
+          ? escapedChars.Replace(matchResult.Groups["escapedArgument"].Value,
+            matchResult2 => matchResult2.Groups["escapedDoubleQuote"].Success ? "\"" : "\\")
+          : matchResult.Groups["rawArgument"].Value
+      ).ToArray();
+    }
+
     protected void InvalidArgumentError(string name, CommandLineParseState ps) {
       ps.Error("Invalid argument \"{0}\" to option {1}", ps.args[ps.i], name);
     }

Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs

@@ -19,7 +19,7 @@ public async Task SetUp() {
     "PluginsAdvancedTest";
 
   protected override string[] CommandLineArgument =>
-    new[] { $@"--dafny:plugins:0=""{LibraryPath},force you""" };
+    new[] { $"--dafny:plugins:0={LibraryPath},force you" };
 
   [TestMethod]
   public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration() {
@@ -35,7 +35,7 @@ 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, DafnyOptions.O.Plugins.Count, "Too many plugins loaded");
+    Assert.AreEqual(1, DafnyOptions.O.Plugins.Count, "Not exactly 1 plugin 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);

Source/DafnyLanguageServer.Test/Various/PluginsTest.cs

@@ -18,7 +18,7 @@ public async Task SetUp() {
     "PluginsTest";
 
   protected override string[] CommandLineArgument =>
-    new[] { $@"--dafny:plugins:0=""{LibraryPath},\""because\\ whatever\""""" };
+    new[] { $@"--dafny:plugins:0={LibraryPath},""because\\ \""whatever""" };
 
   [TestMethod]
   public async Task EnsureItIsPossibleToLoadAPluginWithArguments() {
@@ -28,9 +28,9 @@ public async Task EnsureItIsPossibleToLoadAPluginWithArguments() {
     var resolutionReport = await DiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken.None);
     Assert.AreEqual(documentItem.Uri, resolutionReport.Uri);
     var diagnostics = resolutionReport.Diagnostics.ToArray();
-    Assert.AreEqual(DafnyOptions.O.Plugins.Count, 1, "Too many plugins loaded");
+    Assert.AreEqual(DafnyOptions.O.Plugins.Count, 1, "Not exactly 1 plugin loaded");
     Assert.AreEqual(1, diagnostics.Length, LibraryPath + " did not raise an error.");
-    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);
   }
 

Source/DafnyLanguageServer/README.md

@@ -79,12 +79,17 @@ Options provided through the command line have higher priority than the options
 ### Plugins
 
 ```sh
-# 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)
+# Provides a path to assemblies and optional space-separated command-line arguments after a comma.
 # Repeat with --dafny:plugins:0=... --dafny:plugins:1=... for multiple plugins.
---dafny:plugins:0=example.dll
---dafny:plugins:0=example2.dll,oneArgument
-"--dafny:plugins:0=\"example2.dll,\\\"firstArgument with space\\\" secondArgument\""
+--dafny:plugins:0=path\to\example.dll
+--dafny:plugins:0=path/to/example2.dll,oneArgument
+--dafny:plugins:0=example3.dll,"firstArgument with \" space and quote" secondArgument
+
+# On the command-line, you'd use the following escapes for the first and third examples:
+"--dafny:plugins:0=path\\to\\example.dll"
+"--dafny:plugins:0=example3.dll,\"firstArgument with \\\" space and quote\" secondArgument"
+
+# For just the dafny executable, replace `--dafny:plugins:X` by `--plugin:` that you can repeat.
 ```
 
 #### About plugins