diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 59ffe8bfcb..90d65d9af8 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -107,9 +107,14 @@ static BoogieOptionBag() { }); DafnyOptions.RegisterLegacyBinding(Cores, (o, f) => o.VcsCores = f == 0 ? (1 + System.Environment.ProcessorCount) / 2 : (int)f); - DafnyOptions.RegisterLegacyBinding(NoVerify, (options, value) => { - var shouldVerify = !value && !options.Get(HiddenNoVerify); - options.Verify = shouldVerify; + DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => { + var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify); + options.Verify = shouldVerify; // Boogie won't verify + options.DafnyVerify = + shouldVerify || + options.Get(DeveloperOptionBag.BoogiePrint) != null || + options.Get(DeveloperOptionBag.SplitPrint) != null || + options.Get(DeveloperOptionBag.PassivePrint) != null; }); DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f); diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs index bff35feaa0..94d8b88294 100644 --- a/Source/DafnyCore/Options/DeveloperOptionBag.cs +++ b/Source/DafnyCore/Options/DeveloperOptionBag.cs @@ -21,7 +21,7 @@ Print passified Boogie program translated from Dafny IsHidden = true, ArgumentHelpName = "file", }; - + // This flag is the only one that can trigger /dafnyVerify in the new CLI and I think it's sufficient public static readonly Option BoogiePrint = new("--bprint", @" Print Boogie program translated from Dafny diff --git a/Source/DafnyDriver.Test/OptionsTest.cs b/Source/DafnyDriver.Test/OptionsTest.cs new file mode 100644 index 0000000000..e93c050f1e --- /dev/null +++ b/Source/DafnyDriver.Test/OptionsTest.cs @@ -0,0 +1,77 @@ +using System.CommandLine; +using System.CommandLine.Builder; +using System.CommandLine.Invocation; +using System.CommandLine.Parsing; +using System.Diagnostics; +using System.IO.Pipelines; +using System.Reactive.Concurrency; +using System.Reflection; +using System.Text; +using Microsoft.Dafny; +using Microsoft.Extensions.Logging.Abstractions; +using OmniSharp.Extensions.JsonRpc; +using OmniSharp.Extensions.JsonRpc.Client; +using OmniSharp.Extensions.JsonRpc.Serialization; +using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using XunitAssertMessages; +using Command = System.CommandLine.Command; + +namespace DafnyDriver.Test; + + +public class OptionsTest { + [Fact] + public async Task RunFlagsOverride() { + await TestCliRunArgs([], options => { + Assert.True(options.DafnyVerify); + Assert.True(options.Verify); + return 0; + }); + await TestCliRunArgs(["--no-verify"], options => { + Assert.False(options.DafnyVerify); + Assert.False(options.Verify); + return 0; + }); + await TestCliRunArgs(["--no-verify", "--bprint=-"], options => { + Assert.True(options.DafnyVerify); + Assert.False(options.Verify); + return 0; + }); + await TestCliRunArgs(["--no-verify", "--sprint=-"], options => { + Assert.True(options.DafnyVerify); + Assert.False(options.Verify); + return 0; + }); + await TestCliRunArgs(["--no-verify", "--pprint=-"], options => { + Assert.True(options.DafnyVerify); + Assert.False(options.Verify); + return 0; + }); + } + + private static async Task TestCliRunArgs(string[] cmdArgs, Func optionsCallback) { + var fullArgs = new string[] { + "run" + }; + fullArgs = fullArgs.Concat(cmdArgs).Concat(new string[] { "file.dfy" }).ToArray(); + var callbackCalled = false; + var newOptionsCallback = (DafnyOptions options) => { + callbackCalled = true; + return optionsCallback(options); + }; + Command cmd = RunCommand.Create(newOptionsCallback); + var rootCommand = new RootCommand("Test root command"); + rootCommand.AddCommand(cmd); + var builder = new CommandLineBuilder(rootCommand).UseDefaults(); + var parser = builder.Build(); + TextReader inputReader = new StringReader(""); + var outputWriter = new StringWriter(); + var errorWriter = new StringWriter(); + var console = new WritersConsole(inputReader, outputWriter, errorWriter); + var exitCode = await DafnyNewCli.ExecuteForParser(console, fullArgs, parser); + Assert.Equal("", errorWriter.ToString()); + Assert.Equal(0, exitCode); + Assert.True(callbackCalled); + } +} diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs index ce994f0d1b..6fe26b9c1a 100644 --- a/Source/DafnyDriver/Commands/RunCommand.cs +++ b/Source/DafnyDriver/Commands/RunCommand.cs @@ -49,7 +49,7 @@ static RunCommand() { Concat(DafnyCommands.ConsoleOutputOptions). Concat(DafnyCommands.ResolverOptions); - public static Command Create() { + public static Command Create(Func continuation = null) { var result = new Command("run", "Run the program."); result.AddArgument(DafnyCommands.FileArgument); result.AddArgument(UserProgramArguments); @@ -63,7 +63,9 @@ public static Command Create() { options.Compile = true; options.RunAfterCompile = true; options.ForceCompile = options.Get(BoogieOptionBag.NoVerify); - + if (continuation != null) { + return continuation(options); + } return await SynchronousCliCompilation.Run(options); }); return result; diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs index ce476e9d98..d38d84cd03 100644 --- a/Source/DafnyDriver/DafnyNewCli.cs +++ b/Source/DafnyDriver/DafnyNewCli.cs @@ -172,6 +172,10 @@ private static void ProcessOption(InvocationContext context, Option option, Dafn } public static Task Execute(IConsole console, IReadOnlyList arguments) { + return ExecuteForParser(console, arguments, Parser); + } + + public static Task ExecuteForParser(IConsole console, IReadOnlyList arguments, System.CommandLine.Parsing.Parser parser) { foreach (var symbol in AllSymbols) { if (symbol is Option option) { if (!option.Arity.Equals(ArgumentArity.ZeroOrMore) && !option.Arity.Equals(ArgumentArity.OneOrMore)) { @@ -180,7 +184,7 @@ public static Task Execute(IConsole console, IReadOnlyList argument } } - return Parser.InvokeAsync(arguments.ToArray(), console); + return parser.InvokeAsync(arguments.ToArray(), console); } private static readonly MethodInfo GetValueForOptionMethod; diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index 73c9270560..1056439299 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -287,25 +287,34 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* if (err != null) { exitValue = ExitValue.DAFNY_ERROR; options.Printer.ErrorWriteLine(options.OutputWriter, err); - } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck - && options.DafnyVerify) { + } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck) { + bool verified; + PipelineOutcome outcome; + IDictionary moduleStats; dafnyProgram.ProofDependencyManager = depManager; - var boogiePrograms = - await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList()); - - string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1])); - var (verified, outcome, moduleStats) = - await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId); - - if (options.TrackVerificationCoverage) { - ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options, dafnyProgram.Reporter, depManager); - var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport); - if (coverageReportDir != null) { - await new CoverageReporter(options).SerializeVerificationCoverageReport( - depManager, dafnyProgram, - boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements), - coverageReportDir); + if (!options.DafnyVerify) { + verified = false; + outcome = PipelineOutcome.Done; + moduleStats = new Dictionary(); + } else { + var boogiePrograms = + await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList()); + + string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1])); + (verified, outcome, moduleStats) = + await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId); + + if (options.TrackVerificationCoverage) { + ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options, + dafnyProgram.Reporter, depManager); + var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport); + if (coverageReportDir != null) { + await new CoverageReporter(options).SerializeVerificationCoverageReport( + depManager, dafnyProgram, + boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements), + coverageReportDir); + } } } @@ -329,7 +338,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* } var failBecauseOfDiagnostics = dafnyProgram.Reporter.FailCompilationMessage; - if (!verified) { + if (!verified && options.DafnyVerify) { exitValue = ExitValue.VERIFICATION_ERROR; } else if (!compiled) { exitValue = ExitValue.COMPILE_ERROR; diff --git a/Source/DafnyDriver/WritersConsole.cs b/Source/DafnyDriver/WritersConsole.cs index 471f41dbc7..1dba93bcb2 100644 --- a/Source/DafnyDriver/WritersConsole.cs +++ b/Source/DafnyDriver/WritersConsole.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; -class WritersConsole : IConsole { +public class WritersConsole : IConsole { public TextReader InputWriter { get; } public TextWriter ErrWriter { get; } public TextWriter OutWriter { get; } diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs index ea81a97689..ed92f909ad 100644 --- a/Source/TestDafny/MultiBackendTest.cs +++ b/Source/TestDafny/MultiBackendTest.cs @@ -507,7 +507,7 @@ await output.WriteLineAsync( } await output.WriteLineAsync("Execution failed, for reasons other than known unsupported features. Output:"); await output.WriteLineAsync(outputString); - await output.WriteLineAsync("Error:"); + await output.WriteLineAsync($"Error (code={exitCode}):"); await output.WriteLineAsync(error); return exitCode; }