Merge branch 'master' into issue-5238

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
     }
 
     /// <summary>
-    /// 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.
     /// </summary>
     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

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 {

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; }
+}

Source/DafnyDriver/Commands/GenerateTestsCommand.cs

@@ -80,7 +80,7 @@ public static async Task<ExitValue> 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;
     }

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;
     }

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);

Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs

@@ -82,6 +82,9 @@ public static async Task<int> Run(DafnyOptions options) {
     public static ExitValue GetDafnyFiles(DafnyOptions options,
       out List<DafnyFile> dafnyFiles,
       out List<string> 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);

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<TestResult> VerificationToTestResults(VerificationScopeResult result) {

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);

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -205,20 +205,15 @@ bool FinishedStatus(NamedVerifiableStatus method) {
 
   public async Task<PublishDiagnosticsParams> 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<Diagnostic[]> GetLastDiagnostics(TextDocumentItem documentItem, DiagnosticSeverity minimumSeverity = DiagnosticSeverity.Warning,

Source/DafnyServer/Server.cs

@@ -21,6 +21,7 @@ public static void Main(string[] args) {
 
     public static async Task<int> 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);

Source/DafnyTestGeneration/DafnyInfo.cs

@@ -67,7 +67,7 @@ public IList<Type> 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<Type>();
@@ -81,7 +81,7 @@ public List<TypeParameter> 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<TypeParameter>();
@@ -97,7 +97,7 @@ public List<TypeParameter> 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<Type> 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<Type>();
@@ -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<Expression> GetEnsures(List<string> ins, List<string> 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<Expression>();
@@ -235,7 +235,7 @@ public IEnumerable<Expression> GetRequires(List<string> 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<Expression>();
@@ -254,7 +254,7 @@ public IEnumerable<Expression> GetRequires(List<string> 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<Expression> GetRequires(List<string> 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;

Source/DafnyTestGeneration/TestGenerator.cs

@@ -27,6 +27,9 @@ public static async IAsyncEnumerable<string> 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<ProgramModification> 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<ProgramModification>();
@@ -180,6 +183,10 @@ private static void PopulateCoverageReport(CoverageReport coverageReport, Progra
     /// </summary>
     /// <returns></returns>
     public static async IAsyncEnumerable<TestMethod> 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;

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
+  }
+}

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