diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 933c86c1f6c..56228a4cf01 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -689,6 +689,22 @@ private static PrefixNameModule ShortenPrefix(PrefixNameModule prefixNameModule) return prefixNameModule with { Parts = rest }; } + private static readonly List<(string, string)> incompatibleAttributePairs = + new() { + ("rlimit", "resource_limit") + }; + + private void CheckIncompatibleAttributes(ModuleResolver resolver, Attributes attrs) { + foreach (var pair in incompatibleAttributePairs) { + var attr1 = Attributes.Find(attrs, pair.Item1); + var attr2 = Attributes.Find(attrs, pair.Item2); + if (attr1 is not null && attr2 is not null) { + resolver.reporter.Error(MessageSource.Resolver, attr1.tok, + $"the {pair.Item1} and {pair.Item2} attributes cannot be used together"); + } + } + } + public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useImports) { Contract.Requires(this != null); var sig = new ModuleSignature(); @@ -767,6 +783,9 @@ public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useIm foreach (MemberDecl m in members.Values) { Contract.Assert(!m.HasStaticKeyword || Attributes.Contains(m.Attributes, "opaque_reveal")); + + CheckIncompatibleAttributes(resolver, m.Attributes); + if (m is Function or Method or ConstantField) { sig.StaticMembers[m.Name] = m; } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 9c2f592e14c..e482fd02c74 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -7,6 +7,7 @@ using System.Collections.ObjectModel; using System.CommandLine; using System.Diagnostics; +using System.Globalization; using System.Linq; using System.IO; using System.Reflection; @@ -358,6 +359,10 @@ private static string[] ParsePluginArguments(string argumentsString) { ).ToArray(); } + public static bool TryParseResourceCount(string value, out uint result) { + return uint.TryParse(value, NumberStyles.AllowExponent, null, out result); + } + /// /// Automatic shallow-copy constructor /// diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 675cea0ea44..5bbf99a944e 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -63,7 +63,18 @@ public static class BoogieOptionBag { new("--error-limit", () => 5, "Set the maximum number of errors to report (0 for unlimited)."); public static readonly Option SolverResourceLimit = new("--resource-limit", - @"Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program. Multiplied by 1000 before sending to Z3."); + result => { + var value = result.Tokens[^1].Value; + + if (DafnyOptions.TryParseResourceCount(value, out var number)) { + return number; + } + + result.ErrorMessage = $"Cannot parse resource limit: {value}"; + return 0; + }, + isDefault: false, + @"Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program."); public static readonly Option SolverPlugin = new("--solver-plugin", @"Dafny uses Boogie as part of its verification process. This option allows customising that part using a Boogie plugin. More information about Boogie can be found at https://github.com/boogie-org/boogie. Information on how to construct Boogie plugins can be found by looking at the code in https://github.com/boogie-org/boogie/blob/v2.16.3/Source/Provers/SMTLib/ProverUtil.cs#L316"); @@ -120,7 +131,7 @@ static BoogieOptionBag() { o.TheProverFactory = ProverFactory.Load(o.ProverDllName); } }); - DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = Boogie.Util.BoundedMultiply(v, 1000)); + DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = v); DafnyOptions.RegisterLegacyBinding(SolverLog, (o, v) => o.ProverLogFilePath = v); DafnyOptions.RegisterLegacyBinding(SolverOption, (o, v) => { if (v is not null) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index c4b4a0acbb5..5494a3a705c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -1959,6 +1959,19 @@ public Boogie.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) BigNum.FromUInt(Boogie.Util.BoundedMultiply((uint)litExpr.asBigNum.ToIntSafe, 1000)), litExpr.Immutable); } + + // Do this after the above multiplication because :resource_limit should not be multiplied. + if (name == "resource_limit") { + name = "rlimit"; + if (parms[0] is string str) { + if (DafnyOptions.TryParseResourceCount(str, out var resourceLimit)) { + parms[0] = new Boogie.LiteralExpr(attr.tok, BigNum.FromUInt(resourceLimit), true); + } else { + BoogieGenerator.reporter.Error(MessageSource.Verifier, attr.tok, + $"failed to parse resource count: {parms[0]}"); + } + } + } kv = new Boogie.QKeyValue(Token.NoToken, name, parms, kv); } return kv; diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 094695d5afb..3a00d293a66 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -27,7 +27,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest { public class DafnyLanguageServerTestBase : LanguageProtocolTestBase { protected readonly string SlowToVerify = @" -lemma {:rlimit 100} SquareRoot2NotRational(p: nat, q: nat) +lemma {:resource_limit 100000} SquareRoot2NotRational(p: nat, q: nat) requires p > 0 && q > 0 ensures (p * p) != 2 * (q * q) { @@ -42,7 +42,7 @@ requires p > 0 && q > 0 } }".TrimStart(); - protected string SlowToVerifyNoLimit => SlowToVerify.Replace(" {:rlimit 100}", ""); + protected string SlowToVerifyNoLimit => SlowToVerify.Replace(" {:resource_limit 100000}", ""); protected readonly string NeverVerifies = @" lemma {:neverVerify} HasNeverVerifyAttribute(p: nat, q: nat) diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index cb33dfe5a0e..cda13980ad8 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -127,7 +127,7 @@ public async Task DiagnosticsForVerificationTimeoutHasNameAsRange() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var diagnostics = await GetLastDiagnostics(documentItem); Assert.Contains("Verification out of resource", diagnostics[0].Message); - Assert.Equal(new Range(0, 20, 0, 42), diagnostics[0].Range); + Assert.Equal(new Range(0, 31, 0, 53), diagnostics[0].Range); } [Fact] diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index 0adac6007db..5f54eeb8e2e 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs @@ -70,7 +70,7 @@ await VerifyTrace(@" | : if n <= 1 then n else fib(n-1) + fib(n-2) | :} | : -[ ]:method {:rlimit 1} Test(s: seq) +[ ]:method {:resource_limit 1000} Test(s: seq) [=]: requires |s| >= 1 && s[0] >= 0 { assert fib(10) == 1; assert {:split_here} s[0] >= 0; [ ]:}", true, intermediates: false); } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 521a0bdf2de..a82833e9df5 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -488,7 +488,7 @@ public async Task IndicateClickableWarningSignsOnMethodHoverWhenResourceLimitRea var documentItem = await GetDocumentItem(@" 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{:rlimit 10000} L() +lemma{:resource_limit 10000000} L() { assert f(10, 5) == 0; } ", "testfileSlow.dfy", true); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 124304b40d9..21fe1e30c24 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -430,7 +430,7 @@ await SetUp(options => { var successfulRun = await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken); Assert.True(successfulRun); - var range = new Range(0, 20, 0, 42); + var range = new Range(0, 31, 0, 53); await WaitForStatus(range, PublishedVerificationStatus.Running, CancellationToken); await WaitForStatus(range, PublishedVerificationStatus.Error, CancellationToken); diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 289bb463082..56eca2c2dbc 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index b0c70f35742..93d2527fdff 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 45727f4816a..e6b61fa07aa 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 8510c9484f6..0962deb044a 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index b904a93dfee..3f5667f54f1 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index 4b61fef7812..0bd909f746c 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index aba9385db42..d0a35f0b26c 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ diff --git a/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy b/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy index eac8ed2b1d7..b0a0fb09fee 100644 --- a/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy +++ b/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy @@ -11,7 +11,7 @@ module WriteBytesToFile { theMain("build/../build/fileioexamples", ""); } - method {:rlimit 2000} theMain(outputDir: string, expectedErrorPrefix: string) { + method {:resource_limit 2000000} theMain(outputDir: string, expectedErrorPrefix: string) { // Happy paths: write files to the output dir. (The %diff LIT commands check that we wrote the correct content.) { diff --git a/Source/DafnyStandardLibraries/examples/JSON/JSONExamples.dfy b/Source/DafnyStandardLibraries/examples/JSON/JSONExamples.dfy index 1cceed17084..35832b56c5b 100644 --- a/Source/DafnyStandardLibraries/examples/JSON/JSONExamples.dfy +++ b/Source/DafnyStandardLibraries/examples/JSON/JSONExamples.dfy @@ -15,7 +15,7 @@ module {:options "-functionSyntax:4"} AbstractSyntax { The high-level API works with fairly simple datatype values that contain native Dafny strings. */ - method {:test} {:rlimit 100000} Test() { + method {:test} {:resource_limit 100000000} Test() { /** Use `API.Deserialize` to deserialize a byte string. @@ -138,7 +138,7 @@ module {:options "-functionSyntax:4"} ConcreteSyntax { encoding: each node contains pointers to parts of a string, such that concatenating the fields of all nodes reconstructs the serialized value. */ - method {:test} {:rlimit 100000} Test() { + method {:test} {:resource_limit 100000000} Test() { /** The low-level API exposes the same functions and methods as the high-level @@ -270,4 +270,4 @@ module {:options "-functionSyntax:4"} ConcreteSyntax { sq' } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/examples/dfyconfig.toml b/Source/DafnyStandardLibraries/examples/dfyconfig.toml index 4b85bac48f0..463996a5f82 100644 --- a/Source/DafnyStandardLibraries/examples/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/examples/dfyconfig.toml @@ -5,7 +5,7 @@ standard-libraries = true # but consumers don't have to have this option set # to use the standard libraries in general. reads-clauses-on-methods = true -resource-limit = 1000 +resource-limit = 1000000 warn-as-errors = true warn-redundant-assumptions = true warn-contradictory-assumptions = true diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy index 2ce829018f9..4fdd5b9a22b 100644 --- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy @@ -230,7 +230,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals { LemmaModAutoMinus(n); } - lemma {:rlimit 2000} LemmaModAutoMinus(n: int) + lemma {:resource_limit 2000000} LemmaModAutoMinus(n: int) requires n > 0 ensures ModAutoMinus(n) { diff --git a/Source/DafnyStandardLibraries/src/Std/Base64.dfy b/Source/DafnyStandardLibraries/src/Std/Base64.dfy index cefb455de69..02bd16eaa06 100644 --- a/Source/DafnyStandardLibraries/src/Std/Base64.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Base64.dfy @@ -98,7 +98,7 @@ module Std.Base64 { else (c - 65 as char) as index } - lemma {:rlimit 2000} {:vcs_split_on_every_assert} CharToIndexToChar(c: char) + lemma {:resource_limit 2000000} {:vcs_split_on_every_assert} CharToIndexToChar(c: char) requires IsBase64Char(c) ensures IndexToChar(CharToIndex(c)) == c { @@ -1213,7 +1213,7 @@ module Std.Base64 { AboutDecodeValid(s, DecodeValid(s)); } - lemma {:rlimit 12000} DecodeValidEncode1Padding(s: seq) + lemma {:resource_limit 12000000} DecodeValidEncode1Padding(s: seq) requires IsBase64String(s) requires |s| >= 4 requires Is1Padding(s[(|s| - 4)..]) @@ -1449,7 +1449,7 @@ module Std.Base64 { seq(|b|, i requires 0 <= i < |b| => b[i] as uint8) } - lemma {:vcs_split_on_every_assert} {:rlimit 1000000} UInt8sToBVsToUInt8s(u: seq) + lemma {:vcs_split_on_every_assert} {:resource_limit 1000000000} UInt8sToBVsToUInt8s(u: seq) ensures BVsToUInt8s(UInt8sToBVs(u)) == u { // TODO: reduce resource use diff --git a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy index e4ef670e50d..65358c44dc7 100644 --- a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy @@ -749,7 +749,7 @@ module Std.Collections.Seq { /* Applying a function to a sequence is distributive over concatenation. That is, concatenating two sequences and then applying Map is the same as applying Map to each sequence separately, and then concatenating the two resulting sequences. */ - lemma {:opaque} {:rlimit 1000000} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) + lemma {:opaque} {:resource_limit 1000000000} LemmaMapDistributesOverConcat(f: (T ~> R), xs: seq, ys: seq) requires forall i {:trigger xs[i]}:: 0 <= i < |xs| ==> f.requires(xs[i]) requires forall j {:trigger ys[j]}:: 0 <= j < |ys| ==> f.requires(ys[j]) ensures Map(f, xs + ys) == Map(f, xs) + Map(f, ys) diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy index e5788fa0d01..6aed16f9d0a 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ConcreteSyntax.SpecProperties.dfy @@ -36,7 +36,7 @@ module Std.JSON.ConcreteSyntax.SpecProperties { ensures Spec.ConcatBytes(ts, pt0) == Spec.ConcatBytes(ts, pt1) {} - lemma {:induction ts0} {:rlimit 10000} ConcatBytes_Linear(ts0: seq, ts1: seq, pt: T --> bytes) + lemma {:induction ts0} {:resource_limit 10000000} ConcatBytes_Linear(ts0: seq, ts1: seq, pt: T --> bytes) requires forall d | d in ts0 :: pt.requires(d) requires forall d | d in ts1 :: pt.requires(d) ensures Spec.ConcatBytes(ts0 + ts1, pt) == Spec.ConcatBytes(ts0, pt) + Spec.ConcatBytes(ts1, pt) @@ -47,4 +47,4 @@ module Std.JSON.ConcreteSyntax.SpecProperties { assert ts0 + ts1 == [ts0[0]] + (ts0[1..] + ts1); } } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy index 852ba6d6d83..cad694e4b58 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy @@ -64,7 +64,7 @@ module Std.JSON.Serializer { Failure(o.error) } - function {:vcs_split_on_every_assert} {:rlimit 1000} Number(dec: Values.Decimal): Result { + function {:vcs_split_on_every_assert} {:resource_limit 1000000} Number(dec: Values.Decimal): Result { var minus: jminus := Sign(dec.n); var num: jnum :- Int(Math.Abs(dec.n)); var frac: Maybe := Empty(); @@ -133,4 +133,4 @@ module Std.JSON.Serializer { var val :- Value(js); Success(MkStructural(val)) } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy index bde25681af1..4e8e21814fc 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy @@ -59,7 +59,7 @@ module Std.JSON.ZeroCopy.Deserializer { return Cursor(cs.s, cs.beg, point', cs.end).Split(); } - opaque function {:vcs_split_on_every_assert} {:rlimit 1000000} Structural(cs: FreshCursor, parser: Parser) + opaque function {:vcs_split_on_every_assert} {:resource_limit 1000000000} Structural(cs: FreshCursor, parser: Parser) : (pr: ParseResult>) requires forall cs :: parser.fn.requires(cs) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, st => Spec.Structural(st, parser.spec)) @@ -72,7 +72,7 @@ module Std.JSON.ZeroCopy.Deserializer { type jopt = v: Vs.View | v.Length() <= 1 witness Vs.View.OfBytes([]) - function {:rlimit 100000} TryStructural(cs: FreshCursor) + function {:resource_limit 100000000} TryStructural(cs: FreshCursor) : (sp: Split>) ensures sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)) { @@ -244,11 +244,11 @@ module Std.JSON.ZeroCopy.Deserializer { elems' } - opaque function {:rlimit 10000} {:vcs_split_on_every_assert} AppendLast(ghost cs0: FreshCursor, - ghost json: ValueParser, - elems: Split>, - elem: Split, - sep: Split>) + opaque function {:resource_limit 10000000} {:vcs_split_on_every_assert} AppendLast(ghost cs0: FreshCursor, + ghost json: ValueParser, + elems: Split>, + elem: Split, + sep: Split>) : (elems': Split>) requires elems.cs.StrictlySplitFrom?(json.cs) requires elems.SplitFrom?(cs0, SuffixedElementsSpec) @@ -280,7 +280,7 @@ module Std.JSON.ZeroCopy.Deserializer { elems' } - lemma {:rlimit 10000} AboutTryStructural(cs: FreshCursor) + lemma {:resource_limit 10000000} AboutTryStructural(cs: FreshCursor) ensures var sp := Core.TryStructural(cs); var s0 := sp.t.t.Peek(); @@ -476,7 +476,7 @@ module Std.JSON.ZeroCopy.Deserializer { case OtherError(err) => err } - opaque function {:vcs_split_on_every_assert} {:rlimit 10000} JSON(cs: Cursors.FreshCursor) : (pr: DeserializationResult>) + opaque function {:vcs_split_on_every_assert} {:resource_limit 10000000} JSON(cs: Cursors.FreshCursor) : (pr: DeserializationResult>) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.JSON) { Core.Structural(cs, Parsers.Parser(Values.Value, Spec.Value)).MapFailure(LiftCursorError) @@ -694,7 +694,7 @@ module Std.JSON.ZeroCopy.Deserializer { Success(cs.Split()) } - opaque function {:rlimit 10000} String(cs: FreshCursor): (pr: ParseResult) + opaque function {:resource_limit 10000000} String(cs: FreshCursor): (pr: ParseResult) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.String) { var SP(lq, cs) :- Quote(cs); @@ -755,7 +755,7 @@ module Std.JSON.ZeroCopy.Deserializer { else Success(sp) } - opaque function {:vcs_split_on_every_assert} {:rlimit 100000} Exp(cs: FreshCursor) : (pr: ParseResult>) + opaque function {:vcs_split_on_every_assert} {:resource_limit 100000000} Exp(cs: FreshCursor) : (pr: ParseResult>) ensures pr.Success? ==> pr.value.SplitFrom?(cs, exp => Spec.Maybe(exp, Spec.Exp)) { var SP(e, cs) := @@ -974,7 +974,7 @@ module Std.JSON.ZeroCopy.Deserializer { } } - opaque function {:vcs_split_on_every_assert} {:rlimit 10000} Object(cs: FreshCursor, json: ValueParser) + opaque function {:vcs_split_on_every_assert} {:resource_limit 10000000} Object(cs: FreshCursor, json: ValueParser) : (pr: ParseResult) requires cs.SplitFrom?(json.cs) ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.Object) @@ -985,4 +985,4 @@ module Std.JSON.ZeroCopy.Deserializer { Success(sp) } } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy index ef153a9a698..044b8e64a0e 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy @@ -155,7 +155,7 @@ module Std.JSON.ZeroCopy.Serializer { ensures Spec.Number(num) == num.minus.Bytes() + num.num.Bytes() + Spec.Maybe(num.frac, Spec.Frac) + Spec.Maybe(num.exp, Spec.Exp) {} - lemma {:vcs_split_on_every_assert} {:rlimit 10000} NumberHelper2(num: jnumber, writer: Writer) + lemma {:vcs_split_on_every_assert} {:resource_limit 10000000} NumberHelper2(num: jnumber, writer: Writer) ensures if num.exp.NonEmpty? then ( if num.frac.NonEmpty? then writer.Bytes() + Spec.Number(num) == writer.Bytes() + num.minus.Bytes() + num.num.Bytes() + num.frac.t.period.Bytes() + num.frac.t.num.Bytes() + num.exp.t.e.Bytes() + num.exp.t.sign.Bytes() + num.exp.t.num.Bytes() else writer.Bytes() + Spec.Number(num) == writer.Bytes() + num.minus.Bytes() + num.num.Bytes() + num.exp.t.e.Bytes() + num.exp.t.sign.Bytes() + num.exp.t.num.Bytes() @@ -468,7 +468,7 @@ module Std.JSON.ZeroCopy.Serializer { // needs to call ItemsSpec and the termination checker gets confused by // that. Instead, see Items above. // DISCUSS - method {:rlimit 10000} MembersImpl(obj: jobject, writer: Writer) returns (wr: Writer) + method {:resource_limit 10000000} MembersImpl(obj: jobject, writer: Writer) returns (wr: Writer) decreases obj, 1 ensures wr == MembersSpec(obj, obj.data, writer) { @@ -547,4 +547,4 @@ module Std.JSON.ZeroCopy.Serializer { } wr } -} \ No newline at end of file +} diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml index 07ec5a99d80..d48d60ce73e 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/dfyconfig.toml @@ -12,7 +12,7 @@ reads-clauses-on-methods = true # Options important for sustainable development # of the libraries themselves. -resource-limit = 1000 +resource-limit = 1000000 warn-as-errors = true warn-redundant-assumptions = true warn-contradictory-assumptions = true diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy index 9892385703b..e8679c68069 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf16EncodingForm.dfy @@ -115,7 +115,7 @@ module Std.Unicode.Utf16EncodingForm refines UnicodeEncodingForm { } function - {:rlimit 1200} + {:resource_limit 1200000} DecodeMinimalWellFormedCodeUnitSubsequenceDoubleWord(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 2 ensures 0x10000 <= v <= 0x10FFFF diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy index 795994d89cb..98f73258179 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingForm.dfy @@ -214,7 +214,7 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { } function - {:rlimit 115000} + {:resource_limit 115000000} DecodeMinimalWellFormedCodeUnitSubsequenceTripleByte(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 3 ensures 0x800 <= v <= 0xFFFF @@ -231,7 +231,7 @@ module Std.Unicode.Utf8EncodingForm refines UnicodeEncodingForm { } function - {:rlimit 4000} + {:resource_limit 4000000} DecodeMinimalWellFormedCodeUnitSubsequenceQuadrupleByte(m: MinimalWellFormedCodeUnitSeq): (v: ScalarValue) requires |m| == 4 ensures 0x10000 <= v <= 0x10FFFF diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy index eee8c8c433e..5aa4a6a3a1f 100644 --- a/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Unicode/Utf8EncodingScheme.dfy @@ -54,7 +54,7 @@ module Std.Unicode.Utf8EncodingScheme { * Deserializing a byte sequence and then serializing the result, yields the original byte sequence. */ lemma - {:rlimit 3000} + {:resource_limit 3000000} LemmaDeserializeSerialize(b: seq) ensures Serialize(Deserialize(b)) == b { diff --git a/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml b/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml index 2b40b5ef8fb..afc4a115a7a 100644 --- a/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/src/Std/dfyconfig.toml @@ -12,7 +12,7 @@ reads-clauses-on-methods = true # Options important for sustainable development # of the libraries themselves. -resource-limit = 1000 +resource-limit = 1000000 warn-as-errors = true # These give too many false positives right now, but should be enabled in the future warn-redundant-assumptions = false diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy index c433efd53b2..6142067e8a1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy @@ -136,7 +136,7 @@ class Map { } // Removes key from the domain of M (and does nothing if key wasn't in M to begin with) - method {:rlimit 3000} {:vcs_split_on_every_assert} Remove(key: Key) + method {:resource_limit "3e6"} {:vcs_split_on_every_assert} Remove(key: Key) requires Valid() modifies Repr ensures Valid() && fresh(Repr - old(Repr)) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy index 4686b97830f..1a4ac35e924 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/solverLog.dfy @@ -1,7 +1,7 @@ -// RUN: %verify --solver-log="log.smt2" --resource-limit 10 "%s" > "%t" +// RUN: %verify --solver-log="log.smt2" --resource-limit 10e3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "log.smt2" "%s" -// CHECK: rlimit 10000 +// CHECK: rlimit 10000\) method m() { assert 1 + 1 == 2; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy index 98b2f8bf292..693d0ffd17c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RlimitMultiplier.dfy @@ -1,4 +1,4 @@ -// RUN: %verify "%s" --resource-limit 10000 > "%t" +// RUN: %verify "%s" --resource-limit 10e6 > "%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)} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy index d161585df1b..3855d710829 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy @@ -3,7 +3,7 @@ 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{:rlimit 10000} L() +lemma{:resource_limit 10000000} L() { assert f(10, 5) == 0; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect index 757646ed6c3..2985385d3ec 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect @@ -1,3 +1,3 @@ -git-issue106.dfy(6,21): Verification out of resource (L (correctness)) +git-issue106.dfy(6,32): Verification out of resource (L (correctness)) Dafny program verifier finished with 1 verified, 0 errors, 1 out of resource diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy index dec9da7cfad..3d9a59a6d5c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy @@ -637,7 +637,7 @@ function partitionOfJustHeapRegions(os : set) : (partition : map %t +// RUN: %exits-with 4 %verify --resource-limit 1000000 %s > %t // RUN: %diff "%s.expect" "%t" module Power { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy index eae991a3240..c8fa2bea365 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy @@ -1,5 +1,5 @@ -// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1000 > "%t" -// RUN: ! %verify "%s" --resource-limit 1000 >> "%t" +// RUN: ! %verify "%s" --disable-nonlinear-arithmetic --resource-limit 1e6 > "%t" +// RUN: ! %verify "%s" --resource-limit 1e6 >> "%t" // RUN: %diff "%s.expect" "%t" module Power0 { @@ -102,4 +102,4 @@ module {:disableNonlinearArithmetic false} Power3 { LemmaPowAdds(b, e1 - e2, e2); } -} \ No newline at end of file +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy index e1ff957c19d..2b85d89b705 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/vstte2012/BreadthFirstSearch.dfy @@ -27,7 +27,7 @@ class BreadthFirstSearch // witness. The method could equally well have been written using an // existential quantifier and no ghost out-parameter. method - {:rlimit 8000} + {:resource_limit "8e6"} {:vcs_split_on_every_assert} BFS(source: Vertex, dest: Vertex, ghost AllVertices: set) returns (d: int, ghost path: List) diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index 47ce6ac457f..0310d2cc6e6 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -393,12 +393,15 @@ Print effects are enforced only with `--track-print-effects`. `{:priority N}` assigns a positive priority 'N' to a method or function to control the order in which methods or functions are verified (default: N = 1). -### 11.2.14. `{:rlimit}` {#sec-rlimit} +### 11.2.14. `{:resource_limit}` and `{:rlimit}` {#sec-rlimit} -`{:rlimit N}` limits the verifier resource usage to verify the method or function at `N * 1000`. -This is the per-method equivalent of the command-line flag `/rlimit:N`. +`{:resource_limit N}` limits the verifier resource usage to verify the method or function to `N`. + +This is the per-method equivalent of the command-line flag `/rlimit:N` or `--resource-limit N`. If using [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) as well, the limit will be set for each assertion. +The attribute `{:rlimit N}` is also available, and limits the verifier resource usage to verify the method or function to `N * 1000`. This version is deprecated, however. + To give orders of magnitude about resource usage, here is a list of examples indicating how many resources are used to verify each method: * 8K resource usage diff --git a/docs/dev/news/4975.fix b/docs/dev/news/4975.fix new file mode 100644 index 00000000000..fe67d2072d0 --- /dev/null +++ b/docs/dev/news/4975.fix @@ -0,0 +1 @@ +The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with exponential notation for brevity. The `--resource-limit` flag also now omits the multiplication and allows exponential notation.