diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 3109c167ccb..79d72f30dcf 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.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: | diff --git a/Scripts/package.py b/Scripts/package.py index f543d37715c..aaffbfe4e20 100755 --- a/Scripts/package.py +++ b/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") diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 2983c3dbf3b..59ffe8bfcbe 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -51,8 +51,8 @@ public static class BoogieOptionBag { IsHidden = true }; - public static readonly Option VerificationTimeLimit = new("--verification-time-limit", - "Limit the number of seconds spent trying to verify each procedure") { + public static readonly Option 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", }; diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index d89a6b973fd..0ecaadeae78 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/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 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: diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs index a4cdf8c92b3..51381672ef5 100644 --- a/Source/DafnyDriver/Commands/ServerCommand.cs +++ b/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; diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index f928e3f5043..0236f2ce5f6 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -13,16 +13,6 @@ true - - - false - false - - - - - $(RUNTIME_IDENTIFIER) - @@ -42,8 +32,8 @@ + - diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index 93087fe8e5d..e6e27c8b151 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/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; diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 67513425d4e..92f1fad7dff 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -6,7 +6,6 @@ enable Microsoft.Dafny.LanguageServer ..\..\Binaries\ - true false MIT README.md diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index d736ee1074e..f9cd46eb532 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -10,16 +10,6 @@ MIT - - false - false - - - - - $(RUNTIME_IDENTIFIER) - - diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 016cf01c491..f4f2f78ffd1 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -15,7 +15,6 @@ - diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy new file mode 100644 index 00000000000..e91e3331f33 --- /dev/null +++ b/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)) +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect new file mode 100644 index 00000000000..b7677c39850 --- /dev/null +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy deleted file mode 100644 index 9ce07b0f267..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy +++ /dev/null @@ -1,2 +0,0 @@ -// RUN: %exits-with 1 %baredafny "" 2> "%t" -// RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect deleted file mode 100644 index 3ccac32363e..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect +++ /dev/null @@ -1 +0,0 @@ -Invalid filename: The value cannot be an empty string. (Parameter 'path') diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index e7965e56414..2c2bc4bc249 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/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 seconds +git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after 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 diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 578b63c6924..8fd4ce1c5dc 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/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:` (was `-timeLimit:`) - 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} diff --git a/docs/news/fix.6006 b/docs/news/6006.fix similarity index 100% rename from docs/news/fix.6006 rename to docs/news/6006.fix diff --git a/docs/news/6028.feat b/docs/news/6028.feat new file mode 100644 index 00000000000..2bfb7957467 --- /dev/null +++ b/docs/news/6028.feat @@ -0,0 +1 @@ +Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit) \ No newline at end of file