CBMC: Allow specification of per-proof timeouts

This commit adds support for per-proof timeouts in CBMC proofs to
prevent CI from running for hours on failing or slow proofs. The
implementation leverages Litani's existing timeout mechanism via
the CBMC_TIMEOUT environment variable.

- Add `--per-proof-timeout` argument to `run-cbmc-proofs.py`
  (default: 1800s)
- Pass timeout to Litani via `CBMC_TIMEOUT` environment variable
- Modify `lib/summarize.py` to detect `timeout_reached` flag and
  display "timeout" instead.
- Add `--per-proof-timeout` argument to `tests cbmc` command
- Set explicit 30-minute timeout in CI workflow

Fixes #733

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

.github/actions/cbmc/action.yml

@@ -54,5 +54,5 @@ runs:
         shell: ${{ env.SHELL }}
         run: |
           echo "::group::cbmc_${{ inputs.mldsa_parameter_set }}"
-          tests cbmc --mldsa_parameter_set ${{ inputs.mldsa_parameter_set }};
+          tests cbmc --mldsa_parameter_set ${{ inputs.mldsa_parameter_set }} --per-proof-timeout 1800;
           echo "::endgroup::"

proofs/cbmc/lib/summarize.py

@@ -90,17 +90,31 @@ def _get_status_and_proof_summaries(run_dict):
     for proof_pipeline in run_dict["pipelines"]:
         if proof_pipeline["name"] == "print_tool_versions":
             continue
-        status_pretty_name = proof_pipeline["status"].title().replace("_", " ")
-        try:
-            count_statuses[status_pretty_name] += 1
-        except KeyError:
-            count_statuses[status_pretty_name] = 1
+
+        # Check if any job timed out
+        has_timeout = False
         duration = 0
         for stage in proof_pipeline["ci_stages"]:
             for job in stage["jobs"]:
+                if job.get("timeout_reached", False):
+                    has_timeout = True
                 if "duration" in job.keys():
                     duration += int(job["duration"])
-        proofs.append([proof_pipeline["name"], status_pretty_name, str(duration)])
+
+        # Determine status display
+        if has_timeout:
+            status_pretty_name = "Timeout"
+            duration_str = "--"
+        else:
+            status_pretty_name = proof_pipeline["status"].title().replace("_", " ")
+            duration_str = str(duration)
+
+        try:
+            count_statuses[status_pretty_name] += 1
+        except KeyError:
+            count_statuses[status_pretty_name] = 1
+
+        proofs.append([proof_pipeline["name"], status_pretty_name, duration_str])
     statuses = [["Status", "Count"]]
     for status, count in count_statuses.items():
         statuses.append([status, str(count)])
@@ -134,8 +148,15 @@ def print_proof_results(out_file):
         "Click the 'Summary' button to view a Markdown table "
         "summarizing all proof results"
     )
-    if run_dict["status"] != "success":
+
+    # Check for timeouts by examining status table
+    has_timeout = any(row[0] == "Timeout" for row in status_table[1:])
+    has_failure = run_dict["status"] != "success"
+
+    if has_timeout or has_failure:
         logging.error("Not all proofs passed.")
+        if has_timeout:
+            logging.error("Some proofs timed out.")
         logging.error(msg)
         sys.exit(1)
     logging.info(msg)

proofs/cbmc/run-cbmc-proofs.py

@@ -181,6 +181,13 @@ def get_args():
             "action": "store_true",
             "help": "do property checking without coverage checking",
         },
+        {
+            "flags": ["--per-proof-timeout"],
+            "type": int,
+            "metavar": "SECONDS",
+            "default": 1800,
+            "help": "timeout for each individual proof in seconds (default: 1800)",
+        },
     ]:
         flags = arg.pop("flags")
         pars.add_argument(*flags, **arg)
@@ -342,6 +349,7 @@ async def configure_proof_dirs(  # pylint: disable=too-many-arguments
     enable_memory_profiling,
     report_target,
     debug,
+    timeout,
 ):
     while True:
         print_counter(counter)
@@ -352,6 +360,10 @@ async def configure_proof_dirs(  # pylint: disable=too-many-arguments
         pools = ["ENABLE_POOLS=true"] if enable_pools else []
         profiling = ["ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else []
 
+        # Set up environment with CBMC_TIMEOUT
+        env = os.environ.copy()
+        env["CBMC_TIMEOUT"] = str(timeout)
+
         # delete old reports
         proc = await asyncio.create_subprocess_exec(
             "make",
@@ -373,6 +385,7 @@ async def configure_proof_dirs(  # pylint: disable=too-many-arguments
             report_target,
             "" if debug else "--quiet",
             cwd=path,
+            env=env,
             stdout=asyncio.subprocess.PIPE,
             stderr=asyncio.subprocess.PIPE,
         )
@@ -497,6 +510,7 @@ async def main():  # pylint: disable=too-many-locals
                 enable_memory_profiling,
                 report_target,
                 args.debug,
+                args.per_proof_timeout,
             )
         )
         tasks.append(task)

scripts/tests

@@ -811,6 +811,8 @@ class Tests:
                             "run-cbmc-proofs.py",
                             "--summarize",
                             "--no-coverage",
+                            "--per-proof-timeout",
+                            str(self.args.per_proof_timeout),
                             "-p",
                             func,
                         ]
@@ -867,7 +869,15 @@ class Tests:
                 return
             envvars = {"MLD_CONFIG_PARAMETER_SET": mldsa_parameter_set}
             p = subprocess.run(
-                ["python3", "run-cbmc-proofs.py", "--summarize", "--no-coverage", "-p"]
+                [
+                    "python3",
+                    "run-cbmc-proofs.py",
+                    "--summarize",
+                    "--no-coverage",
+                    "--per-proof-timeout",
+                    str(self.args.per_proof_timeout),
+                    "-p",
+                ]
                 + proofs
                 + self.make_j(),
                 cwd="proofs/cbmc",
@@ -1231,6 +1241,13 @@ def cli():
         default=3600,
     )
 
+    cbmc_parser.add_argument(
+        "--per-proof-timeout",
+        help="Timeout for each individual CBMC proof passed to run-cbmc-proofs.py, in seconds (default: 1800)",
+        type=int,
+        default=1800,
+    )
+
     cbmc_parser.add_argument(
         "-f",
         "--fail-upon-error",