From ece9b76c31672e08d6c9afea67ed810682ce09b7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 22 Mar 2024 04:48:52 -0700 Subject: [PATCH 1/2] fix: Optimize datatype wrappers only in the absence of trait parents (#5234) This PR makes two changes to when the "erase datatype wrapper" optimization is engaged. * The optimization is disabled if the datatype implements any traits. (Previously, the optimization was still allowed under this condition, which had caused malformed code, see issue #5233.) * Allow the optimization in the presence of ghost fields. (Previously, the optimization was disabled if the datatype contained _any_ fields. But ghost fields pose no problems for compilation.) Fixes #5233 ### How has this been tested? The tests (including the test case from the bug report) were added to `comp/ErasableTypeWrappers.dfy`. 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). --- .../Backends/DatatypeWrapperEraser.cs | 12 ++++--- .../LitTest/comp/ErasableTypeWrappers.dfy | 33 ++++++++++++++++++- .../comp/ErasableTypeWrappers.dfy.expect | 2 ++ docs/dev/news/5234.fix | 2 ++ 4 files changed, 43 insertions(+), 6 deletions(-) create mode 100644 docs/dev/news/5234.fix diff --git a/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs b/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs index cd70d585888..efe344eeab8 100644 --- a/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs +++ b/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs @@ -136,9 +136,10 @@ public static bool GetInnerTypeOfErasableDatatypeWrapper(DafnyOptions options, D /// 2 -- be an inductive datatype (not a "codatatype"), and /// 3 -- have exactly one non-ghost constructor, and /// 4 -- that constructor must have exactly one non-ghost destructor parameter (say, "d" of type "D"), and - /// 5 -- have no fields declared as members, and - /// 6 -- the compiled parts of type "D" must not include the datatype itself, and - /// 7 -- not be declared with {:extern} (since extern code may rely on it being there). + /// 5 -- have no non-ghost fields declared as members, and + /// 6 -- have no parent traits, and + /// 7 -- the compiled parts of type "D" must not include the datatype itself, and + /// 8 -- not be declared with {:extern} (since extern code may rely on it being there). /// /// If the conditions above apply, then the method returns true and sets the out-parameter to the core DatatypeDestructor "d". /// From this return, the compiler (that is, the caller) will arrange to compile type "dt" as type "D". @@ -161,12 +162,13 @@ public static bool IsErasableDatatypeWrapper(DafnyOptions options, DatatypeDecl } /// - /// Check for conditions 2, 3, 4, 5, and 7 (but not 0, 1, and 6) mentioned in the description of IsErasableDatatypeWrapper. + /// Check for conditions 2, 3, 4, 5, 6, and 8 (but not 0, 1, and 7) mentioned in the description of IsErasableDatatypeWrapper. /// private static bool FindUnwrappedCandidate(DafnyOptions options, DatatypeDecl datatypeDecl, out DatatypeDestructor coreDtor) { if (datatypeDecl is IndDatatypeDecl && !datatypeDecl.IsExtern(options, out _, out _) && - !datatypeDecl.Members.Any(member => member is Field)) { + !datatypeDecl.Members.Any(member => member is Field { IsGhost: false }) && + datatypeDecl.ParentTraits.Count == 0) { var nonGhostConstructors = datatypeDecl.Ctors.Where(ctor => !ctor.IsGhost).ToList(); if (nonGhostConstructors.Count == 1) { // there is exactly one non-ghost constructor diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy index 22bb3ed1de0..d2ef145f661 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false --type-system-refresh --general-traits=datatype datatype SingletonRecord = SingletonRecord(u: int) datatype GhostOrNot = ghost Ghost(a: int, b: int) | Compiled(x: int) @@ -18,6 +18,7 @@ method Main() { TestMembers(); OptimizationChecks.Test(); PrintRegressionTests.Test(); + ConditionsThatDisableTheOptimization.Test(); } method TestTargetTypesAndConstructors() { @@ -412,3 +413,33 @@ module PrintRegressionTests { print x, "\n"; } } + +// -------------------------------------------------------------------------------- + +module ConditionsThatDisableTheOptimization { + trait Trait { + function F(): int + } + datatype WithTrait extends Trait = WithTrait(u: int) + { + function F(): int { 5 } + } + + datatype WithCompiledField = WithCompiledField(u: int) + { + const n: int := 100 + } + + datatype WithGhostField = WithGhostField(u: int) + { + ghost const n: int := 100 + } + + method Test() { + var t0 := WithTrait(40); + var t1 := WithCompiledField(41); + var t2 := WithGhostField(42); + print t0, " ", t0.F(), " ", (t0 as Trait).F(), "\n"; // WithTrait(40) 5 5 + print t1, " ", t1.n, " ", t2, "\n"; // WithCompiledField(41) 100 42 + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy.expect index e9ca5b48732..1466b3dce90 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy.expect @@ -18,3 +18,5 @@ HasConst.MakeC(4) (4, 4) OptimizationChecks.Ints.Ints(5, 7) OptimizationChecks.Ints.Ints(5, 7) OptimizationChecks.Ints.AnotherIntsWrapper(OptimizationChecks.Ints.Ints(5, 7)) D D 5 5 +ConditionsThatDisableTheOptimization.WithTrait.WithTrait(40) 5 5 +ConditionsThatDisableTheOptimization.WithCompiledField.WithCompiledField(41) 100 42 diff --git a/docs/dev/news/5234.fix b/docs/dev/news/5234.fix new file mode 100644 index 00000000000..826c4a015ef --- /dev/null +++ b/docs/dev/news/5234.fix @@ -0,0 +1,2 @@ +fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits. +feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields. From 153047bc4ab1a67f6899a5f13ad7b1d17f1d16d5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 22 Mar 2024 16:37:23 +0100 Subject: [PATCH 2/2] Do not use DafnyConsolePrinter when using the modular CLI front-end (#5214) ### Description - `DafnyConsolePrinter` globally stores information resulting from verification, which consumes memory. Previously it was causing out of memory issues, and then we reduced the amount of memory it consumed, but it still consumes an amount of memory linear to the amount of verification you're doing in the CLI call. By not using this class, which is not required when using the modular CLI front-end, we remove one cause of memory leaks. ### How has this been tested? - Refactoring, covered by existing tests. 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). --- Source/DafnyCore/DafnyOptions.cs | 3 +- Source/DafnyCore/NullPrinter.cs | 33 +++++++++++++++++++ .../Commands/GenerateTestsCommand.cs | 2 +- Source/DafnyDriver/DafnyNewCli.cs | 2 +- .../Legacy/DafnyBackwardsCompatibleCli.cs | 2 +- .../Legacy/SynchronousCliCompilation.cs | 13 +++++--- .../DafnyDriver/VerificationResultLogger.cs | 1 - .../Synchronization/VerificationStatusTest.cs | 4 +-- .../Util/ClientBasedLanguageServerTest.cs | 21 +++++------- Source/DafnyServer/Server.cs | 1 + Source/DafnyTestGeneration/DafnyInfo.cs | 22 ++++++------- Source/DafnyTestGeneration/TestGenerator.cs | 11 +++++-- 12 files changed, 76 insertions(+), 39 deletions(-) create mode 100644 Source/DafnyCore/NullPrinter.cs diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 900051eadb0..103291e3c7d 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -271,8 +271,7 @@ public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter NormalizeNames = true; EmitDebugInformation = false; Backend = new CsharpBackend(this); - Printer = new DafnyConsolePrinter(this); - Printer.Options = this; + Printer = new NullPrinter(); } public override string VersionNumber { diff --git a/Source/DafnyCore/NullPrinter.cs b/Source/DafnyCore/NullPrinter.cs new file mode 100644 index 00000000000..6bc20d8e2c2 --- /dev/null +++ b/Source/DafnyCore/NullPrinter.cs @@ -0,0 +1,33 @@ +using System.IO; +using Microsoft.Boogie; +using VCGeneration; + +namespace Microsoft.Dafny; + +public class NullPrinter : OutputPrinter { + public void ErrorWriteLine(TextWriter tw, string s) { + } + + public void ErrorWriteLine(TextWriter tw, string format, params object[] args) { + } + + public void AdvisoryWriteLine(TextWriter output, string format, params object[] args) { + } + + public void Inform(string s, TextWriter tw) { + } + + public void WriteTrailer(TextWriter textWriter, Boogie.PipelineStatistics stats) { + } + + public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true) { + } + + public void ReportBplError(Boogie.IToken tok, string message, bool error, TextWriter tw, string category = null) { + } + + public void ReportEndVerifyImplementation(Boogie.Implementation implementation, Boogie.ImplementationRunResult result) { + } + + public Boogie.ExecutionEngineOptions Options { get; set; } +} \ No newline at end of file diff --git a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs index 1fabe0cdc80..ddfa2d72476 100644 --- a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs +++ b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs @@ -80,7 +80,7 @@ public static async Task GenerateTests(DafnyOptions options) { if (dafnyFiles.Count > 1 && options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) { - options.Printer.ErrorWriteLine(options.OutputWriter, + await options.OutputWriter.WriteLineAsync( "*** Error: Only one .dfy file can be specified for testing"); return ExitValue.PREPROCESSING_ERROR; } diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs index d2ea5b4c8fc..5497dfe02ec 100644 --- a/Source/DafnyDriver/DafnyNewCli.cs +++ b/Source/DafnyDriver/DafnyNewCli.cs @@ -154,7 +154,7 @@ private static bool ProcessOption(InvocationContext context, Option option, Dafn dafnyOptions.ApplyBinding(option); } catch (Exception e) { context.ExitCode = (int)ExitValue.PREPROCESSING_ERROR; - dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, + dafnyOptions.OutputWriter.WriteLine( $"Invalid value for option {option.Name}: {e.Message}"); return false; } diff --git a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs index 3020dc3dfce..d513245f711 100644 --- a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs +++ b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs @@ -75,7 +75,7 @@ private static ILegacyParseArguments TryLegacyArgumentParser( if (!keywordForNewMode.Contains(first)) { if (first.Length > 0 && first[0] != '/' && first[0] != '-' && !File.Exists(first) && first.IndexOf('.') == -1) { - dafnyOptions.Printer.ErrorWriteLine(dafnyOptions.OutputWriter, + dafnyOptions.OutputWriter.WriteLine( "*** Error: '{0}': The first input must be a command or a legacy option or file with supported extension", first); return new ExitImmediately(ExitValue.PREPROCESSING_ERROR); diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index 1a382917205..9b20ff6cb92 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -82,6 +82,9 @@ public static async Task Run(DafnyOptions options) { public static ExitValue GetDafnyFiles(DafnyOptions options, out List dafnyFiles, out List otherFiles) { + if (options.Printer is NullPrinter) { + options.Printer = new DafnyConsolePrinter(options); + } if (options.DafnyProject != null) { foreach (var uri in options.DafnyProject.GetRootSourceUris(OnDiskFileSystem.Instance)) { @@ -98,13 +101,13 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, options.CliRootSourceUris.Add(uri); dafnyFiles.Add(DafnyFile.CreateAndValidate(new ConsoleErrorReporter(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken)); } else if (options.CliRootSourceUris.Count == 0) { - options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: No input files were specified in command-line. " + options.Environment); + options.ErrorWriter.WriteLine("*** Error: No input files were specified in command-line. " + options.Environment); return ExitValue.PREPROCESSING_ERROR; } if (options.XmlSink != null) { string errMsg = options.XmlSink.Open(); if (errMsg != null) { - options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: " + errMsg); + options.ErrorWriter.WriteLine("*** Error: " + errMsg); return ExitValue.PREPROCESSING_ERROR; } } @@ -143,10 +146,10 @@ public static ExitValue GetDafnyFiles(DafnyOptions options, isDafnyFile = true; } } catch (ArgumentException e) { - options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: {0}: ", nameToShow, e.Message); + options.ErrorWriter.WriteLine("*** Error: {0}: ", nameToShow, e.Message); return ExitValue.PREPROCESSING_ERROR; } catch (Exception e) { - options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: {0}: {1}", nameToShow, e.Message); + options.ErrorWriter.WriteLine("*** Error: {0}: {1}", nameToShow, e.Message); return ExitValue.PREPROCESSING_ERROR; } @@ -226,7 +229,7 @@ private static IExecutableBackend GetBackend(DafnyOptions options) { if (backend == null) { if (options.CompilerName != null) { var known = String.Join(", ", backends.Select(c => $"'{c.TargetId}' ({c.TargetName})")); - options.Printer.ErrorWriteLine(options.ErrorWriter, + options.ErrorWriter.WriteLine( $"*** 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}"); } else { backend = new NoExecutableBackend(options); diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs index b6f3563a885..df722852558 100644 --- a/Source/DafnyDriver/VerificationResultLogger.cs +++ b/Source/DafnyDriver/VerificationResultLogger.cs @@ -121,7 +121,6 @@ public async Task Finish() { foreach (var formatLogger in formatLoggers) { await formatLogger.Flush(); } - await options.OutputWriter.FlushAsync(); } public static IEnumerable VerificationToTestResults(VerificationScopeResult result) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 5648a76d363..8244ab2a08a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -370,8 +370,8 @@ await SetUp(options => { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); ApplyChange(ref documentItem, new Range(0, 22, 0, 26), "false"); var methodHeader = new Position(0, 7); - await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken); - await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationToken); + var startedVerification = await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken); + Assert.True(startedVerification); var preSaveDiagnostics = await GetLastDiagnostics(documentItem, allowStale: true); Assert.Single(preSaveDiagnostics); await client.SaveDocumentAndWaitAsync(documentItem, CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 10ee6891160..43039a26f37 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -205,20 +205,15 @@ bool FinishedStatus(NamedVerifiableStatus method) { public async Task GetLastDiagnosticsParams(TextDocumentItem documentItem, CancellationToken cancellationToken, bool allowStale = false) { var status = await WaitUntilAllStatusAreCompleted(documentItem, cancellationToken, allowStale); - logger.LogTrace("GetLastDiagnosticsParams status was: " + status.Stringify()); - await Task.Delay(10); - try { - var result = diagnosticsReceiver.History.Last(d => d.Uri == documentItem.Uri); - diagnosticsReceiver.ClearQueue(); - return result; - } catch (InvalidOperationException) { - await output.WriteLineAsync( - $"GetLastDiagnosticsParams didn't find the right diagnostics. History contained: {diagnosticsReceiver.History.Stringify()}"); - var diagnostic = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); - await output.WriteLineAsync( - $"After waiting for diagnostics, got: {diagnostic.Stringify()}"); - throw; + var result = diagnosticsReceiver.History.LastOrDefault(d => d.Uri == documentItem.Uri); + while (result == null) { + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); + result = diagnosticsReceiver.History.LastOrDefault(d => d.Uri == documentItem.Uri); + logger.LogInformation( + $"GetLastDiagnosticsParams didn't find the right diagnostics after getting status {status}. Waited to get these diagnostics: {diagnostics.Stringify()}"); } + diagnosticsReceiver.ClearQueue(); + return result; } public async Task GetLastDiagnostics(TextDocumentItem documentItem, DiagnosticSeverity minimumSeverity = DiagnosticSeverity.Warning, diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 76117e01a2f..c47582e933f 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -21,6 +21,7 @@ public static void Main(string[] args) { public static async Task MainWithWriters(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] args) { var options = DafnyOptions.Create(outputWriter); + options.Printer = new DafnyConsolePrinter(options); options.Set(CommonOptionBag.AllowAxioms, true); Console.SetError(outputWriter); ServerUtils.ApplyArgs(args, options); diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index c25d7e58da1..aaef143ea0a 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -67,7 +67,7 @@ public IList GetReturnTypes(string callable) { { Utils.UseFullName(functions[callable].ResultType) }; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callable}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callable}"); SetNonZeroExitCode = true; return new List(); @@ -81,7 +81,7 @@ public List GetTypeArgs(string callable) { return functions[callable].TypeArgs; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callable}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callable}"); SetNonZeroExitCode = true; return new List(); @@ -97,7 +97,7 @@ public List GetTypeArgsWithParents(string callable) { result.AddRange(functions[callable].TypeArgs); clazz = functions[callable].EnclosingClass; } else { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callable}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callable}"); SetNonZeroExitCode = true; return result; @@ -116,7 +116,7 @@ public IList GetFormalsTypes(string callable) { Utils.UseFullName(arg.Type)).ToList(); ; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callable}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callable}"); SetNonZeroExitCode = true; return new List(); @@ -130,7 +130,7 @@ public bool IsStatic(string callable) { return functions[callable].IsStatic; } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callable}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callable}"); SetNonZeroExitCode = true; return true; @@ -210,7 +210,7 @@ public IEnumerable GetEnsures(List ins, List outs, s .Where(e => e != null); } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callableName}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callableName}"); SetNonZeroExitCode = true; return new List(); @@ -235,7 +235,7 @@ public IEnumerable GetRequires(List ins, string callableName .Where(e => e != null); } - Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: Test Generation failed to identify callable {callableName}"); + Options.ErrorWriter.WriteLine($"*** Error: Test Generation failed to identify callable {callableName}"); SetNonZeroExitCode = true; return new List(); @@ -254,7 +254,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(Options.ErrorWriter, + Options.ErrorWriter.WriteLine( $"*** Error: Test Generation failed to identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; @@ -286,7 +286,7 @@ public IEnumerable GetRequires(List ins, string callableName public bool IsTrait(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, + Options.ErrorWriter.WriteLine( $"*** Error: Test Generation failed to identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; @@ -304,7 +304,7 @@ public bool IsClassType(UserDefinedType/*?*/ type) { public bool IsExtern(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, + Options.ErrorWriter.WriteLine( $"*** Error: Test Generation failed to identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; @@ -315,7 +315,7 @@ public bool IsExtern(UserDefinedType/*?*/ type) { public Constructor/*?*/ GetConstructor(UserDefinedType/*?*/ type) { if (type == null || !classes.ContainsKey(type.Name)) { - Options.Printer.ErrorWriteLine(Options.ErrorWriter, + Options.ErrorWriter.WriteLine( $"*** Error: Test Generation failed to identify type {type?.Name ?? " (null) "}"); SetNonZeroExitCode = true; diff --git a/Source/DafnyTestGeneration/TestGenerator.cs b/Source/DafnyTestGeneration/TestGenerator.cs index 7450939b3e7..0b10ac2d7eb 100644 --- a/Source/DafnyTestGeneration/TestGenerator.cs +++ b/Source/DafnyTestGeneration/TestGenerator.cs @@ -27,6 +27,9 @@ public static async IAsyncEnumerable GetDeadCodeStatistics(Program progr lock (program.Options.ProverOptions) { program.Options.ProcessSolverOptions(new ConsoleErrorReporter(program.Options), Token.Cli); } + if (program.Options.Printer is NullPrinter) { + program.Options.Printer = new DafnyConsolePrinter(program.Options); + } program.Reporter.Options.PrintMode = PrintModes.Everything; @@ -103,7 +106,7 @@ private static IEnumerable GetModifications(Modifications c var success = Inlining.InliningTranslator.TranslateForFutureInlining(program, options, out var boogieProgram); dafnyInfo = null; if (!success) { - options.Printer.ErrorWriteLine(options.ErrorWriter, + options.ErrorWriter.WriteLine( $"*** Error: Failed at resolving or translating the inlined Dafny code."); SetNonZeroExitCode = true; return new List(); @@ -180,6 +183,10 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra /// /// public static async IAsyncEnumerable GetTestMethodsForProgram(Program program, Modifications cache = null) { + if (program.Options.Printer is NullPrinter) { + program.Options.Printer = new DafnyConsolePrinter(program.Options); + } + lock (program.Options.ProverOptions) { program.Options.ProcessSolverOptions(new ConsoleErrorReporter(program.Options), Token.Cli); } @@ -257,7 +264,7 @@ string EscapeDafnyStringLiteral(string str) { PopulateCoverageReport(report, program, cache); if (methodsGenerated == 0) { - options.Printer.ErrorWriteLine(options.ErrorWriter, + await options.ErrorWriter.WriteLineAsync( "*** Error: No tests were generated, because no code points could be " + "proven reachable (do you have a false assumption in the program?)"); SetNonZeroExitCode = true;