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

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

Author: hanno-becker

.github/actions/cbmc/action.yml

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

proofs/cbmc/lib/summarize.py

@@ -90,17 +90,32 @@ 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 = "TIMEOUT"
+        else:
+            status_pretty_name = proof_pipeline["status"].title().replace("_", " ")
+            duration_str = str(duration)
+
+        # Count statuses
+        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 +149,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

@@ -857,6 +857,8 @@ class Tests:
                             "run-cbmc-proofs.py",
                             "--summarize",
                             "--no-coverage",
+                            "--per-proof-timeout",
+                            str(self.args.per_proof_timeout),
                             "-p",
                             func,
                         ]
@@ -911,7 +913,15 @@ class Tests:
                 return
             envvars = {"MLKEM_K": mlkem_k}
             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",
@@ -1287,6 +1297,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",