Skip to content

Commit daf8962

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 daf8962

File tree

1 file changed

+17
-15
lines changed

1 file changed

+17
-15
lines changed

scripts/tests

Lines changed: 17 additions & 15 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
@@ -696,13 +697,6 @@ class Tests:
696697
log = logger(f"CBMC ({i+1}/{num_proofs})", scheme, None, None)
697698
log.info(f"Starting CBMC proof for {func}")
698699
start = time.time()
699-
if self.args.verbose is False:
700-
extra_args = {
701-
"stdout": subprocess.DEVNULL,
702-
"stderr": subprocess.DEVNULL,
703-
}
704-
else:
705-
extra_args = {}
706700
try:
707701
p = subprocess.run(
708702
[
@@ -716,31 +710,34 @@ class Tests:
716710
+ self.make_j(),
717711
cwd="proofs/cbmc",
718712
env=os.environ.copy() | envvars,
719-
capture_output=True,
720713
timeout=self.args.timeout,
714+
capture_output=(self.args.verbose is False),
721715
)
722-
except subprocess.TimeoutExpired:
716+
except subprocess.TimeoutExpired as e:
723717
log.error(f" TIMEOUT (after {self.args.timeout}s)")
724-
log.error(p.stderr)
718+
log.error(e.stderr.decode())
725719
self.fail(f"CBMC proof for {func}")
726720
if self.args.fail_upon_error:
727721
log.error(
728722
"Aborting proofs, as requested by -f/--fail-upon-error"
729723
)
730724
exit(1)
731725
continue
732-
733726
end = time.time()
734727
dur = int(end - start)
735728
if p.returncode != 0:
736729
log.error(f" FAILED (after {dur}s)")
737-
log.error(p.stderr.decode())
730+
if p.stderr is not None:
731+
log.error(p.stderr.decode())
738732
self.fail(f"CBMC proof for {func}")
739733
else:
740734
log.info(f" SUCCESS (after {dur}s)")
741735

742736
def run_cbmc(mldsa_mode):
743-
proofs = list_proofs()
737+
all_proofs = list_proofs()
738+
proofs = all_proofs
739+
scheme = SCHEME.from_mode(mldsa_mode)
740+
log = logger(f"Run CBMC", scheme, None, None)
744741
if self.args.start_with is not None:
745742
try:
746743
idx = proofs.index(self.args.start_with)
@@ -750,7 +747,12 @@ class Tests:
750747
"Could not find function {self.args.start_with}. Running all proofs"
751748
)
752749
if self.args.proof is not None:
753-
proofs = self.args.proof
750+
proofs = []
751+
for pat in self.args.proof:
752+
# Replace wildcards by regexp wildcards
753+
pat = pat.replace("*", ".*")
754+
proofs += list(filter(lambda x: re.match(pat, x), all_proofs))
755+
proofs = sorted(set(proofs))
754756

755757
if self.args.single_step:
756758
run_cbmc_single_step(mldsa_mode, proofs)
@@ -1002,7 +1004,7 @@ def cli():
10021004
"-p",
10031005
"--proof",
10041006
nargs="+",
1005-
help="Space separated list of functions for which to run the CBMC proofs.",
1007+
help='Space separated list of functions for which to run the CBMC proofs. Wildcard patterns "*" are allowed.',
10061008
default=None,
10071009
)
10081010

0 commit comments

Comments
 (0)