Implement :resource_limit attribute (#4975)

### Description

This is an alternative to `:rlimit` that doesn't multiply by 1000 before
sending the value to Z3. With the addition of this new attribute,
`:rlimit` is deprecated.

The `--resource-limit` flag now also passes through the value unchanged,
without a multiplication. This flag is currently not used widely, so the
impact of this breaking change is minimal.

The `:resource_limit` attribute and `--resource-limit` flag now accept
`K`, `M`, and `G` suffixes to allow shorter, easier-to-read limits.

### How has this been tested?

The integration tests have been updated to use `:resource_limit`
wherever they used `:rlimit` previously. Some `--resource-limit` and
`:resource_limit` uses have been updated to use suffixes.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

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;
           }

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);
+    }
+
     /// <summary>
     /// Automatic shallow-copy constructor
     /// </summary>

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<uint> 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<string> 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) {

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;

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)

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]

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<nat>)
+[ ]:method {:resource_limit 1000} Test(s: seq<nat>)
 [=]:  requires |s| >= 1 && s[0] >= 0 { assert fib(10) == 1; assert {:split_here} s[0] >= 0;
 [ ]:}", true, intermediates: false);
   }

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);

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);
 

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.)
     {

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'
   }
-}
+}

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

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)
   {

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<char>)
+  lemma {:resource_limit 12000000} DecodeValidEncode1Padding(s: seq<char>)
     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<uint8>)
+  lemma {:vcs_split_on_every_assert} {:resource_limit 1000000000} UInt8sToBVsToUInt8s(u: seq<uint8>)
     ensures BVsToUInt8s(UInt8sToBVs(u)) == u
   {
     // TODO: reduce resource use

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<T,R>(f: (T ~> R), xs: seq<T>, ys: seq<T>)
+  lemma {:opaque} {:resource_limit 1000000000} LemmaMapDistributesOverConcat<T,R>(f: (T ~> R), xs: seq<T>, ys: seq<T>)
     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)

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<T>(ts0: seq<T>, ts1: seq<T>, pt: T --> bytes)
+  lemma {:induction ts0} {:resource_limit 10000000} ConcatBytes_Linear<T>(ts0: seq<T>, ts1: seq<T>, 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);
     }
   }
-}
+}

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<jnumber> {
+  function {:vcs_split_on_every_assert} {:resource_limit 1000000} Number(dec: Values.Decimal): Result<jnumber> {
     var minus: jminus := Sign(dec.n);
     var num: jnum :- Int(Math.Abs(dec.n));
     var frac: Maybe<jfrac> := Empty();
@@ -133,4 +133,4 @@ module Std.JSON.Serializer {
     var val :- Value(js);
     Success(MkStructural(val))
   }
-}
+}

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<T>(cs: FreshCursor, parser: Parser<T>)
+    opaque function {:vcs_split_on_every_assert} {:resource_limit 1000000000} Structural<T>(cs: FreshCursor, parser: Parser<T>)
       : (pr: ParseResult<Structural<T>>)
       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<Structural<jopt>>)
       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<seq<TSuffixedElement>>,
-                                                                            elem: Split<TElement>,
-                                                                            sep: Split<Structural<jclose>>)
+    opaque function {:resource_limit 10000000} {:vcs_split_on_every_assert} AppendLast(ghost cs0: FreshCursor,
+                                                                                       ghost json: ValueParser,
+                                                                                       elems: Split<seq<TSuffixedElement>>,
+                                                                                       elem: Split<TElement>,
+                                                                                       sep: Split<Structural<jclose>>)
       : (elems': Split<seq<TSuffixedElement>>)
       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<Cursors.Split<JSON>>)
+    opaque function {:vcs_split_on_every_assert} {:resource_limit 10000000} JSON(cs: Cursors.FreshCursor) : (pr: DeserializationResult<Cursors.Split<JSON>>)
       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<jstring>)
+    opaque function {:resource_limit 10000000} String(cs: FreshCursor): (pr: ParseResult<jstring>)
       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<Maybe<jexp>>)
+    opaque function {:vcs_split_on_every_assert} {:resource_limit 100000000} Exp(cs: FreshCursor) : (pr: ParseResult<Maybe<jexp>>)
       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<jobject>)
       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)
     }
   }
-}
+}

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
   }
-}
+}

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