Revert "Run integration tests in single process (dafny-lang#3715)"

This reverts commit 47056fd.

.github/workflows/check-deep-tests-reusable.yml

@@ -16,7 +16,7 @@ jobs:
       uses: actions/checkout@v3
       with:
         path: dafny
-        submodules: recursive
+        submodules: true
     - uses: actions/github-script@v6
       if: github.repository_owner == 'dafny-lang'
       with:

.github/workflows/deep-tests.yml

@@ -32,7 +32,6 @@ 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: true # Until the libraries work again
+        submodules: false # 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,7 +32,6 @@ jobs:
       uses: actions/checkout@v3
       with:
         path: dafny
-        submodules: recursive
     - name: Restore tools
       working-directory: dafny
       run: dotnet tool restore
@@ -87,7 +86,6 @@ jobs:
         uses: actions/checkout@v3
         with:
           path: dafny
-          submodules: recursive
 
       - name: Setup dotnet
         uses: actions/setup-dotnet@v3

.github/workflows/runtime-tests.yml

@@ -24,8 +24,6 @@ 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 + "#")) {
-            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));
+            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));
           }
 #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);
-            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));
+            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));
             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 + "#")) {
-                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));
+                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));
               }
 #endif
             var f = fce.Function as ExtremePredicate;
             if (f != null && focalPredicates.Contains(f)) {
 #if DEBUG_PRINT
                 var r = CloneCallAndAddK(fce);
-                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));
+                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));
                 return r;
 #else
               return CloneCallAndAddK(fce);

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -194,10 +194,6 @@ 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)) {
-      builtIns.Options.OutputWriter.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j);
+      Console.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)) {
-      builtIns.Options.OutputWriter.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j);
+      Console.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) {
-        Options.OutputWriter.Write(text);
+        Console.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).PrintProgramLargeStack(program, true);
+      new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgram(program, true);
       Options.ShowEnv = oldValue;
       var programString = stringWriter.GetStringBuilder().Replace("\"", "\"\"").ToString();
 

Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs

@@ -5,7 +5,6 @@
 using System.Linq;
 using System.Reflection;
 using System.Runtime.Loader;
-using System.Text;
 using System.Text.Json;
 using Microsoft.CodeAnalysis;
 using Microsoft.CodeAnalysis.CSharp;
@@ -45,6 +44,7 @@ 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,40 +93,54 @@ 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");
-    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);
+    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;
       }
+    } else {
+      var emitResult = compilation.Emit(outputPath);
 
-      try {
-        var configuration = JsonSerializer.Serialize(
-          new {
-            runtimeOptions = new {
-              tfm = "net6.0",
-              framework = new {
-                name = "Microsoft.NETCore.App",
-                version = "6.0.0",
-                rollForward = "LatestMinor"
+      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"
+                }
               }
-            }
-          }, new JsonSerializerOptions() { WriteIndented = true });
-        File.WriteAllText(outputJson, configuration + Environment.NewLine);
-      } catch (Exception e) {
-        outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}");
+            }, 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;
       }
-    } 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;
@@ -137,24 +151,37 @@ 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, TextWriter errorWriter) {
+  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string/*?*/ targetFilename, ReadOnlyCollection<string> otherFileNames,
+    object compilationResult, TextWriter outputWriter) {
 
     var crx = (CSharpCompilationResult)compilationResult;
 
     foreach (var otherFileName in otherFileNames) {
       if (Path.GetExtension(otherFileName) == ".dll") {
-        var targetDirectory = Path.GetDirectoryName(crx.CompiledAssembly.Location);
-        File.Copy(otherFileName, Path.Combine(targetDirectory!, Path.GetFileName(otherFileName)), true);
+        AssemblyLoadContext.Default.LoadFromAssemblyPath(Path.GetFullPath(otherFileName));
       }
     }
 
     if (crx.CompiledAssembly == null) {
       throw new Exception("Cannot call run target program on a compilation that failed");
     }
-    var psi = PrepareProcessStartInfo("dotnet", new[] { crx.CompiledAssembly.Location }.Concat(Options.MainArgs));
-    return RunProcess(psi, outputWriter, errorWriter) == 0;
+    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;
   }
 
   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 == "-" ? compiler.Options.OutputWriter : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create));
+      TextWriter wr = filename == "-" ? System.Console.Out : 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) {
-      Options.ErrorWriter.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg);
+      Console.Error.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 = Path.GetDirectoryName(assemblyLocation);
+    var codebase = System.IO.Path.GetDirectoryName(assemblyLocation);
     Contract.Assert(codebase != null);
     compilationResult = null;
     var psi = PrepareProcessStartInfo("g++", new List<string> {
@@ -37,14 +37,13 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
       "-o", ComputeExeName(targetFilename),
       targetFilename
     });
-    return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling C++ files.");
+    return 0 == RunProcess(psi, 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, TextWriter errorWriter) {
+  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection<string> otherFileNames,
+    object compilationResult, TextWriter outputWriter) {
     var psi = PrepareProcessStartInfo(ComputeExeName(targetFilename), Options.MainArgs);
-    return 0 == RunProcess(psi, outputWriter, errorWriter);
+    return 0 == RunProcess(psi, outputWriter);
   }
 
   public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".h" };

Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs

@@ -41,14 +41,13 @@ 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,
-    TextWriter errorWriter) {
+  public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain,
+    string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
     Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
 
-    return RunTargetDafnyProgram(targetFilename, outputWriter, errorWriter, false);
+    return RunTargetDafnyProgram(targetFilename, outputWriter, false);
   }
 
   public DafnyBackend(DafnyOptions options) : base(options) {
   }
-}
+}