From 47056fdff8a5de83da8df712ce0951a3162c2ab5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 11 May 2023 11:54:28 +0200 Subject: [PATCH] Run integration tests in single process (#3715) ### Changes - `dafny run --target=cs` now uses a separate process to run, so the statics of the compiled source code, such as `Console`, are not shared with the Dafny Compiler - Uses of `Console.` are replaced with non-static references. - Move `DafnyFile` class into its own file - Remove `ThreadTaskScheduler` which creates one-shot threads, and instead use a thread pool. Also consistently use large threads for resolution, translation to Boogie, printing and compilation. - Made counter example IDE support thread-safe - The TestDafny project now uses the new CLI UI By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../workflows/check-deep-tests-reusable.yml | 2 +- .github/workflows/deep-tests.yml | 1 + .../workflows/integration-tests-reusable.yml | 2 +- .github/workflows/msbuild.yml | 2 + .github/workflows/runtime-tests.yml | 2 + .../DafnyCore/AST/ExtremeLemmaBodyCloner.cs | 8 +- Source/DafnyCore/AST/Grammar/Printer.cs | 4 + Source/DafnyCore/AST/Types/Types.cs | 4 +- Source/DafnyCore/Auditor/Auditor.cs | 2 +- .../Compilers/CSharp/Compiler-Csharp.cs | 2 +- .../Compilers/CSharp/CsharpBackend.cs | 101 +++---- .../Compilers/CoverageInstrumenter.cs | 4 +- .../Compilers/Cplusplus/Compiler-cpp.cs | 2 +- .../Compilers/Cplusplus/CppCompilerBackend.cs | 11 +- .../DafnyCore/Compilers/Dafny/DafnyBackend.cs | 9 +- .../DafnyCore/Compilers/ExecutableBackend.cs | 50 +++- .../DafnyCore/Compilers/GoLang/GoBackend.cs | 20 +- .../DafnyCore/Compilers/Java/JavaBackend.cs | 14 +- .../Compilers/JavaScript/JavaScriptBackend.cs | 20 +- .../Compilers/Library/LibraryBackend.cs | 5 +- .../Compilers/Python/PythonBackend.cs | 15 +- Source/DafnyCore/Dafny.atg | 6 +- Source/DafnyCore/DafnyConsolePrinter.cs | 11 + Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/DafnyFile.cs | 178 ++++++++++++ Source/DafnyCore/DafnyMain.cs | 274 ++++-------------- Source/DafnyCore/DafnyOptions.cs | 22 +- Source/DafnyCore/Generic/Reporting.cs | 14 +- Source/DafnyCore/Generic/Util.cs | 24 +- Source/DafnyCore/JsonDiagnostics.cs | 6 +- .../DafnyCore/Plugins/IExecutableBackend.cs | 6 +- .../NameResolutionAndTypeInference.cs | 72 ++--- Source/DafnyCore/Resolver/Resolver.cs | 6 +- Source/DafnyCore/Resolver/TypeConstraint.cs | 2 +- .../DafnyCore/Rewriters/ForallStmtRewriter.cs | 10 +- Source/DafnyCore/Rewriters/IRewriter.cs | 16 + Source/DafnyCore/Triggers/TriggerUtils.cs | 4 +- .../DafnyCore/Triggers/TriggersCollector.cs | 2 +- Source/DafnyCore/UndisposableTextWriter.cs | 247 ++++++++++++++++ .../Verifier/Translator.ClassMembers.cs | 4 +- .../Verifier/Translator.TrStatement.cs | 2 +- Source/DafnyCore/Verifier/Translator.cs | 92 +++--- Source/DafnyDriver/CSVTestLogger.cs | 7 +- .../DafnyDriver/Commands/CommandRegistry.cs | 35 ++- Source/DafnyDriver/DafnyDriver.cs | 181 ++++++------ Source/DafnyDriver/TextLogger.cs | 7 +- .../DafnyDriver/VerificationResultLogger.cs | 4 +- .../CodeActions/CodeActionsTest.cs | 4 + .../Completion/DotCompletionTest.cs | 4 + .../DafnyLanguageServerTestBase.cs | 11 +- .../Formatting/FormattingTest.cs | 4 + ...hedLinearVerificationGutterStatusTester.cs | 4 + ...entLinearVerificationGutterStatusTester.cs | 3 + .../LinearVerificationGutterStatusTester.cs | 4 + ...eorderingVerificationGutterStatusTester.cs | 6 +- ...pleLinearVerificationGutterStatusTester.cs | 4 + .../Lookup/DefinitionTest.cs | 4 + .../Lookup/DocumentSymbolTest.cs | 4 + .../Lookup/HoverTest.cs | 4 + .../Lookup/HoverVerificationTest.cs | 4 + .../Lookup/SignatureHelpTest.cs | 4 + .../ProjectFiles/ProjectFilesTest.cs | 4 + .../StandaloneServerTest.cs | 37 ++- .../Synchronization/CloseDocumentTest.cs | 4 + .../DeclarationLocationMigrationTest.cs | 4 + .../Synchronization/DiagnosticsTest.cs | 4 + .../Synchronization/GhostDiagnosticsTest.cs | 4 + .../Synchronization/LookupMigrationTest.cs | 4 + .../Synchronization/OpenDocumentTest.cs | 4 + .../Synchronization/SaveDocumentTest.cs | 4 + .../Synchronization/SymbolMigrationTest.cs | 4 + .../SynchronizationTestBase.cs | 6 +- .../Synchronization/TextInsertionTest.cs | 4 + .../Synchronization/TextReplacementTest.cs | 4 + .../Synchronization/VerificationStatusTest.cs | 4 + .../Unit/GhostStateDiagnosticCollectorTest.cs | 5 +- .../Unit/ParserExceptionTest.cs | 7 +- .../Unit/TextDocumentLoaderTest.cs | 9 +- .../Util/ClientBasedLanguageServerTest.cs | 4 + .../Util/MarkupTestFileTest.cs | 1 - .../Various/CancelVerificationTest.cs | 4 + .../CompilationStatusNotificationTest.cs | 4 + .../Various/ConcurrentInteractionsTest.cs | 4 + .../Various/CounterExampleTest.cs | 4 + .../Various/DiagnosticMigrationTest.cs | 4 + .../Various/ExceptionTests.cs | 4 + .../Various/IncludeFileTest.cs | 4 + .../Various/MultiFileTest.cs | 4 + .../Various/PluginsAdvancedTest.cs | 4 + .../Various/PluginsCodeActionTest.cs | 4 + .../Various/PluginsTest.cs | 4 + .../Various/PluginsTestBase.cs | 4 + .../Various/PluginsTestWithVerification.cs | 4 + .../Various/ResourceUsageTest.cs | 4 + .../Various/StabilityTest.cs | 4 + .../CounterExampleGeneration/DafnyModel.cs | 4 +- .../Language/DafnyLangParser.cs | 2 +- .../Language/DafnyProgramVerifier.cs | 5 +- .../StandaloneServerCli.cs | 6 +- .../Workspace/TextDocumentLoader.cs | 7 +- .../Workspace/ThreadTaskScheduler.cs | 42 --- Source/DafnyPipeline.Test/DocstringTest.cs | 11 +- .../DafnyPipeline.Test/FormatterBaseTest.cs | 18 +- .../FormatterComprehensions.cs | 8 +- .../FormatterForApplySuffixRelated.cs | 9 +- .../FormatterForAssignments.cs | 9 +- .../FormatterForCalcStmt.cs | 9 +- .../FormatterForComments.cs | 8 +- .../FormatterForDatatypeDeclarationTest.cs | 8 +- .../FormatterForExpressions.cs | 8 +- .../DafnyPipeline.Test/FormatterForMembers.cs | 10 +- .../FormatterForSpecifications.cs | 8 +- .../FormatterForStatements.cs | 9 +- .../FormatterForTopLevelDeclarations.cs | 9 +- Source/DafnyPipeline.Test/FormatterIssues.cs | 7 +- .../InterMethodVerificationStability.cs | 16 +- .../IntraMethodVerificationStability.cs | 17 +- Source/DafnyPipeline.Test/Issue1355.cs | 16 +- Source/DafnyPipeline.Test/PluginsTest.cs | 20 +- Source/DafnyPipeline.Test/RelativePaths.cs | 10 +- Source/DafnyPipeline.Test/TranslatorTest.cs | 6 +- Source/DafnyPipeline.Test/Trivia.cs | 12 +- .../WriterFromOutputHelper.cs | 30 ++ Source/DafnyServer/CounterExampleProvider.cs | 10 +- Source/DafnyServer/DafnyHelper.cs | 12 +- Source/DafnyServer/Server.cs | 4 +- Source/DafnyTestGeneration.Test/BasicTypes.cs | 20 +- .../DafnyTestGeneration.Test/Collections.cs | 5 +- Source/DafnyTestGeneration.Test/Setup.cs | 7 +- Source/DafnyTestGeneration.Test/Various.cs | 42 +-- .../WriterFromOutputHelper.cs | 31 ++ Source/DafnyTestGeneration/DafnyInfo.cs | 39 +-- .../GenerateTestsCommand.cs | 2 +- Source/DafnyTestGeneration/Main.cs | 5 +- .../ProgramModification.cs | 14 +- Source/DafnyTestGeneration/Utils.cs | 2 +- Source/IntegrationTests/LitTests.cs | 82 ++++-- .../{TestDafny.cs => MultiBackendTest.cs} | 160 +++++----- Source/TestDafny/TestDafny.csproj | 20 +- Source/XUnitExtensions/Lit/DiffCommand.cs | 3 +- Source/XUnitExtensions/Lit/ExitCommand.cs | 5 +- Source/XUnitExtensions/Lit/ILitCommand.cs | 21 +- .../Lit/LitCommandWithRedirection.cs | 27 +- Source/XUnitExtensions/Lit/LitTestCase.cs | 12 +- .../Lit/MainMethodLitCommand.cs | 9 +- Source/XUnitExtensions/Lit/NotCommand.cs | 5 +- Source/XUnitExtensions/Lit/OrCommand.cs | 7 +- .../XUnitExtensions/Lit/OutputCheckCommand.cs | 4 +- Source/XUnitExtensions/Lit/SedCommand.cs | 3 +- Source/XUnitExtensions/Lit/ShellLitCommand.cs | 3 +- Source/XUnitExtensions/Lit/StdInCommand.cs | 5 +- .../XUnitExtensions/Lit/UnsupportedCommand.cs | 3 +- Source/XUnitExtensions/Lit/XFailCommand.cs | 3 +- Test/comp/Iterators.dfy | 2 + Test/comp/UnicodeStrings.dfy | 2 +- Test/comp/Uninitialized.dfy | 4 + Test/comp/compile3/JustRun.dfy.expect | 1 + Test/dafny0/Strings.dfy | 11 +- Test/git-issues/git-issue-1553.dfy | 3 +- Test/git-issues/git-issue-374.dfy | 4 +- Test/git-issues/git-issue-3883.dfy | 6 +- Test/git-issues/git-issue-610.dfy | 2 +- Test/git-issues/git-issue-674.dfy | 2 +- Test/git-issues/git-issue-684.dfy | 4 +- Test/git-issues/git-issue-784.dfy | 4 +- Test/git-issues/git-issue-817.dfy | 3 + Test/git-issues/git-issue-817a.dfy | 1 + Test/git-issues/git-issue-859.dfy | 4 +- Test/libraries | 2 +- ...stentCompilerBehavior.dfy.testdafny.expect | 5 +- Test/unicodechars/comp/Arrays.dfy | 2 +- .../git-issues/github-issue-2928.dfy | 2 +- customBoogie.patch | 2 +- 173 files changed, 1765 insertions(+), 945 deletions(-) create mode 100644 Source/DafnyCore/DafnyFile.cs create mode 100644 Source/DafnyCore/UndisposableTextWriter.cs delete mode 100644 Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs create mode 100644 Source/DafnyPipeline.Test/WriterFromOutputHelper.cs create mode 100644 Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs rename Source/TestDafny/{TestDafny.cs => MultiBackendTest.cs} (59%) diff --git a/.github/workflows/check-deep-tests-reusable.yml b/.github/workflows/check-deep-tests-reusable.yml index 41770e4c400..c2c6e23dcd2 100644 --- a/.github/workflows/check-deep-tests-reusable.yml +++ b/.github/workflows/check-deep-tests-reusable.yml @@ -16,7 +16,7 @@ jobs: uses: actions/checkout@v3 with: path: dafny - submodules: true + submodules: recursive - uses: actions/github-script@v6 if: github.repository_owner == 'dafny-lang' with: diff --git a/.github/workflows/deep-tests.yml b/.github/workflows/deep-tests.yml index abe08ca34c1..16228a31723 100644 --- a/.github/workflows/deep-tests.yml +++ b/.github/workflows/deep-tests.yml @@ -32,6 +32,7 @@ jobs: uses: actions/checkout@v3 with: ref: ${{ inputs.sha }} + submodules: recursive - name: Get short sha run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 434fd3a76b7..759fdde00b4 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -98,7 +98,7 @@ jobs: uses: actions/checkout@v3 with: path: dafny - submodules: false # Until the libraries work again + submodules: true # Until the libraries work again # - name: Clean up libraries for testing # run: | # rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index 91e8d18540b..2bbbd0b8b19 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -32,6 +32,7 @@ jobs: uses: actions/checkout@v3 with: path: dafny + submodules: recursive - name: Restore tools working-directory: dafny run: dotnet tool restore @@ -86,6 +87,7 @@ jobs: uses: actions/checkout@v3 with: path: dafny + submodules: recursive - name: Setup dotnet uses: actions/setup-dotnet@v3 diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml index 9f8a15f8d3b..ad927af4867 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -24,6 +24,8 @@ jobs: steps: - name: Checkout Dafny uses: actions/checkout@v3 + with: + submodules: true - name: Set up JDK 18 uses: actions/setup-java@v3 with: diff --git a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs index ed0580e97fe..f71835f6ce2 100644 --- a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs +++ b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs @@ -26,7 +26,7 @@ public override Expression CloneExpr(Expression expr) { var e = (FunctionCallExpr)expr; #if DEBUG_PRINT if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) { - Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e)); + Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e)); } #endif // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix. @@ -37,7 +37,7 @@ public override Expression CloneExpr(Expression expr) { if (f != null && focalPredicates.Contains(f)) { #if DEBUG_PRINT var r = CloneCallAndAddK(e); - Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r)); + Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r)); return r; #else return CloneCallAndAddK(e); @@ -58,14 +58,14 @@ public override Expression CloneExpr(Expression expr) { if (fce != null) { #if DEBUG_PRINT if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) { - Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce)); + Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce)); } #endif var f = fce.Function as ExtremePredicate; if (f != null && focalPredicates.Contains(f)) { #if DEBUG_PRINT var r = CloneCallAndAddK(fce); - Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r)); + Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r)); return r; #else return CloneCallAndAddK(fce); diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index d120d38f90e..98f84801b44 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -194,6 +194,10 @@ public static string ToStringWithoutNewline(System.IO.StringWriter wr) { return sb.ToString(0, len); } + public void PrintProgramLargeStack(Program prog, bool afterResolver) { + DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait(); + } + public void PrintProgram(Program prog, bool afterResolver) { Contract.Requires(prog != null); this.afterResolver = afterResolver; diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 158f336d9fc..6dd24bd0600 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1285,7 +1285,7 @@ public static Type Join(Type a, Type b, BuiltIns builtIns) { Contract.Requires(builtIns != null); var j = JoinX(a, b, builtIns); if (builtIns.Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j); + builtIns.Options.OutputWriter.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j); } return j; } @@ -1506,7 +1506,7 @@ public static Type Meet(Type a, Type b, BuiltIns builtIns) { } } if (builtIns.Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j); + builtIns.Options.OutputWriter.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j); } return j; } diff --git a/Source/DafnyCore/Auditor/Auditor.cs b/Source/DafnyCore/Auditor/Auditor.cs index 020885ee5df..e67a2aa469e 100644 --- a/Source/DafnyCore/Auditor/Auditor.cs +++ b/Source/DafnyCore/Auditor/Auditor.cs @@ -137,7 +137,7 @@ internal override void PostResolve(Program program) { _ => $"Internal error: unknown format {reportFormat}" }; if (reportFileName is null) { - Console.Write(text); + Options.OutputWriter.Write(text); } else { if (compareReport) { try { diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 9bcda7fd364..3ae104e763b 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -110,7 +110,7 @@ void EmitDafnySourceAttribute(Program program, ConcreteSyntaxTree wr) { stringWriter.NewLine = Environment.NewLine; var oldValue = Options.ShowEnv; Options.ShowEnv = ExecutionEngineOptions.ShowEnvironment.DuringPrint; - new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgram(program, true); + new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgramLargeStack(program, true); Options.ShowEnv = oldValue; var programString = stringWriter.GetStringBuilder().Replace("\"", "\"\"").ToString(); diff --git a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs index 893ca63fed6..b6cc80d8792 100644 --- a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs @@ -5,6 +5,7 @@ using System.Linq; using System.Reflection; using System.Runtime.Loader; +using System.Text; using System.Text.Json; using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; @@ -44,7 +45,6 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location), MetadataReference.CreateFromFile(Assembly.Load("mscorlib").Location)); - var inMemory = runAfterCompile; compilation = compilation.WithOptions(compilation.Options.WithOutputKind(callToMain != null ? OutputKind.ConsoleApplication : OutputKind.DynamicallyLinkedLibrary)); var tempCompilationResult = new CSharpCompilationResult(); @@ -93,54 +93,40 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target var outputDir = targetFilename == null ? Directory.GetCurrentDirectory() : Path.GetDirectoryName(Path.GetFullPath(targetFilename)); var outputPath = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".dll"); var outputJson = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".runtimeconfig.json"); - if (inMemory) { - using var stream = new MemoryStream(); - var emitResult = compilation.Emit(stream); - if (emitResult.Success) { - tempCompilationResult.CompiledAssembly = Assembly.Load(stream.GetBuffer()); - } else { - outputWriter.WriteLine("Errors compiling program:"); - var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); - foreach (var ce in errors) { - outputWriter.WriteLine(ce.ToString()); - outputWriter.WriteLine(); - } - return false; + var emitResult = compilation.Emit(outputPath); + + if (emitResult.Success) { + tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath); + if (Options.CompileVerbose) { + outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName); } - } else { - var emitResult = compilation.Emit(outputPath); - if (emitResult.Success) { - tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath); - if (Options.CompileVerbose) { - outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName); - } - try { - var configuration = JsonSerializer.Serialize( - new { - runtimeOptions = new { - tfm = "net6.0", - framework = new { - name = "Microsoft.NETCore.App", - version = "6.0.0", - rollForward = "LatestMinor" - } + try { + var configuration = JsonSerializer.Serialize( + new { + runtimeOptions = new { + tfm = "net6.0", + framework = new { + name = "Microsoft.NETCore.App", + version = "6.0.0", + rollForward = "LatestMinor" } - }, new JsonSerializerOptions() { WriteIndented = true }); - File.WriteAllText(outputJson, configuration + Environment.NewLine); - } catch (Exception e) { - outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}"); - return false; - } - } else { - outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName); - var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); - foreach (var ce in errors) { - outputWriter.WriteLine(ce.ToString()); - outputWriter.WriteLine(); - } + } + }, new JsonSerializerOptions() { WriteIndented = true }); + File.WriteAllText(outputJson, configuration + Environment.NewLine); + } catch (Exception e) { + outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}"); return false; } + } else { + outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName); + var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); + foreach (var ce in errors) { + outputWriter.WriteLine(ce.ToString()); + outputWriter.WriteLine(); + } + + return false; } compilationResult = tempCompilationResult; @@ -151,37 +137,24 @@ private class CSharpCompilationResult { public Assembly CompiledAssembly; } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, + string targetFilename /*?*/, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { var crx = (CSharpCompilationResult)compilationResult; foreach (var otherFileName in otherFileNames) { if (Path.GetExtension(otherFileName) == ".dll") { - AssemblyLoadContext.Default.LoadFromAssemblyPath(Path.GetFullPath(otherFileName)); + var targetDirectory = Path.GetDirectoryName(crx.CompiledAssembly.Location); + File.Copy(otherFileName, Path.Combine(targetDirectory!, Path.GetFileName(otherFileName)), true); } } if (crx.CompiledAssembly == null) { throw new Exception("Cannot call run target program on a compilation that failed"); } - var entry = crx.CompiledAssembly.EntryPoint; - if (entry == null) { - throw new Exception("Cannot call run target on a compilation whose assembly has no entry."); - } - try { - Console.OutputEncoding = System.Text.Encoding.UTF8; // Force UTF-8 output in dafny run (#2999) - object[] parameters = entry.GetParameters().Length == 0 ? new object[] { } : new object[] { Options.MainArgs.ToArray() }; - entry.Invoke(null, parameters); - return true; - } catch (System.Reflection.TargetInvocationException e) { - outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message); - outputWriter.WriteLine(e.InnerException.ToString()); - } catch (System.Exception e) { - outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message); - outputWriter.WriteLine(e.ToString()); - } - return false; + var psi = PrepareProcessStartInfo("dotnet", new[] { crx.CompiledAssembly.Location }.Concat(Options.MainArgs)); + return RunProcess(psi, outputWriter, errorWriter) == 0; } public CsharpBackend(DafnyOptions options) : base(options) { diff --git a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs index 0bf23bacfb8..0167bae5816 100644 --- a/Source/DafnyCore/Compilers/CoverageInstrumenter.cs +++ b/Source/DafnyCore/Compilers/CoverageInstrumenter.cs @@ -72,7 +72,7 @@ public void WriteLegendFile() { if (legend != null) { var filename = compiler.Options.CoverageLegendFile; Contract.Assert(filename != null); - TextWriter wr = filename == "-" ? System.Console.Out : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create)); + TextWriter wr = filename == "-" ? compiler.Options.OutputWriter : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create)); { for (var i = 0; i < legend.Count; i++) { var e = legend[i]; @@ -82,4 +82,4 @@ public void WriteLegendFile() { legend = null; } } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index 4de1c249fea..f173a3772fe 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -905,7 +905,7 @@ protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) { } protected void Warn(string msg, IToken tok) { - Console.Error.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg); + Options.ErrorWriter.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg); } // Because we use reference counting (via shared_ptr), the TypeName of a class differs diff --git a/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs b/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs index f997667ab07..9a552d15c6b 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs @@ -19,7 +19,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target bool runAfterCompile, TextWriter outputWriter, out object compilationResult) { var assemblyLocation = System.Reflection.Assembly.GetExecutingAssembly().Location; Contract.Assert(assemblyLocation != null); - var codebase = System.IO.Path.GetDirectoryName(assemblyLocation); + var codebase = Path.GetDirectoryName(assemblyLocation); Contract.Assert(codebase != null); compilationResult = null; var psi = PrepareProcessStartInfo("g++", new List { @@ -37,13 +37,14 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target "-o", ComputeExeName(targetFilename), targetFilename }); - return 0 == RunProcess(psi, outputWriter, "Error while compiling C++ files."); + return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling C++ files."); } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, + string targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { var psi = PrepareProcessStartInfo(ComputeExeName(targetFilename), Options.MainArgs); - return 0 == RunProcess(psi, outputWriter); + return 0 == RunProcess(psi, outputWriter, errorWriter); } public override IReadOnlySet SupportedExtensions => new HashSet { ".h" }; diff --git a/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs b/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs index dce809d58c2..422e17ffa85 100644 --- a/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs +++ b/Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs @@ -41,13 +41,14 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target * The Dafny backend is different from the other backends in that the output code needs to be compiled * by the Dafny compiler itself to another backend for execution. */ - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain, - string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, /*?*/ + string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, + TextWriter errorWriter) { Contract.Requires(targetFilename != null || otherFileNames.Count == 0); - return RunTargetDafnyProgram(targetFilename, outputWriter, false); + return RunTargetDafnyProgram(targetFilename, outputWriter, errorWriter, false); } public DafnyBackend(DafnyOptions options) : base(options) { } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs index 3197893b565..1c5e4ebff8f 100644 --- a/Source/DafnyCore/Compilers/ExecutableBackend.cs +++ b/Source/DafnyCore/Compilers/ExecutableBackend.cs @@ -5,6 +5,9 @@ using System.Diagnostics.Contracts; using System.IO; using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Win32; namespace Microsoft.Dafny.Compilers; @@ -51,6 +54,7 @@ public ProcessStartInfo PrepareProcessStartInfo(string programName, IEnumerable< var psi = new ProcessStartInfo(programName) { UseShellExecute = false, CreateNoWindow = false, // https://github.com/dotnet/runtime/issues/68259 + RedirectStandardOutput = true, }; foreach (var arg in args ?? Enumerable.Empty()) { psi.ArgumentList.Add(arg); @@ -58,23 +62,44 @@ public ProcessStartInfo PrepareProcessStartInfo(string programName, IEnumerable< return psi; } - public int RunProcess(ProcessStartInfo psi, TextWriter outputWriter, string errorMessage = null) { + public int RunProcess(ProcessStartInfo psi, + TextWriter outputWriter, + TextWriter errorWriter, + string errorMessage = null) { return StartProcess(psi, outputWriter) is { } process ? - WaitForExit(process, outputWriter, errorMessage) : -1; + WaitForExit(process, outputWriter, errorWriter, errorMessage) : -1; } - public int WaitForExit(Process process, TextWriter outputWriter, string errorMessage = null) { + public int WaitForExit(Process process, TextWriter outputWriter, TextWriter errorWriter, string errorMessage = null) { + + var errorProcessing = Task.Run(() => { + PassthroughBuffer(process.StandardError, errorWriter); + }); + PassthroughBuffer(process.StandardOutput, outputWriter); process.WaitForExit(); if (process.ExitCode != 0 && errorMessage != null) { outputWriter.WriteLine("{0} Process exited with exit code {1}", errorMessage, process.ExitCode); } + + errorProcessing.Wait(); return process.ExitCode; } + + // We read character by character because we did not find a way to ensure + // final newlines are kept when reading line by line + protected static void PassthroughBuffer(TextReader input, TextWriter output) { + int current; + while ((current = input.Read()) != -1) { + output.Write((char)current); + } + } + public Process StartProcess(ProcessStartInfo psi, TextWriter outputWriter) { string additionalInfo = ""; try { + psi.RedirectStandardError = true; if (Process.Start(psi) is { } process) { return process; } @@ -101,8 +126,9 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target return true; } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, + string targetFilename /*?*/, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { Contract.Requires(dafnyProgramName != null); Contract.Requires(targetProgramText != null); Contract.Requires(otherFileNames != null); @@ -116,7 +142,7 @@ protected static void WriteFromFile(string inputFilename, TextWriter outputWrite SinglePassCompiler.WriteFromStream(rd, outputWriter); } - protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter, bool verify) { + protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWriter, TextWriter errorWriter, bool verify) { /* * In order to work for the continuous integration, we need to call the Dafny compiler using dotnet @@ -124,7 +150,7 @@ protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWri */ var where = System.Reflection.Assembly.GetExecutingAssembly().Location; - where = System.IO.Path.GetDirectoryName(where); + where = Path.GetDirectoryName(where); var dafny = where + "/Dafny.dll"; var opt = Options; @@ -151,16 +177,24 @@ protected bool RunTargetDafnyProgram(string targetFilename, TextWriter outputWri var process = new Process(); process.StartInfo = psi; var outputBuilder = new List(); + var errorBuilder = new List(); process.OutputDataReceived += (sender, args) => outputBuilder.Add(args.Data); + process.ErrorDataReceived += (sender, args) => errorBuilder.Add(args.Data); try { process.Start(); process.BeginOutputReadLine(); + process.BeginErrorReadLine(); process.WaitForExit(); process.CancelOutputRead(); + process.CancelErrorRead(); for (int i = 2; i < outputBuilder.Count - 1; i++) { - Console.WriteLine(outputBuilder[i]); + outputWriter.WriteLine(outputBuilder[i]); + } + + for (int i = 0; i < errorBuilder.Count - 1; i++) { + errorWriter.WriteLine(errorBuilder[i]); } if (process.ExitCode != 0) { diff --git a/Source/DafnyCore/Compilers/GoLang/GoBackend.cs b/Source/DafnyCore/Compilers/GoLang/GoBackend.cs index da53450d233..59746150c2e 100644 --- a/Source/DafnyCore/Compilers/GoLang/GoBackend.cs +++ b/Source/DafnyCore/Compilers/GoLang/GoBackend.cs @@ -22,7 +22,8 @@ protected override SinglePassCompiler CreateCompiler() { return new GoCompiler(Options, Reporter); } - public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, + public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, + string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, bool runAfterCompile, TextWriter outputWriter, out object compilationResult) { compilationResult = null; if (runAfterCompile) { @@ -33,18 +34,21 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target return true; } else { // compile now - return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, outputWriter, callToMain != null, run: false); + return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, + outputWriter, outputWriter, callToMain != null, run: false); } } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, + string targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { - return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, outputWriter, hasMain: true, run: true); + return SendToNewGoProcess(dafnyProgramName, targetFilename, otherFileNames, outputWriter, errorWriter, hasMain: true, run: true); } - private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, ReadOnlyCollection otherFileNames, - TextWriter outputWriter, bool hasMain, bool run) { + private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, + ReadOnlyCollection otherFileNames, + TextWriter outputWriter, TextWriter errorWriter, bool hasMain, bool run) { Contract.Requires(targetFilename != null); foreach (var otherFileName in otherFileNames) { @@ -110,7 +114,7 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, // system. Until Dafny's Go compiler catches up, the GO111MODULE variable has to be set. psi.EnvironmentVariables["GO111MODULE"] = "auto"; - return 0 == RunProcess(psi, outputWriter); + return 0 == RunProcess(psi, outputWriter, errorWriter); } static string GoPath(string filename) { diff --git a/Source/DafnyCore/Compilers/Java/JavaBackend.cs b/Source/DafnyCore/Compilers/Java/JavaBackend.cs index 6c7cc5f23ab..8361e906257 100644 --- a/Source/DafnyCore/Compilers/Java/JavaBackend.cs +++ b/Source/DafnyCore/Compilers/Java/JavaBackend.cs @@ -74,7 +74,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target var compileProcess = PrepareProcessStartInfo("javac", new List { "-encoding", "UTF8" }.Concat(files)); compileProcess.WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename)); compileProcess.EnvironmentVariables["CLASSPATH"] = GetClassPath(targetFilename); - if (0 != RunProcess(compileProcess, outputWriter, "Error while compiling Java files.")) { + if (0 != RunProcess(compileProcess, outputWriter, outputWriter, "Error while compiling Java files.")) { return false; } @@ -112,24 +112,26 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target public bool CreateJar(string/*?*/ entryPointName, string jarPath, string rootDirectory, List files, TextWriter outputWriter) { - System.IO.Directory.CreateDirectory(Path.GetDirectoryName(jarPath)); + Directory.CreateDirectory(Path.GetDirectoryName(jarPath)); var args = entryPointName == null ? // If null, then no entry point is added new List { "cf", jarPath } : new List { "cfe", jarPath, entryPointName }; var jarCreationProcess = PrepareProcessStartInfo("jar", args.Concat(files)); jarCreationProcess.WorkingDirectory = rootDirectory; - return 0 == RunProcess(jarCreationProcess, outputWriter, "Error while creating jar file: " + jarPath); + return 0 == RunProcess(jarCreationProcess, outputWriter, outputWriter, "Error while creating jar file: " + jarPath); } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string /*?*/ targetFilename, - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, + string targetFilename, /*?*/ + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, + TextWriter errorWriter) { string jarPath = Path.ChangeExtension(dafnyProgramName, ".jar"); // Must match that in CompileTargetProgram var psi = PrepareProcessStartInfo("java", new List { "-Dfile.encoding=UTF-8", "-jar", jarPath } .Concat(Options.MainArgs)); // Run the target program in the user's working directory and with the user's classpath psi.EnvironmentVariables["CLASSPATH"] = GetClassPath(null); - return 0 == RunProcess(psi, outputWriter); + return 0 == RunProcess(psi, outputWriter, errorWriter); } private string GetClassPath(string targetFilename) { diff --git a/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs b/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs index 90d5f4a2d8b..13130440a40 100644 --- a/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs +++ b/Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs @@ -41,8 +41,9 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target } } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, - object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/, + string targetFilename, ReadOnlyCollection otherFileNames, + object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { return SendToNewNodeProcess(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, outputWriter); } @@ -73,9 +74,9 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str nodeProcess.StandardInput.Close(); // Fixes a problem of Node on Windows, where Node does not prints to the parent console its standard outputs. var errorProcessing = Task.Run(() => { - PassthroughBuffer(nodeProcess.StandardError, Console.Error); + PassthroughBuffer(nodeProcess.StandardError, Options.ErrorWriter); }); - PassthroughBuffer(nodeProcess.StandardOutput, Console.Out); + PassthroughBuffer(nodeProcess.StandardOutput, Options.OutputWriter); nodeProcess.WaitForExit(); #pragma warning disable VSTHRD002 errorProcessing.Wait(); @@ -87,15 +88,6 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str } } - // We read character by character because we did not find a way to ensure - // final newlines are kept when reading line by line - private static void PassthroughBuffer(TextReader input, TextWriter output) { - int current; - while ((current = input.Read()) != -1) { - output.Write((char)current); - } - } - public JavaScriptBackend(DafnyOptions options) : base(options) { } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs index 344cdc3456c..a8e760e3496 100644 --- a/Source/DafnyCore/Compilers/Library/LibraryBackend.cs +++ b/Source/DafnyCore/Compilers/Library/LibraryBackend.cs @@ -80,9 +80,8 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target } public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string targetFilename, - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { - + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { var dooPath = DooFilePath(dafnyProgramName); - return RunTargetDafnyProgram(dooPath, outputWriter, true); + return RunTargetDafnyProgram(dooPath, outputWriter, errorWriter, true); } } \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/Python/PythonBackend.cs b/Source/DafnyCore/Compilers/Python/PythonBackend.cs index 88d36545999..ac224c8d1cb 100644 --- a/Source/DafnyCore/Compilers/Python/PythonBackend.cs +++ b/Source/DafnyCore/Compilers/Python/PythonBackend.cs @@ -63,6 +63,14 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW return true; } + public override void CleanSourceDirectory(string sourceDirectory) { + var cacheDirectory = Path.Combine(sourceDirectory, "__pycache__"); + try { + Directory.Delete(cacheDirectory, true); + } catch (DirectoryNotFoundException) { + } + } + public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain, string /*?*/ targetFilename, ReadOnlyCollection otherFileNames, bool runAfterCompile, TextWriter outputWriter, out object compilationResult) { @@ -79,12 +87,13 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target return true; } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain, - string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, /*?*/ + string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, + TextWriter errorWriter) { Contract.Requires(targetFilename != null || otherFileNames.Count == 0); var psi = PrepareProcessStartInfo("python3", Options.MainArgs.Prepend(targetFilename)); psi.EnvironmentVariables["PYTHONIOENCODING"] = "utf8"; - return 0 == RunProcess(psi, outputWriter); + return 0 == RunProcess(psi, outputWriter, errorWriter); } public PythonBackend(DafnyOptions options) : base(options) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 9e0804dc723..83366cc694a 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -141,12 +141,12 @@ bool IsAssumeTypeKeyword(IToken la) { /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (bool useStdin, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) /* throws System.IO.IOException */ { +public static int Parse (TextReader fileReaderOverride, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) /* throws System.IO.IOException */ { Contract.Requires(uri != null); Contract.Requires(module != null); string s; - if (useStdin) { - s = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(System.Console.In, new List(), Environment.NewLine); + if (fileReaderOverride != null) { + s = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(fileReaderOverride, new List(), Environment.NewLine); return Parse(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); } else { var newline = SourcePreprocessor.GetNewlineStyle(uri.LocalPath); diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index cb9e429cba9..8416cc6ddfd 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -22,6 +22,17 @@ public class DafnyConsolePrinter : ConsolePrinter { private DafnyOptions options; public ConcurrentBag<(Implementation, VerificationResult)> VerificationResults { get; } = new(); + public override void AdvisoryWriteLine(TextWriter output, string format, params object[] args) { + if (output == Console.Out) { + int foregroundColor = (int)Console.ForegroundColor; + Console.ForegroundColor = ConsoleColor.Yellow; + output.WriteLine(format, args); + Console.ForegroundColor = (ConsoleColor)foregroundColor; + } else { + output.WriteLine(format, args); + } + } + private string GetFileLine(string filename, int lineIndex) { List lines = fsCache.GetOrAdd(filename, key => { try { diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 4a8b2f89b56..2143621793f 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -31,7 +31,7 @@ - + diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs new file mode 100644 index 00000000000..cc44e667409 --- /dev/null +++ b/Source/DafnyCore/DafnyFile.cs @@ -0,0 +1,178 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Reflection.Metadata; +using System.Reflection.PortableExecutable; +using DafnyCore; + +namespace Microsoft.Dafny; + +public class DafnyFile { + public bool UseStdin { get; private set; } + public string FilePath => Uri.LocalPath; + public string CanonicalPath { get; private set; } + public string BaseName { get; private set; } + public bool IsPreverified { get; set; } + public bool IsPrecompiled { get; set; } + public string SourceFilePath { get; private set; } + public Uri Uri { get; private set; } + + // Returns a canonical string for the given file path, namely one which is the same + // for all paths to a given file and different otherwise. The best we can do is to + // make the path absolute -- detecting case and canonicalizing symbolic and hard + // links are difficult across file systems (which may mount parts of other filesystems, + // with different characteristics) and is not supported by .Net libraries + public static Uri Canonicalize(string filePath) { + if (filePath == null || !filePath.StartsWith("file:")) { + return new Uri(Path.GetFullPath(filePath)); + } + + if (Uri.IsWellFormedUriString(filePath, UriKind.RelativeOrAbsolute)) { + return new Uri(filePath); + } + + var potentialPrefixes = new List() { "file:\\", "file:/", "file:" }; + foreach (var potentialPrefix in potentialPrefixes) { + if (filePath.StartsWith(potentialPrefix)) { + var withoutPrefix = filePath.Substring(potentialPrefix.Length); + var tentativeURI = "file:///" + withoutPrefix.Replace("\\", "/"); + if (Uri.IsWellFormedUriString(tentativeURI, UriKind.RelativeOrAbsolute)) { + return new Uri(tentativeURI); + } + // Recovery mechanisms for the language server + return new Uri(filePath.Substring(potentialPrefix.Length)); + } + } + return new Uri(filePath.Substring("file:".Length)); + } + public static List FileNames(IList dafnyFiles) { + var sourceFiles = new List(); + foreach (DafnyFile f in dafnyFiles) { + sourceFiles.Add(f.FilePath); + } + return sourceFiles; + } + public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { + UseStdin = useStdin; + Uri = useStdin ? new Uri("stdin:///") : new Uri(filePath); + BaseName = useStdin ? "" : Path.GetFileName(filePath); + + var extension = useStdin ? ".dfy" : Path.GetExtension(filePath); + if (extension != null) { extension = extension.ToLower(); } + + // Normalizing symbolic links appears to be not + // supported in .Net APIs, because it is very difficult in general + // So we will just use the absolute path, lowercased for all file systems. + // cf. IncludeComparer.CompareTo + CanonicalPath = !useStdin ? Canonicalize(filePath).LocalPath : ""; + filePath = CanonicalPath; + + if (extension == ".dfy" || extension == ".dfyi") { + IsPreverified = false; + IsPrecompiled = false; + SourceFilePath = filePath; + } else if (extension == ".doo") { + IsPreverified = true; + IsPrecompiled = false; + + var dooFile = DooFile.Read(filePath); + + var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath; + if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) { + throw new IllegalDafnyFile(true); + } + + // For now it's simpler to let the rest of the pipeline parse the + // program text back into the AST representation. + // At some point we'll likely want to serialize a program + // more efficiently inside a .doo file, at which point + // the DooFile class should encapsulate the serialization logic better + // and expose a Program instead of the program text. + SourceFilePath = Path.GetTempFileName(); + Uri = new Uri(SourceFilePath); + File.WriteAllText(SourceFilePath, dooFile.ProgramText); + + } else if (extension == ".dll") { + IsPreverified = true; + // Technically only for C#, this is for backwards compatability + IsPrecompiled = true; + + var sourceText = GetDafnySourceAttributeText(filePath); + if (sourceText == null) { throw new IllegalDafnyFile(); } + SourceFilePath = Path.GetTempFileName(); + Uri = new Uri(SourceFilePath); + File.WriteAllText(SourceFilePath, sourceText); + + } else { + throw new IllegalDafnyFile(); + } + } + + private static string GetDafnySourceAttributeText(string dllPath) { + if (!File.Exists(dllPath)) { + throw new IllegalDafnyFile(); + } + using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite); + using var dllPeReader = new PEReader(dllFs); + var dllMetadataReader = dllPeReader.GetMetadataReader(); + + foreach (var attrHandle in dllMetadataReader.CustomAttributes) { + var attr = dllMetadataReader.GetCustomAttribute(attrHandle); + try { + /* The cast from EntityHandle to MemberReferenceHandle is overriden, uses private members, and throws + * an InvalidCastException if it fails. We have no other option than to use it and catch the exception. + */ + var constructor = dllMetadataReader.GetMemberReference((MemberReferenceHandle)attr.Constructor); + var attrType = dllMetadataReader.GetTypeReference((TypeReferenceHandle)constructor.Parent); + if (dllMetadataReader.GetString(attrType.Name) == "DafnySourceAttribute") { + var decoded = attr.DecodeValue(new StringOnlyCustomAttributeTypeProvider()); + return (string)decoded.FixedArguments[0].Value; + } + } catch (InvalidCastException) { + // Ignore - the Handle casts are handled as custom explicit operators, + // and there's no way I can see to test if the cases will succeed ahead of time. + } + } + + return null; + } + + // Dummy implementation of ICustomAttributeTypeProvider, providing just enough + // functionality to successfully decode a DafnySourceAttribute value. + private class StringOnlyCustomAttributeTypeProvider : ICustomAttributeTypeProvider { + public System.Type GetPrimitiveType(PrimitiveTypeCode typeCode) { + if (typeCode == PrimitiveTypeCode.String) { + return typeof(string); + } + throw new NotImplementedException(); + } + + public System.Type GetTypeFromDefinition(MetadataReader reader, TypeDefinitionHandle handle, byte rawTypeKind) { + throw new NotImplementedException(); + } + + public System.Type GetTypeFromReference(MetadataReader reader, TypeReferenceHandle handle, byte rawTypeKind) { + throw new NotImplementedException(); + } + + public System.Type GetSZArrayType(System.Type elementType) { + throw new NotImplementedException(); + } + + public System.Type GetSystemType() { + throw new NotImplementedException(); + } + + public System.Type GetTypeFromSerializedName(string name) { + throw new NotImplementedException(); + } + + public PrimitiveTypeCode GetUnderlyingEnumType(System.Type type) { + throw new NotImplementedException(); + } + + public bool IsSystemType(System.Type type) { + throw new NotImplementedException(); + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 4c268bf590d..3f0f5f98a16 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -10,8 +10,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using System.Reflection.Metadata; -using System.Reflection.PortableExecutable; +using System.Threading; using System.Threading.Tasks; using DafnyCore; using Microsoft.Boogie; @@ -26,195 +25,26 @@ public IllegalDafnyFile(bool processingError = false) { } } - public class DafnyFile { - public bool UseStdin { get; private set; } - public string FilePath => Uri.LocalPath; - public string CanonicalPath { get; private set; } - public string BaseName { get; private set; } - public bool IsPreverified { get; set; } - public bool IsPrecompiled { get; set; } - public string SourceFilePath { get; private set; } - public Uri Uri { get; private set; } - - // Returns a canonical string for the given file path, namely one which is the same - // for all paths to a given file and different otherwise. The best we can do is to - // make the path absolute -- detecting case and canonicalizing symbolic and hard - // links are difficult across file systems (which may mount parts of other filesystems, - // with different characteristics) and is not supported by .Net libraries - public static Uri Canonicalize(string filePath) { - if (filePath == null || !filePath.StartsWith("file:")) { - return new Uri(Path.GetFullPath(filePath)); - } - - if (Uri.IsWellFormedUriString(filePath, UriKind.RelativeOrAbsolute)) { - return new Uri(filePath); - } - - var potentialPrefixes = new List() { "file:\\", "file:/", "file:" }; - foreach (var potentialPrefix in potentialPrefixes) { - if (filePath.StartsWith(potentialPrefix)) { - var withoutPrefix = filePath.Substring(potentialPrefix.Length); - var tentativeURI = "file:///" + withoutPrefix.Replace("\\", "/"); - if (Uri.IsWellFormedUriString(tentativeURI, UriKind.RelativeOrAbsolute)) { - return new Uri(tentativeURI); - } - // Recovery mechanisms for the language server - return new Uri(filePath.Substring(potentialPrefix.Length)); - } - } - return new Uri(filePath.Substring("file:".Length)); - } - public static List FileNames(IList dafnyFiles) { - var sourceFiles = new List(); - foreach (DafnyFile f in dafnyFiles) { - sourceFiles.Add(f.FilePath); - } - return sourceFiles; - } - public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { - UseStdin = useStdin; - Uri = useStdin ? new Uri("stdin:///") : new Uri(filePath); - BaseName = useStdin ? "" : Path.GetFileName(filePath); - - var extension = useStdin ? ".dfy" : Path.GetExtension(filePath); - if (extension != null) { extension = extension.ToLower(); } - - // Normalizing symbolic links appears to be not - // supported in .Net APIs, because it is very difficult in general - // So we will just use the absolute path, lowercased for all file systems. - // cf. IncludeComparer.CompareTo - CanonicalPath = !useStdin ? Canonicalize(filePath).LocalPath : ""; - filePath = CanonicalPath; - - if (extension == ".dfy" || extension == ".dfyi") { - IsPreverified = false; - IsPrecompiled = false; - SourceFilePath = filePath; - } else if (extension == ".doo") { - IsPreverified = true; - IsPrecompiled = false; - - var dooFile = DooFile.Read(filePath); - - var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath; - if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) { - throw new IllegalDafnyFile(true); - } - - // For now it's simpler to let the rest of the pipeline parse the - // program text back into the AST representation. - // At some point we'll likely want to serialize a program - // more efficiently inside a .doo file, at which point - // the DooFile class should encapsulate the serialization logic better - // and expose a Program instead of the program text. - SourceFilePath = Path.GetTempFileName(); - Uri = new Uri(SourceFilePath); - File.WriteAllText(SourceFilePath, dooFile.ProgramText); - - } else if (extension == ".dll") { - IsPreverified = true; - // Technically only for C#, this is for backwards compatability - IsPrecompiled = true; - - var sourceText = GetDafnySourceAttributeText(filePath); - if (sourceText == null) { throw new IllegalDafnyFile(); } - SourceFilePath = Path.GetTempFileName(); - Uri = new Uri(SourceFilePath); - File.WriteAllText(SourceFilePath, sourceText); - - } else { - throw new IllegalDafnyFile(); - } - } - - private static string GetDafnySourceAttributeText(string dllPath) { - if (!File.Exists(dllPath)) { - throw new IllegalDafnyFile(); - } - using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite); - using var dllPeReader = new PEReader(dllFs); - var dllMetadataReader = dllPeReader.GetMetadataReader(); - - foreach (var attrHandle in dllMetadataReader.CustomAttributes) { - var attr = dllMetadataReader.GetCustomAttribute(attrHandle); - try { - /* The cast from EntityHandle to MemberReferenceHandle is overriden, uses private members, and throws - * an InvalidCastException if it fails. We have no other option than to use it and catch the exception. - */ - var constructor = dllMetadataReader.GetMemberReference((MemberReferenceHandle)attr.Constructor); - var attrType = dllMetadataReader.GetTypeReference((TypeReferenceHandle)constructor.Parent); - if (dllMetadataReader.GetString(attrType.Name) == "DafnySourceAttribute") { - var decoded = attr.DecodeValue(new StringOnlyCustomAttributeTypeProvider()); - return (string)decoded.FixedArguments[0].Value; - } - } catch (InvalidCastException) { - // Ignore - the Handle casts are handled as custom explicit operators, - // and there's no way I can see to test if the cases will succeed ahead of time. - } - } - - return null; - } - - // Dummy implementation of ICustomAttributeTypeProvider, providing just enough - // functionality to successfully decode a DafnySourceAttribute value. - private class StringOnlyCustomAttributeTypeProvider : ICustomAttributeTypeProvider { - public System.Type GetPrimitiveType(PrimitiveTypeCode typeCode) { - if (typeCode == PrimitiveTypeCode.String) { - return typeof(string); - } - throw new NotImplementedException(); - } - - public System.Type GetTypeFromDefinition(MetadataReader reader, TypeDefinitionHandle handle, byte rawTypeKind) { - throw new NotImplementedException(); - } - - public System.Type GetTypeFromReference(MetadataReader reader, TypeReferenceHandle handle, byte rawTypeKind) { - throw new NotImplementedException(); - } - - public System.Type GetSZArrayType(System.Type elementType) { - throw new NotImplementedException(); - } - - public System.Type GetSystemType() { - throw new NotImplementedException(); - } - - public System.Type GetTypeFromSerializedName(string name) { - throw new NotImplementedException(); - } - - public PrimitiveTypeCode GetUnderlyingEnumType(System.Type type) { - throw new NotImplementedException(); - } - - public bool IsSystemType(System.Type type) { - throw new NotImplementedException(); - } - } - } - - public class Main { + public class DafnyMain { public static void MaybePrintProgram(Program program, string filename, bool afterResolver) { if (filename == null) { return; } - var tw = filename == "-" ? Console.Out : new StreamWriter(filename); + var tw = filename == "-" ? program.Options.OutputWriter : new StreamWriter(filename); var pr = new Printer(tw, program.Options, program.Options.PrintMode); - pr.PrintProgram(program, afterResolver); + pr.PrintProgramLargeStack(program, afterResolver); } /// /// Returns null on success, or an error string otherwise. /// - public static string ParseCheck(IList/*!*/ files, string/*!*/ programName, DafnyOptions options, out Program program) + public static string ParseCheck(TextReader stdIn, IList /*!*/ files, string /*!*/ programName, + DafnyOptions options, out Program program) //modifies Bpl.options.XmlSink.*; { - string err = Parse(files, programName, options, out program); + string err = Parse(stdIn, files, programName, options, out program); if (err != null) { return err; } @@ -222,12 +52,14 @@ public static string ParseCheck(IList/*!*/ files, string/*!*/ pr return Resolve(program); } - public static string Parse(IList files, string programName, DafnyOptions options, out Program program) { + public static string Parse(TextReader stdIn, IList files, string programName, DafnyOptions options, + out Program program) { Contract.Requires(programName != null); Contract.Requires(files != null); program = null; - var defaultModuleDefinition = new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList()); + var defaultModuleDefinition = + new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList()); ErrorReporter reporter = options.DiagnosticsFormat switch { DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options, defaultModuleDefinition), DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options, defaultModuleDefinition), @@ -242,26 +74,32 @@ public static string Parse(IList files, string programName, DafnyOpti if (options.XmlSink is { IsOpen: true } && !dafnyFile.UseStdin) { options.XmlSink.WriteFileFragment(dafnyFile.FilePath); } + if (options.Trace) { - Console.WriteLine("Parsing " + dafnyFile.FilePath); + options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); } - var include = dafnyFile.IsPrecompiled ? new Include(new Token() { - Uri = dafnyFile.Uri, - col = 1, - line = 0 - }, null, dafnyFile.SourceFilePath, false) : null; + var include = dafnyFile.IsPrecompiled + ? new Include(new Token() { + Uri = dafnyFile.Uri, + col = 1, + line = 0 + }, null, dafnyFile.SourceFilePath, false) + : null; if (include != null) { module.ModuleDef.Includes.Add(include); } - var err = ParseFile(dafnyFile, include, module, builtIns, new Errors(reporter), !dafnyFile.IsPreverified, !dafnyFile.IsPrecompiled); + + var err = ParseFile(stdIn, dafnyFile, include, module, builtIns, new Errors(reporter), !dafnyFile.IsPreverified, + !dafnyFile.IsPrecompiled); if (err != null) { return err; } } if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { - string errString = ParseIncludesDepthFirstNotCompiledFirst(module, builtIns, files.Select(f => f.SourceFilePath).ToHashSet(), new Errors(reporter)); + string errString = ParseIncludesDepthFirstNotCompiledFirst(stdIn, module, builtIns, + files.Select(f => f.SourceFilePath).ToHashSet(), new Errors(reporter)); if (errString != null) { return errString; } @@ -270,7 +108,7 @@ public static string Parse(IList files, string programName, DafnyOpti if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { DependencyMap dmap = new DependencyMap(); dmap.AddIncludes(module.ModuleDef.Includes); - dmap.PrintMap(); + dmap.PrintMap(options); } program = new Program(programName, module, builtIns, reporter); @@ -280,18 +118,27 @@ public static string Parse(IList files, string programName, DafnyOpti return null; // success } + private static readonly TaskScheduler largeThreadScheduler = + CustomStackSizePoolTaskScheduler.Create(0x10000000, Environment.ProcessorCount); + + public static readonly TaskFactory LargeStackFactory = new(CancellationToken.None, + TaskCreationOptions.DenyChildAttach, TaskContinuationOptions.None, largeThreadScheduler); + public static string Resolve(Program program) { - if (program.Options.NoResolve || program.Options.NoTypecheck) { return null; } + if (program.Options.NoResolve || program.Options.NoTypecheck) { + return null; + } var r = new Resolver(program); - r.ResolveProgram(program); + LargeStackFactory.StartNew(() => r.ResolveProgram(program)).Wait(); MaybePrintProgram(program, program.Options.DafnyPrintResolvedFile, true); if (program.Reporter.ErrorCountUntilResolver != 0) { - return string.Format("{0} resolution/type errors detected in {1}", program.Reporter.Count(ErrorLevel.Error), program.Name); + return string.Format("{0} resolution/type errors detected in {1}", program.Reporter.Count(ErrorLevel.Error), + program.Name); } - return null; // success + return null; // success } // Lower-case file names before comparing them, since Windows uses case-insensitive file names @@ -301,7 +148,8 @@ public int Compare(Include x, Include y) { } } - public static string ParseIncludesDepthFirstNotCompiledFirst(ModuleDecl module, BuiltIns builtIns, ISet excludeFiles, Errors errs) { + public static string ParseIncludesDepthFirstNotCompiledFirst(TextReader stdIn, ModuleDecl module, + BuiltIns builtIns, ISet excludeFiles, Errors errs) { var includesFound = new SortedSet(new IncludeComparer()); var allIncludes = ((LiteralModuleDecl)module).ModuleDef.Includes; var notCompiledRoots = allIncludes.Where(include => !include.CompileIncludedCode).ToList(); @@ -325,7 +173,7 @@ public static string ParseIncludesDepthFirstNotCompiledFirst(ModuleDecl module, if (builtIns.Options.PrintIncludesMode != DafnyOptions.IncludesModes.None) { var dependencyMap = new DependencyMap(); dependencyMap.AddIncludes(allIncludes); - dependencyMap.PrintMap(); + dependencyMap.PrintMap(builtIns.Options); } return null; // Success @@ -339,6 +187,7 @@ string TraverseIncludesFrom(int startingIndex) { foreach (var addedItem in addedItems.Reverse()) { stack.Push(addedItem); } + includeIndex = allIncludes.Count; if (stack.Count == 0) { @@ -357,7 +206,7 @@ string TraverseIncludesFrom(int startingIndex) { return ($"Include of file \"{include.IncludedFilename}\" failed."); } - string result = ParseFile(file, include, module, builtIns, errs, false, include.CompileIncludedCode); + string result = ParseFile(stdIn, file, include, module, builtIns, errs, false, include.CompileIncludedCode); if (result != null) { return result; } @@ -367,10 +216,12 @@ string TraverseIncludesFrom(int startingIndex) { } } - private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs, bool verifyThisFile = true, bool compileThisFile = true) { + private static string ParseFile(TextReader stdIn, DafnyFile dafnyFile, Include include, ModuleDecl module, + BuiltIns builtIns, Errors errs, bool verifyThisFile = true, bool compileThisFile = true) { var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; try { - int errorCount = Dafny.Parser.Parse(dafnyFile.UseStdin, dafnyFile.Uri, module, builtIns, errs, verifyThisFile, compileThisFile); + int errorCount = Dafny.Parser.Parse(dafnyFile.UseStdin ? stdIn : null, dafnyFile.Uri, module, builtIns, errs, + verifyThisFile, compileThisFile); if (errorCount != 0) { return $"{errorCount} parse errors detected in {fn}"; } @@ -379,6 +230,7 @@ private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl errs.SemErr(tok, "Unable to open included file"); return $"Error opening file \"{fn}\": {e.Message}"; } + return null; // Success } @@ -400,7 +252,7 @@ to also include a directory containing the `z3` executable. var proverPath = options.ProverOptions.Find(o => o.StartsWith("PROVER_PATH=")); if (proverPath is null && options.Verify) { - Console.WriteLine(z3NotFoundMessage); + options.OutputWriter.WriteLine(z3NotFoundMessage); return (PipelineOutcome.FatalError, new PipelineStatistics()); } @@ -429,11 +281,11 @@ public static string BoogieProgramSuffix(string printFile, string suffix) { public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics statistics) { return (outcome == PipelineOutcome.Done || outcome == PipelineOutcome.VerificationCompleted) - && statistics.ErrorCount == 0 - && statistics.InconclusiveCount == 0 - && statistics.TimeoutCount == 0 - && statistics.OutOfResourceCount == 0 - && statistics.OutOfMemoryCount == 0; + && statistics.ErrorCount == 0 + && statistics.InconclusiveCount == 0 + && statistics.TimeoutCount == 0 + && statistics.OutOfResourceCount == 0 + && statistics.OutOfMemoryCount == 0; } /// @@ -446,8 +298,8 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics /// private static async Task<(PipelineOutcome Outcome, PipelineStatistics Statistics)> BoogiePipelineWithRerun( DafnyOptions options, - TextWriter output, ExecutionEngine engine, Microsoft.Boogie.Program/*!*/ program, string/*!*/ bplFileName, - string programId) { + TextWriter output, ExecutionEngine engine, Microsoft.Boogie.Program /*!*/ program, string /*!*/ bplFileName, + string programId) { Contract.Requires(program != null); Contract.Requires(bplFileName != null); @@ -460,12 +312,13 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics case PipelineOutcome.ResolutionError: case PipelineOutcome.TypeCheckingError: engine.PrintBplFile(bplFileName, program, false, false, options.PrettyPrint); - Console.WriteLine(); - Console.WriteLine( + await options.OutputWriter.WriteLineAsync(); + await options.OutputWriter.WriteLineAsync( "*** Encountered internal translation error - re-running Boogie to get better debug information"); - Console.WriteLine(); + await options.OutputWriter.WriteLineAsync(); - var /*!*/ fileNames = new List { bplFileName }; + var /*!*/ + fileNames = new List { bplFileName }; var reparsedProgram = engine.ParseBoogieProgram(fileNames, true); if (reparsedProgram != null) { engine.ResolveAndTypecheck(reparsedProgram, bplFileName, out _); @@ -482,7 +335,8 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics return (inferAndVerifyOutcome, stats); default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome + Contract.Assert(false); + throw new cce.UnreachableException(); // unexpected outcome } } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index a9c69578d56..be262867127 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -35,10 +35,12 @@ public enum QuantifierSyntaxOptions { public record Options(IDictionary OptionArguments); public class DafnyOptions : Bpl.CommandLineOptions { + public TextWriter ErrorWriter { get; } + public TextReader Input { get; } + public static readonly DafnyOptions Default = new(TextReader.Null, TextWriter.Null, TextWriter.Null); public IList CliRootUris = new List(); - public static DafnyOptions Default = new DafnyOptions(); public ProjectFile ProjectFile { get; set; } public Command CurrentCommand { get; set; } public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2; @@ -206,10 +208,11 @@ public static void RegisterLegacyUi(Option option, } private static DafnyOptions defaultImmutableOptions; - public static DafnyOptions DefaultImmutableOptions => defaultImmutableOptions ??= Create(); + public static DafnyOptions DefaultImmutableOptions => defaultImmutableOptions ??= Create(Console.Out, Console.In); - public static DafnyOptions Create(params string[] arguments) { - var result = new DafnyOptions(); + public static DafnyOptions Create(TextWriter outputWriter, TextReader input = null, params string[] arguments) { + input ??= TextReader.Null; + var result = new DafnyOptions(input, outputWriter, outputWriter); result.Parse(arguments); return result; } @@ -229,8 +232,10 @@ public override bool Parse(string[] arguments) { return base.Parse(arguments.Take(i).ToArray()); } - public DafnyOptions() - : base("dafny", "Dafny program verifier", new Bpl.ConsolePrinter()) { + public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter) + : base(outputWriter, "dafny", "Dafny program verifier", new Bpl.ConsolePrinter()) { + Input = inputReader; + ErrorWriter = errorWriter; ErrorTrace = 0; Prune = true; NormalizeNames = true; @@ -398,7 +403,7 @@ private static string[] ParsePluginArguments(string argumentsString) { /// /// Automatic shallow-copy constructor /// - public DafnyOptions(DafnyOptions src) : this() { + public DafnyOptions(DafnyOptions src) : this(src.Input, src.OutputWriter, src.ErrorWriter) { src.CopyTo(this); } @@ -713,7 +718,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p case "allocated": { ps.GetIntArgument(ref Allocated, 5); if (Allocated != 4) { - Printer.AdvisoryWriteLine(Console.Out, "The /allocated: option is deprecated"); + Printer.AdvisoryWriteLine(OutputWriter, "The /allocated: option is deprecated"); } return true; } @@ -1617,7 +1622,6 @@ Dafny generally accepts Boogie options and passes these on to Boogie. for a similar Boogie program. ".Replace("\n", "\n "); } - } class ErrorReportingCommandLineParseState : Bpl.CommandLineParseState { diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index f6836d5b68a..6bbea88f725 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -189,7 +189,9 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro msg = msg.Replace("\n", "\n "); ConsoleColor previousColor = Console.ForegroundColor; - Console.ForegroundColor = ColorForLevel(level); + if (Options.OutputWriter == Console.Out) { + Console.ForegroundColor = ColorForLevel(level); + } var errorLine = ErrorToString(level, tok, msg); while (tok is NestedToken nestedToken) { tok = nestedToken.Inner; @@ -208,13 +210,15 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro errorLine += "\n" + info; } } - Console.WriteLine(errorLine); + Options.OutputWriter.WriteLine(errorLine); - Console.ForegroundColor = previousColor; + if (Options.OutputWriter == Console.Out) { + Console.ForegroundColor = previousColor; + } return true; - } else { - return false; } + + return false; } public ConsoleErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index 0b995224e7a..c80fa81dd3d 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -483,11 +483,11 @@ public static void PrintFunctionCallGraph(Dafny.Program program) { foreach (var vertex in functionCallGraph.GetVertices()) { var func = vertex.N; - Console.Write("{0},{1}=", func.SanitizedName, func.EnclosingClass.EnclosingModuleDefinition.SanitizedName); + program.Options.OutputWriter.Write("{0},{1}=", func.SanitizedName, func.EnclosingClass.EnclosingModuleDefinition.SanitizedName); foreach (var callee in vertex.Successors) { - Console.Write("{0} ", callee.N.SanitizedName); + program.Options.OutputWriter.Write("{0} ", callee.N.SanitizedName); } - Console.Write("\n"); + program.Options.OutputWriter.Write("\n"); } } @@ -581,9 +581,9 @@ public static void PrintStats(Dafny.Program program) { } // Print out the results, with some nice formatting - Console.WriteLine(""); - Console.WriteLine("Statistics"); - Console.WriteLine("----------"); + program.Options.OutputWriter.WriteLine(""); + program.Options.OutputWriter.WriteLine("Statistics"); + program.Options.OutputWriter.WriteLine("----------"); int max_key_length = 0; foreach (var key in stats.Keys) { @@ -594,7 +594,7 @@ public static void PrintStats(Dafny.Program program) { foreach (var keypair in stats) { string keyString = keypair.Key.PadRight(max_key_length + 2); - Console.WriteLine("{0} {1,4}", keyString, keypair.Value); + program.Options.OutputWriter.WriteLine("{0} {1,4}", keyString, keypair.Value); } } } @@ -625,20 +625,20 @@ public void AddIncludes(IEnumerable includes) { } } - public void PrintMap() { + public void PrintMap(DafnyOptions options) { SortedSet leaves = new SortedSet(); // Files that don't themselves include any files foreach (string target in dependencies.Keys) { - System.Console.Write(target); + options.OutputWriter.Write(target); foreach (string dependency in dependencies[target]) { - System.Console.Write(";" + dependency); + options.OutputWriter.Write(";" + dependency); if (!dependencies.ContainsKey(dependency)) { leaves.Add(dependency); } } - System.Console.WriteLine(); + options.OutputWriter.WriteLine(); } foreach (string leaf in leaves) { - System.Console.WriteLine(leaf); + options.OutputWriter.WriteLine(leaf); } } } diff --git a/Source/DafnyCore/JsonDiagnostics.cs b/Source/DafnyCore/JsonDiagnostics.cs index 73d553c4617..b3bedcffc41 100644 --- a/Source/DafnyCore/JsonDiagnostics.cs +++ b/Source/DafnyCore/JsonDiagnostics.cs @@ -109,9 +109,9 @@ public DafnyJsonConsolePrinter(DafnyOptions options) : base(options) { } public class JsonConsoleErrorReporter : BatchErrorReporter { - public override bool Message(MessageSource source, ErrorLevel level, string errorId, Dafny.IToken tok, string msg) { - if (base.Message(source, level, errorId, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { - new DiagnosticMessageData(source, level, tok, null, msg, null).WriteJsonTo(Console.Out); + public override bool Message(MessageSource source, ErrorLevel level, string errorID, Dafny.IToken tok, string msg) { + if (base.Message(source, level, errorID, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { + new DiagnosticMessageData(source, level, tok, null, msg, null).WriteJsonTo(Options.OutputWriter); return true; } diff --git a/Source/DafnyCore/Plugins/IExecutableBackend.cs b/Source/DafnyCore/Plugins/IExecutableBackend.cs index bb9652fe09f..23f5316554a 100644 --- a/Source/DafnyCore/Plugins/IExecutableBackend.cs +++ b/Source/DafnyCore/Plugins/IExecutableBackend.cs @@ -156,6 +156,8 @@ public abstract bool CompileTargetProgram(string dafnyProgramName, string target /// /// Returns true on success, false on error. Any errors are output to outputWriter. /// - public abstract bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string pathsFilename, - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter); + public abstract bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, + string pathsFilename, + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, + TextWriter errorWriter); } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index 8a5b73fe956..333b9ff173c 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -224,18 +224,18 @@ void PrintTypeConstraintState(int lbl) { if (!Options.Get(CommonOptionBag.TypeInferenceDebug)) { return; } - Console.WriteLine("DEBUG: ---------- type constraints ---------- {0} {1}", lbl, lbl == 0 && currentMethod != null ? currentMethod.Name : ""); + Options.OutputWriter.WriteLine("DEBUG: ---------- type constraints ---------- {0} {1}", lbl, lbl == 0 && currentMethod != null ? currentMethod.Name : ""); foreach (var constraint in AllTypeConstraints) { var super = constraint.Super.Normalize(); var sub = constraint.Sub.Normalize(); - Console.WriteLine(" {0} :> {1}", super is IntVarietiesSupertype ? "int-like" : super is RealVarietiesSupertype ? "real-like" : super.ToString(), sub); + Options.OutputWriter.WriteLine(" {0} :> {1}", super is IntVarietiesSupertype ? "int-like" : super is RealVarietiesSupertype ? "real-like" : super.ToString(), sub); } foreach (var xc in AllXConstraints) { - Console.WriteLine(" {0}", xc); + Options.OutputWriter.WriteLine(" {0}", xc); } - Console.WriteLine(); + Options.OutputWriter.WriteLine(); if (lbl % 2 == 1) { - Console.WriteLine("DEBUG: --------------------------------------"); + Options.OutputWriter.WriteLine("DEBUG: --------------------------------------"); } } @@ -1226,14 +1226,14 @@ private void ConstrainSubtypeRelation_Equal(Type a, Type b, TypeConstraint.Error var proxy = a.Normalize() as TypeProxy; if (proxy != null && proxy.T == null && !Reaches(b, proxy, 1, new HashSet())) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, b); + Options.OutputWriter.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, b); } proxy.T = b; } proxy = b.Normalize() as TypeProxy; if (proxy != null && proxy.T == null && !Reaches(a, proxy, 1, new HashSet())) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, a); + Options.OutputWriter.WriteLine("DEBUG: (invariance) assigning proxy {0}.T := {1}", proxy, a); } proxy.T = a; } @@ -1452,7 +1452,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo if (t != t.NormalizeExpand()) { // force the type to be a base type if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); + Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); } t = t.NormalizeExpand(); followedRequestedAssignment = false; @@ -1460,7 +1460,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo } else { // hijack the setting of proxy; to do that, we decide on a particular int variety now if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Int); + Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Int); } t = Type.Int; followedRequestedAssignment = false; @@ -1473,7 +1473,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo if (t != t.NormalizeExpand()) { // force the type to be a base type if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); + Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, t.NormalizeExpand()); } t = t.NormalizeExpand(); followedRequestedAssignment = false; @@ -1481,7 +1481,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo } else { // hijack the setting of proxy; to do that, we decide on a particular real variety now if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Real); + Options.OutputWriter.WriteLine("DEBUG: hijacking {0}.T := {1} to instead assign {2}", proxy, t, Type.Real); } t = Type.Real; followedRequestedAssignment = false; @@ -1491,7 +1491,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo } // set proxy.T right away, so that we can freely recurse without having to worry about infinite recursion if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: setting proxy {0}.T := {1}", proxy, t); + Options.OutputWriter.WriteLine("DEBUG: setting proxy {0}.T := {1}", proxy, t); } proxy.T = t; @@ -2276,11 +2276,11 @@ Type FindCollectionType(DafnyOptions options, Type t, bool towardsSub, ISet rhss) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { Console.Write("DEBUG: ProcessAssignable: {0} with rhss:", lhs); foreach (var rhs in rhss) { - Console.Write(" {0}", rhs); + Options.OutputWriter.Write(" {0}", rhs); } - Console.Write(" subtypes:"); + Options.OutputWriter.Write(" subtypes:"); foreach (var sub in lhs.SubtypesKeepConstraints) { - Console.Write(" {0}", sub); + Options.OutputWriter.Write(" {0}", sub); } - Console.WriteLine(); + Options.OutputWriter.WriteLine(); } Type join = null; foreach (var rhs in rhss) { @@ -2762,7 +2762,7 @@ private bool ProcessAssignable(TypeProxy lhs, List rhss) { return false; } else { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: ProcessAssignable: assigning proxy {0}.T := {1}", lhs, join); + Options.OutputWriter.WriteLine("DEBUG: ProcessAssignable: assigning proxy {0}.T := {1}", lhs, join); } lhs.T = join; return true; @@ -3042,7 +3042,7 @@ bool AssignKnownEndsFullstrength_SubDirection(TypeProxy proxy) { CloseOverAssignableRhss(proxySubs); if (HasApplicableNullableRefTypeConstraint(proxySubs)) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: Found join {0} for proxy {1}, but weakening it to {2}", joins[0], proxy, joins[0].NormalizeExpand()); + Options.OutputWriter.WriteLine("DEBUG: Found join {0} for proxy {1}, but weakening it to {2}", joins[0], proxy, joins[0].NormalizeExpand()); } AssignProxyAndHandleItsConstraints(proxy, joins[0].NormalizeExpand(), true); return true; @@ -5169,14 +5169,14 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me var r = GetBaseTypeFromProxy((TypeProxy)t, new Dictionary()); if (r != null) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> found improvement through GetBaseTypeFromProxy: {0}", r); + Options.OutputWriter.WriteLine(" ----> found improvement through GetBaseTypeFromProxy: {0}", r); } return r; } } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> found no improvement, giving up"); + Options.OutputWriter.WriteLine(" ----> found no improvement, giving up"); } return t; } @@ -5189,7 +5189,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me return t; // simplification did the trick } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: Member selection{3}: {1} :> {0} :> {2}", t, + Options.OutputWriter.WriteLine("DEBUG: Member selection{3}: {1} :> {0} :> {2}", t, Util.Comma(proxy.SupertypesKeepConstraints, su => su.ToString()), Util.Comma(proxy.SubtypesKeepConstraints, su => su.ToString()), memberName == null ? "" : " (" + memberName + ")"); @@ -5201,14 +5201,14 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me DetermineRootLeaf(joinType, out _, out _, out var headIsRoot, out _); if (joinType.IsDatatype) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> join is a datatype: {0}", joinType); + Options.OutputWriter.WriteLine(" ----> join is a datatype: {0}", joinType); } ConstrainSubtypeRelation(t, joinType, tok, "Member selection requires a supertype of {0} (got something more like {1})", t, joinType); return joinType; } else if (headIsRoot) { // we're good to go -- by picking "join" (whose type parameters have been replaced by fresh proxies), we're not losing any generality if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> improved to {0} through join", joinType); + Options.OutputWriter.WriteLine(" ----> improved to {0} through join", joinType); } AssignProxyAndHandleItsConstraints(proxy, joinType, true); return proxy.NormalizeExpand(); // we return proxy.T instead of join, in case the assignment gets hijacked @@ -5217,7 +5217,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me if (generalArrowType != null) { // pick the supertype "generalArrowType" of "join" if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> improved to {0} through join and function application", generalArrowType); + Options.OutputWriter.WriteLine(" ----> improved to {0} through join and function application", generalArrowType); } ConstrainSubtypeRelation(generalArrowType, t, tok, "Function application requires a subtype of {0} (got something more like {1})", generalArrowType, t); return generalArrowType; @@ -5236,7 +5236,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me var mbr = plausibleMembers.First(); if (mbr.EnclosingClass == cl) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> improved to {0} through member-selection join", joinType); + Options.OutputWriter.WriteLine(" ----> improved to {0} through member-selection join", joinType); } var joinRoot = joinType.NormalizeExpand(); // blow passed any constraints ConstrainSubtypeRelation(joinRoot, t, tok, "Member selection requires a subtype of {0} (got something more like {1})", joinRoot, t); @@ -5259,7 +5259,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me proxyTypeArgs = proxyTypeArgs.ConvertAll(t0 => t0.AsTypeParameter == null ? t0 : (Type)new InferredTypeProxy()); var pickItFromHere = new UserDefinedType(tok, mbr.EnclosingClass.Name, mbr.EnclosingClass, proxyTypeArgs); if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> improved to {0} through join and member lookup", pickItFromHere); + Options.OutputWriter.WriteLine(" ----> improved to {0} through join and member lookup", pickItFromHere); } ConstrainSubtypeRelation(pickItFromHere, t, tok, "Member selection requires a subtype of {0} (got something more like {1})", pickItFromHere, t); return pickItFromHere; @@ -5270,7 +5270,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me } } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> found no improvement, because join does not determine type enough"); + Options.OutputWriter.WriteLine(" ----> found no improvement, because join does not determine type enough"); } } @@ -5285,12 +5285,12 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me if (proxy == meet.Normalize()) { // can this really ever happen? if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> found no improvement (other than the proxy itself)"); + Options.OutputWriter.WriteLine(" ----> found no improvement (other than the proxy itself)"); } return t; } else { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> (merging, then trying to improve further) assigning proxy {0}.T := {1}", proxy, meet); + Options.OutputWriter.WriteLine(" ----> (merging, then trying to improve further) assigning proxy {0}.T := {1}", proxy, meet); } Contract.Assert(proxy != meet); proxy.T = meet; @@ -5300,7 +5300,7 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me } if (!(meet is ArtificialType)) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> improved to {0} through meet", meet); + Options.OutputWriter.WriteLine(" ----> improved to {0} through meet", meet); } if (memberName != null) { AssignProxyAndHandleItsConstraints(proxy, meet, true); @@ -5315,14 +5315,14 @@ public Type PartiallyResolveTypeForMemberSelection(IToken tok, Type t, string me var artificialSuper = proxy.InClusterOfArtificial(AllXConstraints); if (artificialSuper != null) { if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> use artificial supertype: {0}", artificialSuper); + Options.OutputWriter.WriteLine(" ----> use artificial supertype: {0}", artificialSuper); } return artificialSuper; } // we weren't able to do it if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine(" ----> found no improvement using simple things, trying harder once more"); + Options.OutputWriter.WriteLine(" ----> found no improvement using simple things, trying harder once more"); } return PartiallyResolveTypeForMemberSelection(tok, t, memberName, strength + 1); } @@ -5418,7 +5418,7 @@ private void GetRelatedTypeProxies(Type t, ISet proxies) { return; } if (Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine("DEBUG: GetRelatedTypeProxies: finding {0} interesting", proxy); + Options.OutputWriter.WriteLine("DEBUG: GetRelatedTypeProxies: finding {0} interesting", proxy); } proxies.Add(proxy); // close over interesting constraints diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 610ff2e90b6..7049daa9f6c 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -52,7 +52,7 @@ private bool VisibleInScope(Declaration d) { return useCompileSignatures || d.IsVisibleInScope(moduleInfo.VisibilityScope); } - public static FreshIdGenerator defaultTempVarIdGenerator = new FreshIdGenerator(); + public FreshIdGenerator defaultTempVarIdGenerator = new FreshIdGenerator(); public string FreshTempVarName(string prefix, ICodeContext context) { var gen = context is Declaration decl ? decl.IdGenerator : defaultTempVarIdGenerator; @@ -448,7 +448,7 @@ public void ResolveProgram(Program prog) { rewriters.Add(new TimeLimitRewriter(reporter)); rewriters.Add(new ForallStmtRewriter(reporter)); rewriters.Add(new ProvideRevealAllRewriter(this.reporter)); - rewriters.Add(new MatchFlattener(this.reporter, Resolver.defaultTempVarIdGenerator)); + rewriters.Add(new MatchFlattener(this.reporter, defaultTempVarIdGenerator)); if (Options.AutoTriggers) { rewriters.Add(new QuantifierSplittingRewriter(reporter)); @@ -1192,7 +1192,7 @@ private void CheckModuleExportConsistency(ModuleDefinition m) { Cloner cloner = new ScopeCloner(scope); var exportView = cloner.CloneModuleDefinition(m, m.NameNode); if (Options.DafnyPrintExportedViews.Contains(exportDecl.FullName)) { - var wr = Console.Out; + var wr = Options.OutputWriter; wr.WriteLine("/* ===== export set {0}", exportDecl.FullName); var pr = new Printer(wr, Options); pr.PrintTopLevelDecls(exportView.TopLevelDecls, 0, null, null); diff --git a/Source/DafnyCore/Resolver/TypeConstraint.cs b/Source/DafnyCore/Resolver/TypeConstraint.cs index 06eb2de36f7..ada2c42af72 100644 --- a/Source/DafnyCore/Resolver/TypeConstraint.cs +++ b/Source/DafnyCore/Resolver/TypeConstraint.cs @@ -29,7 +29,7 @@ public abstract class ErrorMsg { bool reported; public void FlagAsError(Resolver resolver) { if (resolver.Options.Get(CommonOptionBag.TypeInferenceDebug)) { - Console.WriteLine($"DEBUG: flagging error: {ApproximateErrorMessage()}"); + resolver.Options.OutputWriter.WriteLine($"DEBUG: flagging error: {ApproximateErrorMessage()}"); } resolver.TypeConstraintErrorsToBeReported.Add(this); } diff --git a/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs b/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs index 85a88402782..de5e0203865 100644 --- a/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs +++ b/Source/DafnyCore/Rewriters/ForallStmtRewriter.cs @@ -84,14 +84,14 @@ protected override bool VisitOneStmt(Statement stmt, ref bool st) { var range = Expression.CreateAnd(Resolver.GetImpliedTypeConstraint(i, i.Type), s.Range); var vals = InvertExpression(i, j, range, Fi); #if DEBUG_PRINT - Console.WriteLine("DEBUG: Trying to invert:"); - Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); + resolve.Options.Writer.WriteLine("DEBUG: Trying to invert:"); + resolve.Options.Writer.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); if (vals == null) { - Console.WriteLine("DEBUG: Can't"); + resolve.Options.Writer.WriteLine("DEBUG: Can't"); } else { - Console.WriteLine("DEBUG: The inverse is the disjunction of the following:"); + resolve.Options.Writer.WriteLine("DEBUG: The inverse is the disjunction of the following:"); foreach (var val in vals) { - Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); + resolve.Options.Writer.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); } } #endif diff --git a/Source/DafnyCore/Rewriters/IRewriter.cs b/Source/DafnyCore/Rewriters/IRewriter.cs index 527bba5cec9..c919686f4bd 100644 --- a/Source/DafnyCore/Rewriters/IRewriter.cs +++ b/Source/DafnyCore/Rewriters/IRewriter.cs @@ -13,6 +13,22 @@ public abstract class IRewriter { /// protected ErrorReporter Reporter; + protected DafnyOptions Options => Reporter.Options; + + /// + /// Constructor that accepts an ErrorReporter + /// You can obtain an ErrorReporter two following ways: + /// * Extend a PluginConfiguration class, and override the method GetRewriters(), whose first argument is an ErrorReporter + /// * Have no PluginConfiguration class, and an ErrorReporter will be provided to your class's constructor. + /// + /// Then you can use the protected field "reporter" like the following: + /// + /// reporter.Error(MessageSource.Compiler, token, "[Your plugin] Your error message here"); + /// + /// The token is usually obtained on expressions and statements in the field `tok` + /// If you do not have access to them, use moduleDefinition.GetFirstTopLevelToken() + /// + /// The error reporter. Usually outputs automatically to IDE or command-line protected internal IRewriter(ErrorReporter reporter) { Contract.Requires(reporter != null); this.Reporter = reporter; diff --git a/Source/DafnyCore/Triggers/TriggerUtils.cs b/Source/DafnyCore/Triggers/TriggerUtils.cs index 6f0c6f21c2c..e168888bbb9 100644 --- a/Source/DafnyCore/Triggers/TriggerUtils.cs +++ b/Source/DafnyCore/Triggers/TriggerUtils.cs @@ -188,8 +188,8 @@ internal string JoinStringsWithHeader(string header, IEnumerable lines) } [Conditional("DEBUG_AUTO_TRIGGERS")] - internal static void DebugTriggers(string format, params object[] more) { - Console.Error.WriteLine(format, more); + internal static void DebugTriggers(DafnyOptions options, string format, params object[] more) { + options.ErrorWriter.WriteLine(format, more); } internal static bool AllowsMatchingLoops(ComprehensionExpr quantifier) { diff --git a/Source/DafnyCore/Triggers/TriggersCollector.cs b/Source/DafnyCore/Triggers/TriggersCollector.cs index 592024e7d30..ac636e66c04 100644 --- a/Source/DafnyCore/Triggers/TriggersCollector.cs +++ b/Source/DafnyCore/Triggers/TriggersCollector.cs @@ -234,7 +234,7 @@ expr is MultiSetFormingExpr || } } - TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(options, expr), expr.GetType(), annotation); + TriggerUtils.DebugTriggers(options, "{0} ({1})\n{2}", Printer.ExprToString(options, expr), expr.GetType(), annotation); cache.annotations[expr] = annotation; return annotation; } diff --git a/Source/DafnyCore/UndisposableTextWriter.cs b/Source/DafnyCore/UndisposableTextWriter.cs new file mode 100644 index 00000000000..23d0c297b74 --- /dev/null +++ b/Source/DafnyCore/UndisposableTextWriter.cs @@ -0,0 +1,247 @@ +using System; +using System.IO; +using System.Text; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Dafny; + +public class UndisposableTextWriter : TextWriter { + public UndisposableTextWriter(TextWriter textWriterImplementation) { + this.textWriterImplementation = textWriterImplementation; + } + + public override void Close() { + textWriterImplementation.Close(); + } + + protected override void Dispose(bool disposing) { + WriteLine("Tried to Dispose the writer at: " + new Exception().StackTrace); + } + + public override ValueTask DisposeAsync() { + WriteLine("Tried to DisposeAsync the writer at: " + new Exception().StackTrace); + return ValueTask.CompletedTask; + } + + public override void Flush() { + textWriterImplementation.Flush(); + } + + public override Task FlushAsync() { + return textWriterImplementation.FlushAsync(); + } + + public override void Write(bool value) { + textWriterImplementation.Write(value); + } + + public override void Write(char value) { + textWriterImplementation.Write(value); + } + + public override void Write(char[] buffer) { + textWriterImplementation.Write(buffer); + } + + public override void Write(char[] buffer, int index, int count) { + textWriterImplementation.Write(buffer, index, count); + } + + public override void Write(decimal value) { + textWriterImplementation.Write(value); + } + + public override void Write(double value) { + textWriterImplementation.Write(value); + } + + public override void Write(int value) { + textWriterImplementation.Write(value); + } + + public override void Write(long value) { + textWriterImplementation.Write(value); + } + + public override void Write(object value) { + textWriterImplementation.Write(value); + } + + public override void Write(ReadOnlySpan buffer) { + textWriterImplementation.Write(buffer); + } + + public override void Write(float value) { + textWriterImplementation.Write(value); + } + + public override void Write(string value) { + textWriterImplementation.Write(value); + } + + public override void Write(string format, object arg0) { + textWriterImplementation.Write(format, arg0); + } + + public override void Write(string format, object arg0, object arg1) { + textWriterImplementation.Write(format, arg0, arg1); + } + + public override void Write(string format, object arg0, object arg1, object arg2) { + textWriterImplementation.Write(format, arg0, arg1, arg2); + } + + public override void Write(string format, params object[] arg) { + textWriterImplementation.Write(format, arg); + } + + public override void Write(StringBuilder value) { + textWriterImplementation.Write(value); + } + + public override void Write(uint value) { + textWriterImplementation.Write(value); + } + + public override void Write(ulong value) { + textWriterImplementation.Write(value); + } + + public override Task WriteAsync(char value) { + return textWriterImplementation.WriteAsync(value); + } + + public override Task WriteAsync(char[] buffer, int index, int count) { + return textWriterImplementation.WriteAsync(buffer, index, count); + } + + public override Task WriteAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new CancellationToken()) { + return textWriterImplementation.WriteAsync(buffer, cancellationToken); + } + + public override Task WriteAsync(string value) { + return textWriterImplementation.WriteAsync(value); + } + + public override Task WriteAsync(StringBuilder value, CancellationToken cancellationToken = new CancellationToken()) { + return textWriterImplementation.WriteAsync(value, cancellationToken); + } + + public override void WriteLine() { + textWriterImplementation.WriteLine(); + } + + public override void WriteLine(bool value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(char value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(char[] buffer) { + textWriterImplementation.WriteLine(buffer); + } + + public override void WriteLine(char[] buffer, int index, int count) { + textWriterImplementation.WriteLine(buffer, index, count); + } + + public override void WriteLine(decimal value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(double value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(int value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(long value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(object value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(ReadOnlySpan buffer) { + textWriterImplementation.WriteLine(buffer); + } + + public override void WriteLine(float value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(string value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(string format, object arg0) { + textWriterImplementation.WriteLine(format, arg0); + } + + public override void WriteLine(string format, object arg0, object arg1) { + textWriterImplementation.WriteLine(format, arg0, arg1); + } + + public override void WriteLine(string format, object arg0, object arg1, object arg2) { + textWriterImplementation.WriteLine(format, arg0, arg1, arg2); + } + + public override void WriteLine(string format, params object[] arg) { + textWriterImplementation.WriteLine(format, arg); + } + + public override void WriteLine(StringBuilder value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(uint value) { + textWriterImplementation.WriteLine(value); + } + + public override void WriteLine(ulong value) { + textWriterImplementation.WriteLine(value); + } + + public override Task WriteLineAsync() { + return textWriterImplementation.WriteLineAsync(); + } + + public override Task WriteLineAsync(char value) { + return textWriterImplementation.WriteLineAsync(value); + } + + public override Task WriteLineAsync(char[] buffer, int index, int count) { + return textWriterImplementation.WriteLineAsync(buffer, index, count); + } + + public override Task WriteLineAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = new CancellationToken()) { + return textWriterImplementation.WriteLineAsync(buffer, cancellationToken); + } + + public override Task WriteLineAsync(string value) { + return textWriterImplementation.WriteLineAsync(value); + } + + public override Task WriteLineAsync(StringBuilder value, CancellationToken cancellationToken = new CancellationToken()) { + return textWriterImplementation.WriteLineAsync(value, cancellationToken); + } + + public override IFormatProvider FormatProvider => textWriterImplementation.FormatProvider; + + public override string NewLine { + get => textWriterImplementation.NewLine; + set => textWriterImplementation.NewLine = value; + } + + private TextWriter textWriterImplementation; + public override Encoding Encoding => textWriterImplementation.Encoding; + + + +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 27abffcc08a..11e8c05b1d3 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -906,7 +906,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { var name = MethodName(f, MethodTranslationKind.OverrideCheck); var proc = new Boogie.Procedure(f.tok, name, new List(), Util.Concat(Util.Concat(typeInParams, inParams_Heap), inParams), outParams, - req, mod, ens, etran.TrAttributes(f.Attributes, null)); + false, req, mod, ens, etran.TrAttributes(f.Attributes, null)); AddVerboseName(proc, f.FullDafnyName, MethodTranslationKind.OverrideCheck); sink.AddTopLevelDeclaration(proc); var implInParams = Boogie.Formal.StripWhereClauses(inParams); @@ -1545,7 +1545,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } var name = MethodName(m, kind); - var proc = new Boogie.Procedure(m.tok, name, new List(), inParams, outParams, req, mod, ens, etran.TrAttributes(m.Attributes, null)); + var proc = new Boogie.Procedure(m.tok, name, new List(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(m.Attributes, null)); AddVerboseName(proc, m.FullDafnyName, kind); if (InsertChecksums) { diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index c4b724eeb14..4060cb34757 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -1577,7 +1577,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, } Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok); - builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, body)); + builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, new List(), body)); } void InsertContinueTarget(LoopStmt loop, BoogieStmtListBuilder builder) { diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index eed2d64e6fe..70edf03a82a 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -434,7 +434,7 @@ public PredefinedDecls(Bpl.TypeCtorDecl charType, Bpl.TypeCtorDecl refType, Bpl. PredefinedDecls FindPredefinedDecls(Bpl.Program prog) { Contract.Requires(prog != null); if (prog.Resolve(options) != 0) { - Console.WriteLine("Error: resolution errors encountered in Dafny prelude"); + options.OutputWriter.WriteLine("Error: resolution errors encountered in Dafny prelude"); return null; } @@ -577,85 +577,85 @@ PredefinedDecls FindPredefinedDecls(Bpl.Program prog) { } } if (seqTypeCtor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Seq"); } else if (setTypeCtor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Set"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Set"); } else if (isetTypeCtor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type ISet"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type ISet"); } else if (multiSetTypeCtor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet"); } else if (mapTypeCtor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Map"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Map"); } else if (imapTypeCtor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type IMap"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type IMap"); } else if (arrayLength == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length"); } else if (realFloor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.real.Floor"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.real.Floor"); } else if (ORDINAL_isLimit == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsLimit"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsLimit"); } else if (ORDINAL_isSucc == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsSucc"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsSucc"); } else if (ORDINAL_offset == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#Offset"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#Offset"); } else if (ORDINAL_isNat == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsNat"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function ORD#IsNat"); } else if (mapDomain == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function Map#Domain"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function Map#Domain"); } else if (imapDomain == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Domain"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Domain"); } else if (mapValues == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function Map#Values"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function Map#Values"); } else if (imapValues == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Values"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Values"); } else if (mapItems == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function Map#Items"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function Map#Items"); } else if (imapItems == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Items"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function IMap#Items"); } else if (tuple2Destructors0 == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._0"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._0"); } else if (tuple2Destructors1 == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._1"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function _System.Tuple2._1"); } else if (tuple2Constructor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of function #_System._tuple#2._#Make2"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of function #_System._tuple#2._#Make2"); } else if (bv0TypeDecl == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Bv0"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Bv0"); } else if (fieldNameType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Field"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Field"); } else if (classNameType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type ClassName"); } else if (tyType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Ty"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Ty"); } else if (tyTagType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type TyTag"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type TyTag"); } else if (tyTagFamilyType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type TyTagFamily"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type TyTagFamily"); } else if (nameFamilyType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily"); } else if (datatypeType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType"); } else if (handleType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type HandleType"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type HandleType"); } else if (layerType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type LayerType"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type LayerType"); } else if (dtCtorId == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId"); } else if (charType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type char"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type char"); } else if (refType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type ref"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type ref"); } else if (boxType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type Box"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type Box"); } else if (tickType == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of type TickType"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of type TickType"); } else if (heap == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of $Heap"); } else if (allocField == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of constant alloc"); } else if (tuple2TypeConstructor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of tuple2TypeConstructor"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of tuple2TypeConstructor"); } else if (objectTypeConstructor == null) { - Console.WriteLine("Error: Dafny prelude is missing declaration of objectTypeConstructor"); + options.OutputWriter.WriteLine("Error: Dafny prelude is missing declaration of objectTypeConstructor"); } else { return new PredefinedDecls(charType, refType, boxType, tickType, setTypeCtor, isetTypeCtor, multiSetTypeCtor, @@ -1667,7 +1667,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { } var name = MethodName(iter, kind); - var proc = new Bpl.Procedure(iter.tok, name, new List(), inParams, outParams, req, mod, ens, etran.TrAttributes(iter.Attributes, null)); + var proc = new Bpl.Procedure(iter.tok, name, new List(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(iter.Attributes, null)); AddVerboseName(proc, iter.FullDafnyName, kind); currentModule = null; @@ -4301,7 +4301,7 @@ void AddWellformednessCheck(Function f) { } var proc = new Bpl.Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List(), Concat(Concat(typeInParams, inParams_Heap), inParams), outParams, - req, mod, ens, etran.TrAttributes(f.Attributes, null)); + false, req, mod, ens, etran.TrAttributes(f.Attributes, null)); AddVerboseName(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); @@ -4537,7 +4537,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { var name = MethodName(decl, MethodTranslationKind.SpecWellformedness); var proc = new Bpl.Procedure(decl.tok, name, new List(), inParams, new List(), - req, mod, new List(), etran.TrAttributes(decl.Attributes, null)); + false, req, mod, new List(), etran.TrAttributes(decl.Attributes, null)); AddVerboseName(proc, decl.Name, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); @@ -4690,7 +4690,7 @@ void AddWellformednessCheck(ConstantField decl) { var name = MethodName(decl, MethodTranslationKind.SpecWellformedness); var proc = new Bpl.Procedure(decl.tok, name, new List(), inParams, new List(), - req, varlist, new List(), etran.TrAttributes(decl.Attributes, null)); + false, req, varlist, new List(), etran.TrAttributes(decl.Attributes, null)); AddVerboseName(proc, decl.FullDafnyName, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); @@ -4761,7 +4761,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { var varlist = new List { heapVar, etran.Tick() }; var proc = new Bpl.Procedure(ctor.tok, "CheckWellformed" + NameSeparator + ctor.FullName, new List(), inParams, new List(), - req, varlist, new List(), etran.TrAttributes(ctor.Attributes, null)); + false, req, varlist, new List(), etran.TrAttributes(ctor.Attributes, null)); AddVerboseName(proc, ctor.FullName, MethodTranslationKind.SpecWellformedness); sink.AddTopLevelDeclaration(proc); diff --git a/Source/DafnyDriver/CSVTestLogger.cs b/Source/DafnyDriver/CSVTestLogger.cs index 92d0f8c18fb..6db93b18fb1 100644 --- a/Source/DafnyDriver/CSVTestLogger.cs +++ b/Source/DafnyDriver/CSVTestLogger.cs @@ -12,8 +12,13 @@ public class CSVTestLogger : ITestLoggerWithParameters { private readonly ConcurrentBag results = new(); private TextWriter writer; + private TextWriter logWriter; private string writerFilename; + public CSVTestLogger(TextWriter logWriter) { + this.logWriter = logWriter; + } + public void Initialize(TestLoggerEvents events, string testRunDirectory) { } @@ -72,7 +77,7 @@ private void TestRunCompleteHandler(object sender, TestRunCompleteEventArgs e) { } writer.Close(); - Console.Out.WriteLine("Results File: " + Path.GetFullPath(writerFilename)); + logWriter.WriteLine("Results File: " + Path.GetFullPath(writerFilename)); } } } diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 66dae914255..4655d6d211b 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -17,13 +17,13 @@ namespace Microsoft.Dafny; -internal interface ParseArgumentResult { +public interface ParseArgumentResult { } -record ParseArgumentSuccess(DafnyOptions DafnyOptions) : ParseArgumentResult; +public record ParseArgumentSuccess(DafnyOptions DafnyOptions) : ParseArgumentResult; record ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult ExitResult) : ParseArgumentResult; -static class CommandRegistry { +public static class CommandRegistry { private const string ToolchainDebuggingHelpName = "--help-internal"; private static readonly HashSet Commands = new(); @@ -62,12 +62,29 @@ static CommandRegistry() { public static Argument FileArgument { get; } + class WritersConsole : IConsole { + private readonly TextWriter errWriter; + private readonly TextWriter outWriter; + + public WritersConsole(TextWriter outWriter, TextWriter errWriter) { + this.errWriter = errWriter; + this.outWriter = outWriter; + } + + public IStandardStreamWriter Out => StandardStreamWriter.Create(outWriter ?? TextWriter.Null); + + public bool IsOutputRedirected => outWriter != null; + public IStandardStreamWriter Error => StandardStreamWriter.Create(errWriter ?? TextWriter.Null); + public bool IsErrorRedirected => errWriter != null; + public bool IsInputRedirected => false; + } + [CanBeNull] - public static ParseArgumentResult Create(string[] arguments) { + public static ParseArgumentResult Create(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] arguments) { bool allowHidden = arguments.All(a => a != ToolchainDebuggingHelpName); - + var console = new WritersConsole(outputWriter, errorWriter); var wasInvoked = false; - var dafnyOptions = new DafnyOptions(); + var dafnyOptions = new DafnyOptions(inputReader, outputWriter, errorWriter); var optionValues = new Dictionary(); var options = new Options(optionValues); dafnyOptions.ShowEnv = ExecutionEngineOptions.ShowEnvironment.Never; @@ -100,11 +117,11 @@ public static ParseArgumentResult Create(string[] arguments) { Union(new[] { "--version", "-h", ToolchainDebuggingHelpName, "--help", "[parse]", "[suggest]" }); if (!keywordForNewMode.Contains(first)) { if (first.Length > 0 && first[0] != '/' && first[0] != '-' && !File.Exists(first) && first.IndexOf('.') == -1) { - dafnyOptions.Printer.ErrorWriteLine(Console.Out, + dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, "*** Error: '{0}': The first input must be a command or a legacy option or file with supported extension", first); return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } - var oldOptions = new DafnyOptions(); + var oldOptions = new DafnyOptions(inputReader, outputWriter, errorWriter); if (oldOptions.Parse(arguments)) { return new ParseArgumentSuccess(oldOptions); } @@ -183,7 +200,7 @@ void CommandHandler(InvocationContext context) { builder = AddDeveloperHelp(rootCommand, builder); #pragma warning disable VSTHRD002 - var exitCode = builder.Build().InvokeAsync(arguments).Result; + var exitCode = builder.Build().InvokeAsync(arguments, console).Result; #pragma warning restore VSTHRD002 if (failedToProcessFile) { diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index ee2a630b2f6..1b8d2e85701 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -18,12 +18,15 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; +using System.CommandLine; +using System.CommandLine.IO; using System.Diagnostics.Contracts; using System.IO; using System.Linq; using Microsoft.Boogie; using Bpl = Microsoft.Boogie; using System.Diagnostics; +using System.Threading; using DafnyCore; using Microsoft.Dafny.Plugins; @@ -97,19 +100,29 @@ static DafnyDriver() { }; public static int Main(string[] args) { - int ret = 0; - var thread = new System.Threading.Thread( - new System.Threading.ThreadStart(() => { ret = ThreadMain(args); }), - 0x10000000); // 256MB stack size to prevent stack overflow - thread.Start(); - thread.Join(); - return ret; + return MainWithWriters(Console.Out, Console.Error, Console.In, args); } - public static int ThreadMain(string[] args) { + public static int MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, + string[] args) { + + // Code that shouldn't be needed, but prevents some exceptions when running the integration tests in parallel + // outputWriter = new UndisposableTextWriter(outputWriter); + // errorWriter = new UndisposableTextWriter(errorWriter); + // outputWriter = TextWriter.Synchronized(outputWriter); + // errorWriter = TextWriter.Synchronized(errorWriter); + +#pragma warning disable VSTHRD002 + return Task.Run(() => ThreadMain(outputWriter, errorWriter, inputReader, args)).Result; +#pragma warning restore VSTHRD002 + } + + private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] args) { Contract.Requires(cce.NonNullElements(args)); - var cliArgumentsResult = ProcessCommandLineArguments(args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); + + var cliArgumentsResult = ProcessCommandLineArguments(outputWriter, errorWriter, inputReader, + args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); ExitValue exitValue; switch (cliArgumentsResult) { @@ -140,7 +153,7 @@ public static int ThreadMain(string[] args) { try { VerificationResultLogger.RaiseTestLoggerEvents(dafnyOptions); } catch (ArgumentException ae) { - dafnyOptions.Printer.ErrorWriteLine(Console.Out, $"*** Error: {ae.Message}"); + dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, $"*** Error: {ae.Message}"); exitValue = ExitValue.PREPROCESSING_ERROR; } } @@ -179,12 +192,15 @@ static HashSet SplitOptionValueIntoFiles(HashSet inputs) { return result; } - public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] args, out DafnyOptions options, out List dafnyFiles, out List otherFiles) { + public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter outputWriter, + TextWriter errorWriter, + TextReader inputReader, + string[] args, out DafnyOptions options, out List dafnyFiles, out List otherFiles) { dafnyFiles = new List(); otherFiles = new List(); try { - switch (CommandRegistry.Create(args)) { + switch (CommandRegistry.Create(outputWriter, errorWriter, inputReader, args)) { case ParseArgumentSuccess success: options = success.DafnyOptions; break; @@ -196,7 +212,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar options.RunningBoogieFromCommandLine = true; } catch (ProverException pe) { - new DafnyConsolePrinter(DafnyOptions.Create()).ErrorWriteLine(Console.Out, "*** ProverException: {0}", pe.Message); + new DafnyConsolePrinter(DafnyOptions.Create(outputWriter)).ErrorWriteLine(outputWriter, "*** ProverException: {0}", pe.Message); options = null; return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -211,7 +227,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar if (compiler == null) { if (nonOutOptions.CompilerName != null) { var known = String.Join(", ", compilers.Select(c => $"'{c.TargetId}' ({c.TargetName})")); - options.Printer.ErrorWriteLine(Console.Error, $"No compiler found for target \"{options.CompilerName}\"{(options.CompilerName.StartsWith("-t") || options.CompilerName.StartsWith("--") ? " (use just a target name, not a -t or --target option)" : "")}; expecting one of {known}"); + options.Printer.ErrorWriteLine(options.ErrorWriter, $"No compiler found for target \"{options.CompilerName}\"{(options.CompilerName.StartsWith("-t") || options.CompilerName.StartsWith("--") ? " (use just a target name, not a -t or --target option)" : "")}; expecting one of {known}"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -235,17 +251,17 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar if (options.XmlSink != null) { string errMsg = options.XmlSink.Open(); if (errMsg != null) { - options.Printer.ErrorWriteLine(Console.Error, "*** Error: " + errMsg); + options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: " + errMsg); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } } if (options.ShowEnv == ExecutionEngineOptions.ShowEnvironment.Always) { - Console.WriteLine("---Command arguments"); + outputWriter.WriteLine("---Command arguments"); foreach (string arg in args) { Contract.Assert(arg != null); - Console.WriteLine(arg); + outputWriter.WriteLine(arg); } - Console.WriteLine("--------------------"); + outputWriter.WriteLine("--------------------"); } ISet filesSeen = new HashSet(); @@ -285,23 +301,23 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar if (File.Exists(file) || extension == ".h") { otherFiles.Add(file); } else { - options.Printer.ErrorWriteLine(Console.Out, $"*** Error: file {nameToShow} not found"); + options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {nameToShow} not found"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } } else if (options.Format && Directory.Exists(file)) { options.FoldersToFormat.Add(file); } else if (!isDafnyFile) { if (options.UsingNewCli && string.IsNullOrEmpty(extension) && file.Length > 0) { - options.Printer.ErrorWriteLine(Console.Out, + options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: Command-line argument '{0}' is neither a recognized option nor a filename with a supported extension ({1}).", nameToShow, string.Join(", ", Enumerable.Repeat(".dfy", 1).Concat(supportedExtensions))); } else if (string.IsNullOrEmpty(extension) && file.Length > 0 && (file[0] == '/' || file[0] == '-')) { - options.Printer.ErrorWriteLine(Console.Out, + options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: Command-line argument '{0}' is neither a recognized option nor a filename with a supported extension ({1}).", nameToShow, string.Join(", ", Enumerable.Repeat(".dfy", 1).Concat(supportedExtensions))); } else { - options.Printer.ErrorWriteLine(Console.Out, + options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files ({2})", nameToShow, extension, string.Join(", ", supportedExtensions)); } @@ -311,12 +327,12 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar if (dafnyFiles.Count == 0) { if (!options.Format) { - options.Printer.ErrorWriteLine(Console.Out, "*** Error: The command-line contains no .dfy files"); + options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: The command-line contains no .dfy files"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } if (options.FoldersToFormat.Count == 0) { - options.Printer.ErrorWriteLine(Console.Out, + options.Printer.ErrorWriteLine(options.OutputWriter, "Usage:\ndafny format [--check] [--print] ...\nYou can use '.' for the current directory"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -324,13 +340,13 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar if (dafnyFiles.Count > 1 && options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { - options.Printer.ErrorWriteLine(Console.Out, + options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: Only one .dfy file can be specified for testing"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } if (options.ExtractCounterexample && options.ModelViewFile == null) { - options.Printer.ErrorWriteLine(Console.Out, + options.Printer.ErrorWriteLine(options.OutputWriter, "*** Error: ModelView file must be specified when attempting counterexample extraction"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } @@ -346,7 +362,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny ExitValue exitValue = ExitValue.SUCCESS; if (options.TestGenOptions.WarnDeadCode) { await foreach (var line in DafnyTestGeneration.Main.GetDeadCodeStatistics(dafnyFileNames[0], options)) { - Console.WriteLine(line); + await options.OutputWriter.WriteLineAsync(line); } if (DafnyTestGeneration.Main.setNonZeroExitCode) { exitValue = ExitValue.DAFNY_ERROR; @@ -355,7 +371,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny } if (options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { await foreach (var line in DafnyTestGeneration.Main.GetTestClassForProgram(dafnyFileNames[0], options)) { - Console.WriteLine(line); + await options.OutputWriter.WriteLineAsync(line); } if (DafnyTestGeneration.Main.setNonZeroExitCode) { exitValue = ExitValue.DAFNY_ERROR; @@ -365,8 +381,8 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny if (options.VerifySeparately && 1 < dafnyFiles.Count) { foreach (var f in dafnyFiles) { - Console.WriteLine(); - Console.WriteLine("-------------------- {0} --------------------", f); + await options.OutputWriter.WriteLineAsync(); + await options.OutputWriter.WriteLineAsync($"-------------------- {f} --------------------"); var ev = await ProcessFilesAsync(new List { f }, new List().AsReadOnly(), options, lookForSnapshots, f.FilePath); if (exitValue != ev && ev != ExitValue.SUCCESS) { exitValue = ev; @@ -392,27 +408,27 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny } string programName = dafnyFileNames.Count == 1 ? dafnyFileNames[0] : "the_program"; - Program dafnyProgram; string err; if (Options.Format) { - return DoFormatting(dafnyFiles, Options, programName); + return DoFormatting(dafnyFiles, Options, programName, options.ErrorWriter); } - err = Dafny.Main.ParseCheck(dafnyFiles, programName, options, out dafnyProgram); + err = DafnyMain.ParseCheck(Options.Input, dafnyFiles, programName, options, out var dafnyProgram); if (err != null) { exitValue = ExitValue.DAFNY_ERROR; - options.Printer.ErrorWriteLine(Console.Out, err); + options.Printer.ErrorWriteLine(options.OutputWriter, err); } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck && options.DafnyVerify) { - var boogiePrograms = Translate(engine.Options, dafnyProgram).ToList(); + 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(options, baseName, boogiePrograms, programId); bool compiled; try { - compiled = Compile(dafnyFileNames[0], otherFileNames, dafnyProgram, outcome, moduleStats, verified); + compiled = await Compile(dafnyFileNames[0], otherFileNames, dafnyProgram, outcome, moduleStats, verified); } catch (UnsupportedFeatureException e) { if (!options.Backend.UnsupportedFeatures.Contains(e.Feature)) { throw new Exception($"'{e.Feature}' is not an element of the {options.Backend.TargetId} compiler's UnsupportedFeatures set"); @@ -436,7 +452,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny return exitValue; } - private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions options, string programName) { + private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions options, string programName, TextWriter errorWriter) { var exitValue = ExitValue.SUCCESS; Contract.Assert(dafnyFiles.Count > 0 || options.FoldersToFormat.Count > 0); dafnyFiles = dafnyFiles.Concat(options.FoldersToFormat.SelectMany(folderPath => { @@ -453,7 +469,7 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions foreach (var file in dafnyFiles) { var dafnyFile = file; if (dafnyFile.UseStdin && !doCheck && !doPrint) { - Console.Error.WriteLine("Please use the --check and/or --print option as stdin cannot be formatted in place."); + errorWriter.WriteLine("Please use the --check and/or --print option as stdin cannot be formatted in place."); exitValue = ExitValue.PREPROCESSING_ERROR; continue; } @@ -466,13 +482,13 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions } // Might not be totally optimized but let's do that for now - var err = Dafny.Main.Parse(new List { dafnyFile }, programName, options, out var dafnyProgram); + var err = DafnyMain.Parse(options.Input, new List { dafnyFile }, programName, options, out var dafnyProgram); var originalText = dafnyFile.UseStdin ? Console.In.ReadToEnd() : File.Exists(dafnyFile.FilePath) ? File.ReadAllText(dafnyFile.FilePath) : null; if (err != null) { exitValue = ExitValue.DAFNY_ERROR; - Console.Error.WriteLine(err); + errorWriter.WriteLine(err); failedToParseFiles.Add(dafnyFile.BaseName); } else { var firstToken = dafnyProgram.GetFirstTopLevelToken(); @@ -487,10 +503,10 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions } if (doCheck && (!doPrint || options.CompileVerbose)) { - Console.Out.WriteLine("The file " + - (options.UseBaseNameForFileName - ? Path.GetFileName(dafnyFile.FilePath) - : dafnyFile.FilePath) + " needs to be formatted"); + options.OutputWriter.WriteLine("The file " + + (options.UseBaseNameForFileName + ? Path.GetFileName(dafnyFile.FilePath) + : dafnyFile.FilePath) + " needs to be formatted"); } if (!doCheck && !doPrint) { @@ -499,7 +515,7 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions } } else { if (options.CompileVerbose) { - Console.Error.WriteLine(dafnyFile.BaseName + " was empty."); + options.ErrorWriter.WriteLine(dafnyFile.BaseName + " was empty."); } emptyFiles.Add((options.UseBaseNameForFileName @@ -507,7 +523,7 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions : dafnyFile.FilePath)); } if (doPrint) { - Console.Out.Write(result); + options.OutputWriter.Write(result); } } @@ -535,12 +551,12 @@ string Files(int num) { reportMsg = filesNeedFormatting + reportMsg; if (doCheck) { - Console.Out.WriteLine(neededFormatting > 0 + options.OutputWriter.WriteLine(neededFormatting > 0 ? $"Error: {reportMsg}" : "All files are correctly formatted"); } else if (failedToParseFiles.Count > 0 || options.CompileVerbose) { // We don't display anything if we just format files without verbosity and there was no parse error - Console.Out.WriteLine($"{reportMsg}"); + options.OutputWriter.WriteLine($"{reportMsg}"); } return exitValue; @@ -554,14 +570,14 @@ string Files(int num) { /// the counterexample private static void PrintCounterexample(DafnyOptions options, string modelViewFile) { var model = DafnyModel.ExtractModel(options, File.ReadAllText(modelViewFile)); - Console.WriteLine("Counterexample for first failing assertion: "); + options.OutputWriter.WriteLine("Counterexample for first failing assertion: "); foreach (var state in model.States.Where(state => !state.IsInitialState)) { - Console.WriteLine(state.FullStateName + ":"); + options.OutputWriter.WriteLine(state.FullStateName + ":"); var vars = state.ExpandedVariableSet(-1); foreach (var variable in vars) { - Console.WriteLine($"\t{variable.ShortName} : " + - $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " + - $"{variable.Value}"); + options.OutputWriter.WriteLine($"\t{variable.ShortName} : " + + $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " + + $"{variable.Value}"); } } } @@ -581,7 +597,7 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { if (options.PrintFile != null) { - var nm = nmodules > 1 ? Dafny.Main.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile; + var nm = nmodules > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile; ExecutionEngine.PrintBplFile(options, nm, prog.Item2, false, false, options.PrettyPrint); } @@ -597,7 +613,7 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { IEnumerable> boogiePrograms, string programId) { var concurrentModuleStats = new ConcurrentDictionary(); - var writerManager = new ConcurrentToSequentialWriteManager(Console.Out); + var writerManager = new ConcurrentToSequentialWriteManager(options.OutputWriter); var moduleTasks = boogiePrograms.Select(async program => { await using var moduleWriter = writerManager.AppendWriter(); @@ -609,12 +625,12 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { }).ToList(); await Task.WhenAll(moduleTasks); - await Console.Out.FlushAsync(); + await options.OutputWriter.FlushAsync(); var outcome = moduleTasks.Select(t => t.Result.Outcome) .Aggregate(PipelineOutcome.VerificationCompleted, MergeOutcomes); var isVerified = moduleTasks.Select(t => - Dafny.Main.IsBoogieVerified(t.Result.Outcome, t.Result.Stats)).All(x => x); + Dafny.DafnyMain.IsBoogieVerified(t.Result.Outcome, t.Result.Stats)).All(x => x); return (isVerified, outcome, concurrentModuleStats); } @@ -631,7 +647,7 @@ private static string BoogieProgramSuffix(string printFile, string suffix) { } var result = - await Dafny.Main.BoogieOnce(options, output, engine, baseName, moduleName, program, programId); + await Dafny.DafnyMain.BoogieOnce(options, output, engine, baseName, moduleName, program, programId); watch.Stop(); @@ -705,24 +721,24 @@ private static void WriteModuleStats(DafnyOptions options, TextWriter output, ID } - public static bool Compile(string fileName, ReadOnlyCollection otherFileNames, Program dafnyProgram, + public static async Task Compile(string fileName, ReadOnlyCollection otherFileNames, Program dafnyProgram, PipelineOutcome oc, IDictionary moduleStats, bool verified) { var options = dafnyProgram.Options; var resultFileName = options.DafnyPrintCompiledFile ?? fileName; bool compiled = true; switch (oc) { case PipelineOutcome.VerificationCompleted: - WriteModuleStats(options, Console.Out, moduleStats); + WriteModuleStats(options, options.OutputWriter, moduleStats); if ((options.Compile && verified && !options.UserConstrainedProcsToCheck) || options.ForceCompile) { - compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, true); + compiled = await CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, true); } else if ((2 <= options.SpillTargetCode && verified && !options.UserConstrainedProcsToCheck) || 3 <= options.SpillTargetCode) { - compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, false); + compiled = await CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, false); } break; case PipelineOutcome.Done: - WriteModuleStats(options, Console.Out, moduleStats); + WriteModuleStats(options, options.OutputWriter, moduleStats); if (options.ForceCompile || 3 <= options.SpillTargetCode) { - compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, options.ForceCompile); + compiled = await CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, options.ForceCompile); } break; default: @@ -796,11 +812,10 @@ static void WriteFile(string filename, string text, string moreText = null) { } CheckFilenameIsLegal(filename); - using (TextWriter target = new StreamWriter(new FileStream(filename, System.IO.FileMode.Create))) { - target.Write(text); - if (moreText != null) { - target.Write(moreText); - } + using TextWriter target = new StreamWriter(new FileStream(filename, FileMode.Create)); + target.Write(text); + if (moreText != null) { + target.Write(moreText); } } @@ -826,16 +841,13 @@ private static void CheckFilenameIsLegal(string filename) { /// Generate a C# program from the Dafny program and, if "invokeCompiler" is "true", invoke /// the C# compiler to compile it. /// - public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName, - ReadOnlyCollection otherFileNames, bool invokeCompiler, - TextWriter outputWriter = null) { + public static async Task CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName, + ReadOnlyCollection otherFileNames, bool invokeCompiler) { Contract.Requires(dafnyProgram != null); Contract.Assert(dafnyProgramName != null); - // TODO: `outputWriter` seems to always be passed in as `null`. Remove it? - if (outputWriter == null) { - outputWriter = Console.Out; - } + var outputWriter = dafnyProgram.Options.OutputWriter; + var errorWriter = dafnyProgram.Options.ErrorWriter; // Compile the Dafny program into a string that contains the target program var oldErrorCount = dafnyProgram.Reporter.Count(ErrorLevel.Error); @@ -852,7 +864,7 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP var otherFiles = new Dictionary(); { var output = new ConcreteSyntaxTree(); - compiler.Compile(dafnyProgram, output); + await DafnyMain.LargeStackFactory.StartNew(() => compiler.Compile(dafnyProgram, output)); var writerOptions = new WriterState(); var targetProgramTextWriter = new StringWriter(); var files = new Queue(); @@ -901,15 +913,16 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP if (compiledCorrectly && options.RunAfterCompile) { if (hasMain) { if (options.CompileVerbose) { - outputWriter.WriteLine("Running..."); - outputWriter.WriteLine(); + await outputWriter.WriteLineAsync("Running..."); + await outputWriter.WriteLineAsync(); } - compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, paths.Filename, otherFileNames, compilationResult, outputWriter); + compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, + paths.Filename, otherFileNames, compilationResult, outputWriter, errorWriter); } else { // make sure to give some feedback to the user if (options.CompileVerbose) { - outputWriter.WriteLine("Program compiled successfully"); + await outputWriter.WriteLineAsync("Program compiled successfully"); } } } @@ -944,8 +957,10 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target throw new NotSupportedException(); } - public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string pathsFilename, - ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { + public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, + string pathsFilename, + ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, + TextWriter errorWriter) { throw new NotSupportedException(); } } diff --git a/Source/DafnyDriver/TextLogger.cs b/Source/DafnyDriver/TextLogger.cs index 5d67f26f1af..76fe748c4aa 100644 --- a/Source/DafnyDriver/TextLogger.cs +++ b/Source/DafnyDriver/TextLogger.cs @@ -8,9 +8,14 @@ namespace Microsoft.Dafny; public class TextLogger { private TextWriter tw; + private TextWriter outWriter; + + public TextLogger(TextWriter outWriter) { + this.outWriter = outWriter; + } public void Initialize(Dictionary parameters) { - tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : Console.Out; + tw = parameters.TryGetValue("LogFileName", out string filename) ? new StreamWriter(filename) : outWriter; } public void LogResults(List<(Implementation, VerificationResult)> verificationResults) { diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs index e30d5df7051..905a097c757 100644 --- a/Source/DafnyDriver/VerificationResultLogger.cs +++ b/Source/DafnyDriver/VerificationResultLogger.cs @@ -58,12 +58,12 @@ public static void RaiseTestLoggerEvents(DafnyOptions options) { var logger = new TrxLogger(); logger.Initialize(events, parameters); } else if (loggerName == "csv") { - var csvLogger = new CSVTestLogger(); + var csvLogger = new CSVTestLogger(options.OutputWriter); csvLogger.Initialize(events, parameters); } else if (loggerName == "text") { // This logger doesn't implement the ITestLogger interface because // it uses information that's tricky to encode in a TestResult. - var textLogger = new TextLogger(); + var textLogger = new TextLogger(options.OutputWriter); textLogger.Initialize(parameters); textLogger.LogResults(verificationResults); return; diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index 3f310d1c3cf..df093b57ad2 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -7,6 +7,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; using XunitAssertMessages; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.CodeActions { @@ -308,6 +309,9 @@ private async Task TestCodeAction(string source) { } } + public CodeActionTest(ITestOutputHelper output) : base(output) { + } + private static List ApplyEdits(TextDocumentEdit textDocumentEdit, string output) { var inversedEdits = textDocumentEdit.Edits.ToList() .OrderByDescending(x => x.Range.Start.Line) diff --git a/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs index c54b132846b..048fb3d3b45 100644 --- a/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs +++ b/Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs @@ -6,6 +6,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Completion { public class DotCompletionTest : ClientBasedLanguageServerTest { @@ -217,5 +218,8 @@ method GetConstant() returns (c: int) { Assert.Equal(CompletionItemKind.Method, completionList[0].Kind); Assert.Equal("GetConstant", completionList[0].Label); } + + public DotCompletionTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 1e7fb744a56..e39ddaeaabc 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -20,9 +20,11 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Various; using Microsoft.Dafny.LanguageServer.Language; using OmniSharp.Extensions.LanguageServer.Client; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest { public class DafnyLanguageServerTestBase : LanguageServerTestBase { + protected readonly string SlowToVerify = @" lemma {:timeLimit 3} SquareRoot2NotRational(p: nat, q: nat) requires p > 0 && q > 0 @@ -47,13 +49,16 @@ ensures true public const string LanguageId = "dafny"; protected static int fileIndex; + protected readonly TextWriter output; public ILanguageServer Server { get; private set; } public IDocumentDatabase Documents => Server.GetRequiredService(); - public DafnyLanguageServerTestBase() : base(new JsonRpcTestOptions(LoggerFactory.Create( - builder => builder.AddConsole().SetMinimumLevel(LogLevel.Warning)))) { } + public DafnyLanguageServerTestBase(ITestOutputHelper output) : base(new JsonRpcTestOptions(LoggerFactory.Create( + builder => builder.AddConsole().SetMinimumLevel(LogLevel.Warning)))) { + this.output = new WriterFromOutputHelper(output); + } protected virtual IServiceCollection ServerOptionsAction(LanguageServerOptions serverOptions) { return serverOptions.Services.AddSingleton(serviceProvider => new SlowVerifier( @@ -65,7 +70,7 @@ protected virtual IServiceCollection ServerOptionsAction(LanguageServerOptions s protected virtual async Task InitializeClient( Action clientOptionsAction = null, Action modifyOptions = null) { - var dafnyOptions = DafnyOptions.Create(); + var dafnyOptions = DafnyOptions.Create(output); modifyOptions?.Invoke(dafnyOptions); void NewServerOptionsAction(LanguageServerOptions options) { diff --git a/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs b/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs index 382d9d63436..12f64d43d90 100644 --- a/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs +++ b/Source/DafnyLanguageServer.Test/Formatting/FormattingTest.cs @@ -9,6 +9,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.Formatting; public class FormattingTest : ClientBasedLanguageServerTest { @@ -162,4 +163,7 @@ private async Task FormattingWorksFor(string source, string target = null) { } Assert.Equal(target, finalText); } + + public FormattingTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs index ffdbba5c28e..fbb005f8e46 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs @@ -1,4 +1,5 @@ using System.Threading.Tasks; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -40,4 +41,7 @@ await VerifyTrace(@" . S [S][ ][I][S][S][ ]: //Next: . S [S][ ][I][S][S][ ]:}"); } + + public CachedLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs index 94b372140e7..77ff734ed1b 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ConcurrentLinearVerificationGutterStatusTester.cs @@ -4,6 +4,7 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace.Notifications; using OmniSharp.Extensions.JsonRpc; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -58,4 +59,6 @@ public async Task EnsuresManyDocumentsCanBeVerifiedAtOnce() { } } + public ConcurrentLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs index 655e9f7d37f..45a8055c424 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs @@ -10,6 +10,7 @@ using OmniSharp.Extensions.JsonRpc; using OmniSharp.Extensions.LanguageServer.Client; using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -284,4 +285,7 @@ public string AcceptQuestionMarks(string traceObtained, string expected) { var toReplaceRegex = new Regex(pattern); return toReplaceRegex.Replace(traceObtained, "?"); } + + protected LinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs index d3b7d9e5b0e..3fb5cff9f0f 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/ReorderingVerificationGutterStatusTester.cs @@ -10,6 +10,7 @@ using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -138,7 +139,7 @@ async Task CompareWithExpectation(List expectedSymbols) { $"Expected {string.Join(", ", expectedSymbols)} but got {string.Join(", ", orderAfterChangeSymbols)}." + $"\nOld to new history was: {verificationStatusReceiver.History.Stringify()}"); } catch (OperationCanceledException) { - Console.WriteLine($"Operation cancelled for index {index} when expecting: {string.Join(", ", expectedSymbols)}"); + await output.WriteLineAsync($"Operation cancelled for index {index} when expecting: {string.Join(", ", expectedSymbols)}"); throw; } @@ -231,4 +232,7 @@ public async IAsyncEnumerable> GetRunningOrder(SemaphoreSlim semapho yield return newlyReported.ToList(); } while (!started || foundStatus.NamedVerifiables.Any(v => v.Status < PublishedVerificationStatus.Error)); } + + public ReorderingVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 184ece94a38..5371dec112a 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -1,6 +1,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics; @@ -210,4 +211,7 @@ await VerifyTrace(@" . | | | : true . | | | :}"); } + + public SimpleLinearVerificationGutterStatusTester(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs index 7b7566affc0..659711bbfac 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs @@ -9,6 +9,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class DefinitionTest : ClientBasedLanguageServerTest { @@ -462,5 +463,8 @@ method Q ... }".TrimStart(); await AssertPositionsLineUpWithRanges(source); } + + public DefinitionTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs index 6e1b7b8a03d..d116e7b328f 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs @@ -5,6 +5,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class DocumentSymbolTest : ClientBasedLanguageServerTest { @@ -150,5 +151,8 @@ public async Task CanResolveSymbolsForFunctionWithoutBody() { Assert.Equal(new Range((0, 9), (0, 17)), methodSymbol.SelectionRange); Assert.Equal(SymbolKind.Function, methodSymbol.Kind); } + + public DocumentSymbolTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index faa82646d0c..eb0c639f4f4 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -8,6 +8,7 @@ using System.Threading.Tasks; using JetBrains.Annotations; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Xunit.Abstractions; using Xunit; using XunitAssertMessages; @@ -500,6 +501,9 @@ method test(opt: int) { "); } + public HoverTest(ITestOutputHelper output) : base(output) { + } + [Fact] public async Task HoverShouldDisplayComments() { await AssertHover(@" diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index f3fb54a190e..875f772e10a 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -10,6 +10,7 @@ using OmniSharp.Extensions.JsonRpc; using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Xunit.Abstractions; using Xunit; using XunitAssertMessages; @@ -491,5 +492,8 @@ private Task RequestHover(TextDocumentItem documentItem, Position positio CancellationToken ); } + + public HoverVerificationTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs b/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs index 042bb2bdb87..5004fd263ac 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs @@ -5,6 +5,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class SignatureHelpTest : ClientBasedLanguageServerTest { @@ -189,5 +190,8 @@ method GetProduct(x: int, y: int) returns (p: int) Assert.Equal(MarkupKind.Markdown, markup.Kind); Assert.Equal("```dafny\nfunction A.Multiply(n: int, m: int): int\n```", markup.Value); } + + public SignatureHelpTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 984a601c35b..7037af3371c 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -3,6 +3,7 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest; @@ -30,4 +31,7 @@ public async Task ProjectFileOverridesOptions() { Assert.Empty(diagnostics); } + + public ProjectFilesTest(ITestOutputHelper output) : base(output) { + } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs index 11b04be4e46..ff6f881a7d4 100644 --- a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs +++ b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs @@ -1,14 +1,49 @@ +using System; +using System.IO; +using System.Text; using Microsoft.Dafny.LanguageServer.Workspace; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest; public class StandaloneServerTest { + private readonly TextWriter output; + + public StandaloneServerTest(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } [Fact] public void OptionParsing() { var arguments = new[] { "--documents:verify=onsave", "--verifier:timelimit=3", "--ghost:markStatements=true" }; - var options = Program.GetOptionsFromArgs(arguments); + var options = Program.GetOptionsFromArgs(output, TextReader.Null, arguments); Assert.Equal(VerifyOnMode.Save, options.Get(ServerCommand.Verification)); } } + +public class WriterFromOutputHelper : TextWriter { + private readonly ITestOutputHelper output; + private bool failed = false; + + public WriterFromOutputHelper(ITestOutputHelper output) { + this.output = output; + } + + public override void Write(char value) { + if (!failed) { + failed = true; + WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support."); + } + } + + public override Encoding Encoding => Encoding.Default; + + public override void WriteLine(string value) { + output.WriteLine(value); + } + + public override void WriteLine(string format, params object[] arg) { + output.WriteLine(format, arg); + } +} diff --git a/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs index cc33c64f470..7e9514183ac 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs @@ -4,6 +4,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class CloseDocumentTest : DafnyLanguageServerTestBase, IAsyncLifetime { @@ -46,5 +47,8 @@ function GetConstant(): int { await CloseDocumentAndWaitAsync(documentItem); Assert.Null(await Documents.GetResolvedDocumentAsync(documentItem.Uri)); } + + public CloseDocumentTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs index 4a13e98f748..de051bdddc6 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs @@ -6,6 +6,7 @@ using System.Linq; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class DeclarationLocationMigrationTest : SynchronizationTestBase { @@ -324,5 +325,8 @@ public async Task PassingANullChangeRangePreservesForeignSymbols() { Assert.NotNull(document); Assert.False(TryFindSymbolDeclarationByName(document, "A", out var _)); } + + public DeclarationLocationMigrationTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index 89a7f0b19bb..ee7f1308961 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -9,6 +9,7 @@ using System.Threading; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors; +using Xunit.Abstractions; using Xunit; using XunitAssertMessages; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -1130,5 +1131,8 @@ method Foo() { var diagnostics2 = await GetLastDiagnostics(documentItem, CancellationToken); Assert.True(diagnostics2.Any()); } + + public DiagnosticsTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs index cccd14fe4c0..2fb5eca0df8 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/GhostDiagnosticsTest.cs @@ -4,6 +4,7 @@ using System.Linq; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class GhostDiagnosticsTest : ClientBasedLanguageServerTest { @@ -192,5 +193,8 @@ await SetUp(options => { Assert.Equal("Ghost statement", diagnostics[3].Message); Assert.Equal(new Range((15, 4), (15, 14)), diagnostics[3].Range); } + + public GhostDiagnosticsTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs index 975d8228f9d..5fcd1b575c8 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs @@ -2,6 +2,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class LookupMigrationTest : SynchronizationTestBase { @@ -303,5 +304,8 @@ function GetY(): int { Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((12, 7), out var symbol)); Assert.Equal("x", symbol.Name); } + + public LookupMigrationTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs index c4fe5a4c245..fa8d704488f 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs @@ -6,6 +6,7 @@ using System.Threading.Tasks; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.IO; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { @@ -136,5 +137,8 @@ public async Task EmptyDocumentCanBeIncluded() { Assert.NotNull(document); Assert.True(!document.Diagnostics.Any()); } + + public OpenDocumentTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs index f590235261e..6df0d4fd4ab 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SaveDocumentTest.cs @@ -4,6 +4,7 @@ using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class SaveDocumentTest : ClientBasedLanguageServerTest { @@ -93,5 +94,8 @@ method DoIt() { var message = afterSaveDiagnostics.First(); Assert.Equal(MessageSource.Verifier.ToString(), message.Source); } + + public SaveDocumentTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs index 55f799d8147..a039523a411 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs @@ -4,6 +4,7 @@ using System.Linq; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class SymbolMigrationTest : SynchronizationTestBase { @@ -99,5 +100,8 @@ await ApplyChangeAndWaitCompletionAsync( Assert.True(document.SignatureAndCompletionTable.Resolved); Assert.Single(document.SignatureAndCompletionTable.Locations.Keys.OfType()); } + + public SymbolMigrationTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs b/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs index 98ad629af14..3bc05daa08a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs @@ -4,12 +4,13 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class SynchronizationTestBase : DafnyLanguageServerTestBase, IAsyncLifetime { protected ILanguageClient Client { get; set; } - public async virtual Task InitializeAsync() { + public virtual async Task InitializeAsync() { Client = await InitializeClient(); } @@ -37,5 +38,8 @@ protected Task ApplyChangesAndWaitCompletionAsync(TextDocumentItem documentItem, }); return Client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken); } + + public SynchronizationTestBase(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs index 4b5c0bd1c37..b100816268e 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs @@ -2,6 +2,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class TextInsertionTest : SynchronizationTestBase { @@ -199,5 +200,8 @@ function GetConstant(): int { 1 } }".TrimStart(); Assert.Equal(expected, document.TextDocumentItem.Text); } + + public TextInsertionTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs index db9ff08fac9..b83f6b33b37 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs @@ -2,6 +2,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization { public class TextReplacementTest : SynchronizationTestBase { @@ -252,5 +253,8 @@ public async Task ReplaceCompleteDocumentContent() { Assert.NotNull(document); Assert.Equal(change, document.TextDocumentItem.Text); } + + public TextReplacementTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 3c66308d45a..f339b395227 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -7,6 +7,7 @@ using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; @@ -536,4 +537,7 @@ public async Task SymbolStatusIsMigrated() { var errorStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(migratedRange, errorStatus.NamedVerifiables[0].NameRange); } + + public VerificationStatusTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index 78064d39e00..e6ed3d57b10 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -9,6 +9,7 @@ using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; @@ -29,8 +30,8 @@ public IDisposable BeginScope(TState state) { } } - public GhostStateDiagnosticCollectorTest() { - var options = new DafnyOptions(); + public GhostStateDiagnosticCollectorTest(ITestOutputHelper output) { + var options = new DafnyOptions(TextReader.Null, new WriterFromOutputHelper(output), new WriterFromOutputHelper(output)); options.Set(ServerCommand.GhostIndicators, true); ghostStateDiagnosticCollector = new GhostStateDiagnosticCollector( options, diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 45549e7cc00..99b23a347af 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -1,11 +1,12 @@ using System; using System.Collections.Generic; using Microsoft.Dafny.LanguageServer.Language; -using System.Threading; +using System.IO; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit { @@ -16,9 +17,9 @@ public class ParserExceptionTest { private DafnyLangParser parser; private LastDebugLogger lastDebugLogger; - public ParserExceptionTest() { + public ParserExceptionTest(ITestOutputHelper output) { lastDebugLogger = new LastDebugLogger(); - parser = DafnyLangParser.Create(DafnyOptions.Create(), lastDebugLogger); + parser = DafnyLangParser.Create(DafnyOptions.Create(new WriterFromOutputHelper(output)), lastDebugLogger); } [Fact(Timeout = MaxTestExecutionTimeMs)] diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 09e446c2d1e..67d4097e263 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -4,14 +4,18 @@ using Moq; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System; +using System.IO; using System.Threading; using System.Threading.Tasks; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit { public class TextDocumentLoaderTest { + private readonly TextWriter output; + private Mock parser; private Mock symbolResolver; private Mock symbolTableFactory; @@ -21,7 +25,8 @@ public class TextDocumentLoaderTest { private Mock logger; private Mock diagnosticPublisher; - public TextDocumentLoaderTest() { + public TextDocumentLoaderTest(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); parser = new(); symbolResolver = new(); symbolTableFactory = new(); @@ -30,7 +35,7 @@ public TextDocumentLoaderTest() { logger = new Mock(); diagnosticPublisher = new Mock(); textDocumentLoader = TextDocumentLoader.Create( - DafnyOptions.Create(), + DafnyOptions.Create(this.output, TextReader.Null), parser.Object, symbolResolver.Object, symbolTableFactory.Object, diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 17f894f43a7..84cfae5a31e 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -12,6 +12,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Client; using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Xunit.Abstractions; using Xunit; using XunitAssertMessages; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -188,4 +189,7 @@ public async Task PopNextStatus() { Assert.Equal(1, nextNotification.NamedVerifiables.Count); return nextNotification.NamedVerifiables.Single().Status; } + + public ClientBasedLanguageServerTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs b/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs index 987746a5d8c..d0370b9518d 100644 --- a/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/MarkupTestFileTest.cs @@ -4,7 +4,6 @@ using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util; - public class MarkupTestFileTest { [Fact] public void AnnotatedSpan() { diff --git a/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs index 8ec9c69175b..fcb5527a26b 100644 --- a/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs @@ -6,6 +6,7 @@ using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { @@ -100,5 +101,8 @@ private async Task AssertNothingIsQueued(TextDocumentItem documentItem) { status = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); } } + + public CancelVerificationTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index 9be08a7ede7..e451437e480 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -9,6 +9,7 @@ using JetBrains.Annotations; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { [Collection("Sequential Collection")] // Sequential because we saw test failures after switching to parallel execution @@ -198,5 +199,8 @@ lemma Something(i: int) await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.ParsingFailed); } + + public CompilationStatusNotificationTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs index 214f8ff4526..749ede2ee50 100644 --- a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs @@ -9,6 +9,7 @@ using System.Threading; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { @@ -178,5 +179,8 @@ decreases y } await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout); } + + public ConcurrentInteractionsTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs index 05212317711..87623d8ab90 100644 --- a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs @@ -9,6 +9,7 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { static class StringAssert { @@ -1160,5 +1161,8 @@ public void TestIsNegativeIndexedSeq() { Assert.True( IsNegativeIndexedSeq(new KeyValuePair("seq>", "(Length := 1123, [(- 12345)] := @12)"))); } + + public CounterExampleTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs index 9a43eaebda6..f5a043bb4b3 100644 --- a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs @@ -6,6 +6,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -158,4 +159,7 @@ public async Task VerificationDiagnosticsDoNotShowUpTwice() { Assert.Equal(verificationDiagnostics[0].Message, verificationDiagnostics2[0].Message); await AssertNoDiagnosticsAreComing(CancellationToken); } + + public DiagnosticMigrationTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index f18d1caf969..021f7e6e0f6 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -12,6 +12,7 @@ using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Server; using Xunit; +using Xunit.Abstractions; using LanguageServerExtensions = Microsoft.Dafny.LanguageServer.Workspace.LanguageServerExtensions; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -131,4 +132,7 @@ public Task LoadAsync(DafnyOptions options, DocumentTextBu return loader.LoadAsync(options, textDocument, cancellationToken); } } + + public ExceptionTests(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs index f92d6d5a8cc..36c1753d747 100644 --- a/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/IncludeFileTest.cs @@ -4,6 +4,7 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -40,4 +41,7 @@ ensures Foo(x) {{ Assert.Single(verificationDiagnostics); await AssertNoDiagnosticsAreComing(CancellationToken); } + + public IncludeFileTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs b/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs index 2a6d5497be4..5004cda00e3 100644 --- a/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs @@ -3,6 +3,7 @@ using System.IO; using System.Linq; using System.Threading.Tasks; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { @@ -53,5 +54,8 @@ method Test() { Assert.NotNull(document); Assert.Single(document.Diagnostics); } + + public MultiFileTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs index 58ad75e2e9e..c33c3fae451 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsAdvancedTest.cs @@ -2,6 +2,7 @@ using System.Threading.Tasks; using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Xunit.Abstractions; using Xunit; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -38,4 +39,7 @@ public async Task EnsureErrorMessageCanBeComplexAndTakeIntoAccountConfiguration( Assert.Equal(new Range((3, 15), (3, 32)), related.Current.Location.Range); related.Dispose(); } + + public PluginsAdvancedTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs index 4e69346ccd9..2fd10d008f3 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsCodeActionTest.cs @@ -3,6 +3,7 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using OmniSharp.Extensions.LanguageServer.Protocol.Document; using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -32,4 +33,7 @@ method firstMethod() { Assert.Equal("Insert file header", codeAction.Title); // The rest is tested elsewhere } + + public PluginsDafnyCodeActionTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs index ae80698d523..d2872ba5fba 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTest.cs @@ -2,6 +2,7 @@ using System.Threading.Tasks; using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Xunit.Abstractions; using Xunit; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -27,4 +28,7 @@ public async Task EnsureItIsPossibleToLoadAPluginWithArguments() { Assert.Equal("Impossible to continue because\\ \"whatever", diagnostics[0].Message); Assert.Equal(new Range((0, 0), (0, 8)), diagnostics[0].Range); } + + public PluginsTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs index a894feb7d46..ece6f55460c 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs @@ -7,6 +7,7 @@ using Microsoft.CodeAnalysis; using Microsoft.CodeAnalysis.CSharp; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Xunit.Abstractions; using Xunit; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -73,4 +74,7 @@ void ModifyOptions(DafnyOptions options) { } return base.SetUp(ModifyOptions); } + + protected PluginsTestBase(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs b/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs index 9ba519fa654..e536d99ca5f 100644 --- a/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs +++ b/Source/DafnyLanguageServer.Test/Various/PluginsTestWithVerification.cs @@ -3,6 +3,7 @@ using System.Threading; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Xunit; +using Xunit.Abstractions; using XunitAssertMessages; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -32,4 +33,7 @@ public async Task EnsureItIsPossibleToLoadAPluginAndContinueVerification() { Assert.Equal("value does not satisfy the subset constraints of 'nat'", diagnostics[1].Message); Assert.Equal(new Range((0, 23), (0, 24)), diagnostics[1].Range); } + + public PluginsTestWithVerification(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs b/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs index 4cfddb97031..b91e02ae970 100644 --- a/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ResourceUsageTest.cs @@ -4,6 +4,7 @@ using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various; @@ -30,4 +31,7 @@ method Foo() var processes3 = Process.GetProcessesByName(solverProcessName); Assert.Equal(processes2.Length, processes3.Length); } + + public ResourceUsageTest(ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs b/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs index 027317dae35..bbef0eb8d29 100644 --- a/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs @@ -4,6 +4,7 @@ using System.IO; using System.Threading.Tasks; using Xunit; +using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { /// @@ -57,5 +58,8 @@ method NestedExpression() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); Assert.NotNull(await Documents.GetResolvedDocumentAsync(documentItem.Uri)); } + + public StabilityTest(ITestOutputHelper output) : base(output) { + } } } diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs index 6c61023d9e7..7bd953f0ef0 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs @@ -916,14 +916,14 @@ private List GetFieldNames(Model.Element elt) { if (i == 0) { dimTuple = fIndexField.AppWithResult(elt); if (dimTuple == null) { - Console.Out.WriteLine(PleaseEnableModelCompressFalse); + options.OutputWriter.WriteLine(PleaseEnableModelCompressFalse); continue; } indices[i] = dimTuple.Args[0]; } else { dimTuple = fMultiIndexField.AppWithResult(elt); if (dimTuple == null) { - Console.Out.WriteLine(PleaseEnableModelCompressFalse); + options.OutputWriter.WriteLine(PleaseEnableModelCompressFalse); continue; } indices[i] = dimTuple.Args[1]; diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index f8478a4b732..ff342e00ee2 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -140,7 +140,7 @@ private bool TryParseInclude(Include include, ModuleDecl module, BuiltIns builtI try { var dafnyFile = new DafnyFile(builtIns.Options, include.IncludedFilename); int errorCount = Parser.Parse( - useStdin: false, + (TextReader)null!, dafnyFile.Uri, module, builtIns, diff --git a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs index cff182d2f23..375fa7b3021 100644 --- a/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs +++ b/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs @@ -37,7 +37,6 @@ DafnyOptions options } private const int TranslatorMaxStackSize = 0x10000000; // 256MB - static readonly ThreadTaskScheduler TranslatorScheduler = new(TranslatorMaxStackSize); public async Task> GetVerificationTasksAsync(DocumentAfterResolution document, CancellationToken cancellationToken) { @@ -46,10 +45,10 @@ public async Task> GetVerificationTasksAsync( cancellationToken.ThrowIfCancellationRequested(); - var translated = await Task.Factory.StartNew(() => Translator.Translate(program, errorReporter, new Translator.TranslatorFlags(errorReporter.Options) { + var translated = await DafnyMain.LargeStackFactory.StartNew(() => Translator.Translate(program, errorReporter, new Translator.TranslatorFlags(errorReporter.Options) { InsertChecksums = true, ReportRanges = true - }).ToList(), cancellationToken, TaskCreationOptions.None, TranslatorScheduler); + }).ToList(), cancellationToken); cancellationToken.ThrowIfCancellationRequested(); diff --git a/Source/DafnyLanguageServer/StandaloneServerCli.cs b/Source/DafnyLanguageServer/StandaloneServerCli.cs index cd898823a0c..b4895fd62ee 100644 --- a/Source/DafnyLanguageServer/StandaloneServerCli.cs +++ b/Source/DafnyLanguageServer/StandaloneServerCli.cs @@ -16,15 +16,15 @@ namespace Microsoft.Dafny.LanguageServer { public class Program { public static async Task Main(string[] args) { - var dafnyOptions = GetOptionsFromArgs(args); + var dafnyOptions = GetOptionsFromArgs(Console.Out, Console.In, args); await Server.Start(dafnyOptions); } - public static DafnyOptions GetOptionsFromArgs(string[] args) { + public static DafnyOptions GetOptionsFromArgs(TextWriter outWriter, TextReader input, string[] args) { var configuration = CreateConfiguration(args); - var dafnyOptions = DafnyOptions.Create(); + var dafnyOptions = DafnyOptions.Create(outWriter, input); var verifierOptions = new VerifierOptions(); configuration.Bind(VerifierOptions.Section, verifierOptions); diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 5c0fe1e00e8..ee70d061f4e 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -21,7 +21,6 @@ namespace Microsoft.Dafny.LanguageServer.Workspace { /// public class TextDocumentLoader : ITextDocumentLoader { private const int ResolverMaxStackSize = 0x10000000; // 256MB - private static readonly ThreadTaskScheduler ResolverScheduler = new(ResolverMaxStackSize); private readonly IDafnyParser parser; private readonly ISymbolResolver symbolResolver; @@ -75,10 +74,10 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke public async Task LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument, CancellationToken cancellationToken) { #pragma warning disable CS1998 - return await await Task.Factory.StartNew( - async () => LoadInternal(options, textDocument, cancellationToken), cancellationToken, + return await await DafnyMain.LargeStackFactory.StartNew( + async () => LoadInternal(options, textDocument, cancellationToken), cancellationToken #pragma warning restore CS1998 - TaskCreationOptions.None, ResolverScheduler); + ); } private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuffer textDocument, diff --git a/Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs b/Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs deleted file mode 100644 index bf3c67e48fa..00000000000 --- a/Source/DafnyLanguageServer/Workspace/ThreadTaskScheduler.cs +++ /dev/null @@ -1,42 +0,0 @@ -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Threading; -using System.Threading.Tasks; - -namespace Microsoft.Dafny.LanguageServer.Workspace; - -/// -/// Each queued task runs on a newly-created thread with the required -/// stack size. The default .NET task scheduler is built on the .NET -/// ThreadPool. Its policy allows it to create thousands of threads -/// if it chooses. -/// -public class ThreadTaskScheduler : TaskScheduler { - private readonly int stackSize; - - public ThreadTaskScheduler(int stackSize) { - Contract.Requires(stackSize >= 0); - - this.stackSize = stackSize; - } - - protected override IEnumerable GetScheduledTasks() { - // There is never a queue of scheduled, but not running, tasks. - // So return an empty list. - return new List(); - } - - protected override void QueueTask(Task task) { - Thread th = new Thread(TaskMain!, stackSize); - th.Start(task); - } - - protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued) { - return false; - } - - private void TaskMain(object data) { - Task t = (Task)data; - TryExecuteTask(t); - } -} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs index ed05e0cd6ef..e0ac3d71d56 100644 --- a/Source/DafnyPipeline.Test/DocstringTest.cs +++ b/Source/DafnyPipeline.Test/DocstringTest.cs @@ -8,6 +8,7 @@ using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test { @@ -20,12 +21,18 @@ namespace DafnyPipeline.Test { // Every test is performed with all three newline styles // Every formatted program is formatted again to verify that it stays the same. public class DocstringTest { + private readonly ITestOutputHelper output; + enum Newlines { LF, CR, CRLF }; + public DocstringTest(ITestOutputHelper output) { + this.output = output; + } + private Newlines currentNewlines; [Fact] @@ -419,7 +426,7 @@ protected void DocstringWorksFor(string source, string nodeTokenValue, string? e } protected void DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(new WriterFromOutputHelper(output)); var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { currentNewlines = newLinesType; @@ -454,4 +461,4 @@ private string AdjustNewlines(string programString) { }; } } -} +} \ No newline at end of file diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index e93d7ecfa49..aab142263fd 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -1,18 +1,14 @@ #nullable enable using System; -using System.Collections; using System.Collections.Generic; -using System.Linq; -using System.Diagnostics.Contracts; using System.IO; using System.Text.RegularExpressions; using DafnyTestGeneration; -using JetBrains.Annotations; using Bpl = Microsoft.Boogie; using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; -using Main = Microsoft.Dafny.Main; +using Xunit.Abstractions; namespace DafnyPipeline.Test { @@ -25,6 +21,12 @@ namespace DafnyPipeline.Test { // Every test is performed with all three newline styles // Every formatted program is formatted again to verify that it stays the same. public class FormatterBaseTest { + private readonly TextWriter output; + + public FormatterBaseTest(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } + enum Newlines { LF, CR, @@ -39,7 +41,7 @@ enum Newlines { protected void FormatterWorksFor(string testCase, string? expectedProgramString = null, bool expectNoToken = false, bool reduceBlockiness = true) { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(output); var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { currentNewlines = newLinesType; @@ -81,13 +83,13 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString } // Formatting should work after resolution as well. - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); reprinted = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness)) : programString; if (expectedProgram != reprinted) { - Console.Error.WriteLine("Formatting after resolution generates an error:"); + options.ErrorWriter.WriteLine("Formatting after resolution generates an error:"); Assert.Equal(expectedProgram, reprinted); } var initErrorCount = reporter.ErrorCount; diff --git a/Source/DafnyPipeline.Test/FormatterComprehensions.cs b/Source/DafnyPipeline.Test/FormatterComprehensions.cs index 0e5108c9734..1795182fad9 100644 --- a/Source/DafnyPipeline.Test/FormatterComprehensions.cs +++ b/Source/DafnyPipeline.Test/FormatterComprehensions.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -208,4 +210,6 @@ function test(): int { } -} \ No newline at end of file + public FormatterForComprehensions([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs b/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs index 5839cde9692..dc47cd7e198 100644 --- a/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs +++ b/Source/DafnyPipeline.Test/FormatterForApplySuffixRelated.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -40,4 +42,7 @@ method Test() } "); } -} \ No newline at end of file + + public FormatterForApplySuffixRelated([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForAssignments.cs b/Source/DafnyPipeline.Test/FormatterForAssignments.cs index 57a2d3ffe91..25b53785b59 100644 --- a/Source/DafnyPipeline.Test/FormatterForAssignments.cs +++ b/Source/DafnyPipeline.Test/FormatterForAssignments.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -179,4 +181,7 @@ method Test() { } ", reduceBlockiness: false); } -} \ No newline at end of file + + public FormatterForAssignments([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs b/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs index fb2b320a1b0..16b74ec76d4 100644 --- a/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs +++ b/Source/DafnyPipeline.Test/FormatterForCalcStmt.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -27,4 +29,7 @@ assert true by { } "); } -} \ No newline at end of file + + public FormatterForCalcStmt([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForComments.cs b/Source/DafnyPipeline.Test/FormatterForComments.cs index 2aba9ca3b10..b346ba1ba4d 100644 --- a/Source/DafnyPipeline.Test/FormatterForComments.cs +++ b/Source/DafnyPipeline.Test/FormatterForComments.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -269,4 +271,6 @@ public void FormatterWorksForUtf8InComment() { "); } -} \ No newline at end of file + public FormatterForComments([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs b/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs index 2f3f37ae060..aa9ca091f33 100644 --- a/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs +++ b/Source/DafnyPipeline.Test/FormatterForDatatypeDeclarationTest.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -144,4 +146,6 @@ public void FormatterWorksForSingleDatatypeConstructor() { ", reduceBlockiness: false); } -} \ No newline at end of file + public FormatterForDatatypeDeclarationTest([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForExpressions.cs b/Source/DafnyPipeline.Test/FormatterForExpressions.cs index 22973b02c56..380062015cc 100644 --- a/Source/DafnyPipeline.Test/FormatterForExpressions.cs +++ b/Source/DafnyPipeline.Test/FormatterForExpressions.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -377,4 +379,6 @@ predicate Valid() FormatterWorksFor(testCase, testCase); } -} \ No newline at end of file + public FormatterForExpressions([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForMembers.cs b/Source/DafnyPipeline.Test/FormatterForMembers.cs index 1a0c260d39b..7caa40515a3 100644 --- a/Source/DafnyPipeline.Test/FormatterForMembers.cs +++ b/Source/DafnyPipeline.Test/FormatterForMembers.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -262,6 +264,6 @@ method Main() { } - - -} \ No newline at end of file + public FormatterForMembers([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForSpecifications.cs b/Source/DafnyPipeline.Test/FormatterForSpecifications.cs index e715870ba40..91037888f1a 100644 --- a/Source/DafnyPipeline.Test/FormatterForSpecifications.cs +++ b/Source/DafnyPipeline.Test/FormatterForSpecifications.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -268,4 +270,6 @@ class TestClass { } -} \ No newline at end of file + public FormatterForSpecifications([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForStatements.cs b/Source/DafnyPipeline.Test/FormatterForStatements.cs index 9f1ef494b8f..c04ea0500d8 100644 --- a/Source/DafnyPipeline.Test/FormatterForStatements.cs +++ b/Source/DafnyPipeline.Test/FormatterForStatements.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -432,4 +434,7 @@ method Test() { "; FormatterWorksFor(test, test); } -} \ No newline at end of file + + public FormatterForStatements([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs index b0c423b0f91..d5429cfed98 100644 --- a/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs +++ b/Source/DafnyPipeline.Test/FormatterForTopLevelDeclarations.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -346,4 +348,7 @@ method M... } "); } -} \ No newline at end of file + + public FormatterForTopLevelDeclarations([NotNull] ITestOutputHelper output) : base(output) { + } +} diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs index 41c2a2489c9..73549f96ec2 100644 --- a/Source/DafnyPipeline.Test/FormatterIssues.cs +++ b/Source/DafnyPipeline.Test/FormatterIssues.cs @@ -1,4 +1,6 @@ -using Xunit; +using JetBrains.Annotations; +using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test; @@ -127,4 +129,7 @@ public void FormatterWorksForEmptyDocument() { FormatterWorksFor(@" ", null, true); } + + public FormatterIssues([NotNull] ITestOutputHelper output) : base(output) { + } } diff --git a/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs b/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs index bbd357c5a2f..0298cee3ede 100644 --- a/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs +++ b/Source/DafnyPipeline.Test/InterMethodVerificationStability.cs @@ -8,12 +8,15 @@ using DiffPlex.DiffBuilder.Model; using Microsoft.VisualStudio.TestPlatform.PlatformAbstractions; using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test { // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) // so we can't execute tests that use it in parallel. [Collection("Singleton Test Collection - Resolution")] public class InterMethodVerificationStability { + private readonly ITestOutputHelper output; + [Fact] public void CreatingBoogieVariableNameCollisionsHasExpectedDiff() { var beforeChange = @" @@ -183,6 +186,10 @@ static InterMethodVerificationStability() { private static readonly string dafnyDirectory; + public InterMethodVerificationStability(ITestOutputHelper output) { + this.output = output; + } + private static string DafnyProjectFile => Path.Combine(dafnyDirectory, "Source", "Dafny", "Dafny.csproj"); private static string DefaultDafnyArgs => $"run --no-build --project {DafnyProjectFile} -- -useBaseNameForFileName -compileVerbose:0 /errorTrace:0"; @@ -201,11 +208,10 @@ string GetBoogie(string dafnyProgram, string optionalFileName = null) { dafnyProcess.WaitForExit(); if (dafnyProcess.ExitCode != 0) { - Console.Out.WriteLine("Arguments:", processStartInfo.Arguments); - Console.Out.WriteLine("Result:"); - Console.Out.WriteLine(result); - Console.Out.WriteLine(dafnyProcess.StandardError.ReadToEnd()); - Console.Out.Flush(); + output.WriteLine("Arguments:", processStartInfo.Arguments); + output.WriteLine("Result:"); + output.WriteLine(result); + output.WriteLine(dafnyProcess.StandardError.ReadToEnd()); } Assert.Equal(4, dafnyProcess.ExitCode); return result; diff --git a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs index 556183c4f0a..3d5fd272f72 100644 --- a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs +++ b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs @@ -1,8 +1,6 @@ -using System; using System.Collections.Generic; using System.IO; using System.Linq; -using System.Threading; using System.Threading.Tasks; using DafnyTestGeneration; using Microsoft.Boogie; @@ -10,14 +8,13 @@ using Xunit; using Xunit.Abstractions; using BoogieProgram = Microsoft.Boogie.Program; -using Main = Microsoft.Dafny.Main; -using Parser = Microsoft.Dafny.Parser; namespace DafnyPipeline.Test { // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) // so we can't execute tests that use it in parallel. [Collection("Singleton Test Collection - Resolution")] public class IntraMethodVerificationStability { + private readonly ITestOutputHelper testOutputHelper; // All types of top level declarations. @@ -151,7 +148,7 @@ public IntraMethodVerificationStability(ITestOutputHelper testOutputHelper) { [Fact] public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); var regularBoogie = GetBoogie(options, originalProgram).ToList(); var renamedBoogie = GetBoogie(options, renamedProgram).ToList(); @@ -167,7 +164,7 @@ public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() { [Fact] public async Task EqualProverLogWhenReorderingProgram() { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); options.ProcsToCheck.Add("SomeMethod*"); var reorderedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, reorderedProgram)); @@ -177,7 +174,7 @@ public async Task EqualProverLogWhenReorderingProgram() { [Fact] public async Task EqualProverLogWhenRenamingProgram() { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); options.ProcsToCheck.Add("*SomeMethod*"); var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram)); @@ -188,7 +185,7 @@ public async Task EqualProverLogWhenRenamingProgram() { [Fact] public async Task EqualProverLogWhenAddingUnrelatedProgram() { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper)); options.ProcsToCheck.Add("*SomeMethod *"); var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram + originalProgram)); @@ -211,7 +208,7 @@ private async IAsyncEnumerable GetProverLogsForProgramAsync(DafnyOptions options.ProverLogFilePath = temp1; using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) { foreach (var boogieProgram in boogiePrograms) { - var (outcome, _) = await Main.BoogieOnce(options, Console.Out, engine, "", "", boogieProgram, "programId"); + var (outcome, _) = await DafnyMain.BoogieOnce(options, options.OutputWriter, engine, "", "", boogieProgram, "programId"); testOutputHelper.WriteLine("outcome: " + outcome); } } @@ -239,7 +236,7 @@ IEnumerable GetBoogie(DafnyOptions options, string dafnyProgramTe var dafnyProgram = Utils.Parse(options, dafnyProgramText, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; Assert.NotNull(dafnyProgram); - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCount); return Translator.Translate(dafnyProgram, reporter).Select(t => t.Item2).ToList(); } diff --git a/Source/DafnyPipeline.Test/Issue1355.cs b/Source/DafnyPipeline.Test/Issue1355.cs index 84dae7e1560..8ac93cd5c8e 100644 --- a/Source/DafnyPipeline.Test/Issue1355.cs +++ b/Source/DafnyPipeline.Test/Issue1355.cs @@ -1,28 +1,30 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Diagnostics.Contracts; using System.IO; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; -using Main = Microsoft.Dafny.Main; +using Xunit.Abstractions; namespace DafnyPipeline.Test { // Main.Resolve has static shared state (TypeConstraint.ErrorsToBeReported for example) // so we can't execute tests that use it in parallel. [Collection("Singleton Test Collection - Resolution")] public class Issue1355 { + private readonly TextWriter output; + + public Issue1355(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } + [Fact] public void Test() { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(output); options.DafnyPrelude = "../../../../../Binaries/DafnyPrelude.bpl"; var programString = @"trait Trait { }"; var dafnyProgram = Utils.Parse(options, programString, false); - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); foreach (var prog in Translator.Translate(dafnyProgram, dafnyProgram.Reporter)) { var writer = new StringWriter(); var tokenWriter = new Bpl.TokenTextWriter("virtual", writer, true, options); diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index bdc421ef811..f324fd8362d 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -7,12 +7,18 @@ using Microsoft.CodeAnalysis.CSharp; using Xunit; using Microsoft.Dafny; -using Main = Microsoft.Dafny.Main; +using Xunit.Abstractions; namespace DafnyPipeline.Test; [Collection("Dafny plug-ins tests")] public class PluginsTest { + private readonly TextWriter output; + + public PluginsTest(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } + /// /// This method creates a library and returns the path to that library. /// The library extends a Rewriter so that we can verify that Dafny invokes it if provided in argument. @@ -51,13 +57,13 @@ private string GetLibrary(string name) { public void EnsurePluginIsExecuted() { var library = GetLibrary("rewriterPreventingVerificationWithArgument"); - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(output); options.Plugins.Add(AssemblyPlugin.Load(library, new string[] { "because whatever" })); var programString = "function test(): int { 1 }"; var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); Assert.Equal(1, reporter.Count(ErrorLevel.Error)); Assert.Equal("Impossible to continue because whatever", reporter.AllMessages[ErrorLevel.Error][0].Message); @@ -67,13 +73,13 @@ public void EnsurePluginIsExecuted() { public void EnsurePluginIsExecutedEvenWithoutConfiguration() { var library = GetLibrary("rewriterPreventingVerification"); - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(output); options.Plugins.Add(AssemblyPlugin.Load(library, new string[] { "ignored arguments" })); var programString = "function test(): int { 1 }"; var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); Assert.Equal(1, reporter.ErrorCount); Assert.Equal("Impossible to continue", reporter.AllMessages[ErrorLevel.Error][0].Message); } @@ -82,13 +88,13 @@ public void EnsurePluginIsExecutedEvenWithoutConfiguration() { public void EnsurePluginIsExecutedAndAllowsVerification() { var library = GetLibrary("rewriterAllowingVerification"); - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(output); options.Plugins.Add(AssemblyPlugin.Load(library, new string[] { "ignored arguments" })); var programString = "function test(): int { 1 }"; var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); Assert.Equal(0, reporter.ErrorCountUntilResolver); Assert.Equal(1, reporter.ErrorCount); } diff --git a/Source/DafnyPipeline.Test/RelativePaths.cs b/Source/DafnyPipeline.Test/RelativePaths.cs index 2bd258f6ce1..4d71cc07d1d 100644 --- a/Source/DafnyPipeline.Test/RelativePaths.cs +++ b/Source/DafnyPipeline.Test/RelativePaths.cs @@ -1,14 +1,22 @@ using System.IO; using Microsoft.Dafny; using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test { [Collection("Singleton Test Collection - Resolution")] public class RelativePaths { + private readonly TextWriter output; + + public RelativePaths(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } + [Fact] public void Test() { - Assert.Equal(0, DafnyDriver.ThreadMain(new string[] { "/spillTargetCode:3", "warnings-as-errors.dfy" })); + Assert.Equal(0, DafnyDriver.MainWithWriters(output, output, + TextReader.Null, new[] { "/spillTargetCode:3", "warnings-as-errors.dfy" })); } [Fact] diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index f56f823039b..93e6190a14c 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -1,9 +1,7 @@ using System; using System.Collections.Generic; -using System.Diagnostics; using System.IO; using System.Linq; -using Microsoft.CodeAnalysis; using Bpl = Microsoft.Boogie; using Xunit; using Microsoft.Dafny; @@ -75,7 +73,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption } var expectedLine = program.Split("// Here")[0].Count(c => c == '\n') + 1; Microsoft.Dafny.Type.ResetScopes(); - options = options ?? new DafnyOptions(); + options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); var uri = new Uri("virtual:///virtual"); var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); var module = new LiteralModuleDecl(defaultModuleDefinition, null); @@ -87,7 +85,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); } - Main.Resolve(dafnyProgram); + DafnyMain.Resolve(dafnyProgram); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs index 3e92e11f53e..d67c093591b 100644 --- a/Source/DafnyPipeline.Test/Trivia.cs +++ b/Source/DafnyPipeline.Test/Trivia.cs @@ -1,7 +1,5 @@ using System; using System.Collections.Generic; -using System.Linq; -using System.Diagnostics.Contracts; using System.IO; using System.Text.RegularExpressions; using DafnyTestGeneration; @@ -9,17 +7,25 @@ using BplParser = Microsoft.Boogie.Parser; using Microsoft.Dafny; using Xunit; +using Xunit.Abstractions; namespace DafnyPipeline.Test { [Collection("Singleton Test Collection - Trivia")] public class Trivia { + + private readonly TextWriter output; + + public Trivia(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } + enum Newlines { LF, CR, CRLF }; private Newlines currentNewlines; [Fact] public void TriviaSplitWorksOnLinuxMacAndWindows() { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(output); foreach (Newlines newLinesType in Enum.GetValues(typeof(Newlines))) { currentNewlines = newLinesType; var programString = @" diff --git a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs b/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs new file mode 100644 index 00000000000..c8159df29ef --- /dev/null +++ b/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs @@ -0,0 +1,30 @@ +#nullable enable +using System.IO; +using System.Text; +using Xunit.Abstractions; + +public class WriterFromOutputHelper : TextWriter { + private readonly ITestOutputHelper output; + private bool failed = false; + + public WriterFromOutputHelper(ITestOutputHelper output) { + this.output = output; + } + + public override void Write(char value) { + if (!failed) { + failed = true; + WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support."); + } + } + + public override Encoding Encoding => Encoding.Default; + + public override void WriteLine(string? value) { + output.WriteLine(value); + } + + public override void WriteLine(string format, params object?[] arg) { + output.WriteLine(format, arg); + } +} \ No newline at end of file diff --git a/Source/DafnyServer/CounterExampleProvider.cs b/Source/DafnyServer/CounterExampleProvider.cs index ca135d26e9d..2547adb2097 100644 --- a/Source/DafnyServer/CounterExampleProvider.cs +++ b/Source/DafnyServer/CounterExampleProvider.cs @@ -12,9 +12,13 @@ using Microsoft.Dafny; namespace DafnyServer { - public class CounterExampleProvider { + public sealed class CounterExampleProvider { private const int maximumCounterexampleDepth = 5; - public const string ModelBvd = "./model.bvd"; + public readonly string ModelBvd; + + public CounterExampleProvider() { + ModelBvd = $"./model{GetHashCode()}.bvd"; + } public CounterExample LoadCounterModel(DafnyOptions options) { try { @@ -25,7 +29,7 @@ public CounterExample LoadCounterModel(DafnyOptions options) { } } - private static List LoadModelFromFile(DafnyOptions options) { + private List LoadModelFromFile(DafnyOptions options) { using var wr = new StreamReader(ModelBvd); var output = wr.ReadToEnd(); var models = ExtractModels(output); diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 013f0214eca..51ddc093398 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -23,6 +23,7 @@ class DafnyHelper { private ErrorReporter reporter; private Program dafnyProgram; private IEnumerable> boogiePrograms; + private readonly CounterExampleProvider counterExampleProvider = new(); public DafnyHelper(DafnyOptions options, ExecutionEngine engine, string[] args, string fname, string source) { this.options = options; @@ -44,7 +45,7 @@ private bool Parse() { reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); BuiltIns builtIns = new BuiltIns(options); var success = (Parser.Parse(source, uri, module, builtIns, new Errors(reporter)) == 0 && - Main.ParseIncludesDepthFirstNotCompiledFirst(module, builtIns, new HashSet(), new Errors(reporter)) == null); + DafnyMain.ParseIncludesDepthFirstNotCompiledFirst(Console.In, module, builtIns, new HashSet(), new Errors(reporter)) == null); if (success) { dafnyProgram = new Program(fname, module, builtIns, reporter); } @@ -71,7 +72,7 @@ private bool BoogieOnce(string moduleName, Bpl.Program boogieProgram) { engine.Inline(boogieProgram); //NOTE: We could capture errors instead of printing them (pass a delegate instead of null) - switch (engine.InferAndVerify(Console.Out, boogieProgram, new PipelineStatistics(), + switch (engine.InferAndVerify(options.OutputWriter, boogieProgram, new PipelineStatistics(), #pragma warning disable VSTHRD002 "ServerProgram_" + moduleName, null, DateTime.UtcNow.Ticks.ToString()).Result) { #pragma warning restore VSTHRD002 @@ -105,11 +106,10 @@ public void Symbols() { public void CounterExample() { var listArgs = args.ToList(); - listArgs.Add("/mv:" + CounterExampleProvider.ModelBvd); + listArgs.Add("/mv:" + counterExampleProvider.ModelBvd); ServerUtils.ApplyArgs(listArgs.ToArray(), options); try { if (Parse() && Resolve() && Translate()) { - var counterExampleProvider = new CounterExampleProvider(); foreach (var boogieProgram in boogiePrograms) { RemoveExistingModel(); BoogieOnce(boogieProgram.Item1, boogieProgram.Item2); @@ -123,8 +123,8 @@ public void CounterExample() { } private void RemoveExistingModel() { - if (File.Exists(CounterExampleProvider.ModelBvd)) { - File.Delete(CounterExampleProvider.ModelBvd); + if (File.Exists(counterExampleProvider.ModelBvd)) { + File.Delete(counterExampleProvider.ModelBvd); } } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 07dd05391d7..fa19359990f 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -13,7 +13,7 @@ public class Server { private readonly ExecutionEngine engine; public static void Main(string[] args) { - var options = DafnyOptions.Create(); + var options = DafnyOptions.Create(Console.Out); ServerUtils.ApplyArgs(args, options); var engine = ExecutionEngine.CreateWithoutSharedCache(options); Server server = new Server(engine); @@ -231,4 +231,4 @@ void Exit() { } } -} \ No newline at end of file +} diff --git a/Source/DafnyTestGeneration.Test/BasicTypes.cs b/Source/DafnyTestGeneration.Test/BasicTypes.cs index b0babd2db0d..fb0c12e5184 100644 --- a/Source/DafnyTestGeneration.Test/BasicTypes.cs +++ b/Source/DafnyTestGeneration.Test/BasicTypes.cs @@ -1,12 +1,18 @@ +using System.IO; using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; using Microsoft.Dafny; using Xunit; +using Xunit.Abstractions; namespace DafnyTestGeneration.Test { - public class BasicTypes { + private readonly TextWriter output; + + public BasicTypes(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } [Fact] public async Task Ints() { @@ -22,7 +28,7 @@ method compareToZero(i: int) returns (ret: int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); @@ -51,7 +57,7 @@ method checkIfTrue(b: bool) returns (ret: bool) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(2, methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.checkIfTrue")); @@ -85,7 +91,7 @@ method compareToZero(r: real) returns (ret: int) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(7, methods.Count); Assert.True( @@ -118,7 +124,7 @@ method compareToBase(r: bv10) returns (ret: int) { } } ".TrimStart(); - var program = Utils.Parse(DafnyOptions.Create(), source); + var program = Utils.Parse(DafnyOptions.Create(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True( @@ -149,7 +155,7 @@ method compareToB(c: char) returns (ret: int) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB")); @@ -180,7 +186,7 @@ method compareToB(c: char) returns (b:bool) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(2, methods.Count); Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB")); diff --git a/Source/DafnyTestGeneration.Test/Collections.cs b/Source/DafnyTestGeneration.Test/Collections.cs index f0a3f8e8993..d00130ec6a4 100644 --- a/Source/DafnyTestGeneration.Test/Collections.cs +++ b/Source/DafnyTestGeneration.Test/Collections.cs @@ -1,4 +1,3 @@ -using System; using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; @@ -30,7 +29,7 @@ method compareStringLengthToOne(s: string) returns (ret: int) { } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(new WriterFromOutputHelper(testOutputHelper)), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.True(methods.All(m => @@ -75,7 +74,7 @@ invariant i < |c| { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(new WriterFromOutputHelper(testOutputHelper)), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); if (methods.Count != 3) { // This sometimes occurs on Windows testOutputHelper.WriteLine("methods.Count != 3, printing methods"); diff --git a/Source/DafnyTestGeneration.Test/Setup.cs b/Source/DafnyTestGeneration.Test/Setup.cs index cd537450b48..feaa0c55bd1 100644 --- a/Source/DafnyTestGeneration.Test/Setup.cs +++ b/Source/DafnyTestGeneration.Test/Setup.cs @@ -1,3 +1,4 @@ +using System.IO; using Microsoft.Dafny; namespace DafnyTestGeneration.Test { @@ -5,8 +6,8 @@ namespace DafnyTestGeneration.Test { public class Setup { - public static DafnyOptions GetDafnyOptions(params string[] arguments) { - var options = DafnyOptions.Create(arguments ?? System.Array.Empty()); + public static DafnyOptions GetDafnyOptions(TextWriter writer, params string[] arguments) { + var options = DafnyOptions.Create(writer, TextReader.Null, arguments ?? System.Array.Empty()); options.DefiniteAssignmentLevel = 3; options.WarnShadowing = true; options.VerifyAllModules = true; @@ -19,4 +20,4 @@ public static DafnyOptions GetDafnyOptions(params string[] arguments) { } } -} \ No newline at end of file +} diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs index 4628aeb345c..0ff89fff7a9 100644 --- a/Source/DafnyTestGeneration.Test/Various.cs +++ b/Source/DafnyTestGeneration.Test/Various.cs @@ -1,13 +1,19 @@ +using System.IO; using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; using Microsoft.Dafny; using Xunit; +using Xunit.Abstractions; namespace DafnyTestGeneration.Test { public class Various { + private readonly TextWriter output; + public Various(ITestOutputHelper output) { + this.output = new WriterFromOutputHelper(output); + } [Fact] public async Task NoInlining() { @@ -27,7 +33,7 @@ method a (i:int) returns (r:int) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); Assert.Equal(2, methods.Count(m => m.MethodName == "M.Inlining.b")); @@ -60,7 +66,7 @@ method a (i:int) returns (r:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.a"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -91,7 +97,7 @@ method test (a:int, b:int) returns (r:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -115,7 +121,7 @@ method test(a:int, b:int) returns (r:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -144,7 +150,7 @@ method test(n:int) returns (r:int) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -173,7 +179,7 @@ method test(n:int) returns (r:int) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "M.Inlining.test"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -205,7 +211,7 @@ method eightPaths (i:int) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.Mode = TestGenerationOptions.Modes.Path; @@ -252,7 +258,7 @@ method eightPaths (i:int) returns (divBy2:bool, divBy3:bool, divBy5:bool) { } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.True(methods.Count is >= 2 and <= 6); Assert.True(methods.All(m => m.MethodName == "Paths.eightPaths")); @@ -296,7 +302,7 @@ decreases 3 - counter { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Objects.List.IsACircleOfLessThanThree"; @@ -350,7 +356,7 @@ static method Depth(node: Node) returns (i:int) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "DataTypes.List.Depth"; @@ -388,7 +394,7 @@ method ignoreNonNullableObject(v:Value, b:bool) { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Module.ignoreNonNullableObject"; @@ -416,7 +422,7 @@ requires a > 0 } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.WarnDeadCode = true; var stats = await Main.GetDeadCodeStatistics(program).ToListAsync(); @@ -435,7 +441,7 @@ method m(a:int) returns (b:int) return 1; } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.WarnDeadCode = true; var stats = await Main.GetDeadCodeStatistics(program).ToListAsync(); @@ -456,7 +462,7 @@ method IsEvenLength(s: seq) returns (isEven: bool) } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Test.IsEvenLength"; options.TestGenOptions.SeqLengthLimit = 1; @@ -484,7 +490,7 @@ function Min(a:int, b:int):int { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "Math.Min"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -512,7 +518,7 @@ function Or(a:bool):bool { } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); options.TestGenOptions.TargetMethod = "ShortCircuit.Or"; var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); @@ -542,7 +548,7 @@ module C { function m(r:real):real requires r == 0.0 { r } } ".TrimStart(); - var options = Setup.GetDafnyOptions(); + var options = Setup.GetDafnyOptions(output); var program = Utils.Parse(options, source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Equal(3, methods.Count); @@ -582,7 +588,7 @@ modifies this } } ".TrimStart(); - var program = Utils.Parse(Setup.GetDafnyOptions(), source); + var program = Utils.Parse(Setup.GetDafnyOptions(output), source); var methods = await Main.GetTestMethodsForProgram(program).ToListAsync(); Assert.Single(methods); Assert.True(methods.All(m => diff --git a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs b/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs new file mode 100644 index 00000000000..82c93646a14 --- /dev/null +++ b/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs @@ -0,0 +1,31 @@ +using System.IO; +using System.Text; +using Xunit.Abstractions; + +namespace DafnyTestGeneration.Test; + +public class WriterFromOutputHelper : TextWriter { + private readonly ITestOutputHelper output; + private bool failed; + + public WriterFromOutputHelper(ITestOutputHelper output) { + this.output = output; + } + + public override void Write(char value) { + if (!failed) { + failed = true; + WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support."); + } + } + + public override Encoding Encoding => Encoding.Default; + + public override void WriteLine(string value) { + output.WriteLine(value); + } + + public override void WriteLine(string format, params object[] arg) { + output.WriteLine(format, arg); + } +} \ No newline at end of file diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index 4aa2c7fc577..70095f6b375 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -64,7 +64,7 @@ public IList GetReturnTypes(string callable) { return new List { Utils.UseFullName(functions[callable].ResultType) }; } - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return new List(); } @@ -76,7 +76,7 @@ public List GetTypeArgs(string callable) { if (functions.ContainsKey(callable)) { return functions[callable].TypeArgs; } - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return new List(); } @@ -91,7 +91,7 @@ public List GetTypeArgsWithParents(string callable) { result.AddRange(functions[callable].TypeArgs); clazz = functions[callable].EnclosingClass; } else { - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return result; } @@ -108,7 +108,7 @@ public IList GetFormalsTypes(string callable) { return functions[callable].Formals.Select(arg => Utils.UseFullName(arg.Type)).ToList(); ; } - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return new List(); } @@ -120,7 +120,7 @@ public bool IsStatic(string callable) { if (functions.ContainsKey(callable)) { return functions[callable].IsStatic; } - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callable}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callable}"); SetNonZeroExitCode = true; return true; } @@ -240,7 +240,7 @@ public IEnumerable GetEnsures(List ins, List outs, s new ClonerWithSubstitution(this, subst, receiver).CloneValidOrNull(e.E)) .Where(e => e != null); } - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callableName}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callableName}"); SetNonZeroExitCode = true; return new List(); } @@ -263,7 +263,7 @@ public IEnumerable GetRequires(List ins, string callableName new ClonerWithSubstitution(this, subst, receiver).CloneValidOrNull(e.E)) .Where(e => e != null); } - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify callable {callableName}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify callable {callableName}"); SetNonZeroExitCode = true; return new List(); } @@ -281,7 +281,7 @@ public IEnumerable GetRequires(List ins, string callableName public List<(string name, Type type, bool mutable, string/*?*/ defValue)> GetNonGhostFields(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return new List<(string name, Type type, bool mutable, string/*?*/ defValue)>(); } @@ -311,7 +311,7 @@ public IEnumerable GetRequires(List ins, string callableName public bool IsTrait(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return true; } @@ -373,7 +373,7 @@ public List GetEnsuresForTrait(UserDefinedType/*?*/ type, string name, D } public bool IsExtern(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return true; } @@ -382,7 +382,7 @@ public bool IsExtern(UserDefinedType/*?*/ type) { public Constructor/*?*/ GetConstructor(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Cannot identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; return null; } @@ -427,15 +427,16 @@ private void VisitUserDefinedTypeDeclaration(string newTypeName, if (witness != null) { info.witnessForType[newTypeName] = witness; if (info.Options.TestGenOptions.Verbose) { - Console.Out.WriteLine($"// Values of type {newTypeName} will be " + - $"assigned the default value of " + - $"{Printer.ExprToString(info.Options, info.witnessForType[newTypeName])}"); + info.Options.OutputWriter.WriteLine($"// Values of type {newTypeName} will be " + + $"assigned the default value of " + + $"{Printer.ExprToString(info.Options, info.witnessForType[newTypeName])}"); } } else if (info.Options.TestGenOptions.Verbose) { - info.Options.Printer.ErrorWriteLine(Console.Error, $"*** Error: Values of type {newTypeName} " + - $"will be assigned a default value of type " + - $"{baseType}, which may not match the " + - $"associated condition, if any"); + var message = $@" +*** Error: Values of type {newTypeName} +will be assigned a default value of type {baseType}, +which may not match the associated condition, if any".TrimStart(); + info.Options.Printer.ErrorWriteLine(info.Options.ErrorWriter, message); info.SetNonZeroExitCode = true; } info.subsetToSuperset[newTypeName] = (typeArgs, @@ -620,4 +621,4 @@ public override Expression CloneExpr(Expression expr) { } } } -} \ No newline at end of file +} diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs index 8f115c72ea3..aa403791c77 100644 --- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs +++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs @@ -43,7 +43,7 @@ private enum Mode { /// because we have to modify ProcsToCheck list, which does not have a setter. /// internal static DafnyOptions CopyForProcedure(DafnyOptions options, string procedureToVerify) { - var copy = DafnyOptions.Create(new[] { "/proc:" + procedureToVerify }); + var copy = DafnyOptions.Create(options.OutputWriter, options.Input, new[] { "/proc:" + procedureToVerify }); // Options set by the user: copy.LoopUnrollCount = options.LoopUnrollCount; copy.TestGenOptions.SeqLengthLimit = options.TestGenOptions.SeqLengthLimit; diff --git a/Source/DafnyTestGeneration/Main.cs b/Source/DafnyTestGeneration/Main.cs index c18f46d980c..7a8f7ed687a 100644 --- a/Source/DafnyTestGeneration/Main.cs +++ b/Source/DafnyTestGeneration/Main.cs @@ -85,7 +85,7 @@ private static IEnumerable GetModifications(Modifications c i.VerboseName.Split(" ")[0] == options.TestGenOptions.TargetMethod)); if (!targetFound) { - options.Printer.ErrorWriteLine(Console.Error, + options.Printer.ErrorWriteLine(options.ErrorWriter, "Error: Cannot find method " + options.TestGenOptions.TargetMethod + " (is this name fully-qualified?)"); @@ -135,7 +135,6 @@ public static async IAsyncEnumerable GetTestMethodsForProgram(Progra /// Return a Dafny class (list of lines) with tests for the given Dafny file /// public static async IAsyncEnumerable GetTestClassForProgram(string sourceFile, DafnyOptions options) { - options.PrintMode = PrintModes.Everything; TestMethod.ClearTypesToSynthesize(); var source = await new StreamReader(sourceFile).ReadToEndAsync(); @@ -180,7 +179,7 @@ string EscapeDafnyStringLiteral(string str) { yield return "}"; if (methodsGenerated == 0) { - options.Printer.ErrorWriteLine(Console.Error, + options.Printer.ErrorWriteLine(options.ErrorWriter, "Error: No tests were generated, because no code points could be " + "proven reachable (do you have a false assumption in the program?)"); setNonZeroExitCode = true; diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs index f50efde0ec3..f636d3894a1 100644 --- a/Source/DafnyTestGeneration/ProgramModification.cs +++ b/Source/DafnyTestGeneration/ProgramModification.cs @@ -123,7 +123,7 @@ private static void SetupForCounterexamples(DafnyOptions options) { counterexampleLog = null; if (result is not Task) { if (Options.TestGenOptions.Verbose) { - Console.WriteLine( + await options.OutputWriter.WriteLineAsync( $"// No test can be generated for {uniqueId} " + "because the verifier timed out."); } @@ -140,22 +140,22 @@ private static void SetupForCounterexamples(DafnyOptions options) { coversBlocks.Add(blockId); if (Options.TestGenOptions.Verbose && Options.TestGenOptions.Mode != TestGenerationOptions.Modes.Path) { - Console.WriteLine($"// Test targeting block {uniqueId} also covers block {blockId}"); + await options.OutputWriter.WriteLineAsync($"// Test {uniqueId} covers block {blockId}"); } } } if (Options.TestGenOptions.Verbose && counterexampleLog == null) { if (log == "") { - Console.WriteLine( + await options.OutputWriter.WriteLineAsync( $"// No test is generated for {uniqueId} " + "because the verifier proved that no inputs could cause this block to be visited."); } else if (log.Contains("MODEL") || log.Contains("anon0")) { - Console.WriteLine( + await options.OutputWriter.WriteLineAsync( $"// No test is generated for {uniqueId} " + "because there is no enhanced error trace. This can be caused " + "by a bug in boogie counterexample model parsing."); } else { - Console.WriteLine( + await options.OutputWriter.WriteLineAsync( $"// No test is generated for {uniqueId} " + "because the verifier timed out."); } @@ -165,7 +165,7 @@ private static void SetupForCounterexamples(DafnyOptions options) { public async Task GetTestMethod(Modifications cache, DafnyInfo dafnyInfo, bool returnNullIfNotUnique = true) { if (Options.TestGenOptions.Verbose) { - Console.WriteLine( + await dafnyInfo.Options.OutputWriter.WriteLineAsync( $"// Extracting the test for {uniqueId} from the counterexample..."); } var log = await GetCounterExampleLog(cache); @@ -183,7 +183,7 @@ public async Task GetTestMethod(Modifications cache, DafnyInfo dafny return testMethod; } if (Options.TestGenOptions.Verbose) { - Console.WriteLine( + await dafnyInfo.Options.OutputWriter.WriteLineAsync( $"// Test for {uniqueId} matches a test previously generated " + $"for {duplicate.uniqueId}. This happens when test generation tool " + $"does not know how to differentiate between counterexamples, " + diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 63fd059e5f3..7f82b966cfd 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -80,7 +80,7 @@ public static Type CopyWithReplacements(Type type, List from, List var builtIns = new BuiltIns(options); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); var success = Parser.Parse(source, uri, module, builtIns, - new Errors(reporter)) == 0 && Microsoft.Dafny.Main.ParseIncludesDepthFirstNotCompiledFirst(module, builtIns, + new Errors(reporter)) == 0 && DafnyMain.ParseIncludesDepthFirstNotCompiledFirst(options.Input, module, builtIns, new HashSet(), new Errors(reporter)) == null; var program = new Program(uri.LocalPath, module, builtIns, reporter); diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index 2da0ae27fea..4b15b47c0f0 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -5,6 +5,7 @@ using System.Reflection; using System.Runtime.InteropServices; using Microsoft.Dafny; +using TestDafny; using Xunit; using Xunit.Abstractions; using XUnitExtensions; @@ -22,7 +23,7 @@ public class LitTests { private const bool InvokeMainMethodsDirectly = false; private static readonly Assembly DafnyDriverAssembly = typeof(Dafny.Dafny).Assembly; - private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.TestDafny).Assembly; + private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.MultiBackendTest).Assembly; private static readonly Assembly DafnyServerAssembly = typeof(Server).Assembly; private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net6.0/ @@ -66,40 +67,36 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l var commands = new Dictionary, LitTestConfiguration, ILitCommand>> { { "%baredafny", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, args, config, InvokeMainMethodsDirectly) + DafnyCommand(args, config, InvokeMainMethodsDirectly) }, { "%resolve", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultResolveArgs, args), - config, InvokeMainMethodsDirectly) + DafnyCommand(AddExtraArgs(defaultResolveArgs, args), config, InvokeMainMethodsDirectly) }, { "%translate", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(new[]{"translate"}, args), - config, InvokeMainMethodsDirectly) + DafnyCommand(AddExtraArgs(new[]{"translate"}, args), config, InvokeMainMethodsDirectly) }, { "%verify", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultVerifyArgs, args), - config, InvokeMainMethodsDirectly) + DafnyCommand(AddExtraArgs(defaultVerifyArgs, args), config, InvokeMainMethodsDirectly) }, { "%build", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultBuildArgs, args), - config, InvokeMainMethodsDirectly) + DafnyCommand(AddExtraArgs(defaultBuildArgs, args), config, InvokeMainMethodsDirectly) }, { "%run", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(defaultRunArgs, args), - config, InvokeMainMethodsDirectly) + DafnyCommand(AddExtraArgs(defaultRunArgs, args), config, InvokeMainMethodsDirectly) }, { "%dafny", (args, config) => - MainMethodLitCommand.Parse(DafnyDriverAssembly, AddExtraArgs(DafnyDriver.DefaultArgumentsForTesting, args), - config, InvokeMainMethodsDirectly) + DafnyCommand(AddExtraArgs(DafnyDriver.DefaultArgumentsForTesting, args), config, InvokeMainMethodsDirectly) }, { "%testDafnyForEachCompiler", (args, config) => - MainMethodLitCommand.Parse(TestDafnyAssembly, new []{ "for-each-compiler" }.Concat(args), config, - InvokeMainMethodsDirectly) + MainMethodLitCommand.Parse(TestDafnyAssembly, new []{ "for-each-compiler" }.Concat(args), config, InvokeMainMethodsDirectly) }, { - "%server", (args, config) => - MainMethodLitCommand.Parse(DafnyServerAssembly, args, config, InvokeMainMethodsDirectly) + "%server", (args, config) => // TODO + { + var shellArguments = new[] { DafnyServerAssembly.Location }.Concat(args); + return new ShellLitCommand("dotnet", shellArguments, config.PassthroughEnvironmentVariables); + } }, { - "%boogie", (args, config) => + "%boogie", (args, config) => // TODO new DotnetToolCommand("boogie", args.Concat(DefaultBoogieArguments), config.PassthroughEnvironmentVariables) @@ -108,8 +105,7 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l }, { "%sed", (args, config) => SedCommand.Parse(args.ToArray()) }, { - "%OutputCheck", (args, config) => - OutputCheckCommand.Parse(args, config) + "%OutputCheck", OutputCheckCommand.Parse } }; @@ -148,8 +144,7 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l AddExtraArgs(DafnyDriver.DefaultArgumentsForTesting, args), config.PassthroughEnvironmentVariables); commands["%testDafnyForEachCompiler"] = (args, config) => MainMethodLitCommand.Parse(TestDafnyAssembly, - new[] { "for-each-compiler", "--dafny", dafnyCliPath }.Concat(args), config, - InvokeMainMethodsDirectly); + new[] { "for-each-compiler", "--dafny", dafnyCliPath }.Concat(args), config, false); commands["%server"] = (args, config) => new ShellLitCommand(Path.Join(dafnyReleaseDir, "DafnyServer"), args, config.PassthroughEnvironmentVariables); commands["%boogie"] = (args, config) => @@ -162,6 +157,12 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l Config = new LitTestConfiguration(substitutions, commands, features, DafnyDriver.ReferencedEnvironmentVariables); } + public static ILitCommand DafnyCommand(IEnumerable arguments, LitTestConfiguration config, bool invokeDirectly) { + return invokeDirectly + ? new DafnyDriverLitCommand(arguments, config) + : new ShellLitCommand("dotnet", new[] { DafnyDriverAssembly.Location }.Concat(arguments), config.PassthroughEnvironmentVariables); + } + private readonly ITestOutputHelper output; public LitTests(ITestOutputHelper output) { @@ -176,4 +177,39 @@ public void LitTest(string path) { LitTestCase.Run(path, Config, output); } } + + class DafnyDriverLitCommand : ILitCommand { + private readonly string[] arguments; + + public DafnyDriverLitCommand(IEnumerable arguments, LitTestConfiguration config) { + this.arguments = arguments.ToArray(); + } + + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, + TextWriter errorWriter) { + var exitCode = DafnyDriver.MainWithWriters(outputWriter, errorWriter, inputReader, arguments); + return (exitCode, "", ""); + } + + public override string ToString() { + return $"dafny {string.Join(" ", arguments)}"; + } + } + + class MultiBackendLitCommand : ILitCommand { + private readonly string[] arguments; + + public MultiBackendLitCommand(IEnumerable arguments, LitTestConfiguration config) { + this.arguments = arguments.ToArray(); + } + + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, + TextWriter errorWriter) { + var exitCode = new MultiBackendTest(inputReader, outputWriter, errorWriter).Start(arguments.Prepend("for-each-compiler")); + return (exitCode, "", ""); + } + } } + diff --git a/Source/TestDafny/TestDafny.cs b/Source/TestDafny/MultiBackendTest.cs similarity index 59% rename from Source/TestDafny/TestDafny.cs rename to Source/TestDafny/MultiBackendTest.cs index 5f21c699d95..db63b577e90 100644 --- a/Source/TestDafny/TestDafny.cs +++ b/Source/TestDafny/MultiBackendTest.cs @@ -5,7 +5,6 @@ using Microsoft.Dafny; using Microsoft.Dafny.Plugins; using XUnitExtensions; -using XUnitExtensions.Lit; namespace TestDafny; @@ -15,10 +14,8 @@ public class ForEachCompilerOptions { [Value(0, Required = true, MetaName = "Test file", HelpText = "The *.dfy file to test.")] public string? TestFile { get; set; } = null; - [Option("dafny", HelpText = "The dafny CLI to test with. Defaults to the locally built DafnyDriver project.")] - public string? DafnyCliPath { get; set; } = null; - - [Value(1, MetaName = "Dafny CLI arguments", HelpText = "Any arguments following '--' will be passed to the dafny CLI unaltered.")] public IEnumerable OtherArgs { get; set; } = Array.Empty(); + [Value(1, MetaName = "Dafny CLI arguments", HelpText = "Any arguments following '--' will be passed to the dafny CLI unaltered.")] + public IEnumerable OtherArgs { get; set; } = Array.Empty(); } [Verb("features", HelpText = "Print the Markdown content documenting feature support for each compiler.")] @@ -26,37 +23,45 @@ public class FeaturesOptions { [Value(1)] public IEnumerable OtherArgs { get; set; } = Array.Empty(); } -public class TestDafny { - +public class MultiBackendTest { private static readonly Assembly DafnyAssembly = typeof(Dafny.Dafny).Assembly; + private readonly TextReader input; + private readonly TextWriter output; + private readonly TextWriter errorWriter; + + public MultiBackendTest(TextReader input, TextWriter output, TextWriter errorWriter) { + this.input = input; + this.output = output; + this.errorWriter = errorWriter; + } public static int Main(string[] args) { + return new MultiBackendTest(Console.In, Console.Out, Console.Error).Start(args.ToList()); + } + + public int Start(IEnumerable args) { var result = -1; var parser = new CommandLine.Parser(with => { with.EnableDashDash = true; - with.HelpWriter = Console.Error; + with.HelpWriter = errorWriter; }); var parseResult = parser.ParseArguments(args); - parseResult.WithParsed(options => { - result = ForEachCompiler(options); - }).WithParsed(options => { - result = GenerateCompilerTargetSupportTable(options); - }); + parseResult.WithParsed(options => { result = ForEachCompiler(options); }) + .WithParsed(options => { result = GenerateCompilerTargetSupportTable(options); }); return result; } - private static DafnyOptions? ParseDafnyOptions(IEnumerable dafnyArgs) { - var dafnyOptions = new DafnyOptions(); + private DafnyOptions? ParseDafnyOptions(IEnumerable dafnyArgs) { + var dafnyOptions = new DafnyOptions(input, output, errorWriter); var success = dafnyOptions.Parse(dafnyArgs.ToArray()); return success ? dafnyOptions : null; } - private static int ForEachCompiler(ForEachCompilerOptions options) { - var dafnyOptions = ParseDafnyOptions(options.OtherArgs); - if (dafnyOptions == null) { - return (int)DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR; - } + private int ForEachCompiler(ForEachCompilerOptions options) { + var parseResult = CommandRegistry.Create(TextWriter.Null, TextWriter.Null, TextReader.Null, + new string[] { "verify", options.TestFile! }.Concat(options.OtherArgs).ToArray()); + var dafnyOptions = ((ParseArgumentSuccess)parseResult).DafnyOptions; // First verify the file (and assume that verification should be successful). // Older versions of test files that now use %testDafnyForEachCompiler were sensitive to the number @@ -64,19 +69,19 @@ private static int ForEachCompiler(ForEachCompilerOptions options) { // but this was never meaningful and only added maintenance burden. // Here we only ensure that the exit code is 0. - var dafnyArgs = new List(options.OtherArgs) { - $"/compile:0", + var dafnyArgs = new List() { + $"verify", options.TestFile! - }; + }.Concat(options.OtherArgs).ToArray(); - Console.Out.WriteLine("Verifying..."); + output.WriteLine("Verifying..."); - var (exitCode, output, error) = RunDafny(options.DafnyCliPath, dafnyArgs); + var (exitCode, outputString, error) = RunDafny(dafnyArgs); if (exitCode != 0) { - Console.Out.WriteLine("Verification failed. Output:"); - Console.Out.WriteLine(output); - Console.Out.WriteLine("Error:"); - Console.Out.WriteLine(error); + output.WriteLine("Verification failed. Output:"); + output.WriteLine(outputString); + output.WriteLine("Error:"); + output.WriteLine(error); return exitCode; } @@ -89,6 +94,11 @@ private static int ForEachCompiler(ForEachCompilerOptions options) { var success = true; foreach (var plugin in dafnyOptions.Plugins) { foreach (var compiler in plugin.GetCompilers(dafnyOptions)) { + if (compiler.TargetId == "lib") { + // Some tests still fail when using the lib back-end, for example due to disallowed assumptions being present in the test, + // Such as empty constructors with ensures clauses, generated from iterators + continue; + } var result = RunWithCompiler(options, compiler, expectedOutput); if (result != 0) { success = false; @@ -97,7 +107,7 @@ private static int ForEachCompiler(ForEachCompilerOptions options) { } if (success) { - Console.Out.WriteLine( + output.WriteLine( $"All executions were successful and matched the expected output (or reported errors for known unsupported features)!"); return 0; } else { @@ -105,61 +115,55 @@ private static int ForEachCompiler(ForEachCompilerOptions options) { } } - private static int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend backend, string expectedOutput) { - Console.Out.WriteLine($"Executing on {backend.TargetName}..."); - var dafnyArgs = new List(options.OtherArgs) { - // Here we can pass /noVerify to save time since we already verified the program. - "/noVerify", - // /noVerify is interpreted pessimistically as "did not get verification success", - // so we have to force compiling and running despite this. - "/compile:4", - $"/compileTarget:{backend.TargetId}", - options.TestFile! - }; + private int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend backend, string expectedOutput) { + output.WriteLine($"Executing on {backend.TargetName}..."); + var dafnyArgs = new List() { + "run", + "--no-verify", + $"--target:{backend.TargetId}", + options.TestFile!, + }.Concat(options.OtherArgs); + var (exitCode, outputString, error) = RunDafny(dafnyArgs); - var (exitCode, output, error) = RunDafny(options.DafnyCliPath, dafnyArgs); if (exitCode == 0) { - var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, output); + var diffMessage = AssertWithDiff.GetDiffMessage(expectedOutput, outputString); if (diffMessage == null) { return 0; } - Console.Out.WriteLine(diffMessage); + output.WriteLine(diffMessage); return 1; } // If we hit errors, check for known unsupported features for this compilation target - if (error == "" && OnlyUnsupportedFeaturesErrors(backend, output)) { + if (error == "" && OnlyUnsupportedFeaturesErrors(backend, outputString)) { return 0; } - Console.Out.WriteLine("Execution failed, for reasons other than known unsupported features. Output:"); - Console.Out.WriteLine(output); - Console.Out.WriteLine("Error:"); - Console.Out.WriteLine(error); + output.WriteLine("Execution failed, for reasons other than known unsupported features. Output:"); + output.WriteLine(outputString); + output.WriteLine("Error:"); + output.WriteLine(error); return exitCode; } - private static (int, string, string) RunDafny(string? dafnyCLIPath, IEnumerable arguments) { - var argumentsWithDefaults = arguments.Concat(DafnyDriver.DefaultArgumentsForTesting); - ILitCommand command; - if (dafnyCLIPath != null) { - command = new ShellLitCommand(dafnyCLIPath, argumentsWithDefaults, DafnyDriver.ReferencedEnvironmentVariables); - } else { - var dotnetArguments = new[] { DafnyAssembly.Location }.Concat(argumentsWithDefaults); - command = new ShellLitCommand("dotnet", dotnetArguments, DafnyDriver.ReferencedEnvironmentVariables); - } - return command.Execute(null, null, null, null); + private static (int, string, string) RunDafny(IEnumerable arguments) { + var argumentsWithDefaults = arguments.Concat(DafnyDriver.NewDefaultArgumentsForTesting); + var outputWriter = new StringWriter(); + var errorWriter = new StringWriter(); + var exitCode = DafnyDriver.MainWithWriters(outputWriter, errorWriter, TextReader.Null, argumentsWithDefaults.ToArray()); + var outputString = outputWriter.ToString(); + var error = errorWriter.ToString(); + return (exitCode, outputString, error); } private static bool OnlyUnsupportedFeaturesErrors(IExecutableBackend backend, string output) { - using (StringReader sr = new StringReader(output)) { - string? line; - while ((line = sr.ReadLine()) != null) { - if (!IsAllowedOutputLine(backend, line)) { - return false; - } + using StringReader sr = new StringReader(output); + string? line; + while ((line = sr.ReadLine()) != null) { + if (!IsAllowedOutputLine(backend, line)) { + return false; } } @@ -204,7 +208,7 @@ private static bool IsAllowedOutputLine(IExecutableBackend backend, string line) $"Compiler rejected feature '{feature}', which is not an element of its UnsupportedFeatures set"); } - private static int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOptions) { + private int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOptions) { var dafnyOptions = ParseDafnyOptions(featuresOptions.OtherArgs); if (dafnyOptions == null) { return (int)DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR; @@ -216,20 +220,20 @@ private static int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOp .ToList(); // Header - Console.Out.Write("| Feature |"); + output.Write("| Feature |"); foreach (var compiler in allCompilers) { - Console.Out.Write($" {compiler.TargetName} |"); + output.Write($" {compiler.TargetName} |"); } - Console.Out.WriteLine(); + output.WriteLine(); // Horizontal rule ("|----|---|...") - Console.Out.Write("|-|"); + output.Write("|-|"); foreach (var _ in allCompilers) { - Console.Out.Write($"-|"); + output.Write($"-|"); } - Console.Out.WriteLine(); + output.WriteLine(); var footnotes = new StringBuilder(); foreach (var feature in Enum.GetValues(typeof(Feature)).Cast()) { @@ -241,19 +245,19 @@ private static int GenerateCompilerTargetSupportTable(FeaturesOptions featuresOp footnotes.AppendLine(); } - Console.Out.Write($"| [{description.Description}](#{description.ReferenceManualSection}){footnoteLink} |"); + output.Write($"| [{description.Description}](#{description.ReferenceManualSection}){footnoteLink} |"); foreach (var compiler in allCompilers) { var supported = !compiler.UnsupportedFeatures.Contains(feature); var cell = supported ? " X " : ""; - Console.Out.Write($" {cell} |"); + output.Write($" {cell} |"); } - Console.Out.WriteLine(); + output.WriteLine(); } - Console.Out.WriteLine(); - Console.Out.WriteLine(footnotes); + output.WriteLine(); + output.WriteLine(footnotes); return 0; } -} \ No newline at end of file +} diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj index 03d2c3a702c..83f292e7923 100644 --- a/Source/TestDafny/TestDafny.csproj +++ b/Source/TestDafny/TestDafny.csproj @@ -1,22 +1,24 @@ - Exe - net6.0 - enable - enable - false - - + Exe + net6.0 + enable + enable + false + + + + - + - + PreserveNewest diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index eee6070ed64..281d1ffb72e 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -28,7 +28,8 @@ public static ILitCommand Parse(string[] args) { return new DiffCommand(expectedPath, actualPath); } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { var expected = File.ReadAllText(expectedPath); var actual = File.ReadAllText(actualPath); var diffMessage = AssertWithDiff.GetDiffMessage(expected, actual); diff --git a/Source/XUnitExtensions/Lit/ExitCommand.cs b/Source/XUnitExtensions/Lit/ExitCommand.cs index e4499d7b1d7..793e224f6e3 100644 --- a/Source/XUnitExtensions/Lit/ExitCommand.cs +++ b/Source/XUnitExtensions/Lit/ExitCommand.cs @@ -12,8 +12,9 @@ public ExitCommand(int exitCode, ILitCommand operand) { this.operand = operand; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { - var (exitCode, output, error) = operand.Execute(outputHelper, inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { + var (exitCode, output, error) = operand.Execute(inputReader, outputWriter, errorWriter); if (exitCode == expectedExitCode) { return (0, output, error); } else { diff --git a/Source/XUnitExtensions/Lit/ILitCommand.cs b/Source/XUnitExtensions/Lit/ILitCommand.cs index da9cfabcac3..83318221af4 100644 --- a/Source/XUnitExtensions/Lit/ILitCommand.cs +++ b/Source/XUnitExtensions/Lit/ILitCommand.cs @@ -16,15 +16,26 @@ public enum Kind { Verbatim, MustGlob } class DelayedLitCommand : ILitCommand { private readonly Func factory; + private ILitCommand? command; public DelayedLitCommand(Func factory) { this.factory = factory; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, - TextWriter? errorWriter) { - var command = factory(); - return command.Execute(outputHelper, inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, + TextWriter errorWriter) { + if (command == null) { + command = factory(); + } + return command.Execute(inputReader, outputWriter, errorWriter); + } + + public override string? ToString() { + if (command == null) { + command = factory(); + } + return command!.ToString(); } } public interface ILitCommand { @@ -80,6 +91,6 @@ public static Token[] Tokenize(string line) { return result.ToArray(); } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter); + public (int, string, string) Execute(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter); } } diff --git a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs index 962903e9f96..51a39441f97 100644 --- a/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs +++ b/Source/XUnitExtensions/Lit/LitCommandWithRedirection.cs @@ -77,11 +77,12 @@ public LitCommandWithRedirection(ILitCommand command, string? inputFile, string? this.errorFile = errorFile; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inReader, TextWriter? outWriter, TextWriter? errWriter) { + public (int, string, string) Execute(TextReader inReader, TextWriter outWriter, + TextWriter errWriter) { var inputReader = inputFile != null ? new StreamReader(inputFile) : inReader; var outputWriter = outputFile != null ? new StreamWriter(outputFile, append) : outWriter; var errorWriter = errorFile != null ? new StreamWriter(errorFile, append) : errWriter; - var result = command.Execute(outputHelper, inputReader, outputWriter, errorWriter); + var result = command.Execute(inputReader, outputWriter, errorWriter); inputReader?.Close(); outputWriter?.Close(); errorWriter?.Close(); @@ -116,3 +117,25 @@ public override string ToString() { } } } + +public class WriterFromOutputHelper : TextWriter { + private readonly ITestOutputHelper output; + + public WriterFromOutputHelper(ITestOutputHelper output) { + this.output = output; + } + + public override void Write(char value) { + + } + + public override Encoding Encoding => Encoding.Default; + + public override void WriteLine(string? value) { + output.WriteLine(value); + } + + public override void WriteLine(string format, params object?[] arg) { + output.WriteLine(format, arg); + } +} \ No newline at end of file diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs index 1ed0680d6e3..9b3e96f66a9 100644 --- a/Source/XUnitExtensions/Lit/LitTestCase.cs +++ b/Source/XUnitExtensions/Lit/LitTestCase.cs @@ -61,7 +61,7 @@ public LitTestCase(string filePath, IEnumerable commands, bool expe this.expectFailure = expectFailure; } - public void Execute(ITestOutputHelper? outputHelper) { + public void Execute(ITestOutputHelper outputHelper) { Directory.CreateDirectory(Path.Join(Path.GetDirectoryName(filePath), "Output")); // For debugging. Only printed on failure in case the true cause is buried in an earlier command. List<(string, string)> results = new(); @@ -70,9 +70,11 @@ public void Execute(ITestOutputHelper? outputHelper) { int exitCode; string output; string error; + var outputWriter = new StringWriter(); + var errorWriter = new StringWriter(); try { - outputHelper?.WriteLine($"Executing command: {command}"); - (exitCode, output, error) = command.Execute(outputHelper, null, null, null); + outputHelper.WriteLine($"Executing command: {command}"); + (exitCode, output, error) = command.Execute(TextReader.Null, outputWriter, errorWriter); } catch (Exception e) { throw new Exception($"Exception thrown while executing command: {command}", e); } @@ -80,7 +82,7 @@ public void Execute(ITestOutputHelper? outputHelper) { if (expectFailure) { if (exitCode != 0) { throw new SkipException( - $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output}\nError:\n{error}"); + $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output + outputWriter}\nError:\n{error + errorWriter}"); } } @@ -92,7 +94,7 @@ public void Execute(ITestOutputHelper? outputHelper) { } throw new Exception( - $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output}\nError:\n{error}"); + $"Command returned non-zero exit code ({exitCode}): {command}\nOutput:\n{output + outputWriter}\nError:\n{error + errorWriter}"); } results.Add((output, error)); diff --git a/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs b/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs index 19277f978c7..c4412cc8bb7 100644 --- a/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs +++ b/Source/XUnitExtensions/Lit/MainMethodLitCommand.cs @@ -21,7 +21,8 @@ public static ILitCommand Parse(Assembly assembly, IEnumerable arguments return invokeDirectly ? result : result.ToShellCommand(config); } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { if (inputReader != null) { Console.SetIn(inputReader); } @@ -32,8 +33,8 @@ public static ILitCommand Parse(Assembly assembly, IEnumerable arguments Console.SetError(errorWriter); } - var entry = assembly.EntryPoint!; - var exitCode = (int)entry.Invoke(null, new object[] { arguments })!; + var result = assembly.EntryPoint!.Invoke(null, new object[] { arguments }); + var exitCode = result == null ? 0 : (int)result; return (exitCode, "", ""); } @@ -51,4 +52,4 @@ public override string ToString() { return builder.ToString(); } } -} \ No newline at end of file +} diff --git a/Source/XUnitExtensions/Lit/NotCommand.cs b/Source/XUnitExtensions/Lit/NotCommand.cs index f373ba765e5..bcf62f65ce2 100644 --- a/Source/XUnitExtensions/Lit/NotCommand.cs +++ b/Source/XUnitExtensions/Lit/NotCommand.cs @@ -10,8 +10,9 @@ public NotCommand(ILitCommand operand) { this.operand = operand; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { - var (exitCode, output, error) = operand.Execute(outputHelper, inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { + var (exitCode, output, error) = operand.Execute(inputReader, outputWriter, errorWriter); return (exitCode == 0 ? 1 : 0, output, error); } diff --git a/Source/XUnitExtensions/Lit/OrCommand.cs b/Source/XUnitExtensions/Lit/OrCommand.cs index 02811594e07..ee6d6afb911 100644 --- a/Source/XUnitExtensions/Lit/OrCommand.cs +++ b/Source/XUnitExtensions/Lit/OrCommand.cs @@ -11,13 +11,14 @@ public OrCommand(ILitCommand lhs, ILitCommand rhs) { this.rhs = rhs; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { - var (leftExitCode, leftOutput, leftError) = lhs.Execute(outputHelper, inputReader, outputWriter, errorWriter); + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { + var (leftExitCode, leftOutput, leftError) = lhs.Execute(inputReader, outputWriter, errorWriter); if (leftExitCode == 0) { return (leftExitCode, leftOutput, leftError); } - var (rightExitCode, rightOutput, rightError) = rhs.Execute(outputHelper, inputReader, outputWriter, errorWriter); + var (rightExitCode, rightOutput, rightError) = rhs.Execute(inputReader, outputWriter, errorWriter); return (rightExitCode, leftOutput + rightOutput, leftError + rightError); } diff --git a/Source/XUnitExtensions/Lit/OutputCheckCommand.cs b/Source/XUnitExtensions/Lit/OutputCheckCommand.cs index 23ee3a8e391..3eba773e5a4 100644 --- a/Source/XUnitExtensions/Lit/OutputCheckCommand.cs +++ b/Source/XUnitExtensions/Lit/OutputCheckCommand.cs @@ -185,8 +185,8 @@ public static ILitCommand Parse(IEnumerable args, LitTestConfiguration c return result!; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, - TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { if (options.FileToCheck == null) { return (0, "", ""); } diff --git a/Source/XUnitExtensions/Lit/SedCommand.cs b/Source/XUnitExtensions/Lit/SedCommand.cs index 8d47c9fe81a..66846045055 100644 --- a/Source/XUnitExtensions/Lit/SedCommand.cs +++ b/Source/XUnitExtensions/Lit/SedCommand.cs @@ -39,7 +39,8 @@ public static ILitCommand Parse(string[] args) { return new SedCommand(regexp, replaceBy, file); } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { var fileContent = File.ReadAllText(file); try { var stdOutput = Regex.Replace(fileContent, "(?m)" + regexp, replaceBy); diff --git a/Source/XUnitExtensions/Lit/ShellLitCommand.cs b/Source/XUnitExtensions/Lit/ShellLitCommand.cs index 98fdcc19315..c6dbd81136b 100644 --- a/Source/XUnitExtensions/Lit/ShellLitCommand.cs +++ b/Source/XUnitExtensions/Lit/ShellLitCommand.cs @@ -18,7 +18,8 @@ public ShellLitCommand(string shellCommand, IEnumerable arguments, IEnum this.passthroughEnvironmentVariables = passthroughEnvironmentVariables.ToArray(); } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { using var process = new Process(); process.StartInfo.FileName = shellCommand; diff --git a/Source/XUnitExtensions/Lit/StdInCommand.cs b/Source/XUnitExtensions/Lit/StdInCommand.cs index 3d10baf5577..df1768cb800 100644 --- a/Source/XUnitExtensions/Lit/StdInCommand.cs +++ b/Source/XUnitExtensions/Lit/StdInCommand.cs @@ -13,9 +13,10 @@ public StdInCommand(string stdin, ILitCommand operand) { this.operand = operand; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { inputReader = new StringReader(stdin); - return operand.Execute(outputHelper, inputReader, outputWriter, errorWriter); + return operand.Execute(inputReader, outputWriter, errorWriter); } public override string ToString() { diff --git a/Source/XUnitExtensions/Lit/UnsupportedCommand.cs b/Source/XUnitExtensions/Lit/UnsupportedCommand.cs index 6aa1e004c70..b5480d52724 100644 --- a/Source/XUnitExtensions/Lit/UnsupportedCommand.cs +++ b/Source/XUnitExtensions/Lit/UnsupportedCommand.cs @@ -19,7 +19,8 @@ public UnsupportedCommand(IEnumerable features) { Features = features; } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { return (0, "", ""); } } diff --git a/Source/XUnitExtensions/Lit/XFailCommand.cs b/Source/XUnitExtensions/Lit/XFailCommand.cs index 9310c84064b..edad57bf4de 100644 --- a/Source/XUnitExtensions/Lit/XFailCommand.cs +++ b/Source/XUnitExtensions/Lit/XFailCommand.cs @@ -14,7 +14,8 @@ public static ILitCommand Parse(string line, LitTestConfiguration config) { throw new ArgumentException($"Unrecognized arguments to XFAIL: {line}"); } - public (int, string, string) Execute(ITestOutputHelper? outputHelper, TextReader? inputReader, TextWriter? outputWriter, TextWriter? errorWriter) { + public (int, string, string) Execute(TextReader inputReader, + TextWriter outputWriter, TextWriter errorWriter) { return (0, "", ""); } } diff --git a/Test/comp/Iterators.dfy b/Test/comp/Iterators.dfy index 663ade95863..0512ddb93b0 100644 --- a/Test/comp/Iterators.dfy +++ b/Test/comp/Iterators.dfy @@ -8,6 +8,8 @@ class C { print "x is ", x, "\n"; Client(); RegressionClient(); + r := *; + s := *; } } diff --git a/Test/comp/UnicodeStrings.dfy b/Test/comp/UnicodeStrings.dfy index fd512dd4510..30cde9aca69 100644 --- a/Test/comp/UnicodeStrings.dfy +++ b/Test/comp/UnicodeStrings.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:1 +// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char method AssertAndExpect(p: bool) requires p diff --git a/Test/comp/Uninitialized.dfy b/Test/comp/Uninitialized.dfy index 220495ad5e1..1b69f1be4ec 100644 --- a/Test/comp/Uninitialized.dfy +++ b/Test/comp/Uninitialized.dfy @@ -140,12 +140,16 @@ module {:options "/functionSyntax:4"} EnumerationTests { method PickEnumValue() returns (r: Enum) { if e: Enum :| e.Is(13) { r := e; + } else { + r := *; } } method PickAllGhostValue() returns (r: AllGhost) { if ag: AllGhost :| ag.Is(13) { r := ag; + } else { + r := *; } } } diff --git a/Test/comp/compile3/JustRun.dfy.expect b/Test/comp/compile3/JustRun.dfy.expect index 06ceaa6e321..95909991d55 100644 --- a/Test/comp/compile3/JustRun.dfy.expect +++ b/Test/comp/compile3/JustRun.dfy.expect @@ -1,5 +1,6 @@ Dafny program verifier finished with 0 verified, 0 errors +Compiled assembly into JustRun.dll Running... hello, Dafny diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy index b0010970e6f..039c09a69aa 100644 --- a/Test/dafny0/Strings.dfy +++ b/Test/dafny0/Strings.dfy @@ -1,12 +1,14 @@ -// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:0 +// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char=false method Char(a: char, s: string, i: int) returns (b: char) { - var ch: char; + var ch: char := *; if a == ch { b := ch; } else if 0 <= i < |s| { b := s[i]; + } else { + b := *; } } @@ -18,7 +20,8 @@ method {:MyAttribute "hello", "hi" + "there", 57} AttrTest() method M(a: char, b: char) returns (s: string, t: seq) ensures |s| == 3 ==> t == [a, b, b]; -{ +{ + s := *; s := s + [a, b, b] + s; t := s; s := t[0..|s|]; @@ -32,7 +35,7 @@ method M(a: char, b: char) returns (s: string, t: seq) // strings rather than printing them and relying on the diff with the expect file. method Main() { - var ch: char; + var ch: char := *; var s, t := M(ch, ch); print "ch = ", ch, "\n"; print "The string is: " + s + "\n"; diff --git a/Test/git-issues/git-issue-1553.dfy b/Test/git-issues/git-issue-1553.dfy index 530608808d9..6267018c92d 100644 --- a/Test/git-issues/git-issue-1553.dfy +++ b/Test/git-issues/git-issue-1553.dfy @@ -1,10 +1,11 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" +method Main() { } method Test() { var r: R; var s: seq; diff --git a/Test/git-issues/git-issue-374.dfy b/Test/git-issues/git-issue-374.dfy index bdbc7099d31..4c031b7d3ff 100644 --- a/Test/git-issues/git-issue-374.dfy +++ b/Test/git-issues/git-issue-374.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" @@ -13,7 +13,7 @@ class C { ghost function f() : int { 0 } -method main() { +method Main() { var c := new C(f()); } diff --git a/Test/git-issues/git-issue-3883.dfy b/Test/git-issues/git-issue-3883.dfy index aaed6ae9512..018dfcacf43 100644 --- a/Test/git-issues/git-issue-3883.dfy +++ b/Test/git-issues/git-issue-3883.dfy @@ -46,14 +46,14 @@ type ST0 = x: int | x % 5 == 1 witness 16 type ST1 = x: int | (if var m: map := map[]; m == map[] then 0 else 8) <= x method DoIt() { - var t0: ST0; - var t1: ST1; + var t0: ST0 := *; + var t1: ST1 := *; Print(t0, " "); // 16-16 Print(t1, "\n"); // 0-0 } method Print(x: X, suffix: string) { - var y: X; + var y: X := *; print x, "-", y, suffix; } diff --git a/Test/git-issues/git-issue-610.dfy b/Test/git-issues/git-issue-610.dfy index dc090e6ff6b..5e958f768ce 100644 --- a/Test/git-issues/git-issue-610.dfy +++ b/Test/git-issues/git-issue-610.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" +// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment type pos = i:int | i > 0 witness 1 diff --git a/Test/git-issues/git-issue-674.dfy b/Test/git-issues/git-issue-674.dfy index d1643b53019..30a22bd2f8f 100644 --- a/Test/git-issues/git-issue-674.dfy +++ b/Test/git-issues/git-issue-674.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" +// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment type pos = i:int | i > 0 witness 1 diff --git a/Test/git-issues/git-issue-684.dfy b/Test/git-issues/git-issue-684.dfy index bf2983f1cdf..b1fbd7ab036 100644 --- a/Test/git-issues/git-issue-684.dfy +++ b/Test/git-issues/git-issue-684.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" @@ -14,3 +14,5 @@ method TestNestedLet() { var Level2(u, Level1(v)) := x; } +method Main() {} + diff --git a/Test/git-issues/git-issue-784.dfy b/Test/git-issues/git-issue-784.dfy index ae71b0b8f47..78b83f01064 100644 --- a/Test/git-issues/git-issue-784.dfy +++ b/Test/git-issues/git-issue-784.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" @@ -31,3 +31,5 @@ datatype List = Nil | Cons(T, List) { x.AppAssoc(Concat(xs), Concat(l2)); } } + +method Main() {} diff --git a/Test/git-issues/git-issue-817.dfy b/Test/git-issues/git-issue-817.dfy index e7ee0a13d6a..006c718d256 100644 --- a/Test/git-issues/git-issue-817.dfy +++ b/Test/git-issues/git-issue-817.dfy @@ -30,6 +30,7 @@ method m() returns (rr: Result) { assert d.v == 42; assert dd.v == 100; expect d.v == 42 && dd.v == 100; + rr := *; } method mm() returns (rr: Result) { @@ -45,6 +46,7 @@ method mm() returns (rr: Result) { print d[0], " ", dd[0], " ", d != dd, "\n"; // 42 100 true assert d[0] == 42 && dd[0] == 100; expect d[0] == 42 && dd[0] == 100; + rr := *; } method mmm() returns (rr: Result) { @@ -60,6 +62,7 @@ method mmm() returns (rr: Result) { print d[0,0], " ", dd[0,0], " ", d != dd, "\n"; // 42 100 true assert d[0,0] == 42 && dd[0,0] == 100; expect d[0,0] == 42 && dd[0,0] == 100; + rr := *; } class C { diff --git a/Test/git-issues/git-issue-817a.dfy b/Test/git-issues/git-issue-817a.dfy index f4402a28f5e..97826e1aea3 100644 --- a/Test/git-issues/git-issue-817a.dfy +++ b/Test/git-issues/git-issue-817a.dfy @@ -35,6 +35,7 @@ method P() returns (r: Result){ assert a[7] == 200; assert c.data == 9; print c.data, " ", a[7], " ", a[9], "\n"; // 9 200 142 + r := *; } method Main() { diff --git a/Test/git-issues/git-issue-859.dfy b/Test/git-issues/git-issue-859.dfy index 991a447cd5e..461942b734d 100644 --- a/Test/git-issues/git-issue-859.dfy +++ b/Test/git-issues/git-issue-859.dfy @@ -6,7 +6,9 @@ datatype FailureCompatible = Make { function Extract(): (r: real) { 0.0 } } -method M() returns (r: FailureCompatible) { } +method M() returns (r: FailureCompatible) { + r := *; +} method N() returns (x: int) { var s: real :- M(); diff --git a/Test/libraries b/Test/libraries index 44f5891e7b5..7c386fa0b4a 160000 --- a/Test/libraries +++ b/Test/libraries @@ -1 +1 @@ -Subproject commit 44f5891e7b5b21a5f13f139b22fb5559b46de36f +Subproject commit 7c386fa0b4a267715f9bd49948d1af68e1631e6b diff --git a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect index 50785ca4277..67098a5e6cb 100644 --- a/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect +++ b/Test/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect @@ -6,8 +6,8 @@ Diff (changing expected into actual): Dafny program verifier did not attempt verification -System.Func`2[System.Numerics.BigInteger,System.Numerics.BigInteger] -+function (_1_x) { -+ return _1_x; ++function (_3_x) { ++ return _3_x; + } @@ -39,5 +39,4 @@ Diff (changing expected into actual): Executing on C++... -Executing on Dafny Library (.doo)... Executing on Simple Dafny... diff --git a/Test/unicodechars/comp/Arrays.dfy b/Test/unicodechars/comp/Arrays.dfy index d206b7dc373..e0aa3ea7b93 100644 --- a/Test/unicodechars/comp/Arrays.dfy +++ b/Test/unicodechars/comp/Arrays.dfy @@ -1,2 +1,2 @@ -// RUN: %testDafnyForEachCompiler "%s" -- /unicodeChar:1 +// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char include "../../comp/Arrays.dfy" diff --git a/Test/unicodechars/git-issues/github-issue-2928.dfy b/Test/unicodechars/git-issues/github-issue-2928.dfy index 00d9026ba6a..414164a8fe2 100644 --- a/Test/unicodechars/git-issues/github-issue-2928.dfy +++ b/Test/unicodechars/git-issues/github-issue-2928.dfy @@ -1,3 +1,3 @@ -// RUN: %testDafnyForEachCompiler %s -- /unicodeChar:1 +// RUN: %testDafnyForEachCompiler %s -- --unicode-char include "../../git-issues/github-issue-2928.dfy" diff --git a/customBoogie.patch b/customBoogie.patch index 897f7c4876a..af1c84b0564 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- +