Out of resources error reporting

Source/DafnyDriver/CliCompilation.cs

@@ -14,6 +14,7 @@
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Extensions.Logging;
+using VC;
 using Token = Microsoft.Dafny.Token;
 
 namespace DafnyDriver.Commands;
@@ -181,10 +182,13 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
 
         if (Options.Get(CommonOptionBag.ProgressOption)) {
           var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token);
+          var runResult = completed.Result;
+          var resourcesUsed = runResult.ResourceCount.ToString("E1", CultureInfo.InvariantCulture);
           Options.OutputWriter.WriteLine(
-            $"Verified part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
-            $", on line {token.line} (time: {completed.Result.RunTime.Milliseconds}ms, " +
-            $"resource count: {completed.Result.ResourceCount.ToString("E1", CultureInfo.InvariantCulture)})");
+            $"Verification part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
+            $", on line {token.line}, " +
+            $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" +
+            $", taking {runResult.RunTime.Milliseconds}ms and consuming {resourcesUsed} resources");
         }
         if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
           canVerifyResult.Finished.TrySetResult();
@@ -260,6 +264,19 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
     }
   }
 
+  public static string DescribeOutcome(VcOutcome outcome) {
+    return outcome switch {
+      VcOutcome.Correct => "verified successfully",
+      VcOutcome.Errors => "could not prove all assertions",
+      VcOutcome.Inconclusive => "was inconclusive",
+      VcOutcome.TimedOut => "timed out",
+      VcOutcome.OutOfResource => "ran out of resources",
+      VcOutcome.OutOfMemory => "ran out of memory",
+      VcOutcome.SolverException => "ran into a solver exception",
+      _ => throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null)
+    };
+  }
+
   private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int? line) {
     var symbolFilter = Options.Get(VerifyCommand.FilterSymbol);
     if (symbolFilter != null) {

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -163,7 +163,7 @@ public static void ReportVerificationDiagnostics(CliCompilation compilation, IOb
       // We use an intermediate reporter so we can sort the diagnostics from all parts by token
       var batchReporter = new BatchErrorReporter(compilation.Options);
       foreach (var completed in result.Results) {
-        Compilation.ReportDiagnosticsInResult(compilation.Options, result.CanVerify.FullDafnyName, result.CanVerify.NameToken,
+        Compilation.ReportDiagnosticsInResult(compilation.Options, result.CanVerify.FullDafnyName, completed.Task.Token,
           (uint)completed.Result.RunTime.Seconds,
           completed.Result, batchReporter);
       }

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy

@@ -1,5 +1,5 @@
 // RUN: %verify --progress --cores=1 %s &> %t.raw
-// RUN: %sed 's/time: \d*ms/redacted/g' "%t".raw > %t
+// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
 
 method {:isolate_assertions} Foo() {

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy.expect

@@ -1,8 +1,8 @@
 Verified 0/2 symbols. Waiting for Foo to verify.
-Verified part 1/3 of Foo, on line 5 (redacted, resource count: 8.7E+002)
-Verified part 2/3 of Foo, on line 6 (redacted, resource count: 3.1E+003)
-Verified part 3/3 of Foo, on line 7 (redacted, resource count: 2.8E+003)
+Verification part 1/3 of Foo, on line 5, verified successfully, redacted and consuming 8.7E+002 resources
+Verification part 2/3 of Foo, on line 6, verified successfully, redacted and consuming 3.1E+003 resources
+Verification part 3/3 of Foo, on line 7, verified successfully, redacted and consuming 2.8E+003 resources
 Verified 1/2 symbols. Waiting for Bar to verify.
-Verified part 1/1 of Bar, on line 10 (redacted, resource count: 3.1E+003)
+Verification part 1/1 of Bar, on line 10, verified successfully, redacted and consuming 3.1E+003 resources
 
 Dafny program verifier finished with 4 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy

@@ -0,0 +1,13 @@
+// RUN: ! %verify --isolate-assertions --progress "%s" &> %t.raw
+// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
+// RUN: %diff "%s.expect" %t
+
+ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)}
+
+lemma{:resource_limit 10000000} L()
+{
+  assert true;
+  assert f(10, 5) == 0; // runs out of resources
+  assert true;
+  assert f(10, 6) == 0; // runs out of resources
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy.expect

@@ -0,0 +1,26 @@
+Verified 0/2 symbols. Waiting for f to verify.
+Verification part 1/11 of f, on line 5, verified successfully, redacted and consuming 9.5E+002 resources
+Verification part 2/11 of f, on line 5, verified successfully, redacted and consuming 6.2E+003 resources
+Verification part 3/11 of f, on line 5, verified successfully, redacted and consuming 6.7E+003 resources
+Verification part 4/11 of f, on line 5, verified successfully, redacted and consuming 6.7E+003 resources
+Verification part 5/11 of f, on line 5, verified successfully, redacted and consuming 5.8E+003 resources
+Verification part 6/11 of f, on line 5, verified successfully, redacted and consuming 5.9E+003 resources
+Verification part 7/11 of f, on line 5, verified successfully, redacted and consuming 5.9E+003 resources
+Verification part 8/11 of f, on line 5, verified successfully, redacted and consuming 7.8E+003 resources
+Verification part 9/11 of f, on line 5, verified successfully, redacted and consuming 6.0E+003 resources
+Verification part 10/11 of f, on line 5, verified successfully, redacted and consuming 6.0E+003 resources
+Verification part 11/11 of f, on line 5, verified successfully, redacted and consuming 6.1E+003 resources
+Verification part 1/9 of L, on line 7, verified successfully, redacted and consuming 8.7E+002 resources
+Verified 1/2 symbols. Waiting for L to verify.
+Verification part 2/9 of L, on line 9, verified successfully, redacted and consuming 5.6E+003 resources
+Verification part 3/9 of L, on line 10, verified successfully, redacted and consuming 5.8E+003 resources
+Verification part 4/9 of L, on line 10, verified successfully, redacted and consuming 6.0E+003 resources
+Verification part 5/9 of L, on line 11, verified successfully, redacted and consuming 5.5E+003 resources
+Verification part 6/9 of L, on line 12, verified successfully, redacted and consuming 5.5E+003 resources
+Verification part 7/9 of L, on line 12, verified successfully, redacted and consuming 6.8E+003 resources
+Verification part 8/9 of L, on line 10, ran out of resources, redacted and consuming 1.0E+007 resources
+Verification part 9/9 of L, on line 12, ran out of resources, redacted and consuming 1.0E+007 resources
+outOfResourceAndIsolateAssertions.dfy(10,18): Error: Verification out of resource (L)
+outOfResourceAndIsolateAssertions.dfy(12,18): Error: Verification out of resource (L)
+
+Dafny program verifier finished with 18 verified, 0 errors, 2 out of resource

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy

@@ -1,5 +1,5 @@
 // RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw
-// RUN: %sed 's/time: \d*ms/redacted/g' "%t".raw > %t
+// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
 
 method Foo() 

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy.expect

@@ -1,19 +1,19 @@
 Verified 0/5 symbols. Waiting for Foo to verify.
-Verified part 1/3 of Foo, on line 5 (redacted, resource count: 8.7E+002)
-Verified part 2/3 of Foo, on line 7 (redacted, resource count: 3.1E+003)
-Verified part 3/3 of Foo, on line 8 (redacted, resource count: 2.8E+003)
+Verification part 1/3 of Foo, on line 5, verified successfully, redacted and consuming 8.7E+002 resources
+Verification part 2/3 of Foo, on line 7, verified successfully, redacted and consuming 3.1E+003 resources
+Verification part 3/3 of Foo, on line 8, verified successfully, redacted and consuming 2.8E+003 resources
 Verified 1/5 symbols. Waiting for Faz to verify.
-Verified part 1/2 of Faz, on line 11 (redacted, resource count: 8.7E+002)
-Verified part 2/2 of Faz, on line 11 (redacted, resource count: 3.1E+003)
+Verification part 1/2 of Faz, on line 11, verified successfully, redacted and consuming 8.7E+002 resources
+Verification part 2/2 of Faz, on line 11, verified successfully, redacted and consuming 3.1E+003 resources
 Verified 2/5 symbols. Waiting for Fopple to verify.
-Verified part 1/2 of Fopple, on line 13 (redacted, resource count: 8.7E+002)
-Verified part 2/2 of Fopple, on line 13 (redacted, resource count: 3.1E+003)
+Verification part 1/2 of Fopple, on line 13, verified successfully, redacted and consuming 8.7E+002 resources
+Verification part 2/2 of Fopple, on line 13, verified successfully, redacted and consuming 3.1E+003 resources
 Verified 3/5 symbols. Waiting for Burp to verify.
-Verified part 1/3 of Burp, on line 15 (redacted, resource count: 8.7E+002)
-Verified part 2/3 of Burp, on line 17 (redacted, resource count: 3.1E+003)
-Verified part 3/3 of Burp, on line 18 (redacted, resource count: 2.8E+003)
+Verification part 1/3 of Burp, on line 15, verified successfully, redacted and consuming 8.7E+002 resources
+Verification part 2/3 of Burp, on line 17, verified successfully, redacted and consuming 3.1E+003 resources
+Verification part 3/3 of Burp, on line 18, verified successfully, redacted and consuming 2.8E+003 resources
 Verified 4/5 symbols. Waiting for Blanc to verify.
-Verified part 1/2 of Blanc, on line 21 (redacted, resource count: 8.7E+002)
-Verified part 2/2 of Blanc, on line 21 (redacted, resource count: 3.1E+003)
+Verification part 1/2 of Blanc, on line 21, verified successfully, redacted and consuming 8.7E+002 resources
+Verification part 2/2 of Blanc, on line 21, verified successfully, redacted and consuming 3.1E+003 resources
 
 Dafny program verifier finished with 12 verified, 0 errors

docs/dev/news/5281.feat

@@ -0,0 +1 @@
+Improved error reporting when verification times out or runs out of resources, so that when using --isolate-assertions, the error message points to the problematic assertion.