Use resource limit in most places in test suite (dafny-lang#4972)

### Description

A few exceptions remain, but this will allow testing the general idea. There is still _also_ a time limit, because that does help ensure that the test suite terminates in a predictable amount of time. Over time, it may make sense to reduce the overall resource limit and raise it locally for the few tests that need it.

Fixes dafny-lang#2985

### How has this been tested?

It changes the behavior of the existing test suite. Passing existing tests confirms that it's working correctly.

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

Source/DafnyDriver/DafnyCliTests.cs

@@ -42,8 +42,11 @@ static DafnyCliTests() {
     // We do not want output such as "Compiled program written to Foo.cs"
     // from the compilers, since that changes with the target language
     "/compileVerbose:0",
-
-    // Set a default time limit, to catch cases where verification time runs off the rails
+
+    // Set a default resource limit, to catch cases where verification runs off the rails
+    "/rlimit:50000000",
+
+    // Also include a time limit, because we do care about using too much time.
     "/timeLimit:300",
 
     // test results do not include source code snippets
@@ -57,10 +60,13 @@ static DafnyCliTests() {
     // We do not want absolute or relative paths in error messages, just the basename of the file
     "--use-basename-for-filename",
 
-    // Set a default time limit, to catch cases where verification time runs off the rails
-    "--verification-time-limit=300",
+    // Set a default resource limit, to catch cases where verification runs off the rails
+    "--resource-limit:50e6",
+
+    // Also include a time limit, because we do care about using too much time.
+    "--verification-time-limit:300",
 
     // test results do not include source code snippets
     "--show-snippets:false"
   };
-}
+}

Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs

