diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs index 4eab012bc8..7f9503f9d2 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/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index c7c9d8bbbd..bf1a439cd9 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -22,6 +22,7 @@ using JetBrains.Annotations; using Microsoft.Dafny; using Microsoft.Dafny.Triggers; +using Serilog.Events; using PODesc = Microsoft.Dafny.ProofObligationDescription; using static Microsoft.Dafny.GenericErrors; @@ -700,6 +701,10 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { return new Bpl.Program(); } + if (Options.Get(CommonOptionBag.LogLevelOption).CompareTo(LogEventLevel.Verbose) <= 0) { + Options.OutputWriter.WriteLine("Starting translation to Boogie of module " + forModule.FullDafnyName); + } + foreach (var plugin in p.Options.Plugins) { foreach (var rewriter in plugin.GetRewriters(p.Reporter)) { rewriter.PreVerify(forModule); diff --git a/Source/DafnyDriver.Test/OptionsTest.cs b/Source/DafnyDriver.Test/OptionsTest.cs deleted file mode 100644 index e93c050f1e..0000000000 --- a/Source/DafnyDriver.Test/OptionsTest.cs +++ /dev/null @@ -1,77 +0,0 @@ -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 6fe26b9c1a..ce994f0d1b 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(Func continuation = null) { + public static Command Create() { var result = new Command("run", "Run the program."); result.AddArgument(DafnyCommands.FileArgument); result.AddArgument(UserProgramArguments); @@ -63,9 +63,7 @@ public static Command Create(Func continuation = null) { 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 100f6311b5..399b6b5d35 100644 --- a/Source/DafnyDriver/DafnyNewCli.cs +++ b/Source/DafnyDriver/DafnyNewCli.cs @@ -172,10 +172,6 @@ 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)) { @@ -184,7 +180,7 @@ public static Task ExecuteForParser(IConsole console, IReadOnlyList } } - return parser.InvokeAsync(arguments.ToArray(), console); + return Parser.InvokeAsync(arguments.ToArray(), console); } private static readonly MethodInfo GetValueForOptionMethod; diff --git a/Source/DafnyDriver/WritersConsole.cs b/Source/DafnyDriver/WritersConsole.cs index 1dba93bcb2..471f41dbc7 100644 --- a/Source/DafnyDriver/WritersConsole.cs +++ b/Source/DafnyDriver/WritersConsole.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; -public class WritersConsole : IConsole { +class WritersConsole : IConsole { public TextReader InputWriter { get; } public TextWriter ErrWriter { get; } public TextWriter OutWriter { get; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCases.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCases.dfy new file mode 100644 index 0000000000..8883498478 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCases.dfy @@ -0,0 +1,25 @@ +// RUN: %baredafny run %args --log-level verbose "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check" + +// RUN: %baredafny run %args --log-level verbose --no-verify "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesNoTranslation.check" + +// RUN: %baredafny run %args --log-level verbose --no-verify --bprint:file.bpl "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check" + +// RUN: %baredafny run %args --log-level verbose --no-verify --sprint:file.bpl "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check" + +// RUN: %baredafny run %args --log-level verbose --no-verify --sprint:file.bpl "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check" + +module VerifiableModule { + @Test + method CanTest() { + assert 1 == 1; + expect 1 == 1; + } + method Main() { + CanTest(); + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesNoTranslation.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesNoTranslation.check new file mode 100644 index 0000000000..5329d57f94 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesNoTranslation.check @@ -0,0 +1 @@ +// CHECK-NOT: Starting translation to Boogie of module VerifiableModule diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesTranslate.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesTranslate.check new file mode 100644 index 0000000000..5fd0f326b6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesTranslate.check @@ -0,0 +1 @@ +// CHECK: Starting translation to Boogie of module VerifiableModule