Check for mistyped options when using dafny run

Source/DafnyDriver/Commands/RunCommand.cs

@@ -1,8 +1,12 @@
 using System;
 using System.Collections.Generic;
 using System.CommandLine;
+using System.CommandLine.Invocation;
+using System.CommandLine.Parsing;
+using System.Data;
 using System.IO;
 using System.Linq;
+using System.Threading.Tasks;
 using DafnyCore;
 
 namespace Microsoft.Dafny;
@@ -51,17 +55,43 @@ public static Command Create() {
     var result = new Command("run", "Run the program.");
     result.AddArgument(DafnyCommands.FileArgument);
     result.AddArgument(UserProgramArguments);
+    // result.TreatUnmatchedTokensAsErrors = false;
     foreach (var option in Options) {
       result.AddOption(option);
     }
-    DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, context) => {
+    DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, context) => {
+      await CheckForMistypedDafnyOption(context, options);
       options.MainArgs = context.ParseResult.GetValueForArgument(UserProgramArguments).ToList();
       options.Compile = true;
       options.RunAfterCompile = true;
       options.ForceCompile = options.Get(BoogieOptionBag.NoVerify);
 
-      return SynchronousCliCompilation.Run(options);
+      return await SynchronousCliCompilation.Run(options);
     });
     return result;
   }
+
+  /// <summary>
+  /// This check tries to determine if users tried to use a Dafny option but mistyped the option name.
+  /// This check uses the position of a `--` token in a way that is not compliant with POSIX conventions,
+  /// but we believe this is worth the improved feedback.
+  /// </summary>
+  private static async Task CheckForMistypedDafnyOption(InvocationContext context, DafnyOptions options) {
+    var userProgramArgumentTokens = context.ParseResult.FindResultFor(UserProgramArguments)!.Tokens.Select(t => t.Value).ToHashSet();
+    foreach (var token in context.ParseResult.Tokens) {
+      // This check may lead to false positives if CLI is given the same value twice,
+      // once as a Dafny option and once as a user program argument
+      // The problem is that the tokens in context.ParseResult.FindResultFor(UserProgramArguments)!.Tokens
+      // are not aware of their position in the argument list,
+      // and cannot be compared with the tokens in context.ParseResult.Tokens,
+      // so it's not possible to determine whether they occurred before the -- or not.
+      var valueOfUserProgramArgument = userProgramArgumentTokens.Contains(token.Value);
+      if (token.Value.StartsWith("--") && token.Type == TokenType.Argument && valueOfUserProgramArgument) {
+        await options.ErrorWriter.WriteLineAsync($"Argument {token.Value} is not a Dafny option so it was interpreted as an argument to the user program, even though it starts with '--'. Move this argument to after a `--` token to silence this message.");
+      }
+      if (token.Value == "--") {
+        break;
+      }
+    }
+  }
 }

Source/DafnyDriver/DafnyNewCli.cs

@@ -26,6 +26,7 @@ public static class DafnyNewCli {
 
   private static void AddCommand(Command command) {
     RootCommand.AddCommand(command);
+    RootCommand.TreatUnmatchedTokensAsErrors = false;
   }
 
   static DafnyNewCli() {

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy

@@ -0,0 +1,19 @@
+// RUN: %run %s blie 2 &> %t
+// RUN: %run %s --blie --2 &>> %t
+// RUN: %run %s -- --bla --2 &>> %t
+// RUN: %diff "%s.expect" "%t"
+
+method Main(args: seq<string>) {
+  if |args| != 3 {
+    print "Expected 3 arguments, got ", |args|;
+  } else {
+    print args[1], " says ";
+    if args[2] == "1" {
+      print "hello\n";
+    } else if args[2] == "2" {
+      print "howdy\n";
+    } else {
+      print args[2],"\n";
+    }
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy.expect

@@ -0,0 +1,11 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+blie says howdy
+Argument --blie is not a Dafny option so it was interpreted as an argument to the user program, even though it starts with '--'. Move this argument to after a `--` token to silence this message.
+Argument --2 is not a Dafny option so it was interpreted as an argument to the user program, even though it starts with '--'. Move this argument to after a `--` token to silence this message.
+
+Dafny program verifier finished with 1 verified, 0 errors
+--blie says --2
+
+Dafny program verifier finished with 1 verified, 0 errors
+--bla says --2

Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs

@@ -41,12 +41,25 @@ public static LitCommandWithRedirection Parse(Token[] tokens, LitTestConfigurati
         errorFile = config.ApplySubstitutions(argumentList[redirectErrorIndex + 1].Value).Single();
         argumentList.RemoveRange(redirectErrorIndex, 2);
       }
+      var redirectOutAndErrorIndex = argumentList.FindIndex(t => t.Value == "&>");
+      if (redirectOutAndErrorIndex >= 0) {
+        outputFile = config.ApplySubstitutions(argumentList[redirectOutAndErrorIndex + 1].Value).Single();
+        errorFile = outputFile;
+        argumentList.RemoveRange(redirectOutAndErrorIndex, 2);
+      }
       var redirectErrorAppendIndex = argumentList.FindIndex(t => t.Value == "2>>");
       if (redirectErrorAppendIndex >= 0) {
         errorFile = config.ApplySubstitutions(argumentList[redirectErrorAppendIndex + 1].Value).Single();
         appendOutput = true;
         argumentList.RemoveRange(redirectErrorAppendIndex, 2);
       }
+      var redirectOutAndErrorAppendIndex = argumentList.FindIndex(t => t.Value == "&>>");
+      if (redirectOutAndErrorAppendIndex >= 0) {
+        outputFile = config.ApplySubstitutions(argumentList[redirectOutAndErrorAppendIndex + 1].Value).Single();
+        errorFile = outputFile;
+        appendOutput = true;
+        argumentList.RemoveRange(redirectOutAndErrorAppendIndex, 2);
+      }
 
       ILitCommand CreateCommand() {
         var arguments = argumentList.SelectMany(a => config.ApplySubstitutions(a.Value).Select(v => a with { Value = v }))
@@ -82,19 +95,21 @@ public LitCommandWithRedirection(ILitCommand command, string? inputFile, string?
     public async Task<int> Execute(TextReader inputReader, TextWriter outWriter, TextWriter errWriter) {
       var outputWriters = new List<TextWriter> { outWriter };
       var writersToClose = new List<StreamWriter>();
+      var errorWriters = new List<TextWriter> { errWriter };
       if (OutputFile != null) {
         var outputStreamWriter = new StreamWriter(OutputFile, Append);
         writersToClose.Add(outputStreamWriter);
         outputWriters.Add(outputStreamWriter);
-      }
-      inputReader = InputFile != null ? new StreamReader(InputFile) : inputReader;
-
-      var errorWriters = new List<TextWriter> { errWriter };
-      if (ErrorFile != null) {
+        if (OutputFile == ErrorFile) {
+          errorWriters.Add(outputStreamWriter);
+        }
+      } else if (ErrorFile != null) {
         var errorStreamWriter = new StreamWriter(ErrorFile, Append);
         writersToClose.Add(errorStreamWriter);
         errorWriters.Add(errorStreamWriter);
       }
+      inputReader = InputFile != null ? new StreamReader(InputFile) : inputReader;
+
       var result = await Command.Execute(inputReader,
         new CombinedWriter(outWriter.Encoding, outputWriters),
         new CombinedWriter(errWriter.Encoding, errorWriters));

docs/dev/news/5097.feat

@@ -0,0 +1 @@
+Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name.