@@ -20,7 +20,7 @@ await SetUp(options => {
       var documentItem = CreateTestDocument(SlowToVerify2, "ChangingTheDocumentStopsOnChangeVerification.dfy");
       client.OpenDocument(documentItem);
 
-      await WaitForStatus(new Range(11, 23, 11, 27), PublishedVerificationStatus.Running, CancellationToken);
+      await WaitForStatus(new Range(11, 32, 11, 36), PublishedVerificationStatus.Running, CancellationToken);
 
       // Should cancel the previous request.
       ApplyChange(ref documentItem, new Range((12, 9), (12, 23)), "true");
@@ -37,7 +37,7 @@ await SetUp(options => {
       client.OpenDocument(documentItem);
       client.SaveDocument(documentItem);
 
-      await WaitForStatus(new Range(11, 23, 11, 27), PublishedVerificationStatus.Running, CancellationToken);
+      await WaitForStatus(new Range(11, 32, 11, 36), PublishedVerificationStatus.Running, CancellationToken);
 
       // Should cancel the previous request.
       ApplyChange(ref documentItem, new Range((12, 9), (12, 23)), "true");
@@ -57,7 +57,7 @@ await SetUp(options => {
       Assert.True(await client.RunSymbolVerification(documentItem, new Position(11, 23), CancellationToken));
       Assert.True(await client.RunSymbolVerification(documentItem, new Position(0, 23), CancellationToken));
 
-      await WaitForStatus(new Range(11, 23, 11, 27), PublishedVerificationStatus.Running, CancellationToken);
+      await WaitForStatus(new Range(11, 32, 11, 36), PublishedVerificationStatus.Running, CancellationToken);
 
       // Should cancel the previous request.
       ApplyChange(ref documentItem, new Range((12, 9), (12, 23)), "true");
@@ -80,7 +80,7 @@ await SetUp(options => {
     Ack(m - 1, Ack(m, n - 1))
 }
 
-method {:timeLimit 10} test() {
+method {:resource_limit ""10e6""} test() {
   assert Ack(5, 5) == 0;
 }".TrimStart();
 

Source/IntegrationTests/LitTests.cs

@@ -61,14 +61,14 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
       // The metatests/StdLibsOffByDefaultInTests.dfy test directly enforces this.
 
       string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false" };
-      string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300" };
-      //string[] defaultTranslateArgs = new[] { "translate", "--use-basename-for-filename", "--cores:2", "--standard-libraries:false", "--verification-time-limit:300" };
-      string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300" };
-      string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" };
+      //string[] defaultTranslateArgs = new[] { "translate", "--use-basename-for-filename", "--cores:2", "--standard-libraries:false", "--verification-time-limit:300", "--resource-limit:50e6" };
+      string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" };
+      string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" };
 
       var substitutions = new Dictionary<string, object> {
         { "%diff", "diff" },
-        { "%trargs", "--use-basename-for-filename --show-snippets:false, --standard-libraries:false --cores:2 --verification-time-limit:300" },
+        { "%trargs", "--use-basename-for-filename --show-snippets:false, --standard-libraries:false --cores:2 --verification-time-limit:300 --resource-limit:50e6" },
         { "%binaryDir", "." },
         { "%z3", Path.Join("z3", "bin", $"z3-{DafnyOptions.DefaultZ3Version}") },
         { "%repositoryRoot", RepositoryRoot.Replace(@"\", "/") },

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/Makefile

@@ -22,7 +22,7 @@ vars:
 	echo $(EXECS)
 
 %.cpp: %.dfy $(DAFNY) $(DAFNY_DEPS)
-	$(DAFNY) /timeLimit:10 /compile:0 /spillTargetCode:3 /compileTarget:cpp ExternDefs.h $<
+	$(DAFNY) /timeLimit:10 /rlimit:200000 /compile:0 /spillTargetCode:3 /compileTarget:cpp ExternDefs.h $<
 
 %.cs: %.dfy $(DAFNY) $(DAFNY_DEPS)
 	$(DAFNY) /noVerify /compile:0 /spillTargetCode:3 /compileTarget:cs $<

Source/IntegrationTests/TestFiles/LitTests/LitTest/cloudmake/CloudMake-CachedBuilds.dfy

@@ -615,7 +615,7 @@ abstract module M0 {
     var _, _ := EvalLemma(expr, st, env, useCache);
   }
 
-  lemma {:induction false} {:timeLimit 30} EvalLemma(expr: Expression, st: State, env: Env, useCache: bool) returns (outExpr: Expression, outSt: State)
+  lemma {:induction false} {:resource_limit "30e6"} EvalLemma(expr: Expression, st: State, env: Env, useCache: bool) returns (outExpr: Expression, outSt: State)
     requires ValidState(st) && ValidEnv(env)
     requires useCache ==> ConsistentCache(st)
     ensures
@@ -1196,7 +1196,7 @@ abstract module M0 {
       }
     }
   }
-  lemma {:timeLimit 15} StateCorrespondence_Ctor(stOrig: State, st: State, sts: set<State>, stC: State, stsC: set<State>)
+  lemma {:resource_limit "15e6"} StateCorrespondence_Ctor(stOrig: State, st: State, sts: set<State>, stC: State, stsC: set<State>)
     requires ValidState(st) && forall s :: s in sts ==> ValidState(s)
     requires Extends(stOrig, st) && forall s :: s in sts ==> Extends(stOrig, s)
     requires StateCorrespondence(st, stC)

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/incompatibleAttributes.dfy

@@ -0,0 +1,6 @@
+// RUN: %exits-with 2 %resolve "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method {:rlimit 10} {:resource_limit 10000} M() {
+  assert true;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/incompatibleAttributes.dfy.expect

@@ -0,0 +1,2 @@
+incompatibleAttributes.dfy(4,9): Error: the rlimit and resource_limit attributes cannot be used together
+1 resolution/type errors detected in incompatibleAttributes.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/MinWindowMax.dfy

@@ -25,7 +25,7 @@ method Main() {
   print "Window size 5:  min window-max is ", m, "\n";  // 3
 }
 
-method MinimumWindowMax(a: array<int>, W: int) returns (m: int, start: int)
+method {:resource_limit "100e6"} {:vcs_split_on_every_assert} MinimumWindowMax(a: array<int>, W: int) returns (m: int, start: int)
   requires 1 <= W <= a.Length
   ensures 0 <= start <= a.Length - W
   ensures m == Max(a, start, W)

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/gcd.dfy

@@ -98,7 +98,7 @@ lemma GcdIdempotent(x: pos)
   assert x in Factors(x) * Factors(x);
 }
 
-lemma GcdSubtract(x: pos, y: pos)
+lemma {:resource_limit "500e6"} GcdSubtract(x: pos, y: pos)
   requires x < y
   ensures Gcd(x, y) == Gcd(x, y - x)
 {

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2477.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --show-snippets:false --use-basename-for-filename --cores:2 --verification-time-limit:300 "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --use-basename-for-filename --cores:2 --verification-time-limit:300 --resource-limit:5e6 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 trait T {

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3571.dfy

@@ -6,7 +6,7 @@
 // RUN: %resolve --prelude "%s" --prelude "%s"  "%s" >> "%t"
 // RUN: %verify --cores:2 --cores:1  "%s" >> "%t"
 // RUN: %verify --solver-log x.tct --solver-log y.txt  "%s" >> "%t"
-// RUN: %verify --resource-limit 100 --resource-limit 200  "%s" >> "%t"
+// RUN: %verify --resource-limit 100e3 --resource-limit 200e3  "%s" >> "%t"
 // RUN: %verify --solver-path x --solver-path y  "%s" >> "%t"
 // RUN: %verify --verification-time-limit 300 --verification-time-limit 500  "%s" >> "%t"
 // RUN: %verify --error-limit:10 --error-limit:5  "%s" >> "%t"

Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg

@@ -123,7 +123,10 @@ dafnyArgs = [
     # from the compilers, since that changes with the target language
     'compileVerbose:0',
 
-    # Set a default time limit, to catch cases where verification time runs off the rails
+    # Set a default resource limit, to catch cases where verification runs off the rails
+    'rlimit:50000000',
+
+    # Also include a time limit, because we do care about using too much time.
     'timeLimit:300',
 
     # Disallow standard libraries by default in tests,
@@ -172,11 +175,11 @@ if os.name != "nt":
     ver = os.uname().version
 
 config.substitutions.append( ('%resolve', dafnyExecutable + " resolve --standard-libraries:false " + standardArguments ) )
-config.substitutions.append( ('%verify', dafnyExecutable + " verify --cores:2 --verification-time-limit:300 --standard-libraries:false " + standardArguments) )
+config.substitutions.append( ('%verify', dafnyExecutable + " verify --cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments) )
 config.substitutions.append( ('%translate', dafnyExecutable + " translate"  ) )
-config.substitutions.append( ('%trargs', "--cores:2 --verification-time-limit:300 --standard-libraries:false " ) )
-config.substitutions.append( ('%build', dafnyExecutable + " build --cores:2 --verification-time-limit:300 --standard-libraries:false " + standardArguments ) )
-config.substitutions.append( ('%run', dafnyExecutable + " run --cores:2 --verification-time-limit:300 --standard-libraries:false " + standardArguments ) )
+config.substitutions.append( ('%trargs', "--cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " ) )
+config.substitutions.append( ('%build', dafnyExecutable + " build --cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments ) )
+config.substitutions.append( ('%run', dafnyExecutable + " run --cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments ) )
 
 config.substitutions.append( ('%repositoryRoot', repositoryRoot) )
 config.substitutions.append( ('%binaryDir', binaryDir) )

Source/IntegrationTests/TestFiles/LitTests/LitTest/runTests.py

@@ -40,7 +40,7 @@ class Defaults:
     EXCLUDED_FOLDERS = ["Inputs", "Output", "sandbox", "desktop"]
     DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe"))
     COMPILER = [DAFNY_BIN]
-    FLAGS = ["/useBaseNameForFileName", "/compile:1", "/compileVerbose:0", "/timeLimit:300"]
+    FLAGS = ["/useBaseNameForFileName", "/compile:1", "/compileVerbose:0", "/timeLimit:300", "/rlimit:500000000"]
     EXTENSIONS = [".dfy", ".transcript"]
 
 class Colors:

Source/TestDafny/MultiBackendTest.cs

@@ -298,6 +298,8 @@ private static bool OptionAppliesToVerifyCommand(string option) {
       CommonOptionBag.SpillTranslation,
       CommonOptionBag.OptimizeErasableDatatypeWrapper,
       CommonOptionBag.AddCompileSuffix,
+      BoogieOptionBag.SolverResourceLimit,
+      BoogieOptionBag.VerificationTimeLimit,
       RunCommand.MainOverride,
     }.Select(o => o.Name);