Dispose executionEngine where it is used, and don't use it when not n…

…eeded (dafny-lang#4286)

Reduces memory usage by closing more Z3 processes and creating fewer

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

Source/DafnyDriver/DafnyDriver.cs

@@ -30,10 +30,9 @@
 
 namespace Microsoft.Dafny {
 
-  public class DafnyDriver {
+  public class DafnyDriver : IDisposable {
     public DafnyOptions Options { get; }
 
-
     private readonly ExecutionEngine engine;
 
     private DafnyDriver(DafnyOptions dafnyOptions) {
@@ -138,10 +137,11 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T
             return 0;
           }
 
-          var driver = new DafnyDriver(dafnyOptions);
+          using (var driver = new DafnyDriver(dafnyOptions)) {
 #pragma warning disable VSTHRD002
-          exitValue = driver.ProcessFilesAsync(dafnyFiles, otherFiles.AsReadOnly(), dafnyOptions).Result;
+            exitValue = driver.ProcessFilesAsync(dafnyFiles, otherFiles.AsReadOnly(), dafnyOptions).Result;
 #pragma warning restore VSTHRD002
+          }
           break;
         case CommandLineArgumentsResult.PREPROCESSING_ERROR:
           return (int)ExitValue.PREPROCESSING_ERROR;
@@ -959,6 +959,9 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
 
     #endregion
 
+    public void Dispose() {
+      engine.Dispose();
+    }
   }
 
   class NoExecutableBackend : IExecutableBackend {

Source/DafnyPipeline.Test/ImplicitAssertionTest.cs

@@ -161,8 +161,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption
       Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}");
     }
 
-    var engine = Bpl.ExecutionEngine.CreateWithoutSharedCache(options);
-    var boogiePrograms = DafnyDriver.Translate(engine.Options, dafnyProgram).ToList();
+    var boogiePrograms = DafnyDriver.Translate(options, dafnyProgram).ToList();
     Assert.Single(boogiePrograms);
     var boogieProgram = boogiePrograms[0].Item2;
     var encountered = new List<string>();

Source/DafnyServer/Server.cs

@@ -8,7 +8,7 @@
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
-  public class Server {
+  public class Server : IDisposable {
     private bool running;
     private readonly ExecutionEngine engine;
 
@@ -228,6 +228,11 @@ VerificationTask ReadVerificationTask(bool inputIsPlaintext) {
 
     void Exit() {
       this.running = false;
+      Dispose();
+    }
+
+    public void Dispose() {
+      engine.Dispose();
     }
   }
 

Source/DafnyTestGeneration/ProgramModification.cs

@@ -106,29 +106,30 @@ private static void SetupForCounterexamples(DafnyOptions options) {
       }
       var options = GenerateTestsCommand.CopyForProcedure(Options, procedure);
       SetupForCounterexamples(options);
-      var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-      var guid = Guid.NewGuid().ToString();
-      program.Resolve(options);
-      program.Typecheck(options);
-      engine.EliminateDeadVariables(program);
-      engine.CollectModSets(program);
-      engine.Inline(program);
       var writer = new StringWriter();
-      var result = await Task.WhenAny(engine.InferAndVerify(writer, program,
+      using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) {
+        var guid = Guid.NewGuid().ToString();
+        program.Resolve(options);
+        program.Typecheck(options);
+        engine.EliminateDeadVariables(program);
+        engine.CollectModSets(program);
+        engine.Inline(program);
+        var result = await Task.WhenAny(engine.InferAndVerify(writer, program,
             new PipelineStatistics(), null,
             _ => { }, guid),
           Task.Delay(TimeSpan.FromSeconds(Options.TimeLimit <= 0 ?
             TestGenerationOptions.DefaultTimeLimit : Options.TimeLimit)));
-      program = null; // allows to garbage collect what is no longer needed
-      counterexampleStatus = Status.Failure;
-      counterexampleLog = null;
-      if (result is not Task<PipelineOutcome>) {
-        if (Options.Verbose) {
-          await options.OutputWriter.WriteLineAsync(
-            $"// No test can be generated for {uniqueId} " +
-            "because the verifier timed out.");
+        program = null; // allows to garbage collect what is no longer needed
+        counterexampleStatus = Status.Failure;
+        counterexampleLog = null;
+        if (result is not Task<PipelineOutcome>) {
+          if (Options.Verbose) {
+            await options.OutputWriter.WriteLineAsync(
+              $"// No test can be generated for {uniqueId} " +
+              "because the verifier timed out.");
+          }
+          return counterexampleLog;
         }
-        return counterexampleLog;
       }
       var log = writer.ToString();
       // make sure that there is a counterexample (i.e. no parse errors, etc):

Source/DafnyTestGeneration/ProgramModifier.cs

@@ -60,8 +60,7 @@ public IEnumerable<ProgramModification> GetModifications(
       program = new FunctionToMethodCallRewriter(this, options).VisitProgram(program);
       program = new AddImplementationsForCalls(options).VisitProgram(program);
       program = new RemoveChecks(options).VisitProgram(program);
-      var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-      engine.CoalesceBlocks(program); // removes redundant basic blocks
+      BlockCoalescer.CoalesceBlocks(program);
       var annotator = new AnnotationVisitor(this, options);
       program = annotator.VisitProgram(program);
       AddAxioms(options, program);