diff --git a/test/cbmc/proofs/lib/print_tool_versions.py b/test/cbmc/proofs/lib/print_tool_versions.py new file mode 100755 index 0000000000..bdeb429e3d --- /dev/null +++ b/test/cbmc/proofs/lib/print_tool_versions.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + + +import logging +import pathlib +import shutil +import subprocess + + +_TOOLS = [ + "cadical", + "cbmc", + "cbmc-viewer", + "cbmc-starter-kit-update", + "kissat", + "litani", +] + + +def _format_versions(table): + lines = [ + "", + '', + ] + for tool, version in table.items(): + if version: + v_str = f'
{version}
' + else: + v_str = 'not found' + lines.append( + f'' + f'') + lines.append("
Tool Versions
{tool}:{v_str}
") + return "\n".join(lines) + + +def _get_tool_versions(): + ret = {} + for tool in _TOOLS: + err = f"Could not determine version of {tool}: " + ret[tool] = None + if not shutil.which(tool): + logging.error("%s'%s' not found on $PATH", err, tool) + continue + cmd = [tool, "--version"] + proc = subprocess.Popen(cmd, text=True, stdout=subprocess.PIPE) + try: + out, _ = proc.communicate(timeout=10) + except subprocess.TimeoutExpired: + logging.error("%s'%s --version' timed out", err, tool) + continue + if proc.returncode: + logging.error( + "%s'%s --version' returned %s", err, tool, str(proc.returncode)) + continue + ret[tool] = out.strip() + return ret + + +def main(): + exe_name = pathlib.Path(__file__).name + logging.basicConfig(format=f"{exe_name}: %(message)s") + + table = _get_tool_versions() + out = _format_versions(table) + print(out) + + +if __name__ == "__main__": + main() diff --git a/test/cbmc/proofs/lib b/test/cbmc/proofs/lib/summarize.py old mode 100755 new mode 100644 similarity index 100% rename from test/cbmc/proofs/lib rename to test/cbmc/proofs/lib/summarize.py diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py index de89bff6d2..429d787342 100755 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -152,7 +152,7 @@ def run_build(jobs): cmd = ["litani", "run-build"] if jobs: cmd.extend(["-j", str(jobs)]) - run_cmd(cmd, check=True, timeout=3600) + run_cmd(cmd, check=True) def add_proof_jobs(proof_directory, proof_root): @@ -301,7 +301,13 @@ def main(): if not args.no_standalone: run_build(args.parallel_jobs) + out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest" + out_dir = out_sym.resolve() + + local_copy = pathlib.Path("output")/"latest" + local_copy.parent.mkdir(exist_ok=True) + local_copy.symlink_to(out_dir) + if __name__ == "__main__": main() -