Skip to content

Commit d2a700f

Browse files
committed
CBMC tests: Allow wildcard pattern in list of proofs to run
- This commit is ported from: - mlkem, commit: 615d972 - This commit adds support for the use of wildcard pattern `*` in invocations of `tests cbmc`. Example: ``` tests cbmc -p "*poly*" ``` This will run all tests for functions containing "poly". - As before, multiple patterns can be provided, e.g. ``` tests cbmc -p "*keccak*" "*once*" ``` Signed-off-by: willieyz <[email protected]>
1 parent 7c94d55 commit d2a700f

File tree

1 file changed

+12
-3
lines changed

1 file changed

+12
-3
lines changed

scripts/tests

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import time
1616
import logging
1717
import subprocess
1818
import json
19+
import re
1920

2021
from enum import Enum
2122
from functools import reduce
@@ -740,7 +741,10 @@ class Tests:
740741
log.info(f" SUCCESS (after {dur}s)")
741742

742743
def run_cbmc(mldsa_mode):
743-
proofs = list_proofs()
744+
all_proofs = list_proofs()
745+
proofs = all_proofs
746+
scheme = SCHEME.from_mode(mldsa_mode)
747+
log = logger(f"Run CBMC", scheme, None, None)
744748
if self.args.start_with is not None:
745749
try:
746750
idx = proofs.index(self.args.start_with)
@@ -750,7 +754,12 @@ class Tests:
750754
"Could not find function {self.args.start_with}. Running all proofs"
751755
)
752756
if self.args.proof is not None:
753-
proofs = self.args.proof
757+
proofs = []
758+
for pat in self.args.proof:
759+
# Replace wildcards by regexp wildcards
760+
pat = pat.replace("*", ".*")
761+
proofs += list(filter(lambda x: re.match(pat, x), all_proofs))
762+
proofs = sorted(set(proofs))
754763

755764
if self.args.single_step:
756765
run_cbmc_single_step(mldsa_mode, proofs)
@@ -1002,7 +1011,7 @@ def cli():
10021011
"-p",
10031012
"--proof",
10041013
nargs="+",
1005-
help="Space separated list of functions for which to run the CBMC proofs.",
1014+
help='Space separated list of functions for which to run the CBMC proofs. Wildcard patterns "*" are allowed.',
10061015
default=None,
10071016
)
10081017

0 commit comments

Comments
 (0)