Merge branch 'master' into fix_5746

.github/workflows/integration-tests-reusable.yml

@@ -72,6 +72,11 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{ env.dotnet-version }}
+    #  Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 6.0.x
     - name: C++ for ubuntu 20.04
       if: matrix.os == 'ubuntu-20.04'
       run: |

Scripts/package.py

@@ -161,7 +161,6 @@ def build(self):
         if path.exists(self.buildDirectory):
             shutil.rmtree(self.buildDirectory)
         run(["make", "--quiet", "clean"])
-        self.run_publish("DafnyLanguageServer")
         self.run_publish("DafnyServer")
         self.run_publish("DafnyRuntime", "netstandard2.0")
         self.run_publish("DafnyRuntime", "net452")

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/DafnyDriver/Commands/ServerCommand.cs

@@ -1,6 +1,4 @@
-using System.Collections.Generic;
 using System.CommandLine;
-using DafnyCore;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;

Source/DafnyDriver/DafnyDriver.csproj

@@ -13,16 +13,6 @@
 
       <IsPackable>true</IsPackable>
   </PropertyGroup>
-
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
-    <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
-    <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
-  </PropertyGroup>
-
-  <!-- Working around some stange behavior in dotnet publish: https://github.com/dotnet/sdk/issues/10566 -->
-  <PropertyGroup Condition="$(RUNTIME_IDENTIFIER) != ''">
-    <RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>
-  </PropertyGroup>
 
   <ItemGroup>
     <PackageReference Include="Microsoft.TestPlatform.Extensions.TrxLogger" Version="17.9.0" />
@@ -42,8 +32,8 @@
 
   <ItemGroup>
     <ProjectReference Include="..\DafnyCore\DafnyCore.csproj" />
+    <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
     <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs

@@ -4,7 +4,6 @@
 using System.Linq;
 using System.Text.Json.Nodes;
 using DafnyCore.Verifier;
-using DafnyServer;
 using Microsoft.Boogie;
 using VC;
 

Source/DafnyLanguageServer/DafnyLanguageServer.csproj

@@ -6,7 +6,6 @@
     <Nullable>enable</Nullable>
     <RootNamespace>Microsoft.Dafny.LanguageServer</RootNamespace>
     <OutputPath>..\..\Binaries\</OutputPath>
-    <IsPackable>true</IsPackable>
     <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
     <PackageReadmeFile>README.md</PackageReadmeFile>

Source/DafnyServer/DafnyServer.csproj

@@ -10,16 +10,6 @@
       <PackageLicenseExpression>MIT</PackageLicenseExpression>
   </PropertyGroup>
 
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
-    <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
-    <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
-  </PropertyGroup>
-
-  <!-- Working around some stange behavior in dotnet publish: https://github.com/dotnet/sdk/issues/10566 -->
-  <PropertyGroup Condition="$(RUNTIME_IDENTIFIER) != ''">
-    <RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>
-  </PropertyGroup>
-
   <ItemGroup>
     <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />

Source/DafnyTestGeneration/DafnyTestGeneration.csproj

@@ -15,7 +15,6 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>
 

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)