From 408c3841eacad990110631194d8aa73786d2e685 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 3 Mar 2023 22:35:42 +0000 Subject: Add CBMC proof-running GitHub Action (#924) This commit adds a GitHub Action that runs the CBMC proofs upon every push and pull request. This is intended to replace the current CBMC CI. --- .github/workflows/ci.yml | 18 ++- .../Test/CBMC/proofs/lib/print_tool_versions.py | 74 +++++++++++ FreeRTOS/Test/CBMC/proofs/lib/summarize.py | 143 +++++++++++++++++++++ FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py | 7 + 4 files changed, 238 insertions(+), 4 deletions(-) create mode 100755 FreeRTOS/Test/CBMC/proofs/lib/print_tool_versions.py create mode 100755 FreeRTOS/Test/CBMC/proofs/lib/summarize.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 24e630380..5887c1172 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -172,7 +172,17 @@ jobs: path: ./freertos_lts_memory_estimates.json retention-days: 2 - - - - + proof_ci: + runs-on: cbmc_ubuntu-latest_16-core + steps: + - uses: actions/checkout@v2 + - run: | + git submodule update --init --checkout --recursive --depth 1 + sudo apt-get update + sudo apt-get install --yes --no-install-recommends gcc-multilib + - name: Set up CBMC runner + uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main + - name: Run CBMC + uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main + with: + proofs_dir: FreeRTOS/Test/CBMC/proofs diff --git a/FreeRTOS/Test/CBMC/proofs/lib/print_tool_versions.py b/FreeRTOS/Test/CBMC/proofs/lib/print_tool_versions.py new file mode 100755 index 000000000..bdeb429e3 --- /dev/null +++ b/FreeRTOS/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/FreeRTOS/Test/CBMC/proofs/lib/summarize.py b/FreeRTOS/Test/CBMC/proofs/lib/summarize.py new file mode 100755 index 000000000..50dbcc33c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/lib/summarize.py @@ -0,0 +1,143 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + +import argparse +import json +import logging +import os +import sys + + +DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize +an execution of CBMC proofs.""" + + +def get_args(): + """Parse arguments for summarize script.""" + parser = argparse.ArgumentParser(description=DESCRIPTION) + for arg in [{ + "flags": ["--run-file"], + "help": "path to the Litani run.json file", + "required": True, + }]: + flags = arg.pop("flags") + parser.add_argument(*flags, **arg) + return parser.parse_args() + + +def _get_max_length_per_column_list(data): + ret = [len(item) + 1 for item in data[0]] + for row in data[1:]: + for idx, item in enumerate(row): + ret[idx] = max(ret[idx], len(item) + 1) + return ret + + +def _get_table_header_separator(max_length_per_column_list): + line_sep = "" + for max_length_of_word_in_col in max_length_per_column_list: + line_sep += "|" + "-" * (max_length_of_word_in_col + 1) + line_sep += "|\n" + return line_sep + + +def _get_entries(max_length_per_column_list, row_data): + entries = [] + for row in row_data: + entry = "" + for idx, word in enumerate(row): + max_length_of_word_in_col = max_length_per_column_list[idx] + space_formatted_word = (max_length_of_word_in_col - len(word)) * " " + entry += "| " + word + space_formatted_word + entry += "|\n" + entries.append(entry) + return entries + + +def _get_rendered_table(data): + table = [] + max_length_per_column_list = _get_max_length_per_column_list(data) + entries = _get_entries(max_length_per_column_list, data) + for idx, entry in enumerate(entries): + if idx == 1: + line_sep = _get_table_header_separator(max_length_per_column_list) + table.append(line_sep) + table.append(entry) + table.append("\n") + return "".join(table) + + +def _get_status_and_proof_summaries(run_dict): + """Parse a dict representing a Litani run and create lists summarizing the + proof results. + + Parameters + ---------- + run_dict + A dictionary representing a Litani run. + + + Returns + ------- + A list of 2 lists. + The first sub-list maps a status to the number of proofs with that status. + The second sub-list maps each proof to its status. + """ + count_statuses = {} + proofs = [["Proof", "Status"]] + for proof_pipeline in run_dict["pipelines"]: + status_pretty_name = proof_pipeline["status"].title().replace("_", " ") + try: + count_statuses[status_pretty_name] += 1 + except KeyError: + count_statuses[status_pretty_name] = 1 + if proof_pipeline["name"] == "print_tool_versions": + continue + proofs.append([proof_pipeline["name"], status_pretty_name]) + statuses = [["Status", "Count"]] + for status, count in count_statuses.items(): + statuses.append([status, str(count)]) + return [statuses, proofs] + + +def print_proof_results(out_file): + """ + Print 2 strings that summarize the proof results. + When printing, each string will render as a GitHub flavored Markdown table. + """ + output = "## Summary of CBMC proof results\n\n" + with open(out_file, encoding='utf-8') as run_json: + run_dict = json.load(run_json) + status_table, proof_table = _get_status_and_proof_summaries(run_dict) + for summary in (status_table, proof_table): + output += _get_rendered_table(summary) + + print(output) + sys.stdout.flush() + + github_summary_file = os.getenv("GITHUB_STEP_SUMMARY") + if github_summary_file: + with open(github_summary_file, "a") as handle: + print(output, file=handle) + handle.flush() + else: + logging.warning( + "$GITHUB_STEP_SUMMARY not set, not writing summary file") + + msg = ( + "Click the 'Summary' button to view a Markdown table " + "summarizing all proof results") + if run_dict["status"] != "success": + logging.error("Not all proofs passed.") + logging.error(msg) + sys.exit(1) + logging.info(msg) + + +if __name__ == '__main__': + args = get_args() + logging.basicConfig(format="%(levelname)s: %(message)s") + try: + print_proof_results(args.run_file) + except Exception as ex: # pylint: disable=broad-except + logging.critical("Could not print results. Exception: %s", str(ex)) diff --git a/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py b/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py index f95de775b..661a589ac 100755 --- a/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py +++ b/FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py @@ -301,6 +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() -- cgit v1.2.1