CBMC/CI: Bump disk space to 64G

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

Author: hanno-becker

.github/workflows/cbmc.yml

@@ -24,9 +24,9 @@ jobs:
     uses: ./.github/workflows/ci_ec2_reusable.yml
     with:
       name: CBMC (ML-DSA-${{ matrix.parameter_set }}${{ matrix.reduce_ram && ', REDUCE_RAM' || '' }})
-      ec2_instance_type: c7g.4xlarge
+      ec2_instance_type: r7g.4xlarge
       ec2_ami: ubuntu-latest (aarch64)
-      ec2_volume_size: 20
+      ec2_volume_size: 64
       compile_mode: native
       opt: no_opt
       lint: false

nix/cbmc/default.nix

@@ -37,8 +37,8 @@ buildEnv {
       });
 
       inherit
-        bitwuzla # 0.8.2
-        cvc5 # 1.3.2
+        bitwuzla# 0.8.2
+        cvc5# 1.3.2
         ninja; # 1.13.2
     };
 }

proofs/cbmc/lib/cvc5_arrays_exp

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# Enable the experimental array theory in cvc5. CBMC encodes parts of
+# the CPROVER library using STORE_ALL, which cvc5 only accepts under
+# --arrays-exp.
+#
+# `exec` is load-bearing: without it bash sits between cbmc and cvc5,
+# holds the stdout FD open after cvc5 closes it, and cbmc's reader
+# stops mid-stream and treats every property verdict as ERROR even
+# though cvc5 returned `unsat`.
+exec cvc5 --arrays-exp "$@"

proofs/cbmc/run-cbmc-proofs.py

@@ -199,6 +199,14 @@ def get_args():
                 "solvers in the canonical list (Z3, BITWUZLA, CVC5)"
             ),
         },
+        {
+            "flags": ["--default-solver-only"],
+            "action": "store_true",
+            "help": (
+                "for each harness, run only the solver named by its "
+                "CBMC_DEFAULT_SOLVER. Cannot be combined with --solver."
+            ),
+        },
     ]:
         flags = arg.pop("flags")
         pars.add_argument(*flags, **arg)
@@ -361,6 +369,25 @@ def read_solver_matrix(proof_dir):
     return out
 
 
+def read_default_solver(proof_dir):
+    """Return CBMC_DEFAULT_SOLVER for a per-harness Makefile."""
+    cmd = ["make", "--no-print-directory", "echo-default-solver"]
+    proc = subprocess.run(
+        cmd,
+        cwd=proof_dir,
+        universal_newlines=True,
+        stdout=subprocess.PIPE,
+        stderr=subprocess.PIPE,
+        check=False,
+    )
+    if proc.returncode:
+        logging.critical(
+            "Could not read default solver from %s: %s", proof_dir, proc.stderr
+        )
+        sys.exit(1)
+    return proc.stdout.strip()
+
+
 def read_proof_uid(proof_dir):
     """Read PROOF_UID from a per-harness Makefile."""
     with (pathlib.Path(proof_dir) / "Makefile").open() as handle:
@@ -542,6 +569,10 @@ async def main():  # pylint: disable=too-many-locals
         logging.critical("No proof directories found")
         sys.exit(1)
 
+    if args.default_solver_only and args.solver:
+        logging.critical("--default-solver-only and --solver are mutually exclusive")
+        sys.exit(1)
+
     selected_solvers = args.solver if args.solver else list(ALL_SOLVERS)
     for s in selected_solvers:
         if s not in ALL_SOLVERS:
@@ -552,14 +583,21 @@ async def main():  # pylint: disable=too-many-locals
 
     # Enforce PROOF_UID uniqueness up-front, then expand each proof
     # directory into the Cartesian product with its solver matrix.
+    # When --default-solver-only is given, the per-harness solver list
+    # collapses to {CBMC_DEFAULT_SOLVER}; otherwise every solver in
+    # selected_solvers that the matrix declares enabled is used.
     proof_uids = {}
     pairs_to_run = []  # (proof_dir, solver)
     omitted_pairs = []  # (proof_uid, solver)
     for proof_dir in proof_dirs:
         check_uid_uniqueness(proof_dir, proof_uids)
         proof_uid = read_proof_uid(proof_dir)
         matrix = read_solver_matrix(proof_dir)
-        for solver in selected_solvers:
+        if args.default_solver_only:
+            per_harness_solvers = [read_default_solver(proof_dir)]
+        else:
+            per_harness_solvers = selected_solvers
+        for solver in per_harness_solvers:
             if matrix.get(solver):
                 pairs_to_run.append((proof_dir, solver))
             else:

scripts/tests

@@ -918,6 +918,15 @@ class Tests:
                 print(p)
             exit(0)
 
+        def solver_args():
+            args = []
+            if self.args.default_solver_only:
+                args.append("--default-solver-only")
+            if self.args.solver:
+                for s in self.args.solver:
+                    args += ["--solver", s]
+            return args
+
         def run_cbmc_single_step(mldsa_parameter_set, proofs):
             envvars = {"MLD_CONFIG_PARAMETER_SET": mldsa_parameter_set}
             if self.args.reduce_ram:
@@ -940,6 +949,7 @@ class Tests:
                             "-p",
                             func,
                         ]
+                        + solver_args()
                         + self.make_j(),
                         cwd="proofs/cbmc",
                         env=os.environ.copy() | envvars,
@@ -1004,6 +1014,7 @@ class Tests:
                     "-p",
                 ]
                 + proofs
+                + solver_args()
                 + self.make_j()
             )
             if self.args.output_result_json:
@@ -1478,6 +1489,28 @@ def cli():
         default=False,
     )
 
+    cbmc_parser.add_argument(
+        "--solver",
+        action="append",
+        help=(
+            "Restrict CBMC run to the given solver (repeatable). Forwarded "
+            "to run-cbmc-proofs.py --solver. Default: all solvers in the "
+            "canonical list (Z3, BITWUZLA, CVC5)."
+        ),
+        default=None,
+    )
+
+    cbmc_parser.add_argument(
+        "--default-solver-only",
+        help=(
+            "For each harness, run only the solver named by its "
+            "CBMC_DEFAULT_SOLVER. Forwarded to run-cbmc-proofs.py. "
+            "Cannot be combined with --solver."
+        ),
+        action="store_true",
+        default=False,
+    )
+
     # hol_light arguments
     hol_light_parser = cmd_subparsers.add_parser(
         "hol_light",