Implement :resource_limit attribute
#4975
Conversation
Update several tests to use this form on the command line and in attributes.
Source/DafnyCore/DafnyOptions.cs
Outdated
| @@ -358,6 +358,27 @@ public enum IncludesModes { | |||
| ).ToArray(); | |||
| } | |||
|
|
|||
| public static bool TryParseResourceCount(string value, out uint number) { | |||
| uint multiplier = 1; | |||
| if (value.EndsWith("G")) { | |||
There was a problem hiding this comment.
Have you considered using C#'s default numeric string parser with exponent notation? The notation would then be nnnExx, like 123E9. I think it might be easier to change the amount of resources using that notation, then if you need to change for example 100M into 1G
uint.TryParse(value, NumberStyles.AllowExponent, null, out var result);
There was a problem hiding this comment.
Oh, that might be nice. Thanks for pointing it out!
Source/DafnyCore/DafnyOptions.cs
Outdated
| @@ -358,6 +358,27 @@ public enum IncludesModes { | |||
| ).ToArray(); | |||
| } | |||
|
|
|||
| public static bool TryParseResourceCount(string value, out uint number) { | |||
There was a problem hiding this comment.
Could you rename the parameter number to result ? number says something that's already known from the type.
There was a problem hiding this comment.
Definitely in favor of this cleanup ASAP.
This flag is currently not used widely, so the impact of this breaking change is minimal.
What also makes me okay with this is that it's a hard breakage: if someone upgrades without being aware of it their verification will likely fail because their limit is suddenly 1/1000th what it was. And if it doesn't then yay, they are better protected against brittleness! :)
docs/dev/news/4975.fix
Outdated
| @@ -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. | |||
There was a problem hiding this comment.
I'd also mention the change in behavior of --resource-limit
| result.ErrorMessage = $"Cannot parse resource limit: {value}"; | ||
| return 0; | ||
| }, | ||
| false, |
There was a problem hiding this comment.
What parameter is this? Consider using a named argument or a comment.
| @@ -1959,6 +1959,19 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap) | |||
| 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. | |||
There was a problem hiding this comment.
We should probably just reject using both attributes at once. At a minimum that check would be here, but perhaps there's a cleaner spot in resolution to catch it earlier?
| 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. |
There was a problem hiding this comment.
Hey while you're adding attribute aliases, how about {:isolate_assertions}? ;)
(Not literally in this PR of course)
I'll update the description (and merge message) to mention that. :) |
Description
This is an alternative to
:rlimitthat doesn't multiply by 1000 before sending the value to Z3. With the addition of this new attribute,:rlimitis deprecated.The
--resource-limitflag 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. Verification pipelines that are affected will break immediately, and be easy to fix.The
:resource_limitattribute and--resource-limitflag now accept exponential notation to allow shorter, easier-to-read limits.Fixes #4962.
How has this been tested?
The integration tests have been updated to use
:resource_limitwherever they used:rlimitpreviously. Some--resource-limitand:resource_limituses have been updated to use exponential notation.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.