Run integration tests in single process (dafny-lang#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

<small>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).</small>

.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:

.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

.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

.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

.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:

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

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;

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

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 {

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

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<string> otherFileNames,
-    object compilationResult, TextWriter outputWriter) {
+  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain,
+    string targetFilename /*?*/, ReadOnlyCollection<string> 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) {

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

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

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<string> {
@@ -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<string> otherFileNames,
-    object compilationResult, TextWriter outputWriter) {
+  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/,
+    string targetFilename, ReadOnlyCollection<string> 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<string> SupportedExtensions => new HashSet<string> { ".h" };

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<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
+  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, /*?*/
+    string targetFilename, ReadOnlyCollection<string> 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) {
   }
-}
+}