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

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