Set a default verification time limit (#6028)

Fixes dafny-lang/ide-vscode#514

### What was changed?
Set a default verification time limit

### How has this been tested?
Added a CLI test that checks there is a default time-out

<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/DafnyCore/Options/BoogieOptionBag.cs

@@ -51,8 +51,8 @@ public static class BoogieOptionBag {
     IsHidden = true
   };
 
-  public static readonly Option<uint> VerificationTimeLimit = new("--verification-time-limit",
-    "Limit the number of seconds spent trying to verify each procedure") {
+  public static readonly Option<uint> VerificationTimeLimit = new("--verification-time-limit", () => 30,
+    "Limit the number of seconds spent trying to verify each assertion batch. A value of 0 indicates no limit") {
     ArgumentHelpName = "seconds",
   };
 

Source/DafnyCore/Pipeline/Compilation.cs

@@ -4,6 +4,7 @@
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.CommandLine;
+using System.CommandLine.Help;
 using System.IO;
 using System.Linq;
 using System.Reactive;
@@ -560,17 +561,96 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
       errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel);
     }
 
-    // This reports problems that are not captured by counter-examples, like a time-out
-    // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options.
-    var boogieEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(),
-      CustomStackSizePoolTaskScheduler.Create(0, 0));
-    boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, null, false),
-      name, token, null, TextWriter.Null,
-      timeLimit, result.CounterExamples);
+    var outcomeError = ReportOutcome(options, outcome, name, token, timeLimit, result.CounterExamples);
+    if (outcomeError != null) {
+      errorReporter.ReportBoogieError(outcomeError, null, false);
+    }
+  }
+
+  private static ErrorInformation? ReportOutcome(DafnyOptions options,
+      VcOutcome vcOutcome, string name,
+      IToken token, uint timeLimit, List<Counterexample> errors) {
+    ErrorInformation? errorInfo = null;
+
+    switch (vcOutcome) {
+      case VcOutcome.Correct:
+        break;
+      case VcOutcome.Errors:
+      case VcOutcome.TimedOut: {
+          if (vcOutcome != VcOutcome.TimedOut &&
+              (!errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) {
+            break;
+          }
+
+          string msg = string.Format("Verification of '{1}' timed out after {0} seconds. (the limit can be increased using --verification-time-limit)", timeLimit, name);
+          errorInfo = ErrorInformation.Create(token, msg);
+
+          //  Report timed out assertions as auxiliary info.
+          var comparer = new CounterexampleComparer();
+          var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(comparer)
+            .OrderBy(x => x, comparer).ToList();
+          if (0 < timedOutAssertions.Count) {
+            errorInfo!.Msg += $" with {timedOutAssertions.Count} check(s) that timed out individually";
+          }
+
+          foreach (Counterexample error in timedOutAssertions) {
+            IToken tok;
+            string auxMsg = null!;
+            switch (error) {
+              case CallCounterexample callCounterexample:
+                tok = callCounterexample.FailingCall.tok;
+                auxMsg = callCounterexample.FailingCall.Description.FailureDescription;
+                break;
+              case ReturnCounterexample returnCounterexample:
+                tok = returnCounterexample.FailingReturn.tok;
+                auxMsg = returnCounterexample.FailingReturn.Description.FailureDescription;
+                break;
+              case AssertCounterexample assertError: {
+                  tok = assertError.FailingAssert.tok;
+                  if (!(assertError.FailingAssert.ErrorMessage == null ||
+                        ((ExecutionEngineOptions)options).ForceBplErrors)) {
+                    auxMsg = assertError.FailingAssert.ErrorMessage;
+                  }
+
+                  auxMsg ??= assertError.FailingAssert.Description.FailureDescription;
+                  break;
+                }
+              default: throw new Exception();
+            }
+
+            errorInfo.AddAuxInfo(tok, auxMsg, "Unverified check due to timeout");
+          }
+
+          break;
+        }
+      case VcOutcome.OutOfResource: {
+          string msg = "Verification out of resource (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+      case VcOutcome.OutOfMemory: {
+          string msg = "Verification out of memory (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+      case VcOutcome.SolverException: {
+          string msg = "Verification encountered solver exception (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+
+      case VcOutcome.Inconclusive: {
+          string msg = "Verification inconclusive (" + name + ")";
+          errorInfo = ErrorInformation.Create(token, msg);
+        }
+        break;
+    }
+
+    return errorInfo;
   }
 
   private static void AddAssertedExprToCounterExampleErrorInfo(
-      DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) {
+    DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) {
     Boogie.ProofObligationDescription? boogieProofObligationDesc = null;
     switch (errorInformation.Kind) {
       case ErrorKind.Assertion:

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy

@@ -0,0 +1,17 @@
+// RUN: ! %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Foo() {
+  // Assert something that takes a long time to verify
+  assert Ack(4, 2) == 1;
+}
+
+function Ack(m: nat, n: nat): nat
+{
+  if m == 0 then
+    n + 1
+  else if n == 0 then
+    Ack(m - 1, 1)
+  else
+    Ack(m - 1, Ack(m, n - 1))
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect

@@ -0,0 +1,7 @@
+defaultTimeLimit.dfy(4,7): Error: Verification of 'Foo' timed out after 30 seconds. (the limit can be increased using --verification-time-limit)
+  |
+4 | method Foo() {
+  |        ^^^
+
+
+Dafny program verifier finished with 1 verified, 0 errors, 1 time out

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect

@@ -1,5 +1,5 @@
 git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated
-git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
+git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds. (the limit can be increased using --verification-time-limit)
 git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved
 git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved

docs/DafnyRef/UserGuide.md

@@ -2769,7 +2769,7 @@ The following options are also commonly used:
   but a large positive number reports more errors per run
 
 * `--verification-time-limit:<n>` (was `-timeLimit:<n>`) - limits 
-  the number of seconds spent trying to verify each procedure.
+  the number of seconds spent trying to verify each assertion batch.
 
 
 ### 13.9.11. Controlling test generation {#sec-controlling-test-gen}

docs/news/6028.feat

@@ -0,0 +1 @@
+Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit)