From f1519da74fb1a869e2389cd1feb69112294076aa Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@adacore.com>
Date: Tue, 10 Sep 2024 17:01:47 +0200
Subject: [PATCH] Enable configuration of prover memory limit for feature tests

Ref. eng/recordflux/RecordFlux#1786
---
 tests/feature/__init__.py                     |  1 +
 .../fsm_comprehension_on_sequence/config.yml  |  1 +
 tests/utils.py                                | 20 +++++++++++++++----
 tests/verification/feature_test.py            |  2 ++
 4 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/tests/feature/__init__.py b/tests/feature/__init__.py
index 719888777..a94e773f1 100644
--- a/tests/feature/__init__.py
+++ b/tests/feature/__init__.py
@@ -32,6 +32,7 @@
 class ProofConfig(BaseModel):  # type: ignore[misc]
     enabled: bool = Field(default=True)
     timeout: int = Field(default=60)
+    memlimit: int = Field(default=1500)
     units: ty.Sequence[str] = Field(default_factory=list)
 
     model_config = ConfigDict(extra="forbid")
diff --git a/tests/feature/fsm_comprehension_on_sequence/config.yml b/tests/feature/fsm_comprehension_on_sequence/config.yml
index a96fb6dad..2e8ee1258 100644
--- a/tests/feature/fsm_comprehension_on_sequence/config.yml
+++ b/tests/feature/fsm_comprehension_on_sequence/config.yml
@@ -8,3 +8,4 @@ sequence: |
   Read Channel: 5 0 9 1 0 1 2 1 0 2 2 3
   State: Send_2
 proof:
+  memlimit: 3000
diff --git a/tests/utils.py b/tests/utils.py
index 92167079c..2cd0899fa 100644
--- a/tests/utils.py
+++ b/tests/utils.py
@@ -238,10 +238,19 @@ def assert_provable_code(  # noqa: PLR0913
     tmp_path: pathlib.Path,
     main: str | None = None,
     prefix: str | None = None,
-    timeout: int = 60,
+    timeout: int | None = None,
+    memlimit: int | None = None,
     units: Sequence[str] | None = None,
 ) -> None:
-    _create_files(tmp_path, model, integration, main, prefix, proof_timeout=timeout)
+    _create_files(
+        tmp_path,
+        model,
+        integration,
+        main,
+        prefix,
+        proof_timeout=timeout,
+        proof_memlimit=memlimit,
+    )
 
     def run(command: Sequence[str]) -> None:
         p = subprocess.run(
@@ -271,12 +280,15 @@ def _create_files(  # noqa: PLR0913
     main: str | None = None,
     prefix: str | None = None,
     debug: Debug = Debug.BUILTIN,
-    proof_timeout: int = 60,
+    proof_timeout: int | None = None,
+    proof_memlimit: int | None = None,
 ) -> None:
     shutil.copy("defaults.gpr", tmp_path)
     shutil.copy("defaults.adc", tmp_path)
     shutil.copy("defaults_backward_compatible.adc", tmp_path)
     main = f'"{main}"' if main else ""
+    timeout = f', "--timeout={proof_timeout}"' if proof_timeout else ""
+    memlimit = f', "--memlimit={proof_memlimit}"' if proof_memlimit else ""
     (tmp_path / "test.gpr").write_text(
         textwrap.dedent(
             f"""\
@@ -308,7 +320,7 @@ def _create_files(  # noqa: PLR0913
 
                package Prove is
                   for Proof_Switches ("Ada") use
-                     Defaults.Proof_Switches & ("--steps=0", "--timeout={proof_timeout}");
+                     Defaults.Proof_Switches & ("--steps=0"{timeout}{memlimit});
                end Prove;
             end Test;""",
         ),
diff --git a/tests/verification/feature_test.py b/tests/verification/feature_test.py
index 580e60829..246f68f49 100644
--- a/tests/verification/feature_test.py
+++ b/tests/verification/feature_test.py
@@ -35,6 +35,7 @@ def test_provability(feature: str, tmp_path: Path) -> None:
         tmp_path,
         main=main,
         timeout=config.proof.timeout,
+        memlimit=config.proof.memlimit,
         units=[*units, *config.proof.units],
     )
 
@@ -71,6 +72,7 @@ def test_provability_with_external_io_buffers(feature: str, tmp_path: Path) -> N
         tmp_path,
         main=MAIN,
         timeout=config.proof.timeout,
+        memlimit=config.proof.memlimit,
         units=[
             "main",
             "lib",