From aed940a9aaea220ee4c3f869c9cd5c54b2dc50bd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 23 Feb 2024 12:32:23 +0100 Subject: [PATCH 01/10] Add a warning to dafny run when users are likely to accidentaly have mistyped an option name --- Source/DafnyDriver/Commands/RunCommand.cs | 34 +++++++++++++++++-- Source/DafnyDriver/DafnyNewCli.cs | 1 + .../LitTests/LitTest/cli/runArgument.dfy | 19 +++++++++++ .../LitTest/cli/runArgument.dfy.expect | 11 ++++++ .../Lit/LitCommandWithRedirection.cs | 28 ++++++++++++--- 5 files changed, 86 insertions(+), 7 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy.expect diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs index 6321e990077..9f86ddc5cdd 100644 --- a/Source/DafnyDriver/Commands/RunCommand.cs +++ b/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; } + + /// + /// 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 is a way that is not compliant with POSIX conventions, + /// but we believe this is worth the improved feedback. + /// + 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 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; + } + } + } } diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs index 154ecfc8d26..d2ea5b4c8fc 100644 --- a/Source/DafnyDriver/DafnyNewCli.cs +++ b/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() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy new file mode 100644 index 00000000000..c1f8455a709 --- /dev/null +++ b/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) { + 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"; + } + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy.expect new file mode 100644 index 00000000000..57a2f0fd11f --- /dev/null +++ b/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 diff --git a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs index addf196b88e..6ccf12ccae4 100644 --- a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs +++ b/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 })) @@ -81,15 +94,20 @@ public LitCommandWithRedirection(ILitCommand command, string? inputFile, string? public async Task Execute(TextReader inputReader, TextWriter outWriter, TextWriter errWriter) { var outputWriters = new List { outWriter }; + var errorWriters = new List { errWriter }; if (OutputFile != null) { - outputWriters.Add(new StreamWriter(OutputFile, Append)); + var writer = new StreamWriter(OutputFile, Append); + outputWriters.Add(writer); + if (ErrorFile == OutputFile) { + errorWriters.Add(writer); + } + } else { + if (ErrorFile != null) { + errorWriters.Add(new StreamWriter(ErrorFile, Append)); + } } inputReader = InputFile != null ? new StreamReader(InputFile) : inputReader; - var errorWriters = new List { errWriter }; - if (ErrorFile != null) { - errorWriters.Add(new StreamWriter(ErrorFile, Append)); - } var result = await Command.Execute(inputReader, new CombinedWriter(outWriter.Encoding, outputWriters), new CombinedWriter(errWriter.Encoding, errorWriters)); From fb71bd38957b78636c7a66c2c233ce93e20dc89d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 23 Feb 2024 12:38:28 +0100 Subject: [PATCH 02/10] Fix typo --- Source/DafnyDriver/Commands/RunCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs index 9f86ddc5cdd..226e0dce20e 100644 --- a/Source/DafnyDriver/Commands/RunCommand.cs +++ b/Source/DafnyDriver/Commands/RunCommand.cs @@ -73,7 +73,7 @@ public static Command Create() { /// /// 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 is a way that is not compliant with POSIX conventions, + /// 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. /// private static async Task CheckForMistypedDafnyOption(InvocationContext context, DafnyOptions options) { From f73d079617381a1e5e6b38cfaf0ad618a00585bb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 23 Feb 2024 12:38:53 +0100 Subject: [PATCH 03/10] Improve comment --- Source/DafnyDriver/Commands/RunCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs index 226e0dce20e..5cdc4025c70 100644 --- a/Source/DafnyDriver/Commands/RunCommand.cs +++ b/Source/DafnyDriver/Commands/RunCommand.cs @@ -79,7 +79,7 @@ public static Command Create() { 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 given the same value twice, + // 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, From 05ea0bc272b8807e4e17661f5480c58aacf83ad3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 23 Feb 2024 12:45:06 +0100 Subject: [PATCH 04/10] Add release notes --- docs/dev/news/5097.feat | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/5097.feat diff --git a/docs/dev/news/5097.feat b/docs/dev/news/5097.feat new file mode 100644 index 00000000000..b275d72aea1 --- /dev/null +++ b/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. \ No newline at end of file From c66a3889bc47dd0bb147ea4312d5a8fc2c27f7de Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 26 Feb 2024 11:37:09 +0100 Subject: [PATCH 05/10] Fix bugs in CombinedWriter async methods --- Source/XUnitExtensions/Lit/CombinedWriter.cs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/Source/XUnitExtensions/Lit/CombinedWriter.cs b/Source/XUnitExtensions/Lit/CombinedWriter.cs index 64c3c6b0391..e10263a4d04 100644 --- a/Source/XUnitExtensions/Lit/CombinedWriter.cs +++ b/Source/XUnitExtensions/Lit/CombinedWriter.cs @@ -1,7 +1,9 @@ +using System; using System.Collections.Generic; using System.IO; using System.Linq; using System.Text; +using System.Threading; using System.Threading.Tasks; namespace XUnitExtensions.Lit; @@ -46,4 +48,21 @@ public override Task WriteAsync(char value) { public override Task WriteAsync(char[] buffer, int index, int count) { return Task.WhenAll(writers.Select(w => w.WriteAsync(buffer, index, count))); } + + public override Task WriteLineAsync(char[] buffer, int index, int count) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(buffer, index, count))); + + } + + public override Task WriteLineAsync(string? value) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(value))); + } + + public override Task WriteLineAsync(char value) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(value))); + } + + public override Task WriteLineAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new()) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(buffer, cancellationToken))); + } } \ No newline at end of file From 363d077a0f129ee10b7308164029444b4c797753 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 26 Feb 2024 11:38:24 +0100 Subject: [PATCH 06/10] Silence warning --- .../TestFiles/LitTests/LitTest/cli/runArgument.dfy | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy index c1f8455a709..86dcc904753 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy @@ -1,3 +1,4 @@ +// NONUNIFORM: This tests front-end behavior, and is back-end independent. // RUN: %run %s blie 2 &> %t // RUN: %run %s --blie --2 &>> %t // RUN: %run %s -- --bla --2 &>> %t From 96e8a4e0bd973bbe5badcdac062c0ebd3e151375 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 26 Feb 2024 12:54:08 +0100 Subject: [PATCH 07/10] Trigger CI From 2fa02b6038deada3a4111257e8e74a4b6c99ca8e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 4 Mar 2024 12:21:09 +0100 Subject: [PATCH 08/10] Add missing overrides to CombinedWriters --- Source/XUnitExtensions/Lit/CombinedWriter.cs | 23 +++++++++++++++----- 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/Source/XUnitExtensions/Lit/CombinedWriter.cs b/Source/XUnitExtensions/Lit/CombinedWriter.cs index b6df9cd3cfd..b9753867d27 100644 --- a/Source/XUnitExtensions/Lit/CombinedWriter.cs +++ b/Source/XUnitExtensions/Lit/CombinedWriter.cs @@ -45,24 +45,35 @@ public override Task WriteAsync(char value) { return Task.WhenAll(writers.Select(w => w.WriteAsync(value))); } + public override Task WriteAsync(string? value) { + return Task.WhenAll(writers.Select(w => w.WriteAsync(value))); + } + public override Task WriteAsync(char[] buffer, int index, int count) { return Task.WhenAll(writers.Select(w => w.WriteAsync(buffer, index, count))); } - public override Task WriteLineAsync(char[] buffer, int index, int count) { - return Task.WhenAll(writers.Select(w => w.WriteLineAsync(buffer, index, count))); + public override Task WriteAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new()) { + return Task.WhenAll(writers.Select(w => w.WriteAsync(buffer, cancellationToken))); + } + public override Task WriteLineAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new()) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(buffer, cancellationToken))); } - public override Task WriteLineAsync(string? value) { + public override Task WriteLineAsync(char value) { return Task.WhenAll(writers.Select(w => w.WriteLineAsync(value))); } - public override Task WriteLineAsync(char value) { + public override Task WriteLineAsync(string? value) { return Task.WhenAll(writers.Select(w => w.WriteLineAsync(value))); } - public override Task WriteLineAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new()) { - return Task.WhenAll(writers.Select(w => w.WriteLineAsync(buffer, cancellationToken))); + public override Task WriteLineAsync(char[] buffer, int index, int count) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(buffer, index, count))); + } + + public override Task WriteLineAsync(StringBuilder? value, CancellationToken cancellationToken = new()) { + return Task.WhenAll(writers.Select(w => w.WriteLineAsync(value, cancellationToken))); } } \ No newline at end of file From aff4bc08129916ccc12e5a13095a7ab69f550814 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 4 Mar 2024 13:31:58 +0100 Subject: [PATCH 09/10] Add debugging --- Source/XUnitExtensions/Lit/CombinedWriter.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/XUnitExtensions/Lit/CombinedWriter.cs b/Source/XUnitExtensions/Lit/CombinedWriter.cs index b9753867d27..1323c148719 100644 --- a/Source/XUnitExtensions/Lit/CombinedWriter.cs +++ b/Source/XUnitExtensions/Lit/CombinedWriter.cs @@ -66,6 +66,7 @@ public override Task WriteLineAsync(char value) { } public override Task WriteLineAsync(string? value) { + Console.WriteLine("WriteLineAsync from CombinedWriter called"); return Task.WhenAll(writers.Select(w => w.WriteLineAsync(value))); } From 883165e18d911457b87182948cba91c24e034b39 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 12 Mar 2024 16:05:17 +0100 Subject: [PATCH 10/10] Use OutputWriter instead of ErrorWriter to hopefully get a reliable order --- Source/DafnyDriver/Commands/RunCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs index 5cdc4025c70..1ea8160c9c4 100644 --- a/Source/DafnyDriver/Commands/RunCommand.cs +++ b/Source/DafnyDriver/Commands/RunCommand.cs @@ -87,7 +87,7 @@ private static async Task CheckForMistypedDafnyOption(InvocationContext context, // 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."); + await options.OutputWriter.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;