Remove .Wait call to see if this resolved CI timeouts (#925)

boogie-org · Jul 31, 2024 · 5d6c113 · 5d6c113
1 parent b5ea010
commit 5d6c113
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 23 deletions.
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -542,7 +542,7 @@ public async Task<PipelineOutcome> InferAndVerify(
 
       var start = DateTime.UtcNow;
 
-      var processedProgram = PreProcessProgramVerification(program);
+      var processedProgram = await PreProcessProgramVerification(program);
 
       foreach (var action in Options.UseResolvedProgram) {
         action(Options, processedProgram);
@@ -578,7 +578,7 @@ public async Task<PipelineOutcome> InferAndVerify(
       return outcome;
     }
 
-    private ProcessedProgram PreProcessProgramVerification(Program program)
+    private Task<ProcessedProgram> PreProcessProgramVerification(Program program)
     {
       return LargeThreadTaskFactory.StartNew(() =>
       {
@@ -613,7 +613,7 @@ private ProcessedProgram PreProcessProgramVerification(Program program)
 
         program.DeclarationDependencies = Pruner.ComputeDeclarationDependencies(Options, program);
         return processedProgram;
-      }).Result;
+      });
     }
 
     private ProcessedProgram ExtractLoops(Program program)
@@ -711,7 +711,7 @@ public void Error(IToken tok, string msg)
       }
     }
 
-    public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program)
+    public async Task<IReadOnlyList<IVerificationTask>> GetVerificationTasks(Program program)
     {
       var sink = new CollectingErrorSink();
       var resolutionErrors = program.Resolve(Options, sink);
@@ -731,7 +731,7 @@ public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program)
       CoalesceBlocks(program);
       Inline(program);
 
-      var processedProgram = PreProcessProgramVerification(program);
+      var processedProgram = await PreProcessProgramVerification(program);
       return GetPrioritizedImplementations(program).SelectMany(implementation =>
       {
         var writer = TextWriter.Null;

diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -62,10 +62,7 @@ procedure Procedure(y: int)
     Parser.Parse(programString, "fakeFilename10", out var program);
     var options = CommandLineOptions.FromArguments(TextWriter.Null);
     var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-    Assert.Throws<ArgumentException>(() =>
-    {
-      var tasks = engine.GetVerificationTasks(program);
-    });
+    Assert.ThrowsAsync<ArgumentException>(() => engine.GetVerificationTasks(program));
   }
 
   [Test]
@@ -80,10 +77,7 @@ procedure Procedure(y: int)
     Parser.Parse(programString, "fakeFilename10", out var program);
     var options = CommandLineOptions.FromArguments(TextWriter.Null);
     var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-    Assert.Throws<ArgumentException>(() =>
-    {
-      var tasks = engine.GetVerificationTasks(program);
-    });
+    Assert.ThrowsAsync<ArgumentException>(() => engine.GetVerificationTasks(program));
   }
 
   [Test]
@@ -102,7 +96,7 @@ procedure Procedure(y: int)
     options.VcsSplitOnEveryAssert = true;
     options.PrintErrorModel = 1;
     var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-    var tasks = engine.GetVerificationTasks(program);
+    var tasks = await engine.GetVerificationTasks(program);
 
     // The first split is empty. Maybe it can be optimized away
     Assert.AreEqual(5, tasks.Count);
@@ -133,7 +127,7 @@ procedure Second(y: int)
     var options = CommandLineOptions.FromArguments(TextWriter.Null);
     options.PrintErrorModel = 1;
     var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-    var tasks = engine.GetVerificationTasks(program);
+    var tasks = await engine.GetVerificationTasks(program);
     Assert.AreEqual(2, tasks.Count);
     Assert.NotNull(tasks[0].Split.Implementation);
     var result1 = await tasks[0].TryRun()!.ToTask();
@@ -292,7 +286,7 @@ procedure Foo(x: int) {
 }".TrimStart();
     var result = Parser.Parse(source, "fakeFilename1", out var program);
     Assert.AreEqual(0, result);
-    var tasks = engine.GetVerificationTasks(program)[0];
+    var tasks = (await engine.GetVerificationTasks(program))[0];
     var statusList1 = new List<IVerificationStatus>();
     var firstStatuses = tasks.TryRun()!;
     await firstStatuses.Where(s => s is Running).FirstAsync().ToTask();
@@ -328,7 +322,7 @@ procedure Foo(x: int) {
 }".TrimStart();
     var result = Parser.Parse(source, "fakeFilename1", out var program);
     Assert.AreEqual(0, result);
-    var task = engine.GetVerificationTasks(program)[0];
+    var task = (await engine.GetVerificationTasks(program))[0];
     var statusList1 = new List<IVerificationStatus>();
     var firstStatuses = task.TryRun()!;
     var runDuringRun1 = task.TryRun();
@@ -372,7 +366,7 @@ public async Task FromSeedResetsState() {
 }".TrimStart();
     Parser.Parse(source, "fakeFilename1", out var program);
     Assert.AreEqual("Bad", program.Implementations.ElementAt(0).Name);
-    var tasks = engine.GetVerificationTasks(program);
+    var tasks = await engine.GetVerificationTasks(program);
     var task = tasks[0];
     await task.TryRun()!.ToTask();
     var secondResult = task.FromSeed(100).TryRun()!;
@@ -402,7 +396,7 @@ public async Task StatusTest() {
 ";
     Parser.Parse(programString, "fakeFilename1", out var program);
     Assert.AreEqual("Bad", program.Implementations.ElementAt(0).Name);
-    var tasks = engine.GetVerificationTasks(program);
+    var tasks = await engine.GetVerificationTasks(program);
     var statusList = new List<(string, IVerificationStatus)>();
 
     var first = tasks[0];
@@ -472,11 +466,13 @@ public async Task SolverCrash()
     // We limit the number of checkers to 1.
     options.VcsCores = 1;
 
-    var outcome1 = await executionEngine.GetVerificationTasks(terminatingProgram)[0].TryRun()!.ToTask();
-    Assert.IsTrue(outcome1 is Completed completed && completed.Result.Outcome == SolverOutcome.Undetermined);
+    var tasks1 = await executionEngine.GetVerificationTasks(terminatingProgram);
+    var outcome1 = await tasks1[0].TryRun()!.ToTask();
+    Assert.IsTrue(outcome1 is Completed { Result.Outcome: SolverOutcome.Undetermined });
     options.CreateSolver = (_ ,_ ) => new UnsatSolver();
-    var outcome2 = await executionEngine.GetVerificationTasks(terminatingProgram)[0].TryRun()!.ToTask();
-    Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.Outcome == SolverOutcome.Valid);
+    var tasks2 = await executionEngine.GetVerificationTasks(terminatingProgram);
+    var outcome2 = await tasks2[0].TryRun()!.ToTask();
+    Assert.IsTrue(outcome2 is Completed { Result.Outcome: SolverOutcome.Valid });
   }
 
   [Test]