diff options
author | Kareem Khazem <karkhaz@karkhaz.com> | 2023-03-03 22:35:42 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-03-03 14:35:42 -0800 |
commit | 408c3841eacad990110631194d8aa73786d2e685 (patch) | |
tree | 558e1d2fee224501d166b203f67f0e72dcee41fc | |
parent | 9fa0fb7f0d82086035ccfdd4bec73a16c41f9d48 (diff) | |
download | freertos-git-408c3841eacad990110631194d8aa73786d2e685.tar.gz |
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.
-rw-r--r-- | .github/workflows/ci.yml | 18 | ||||
-rwxr-xr-x | FreeRTOS/Test/CBMC/proofs/lib/print_tool_versions.py | 74 | ||||
-rwxr-xr-x | FreeRTOS/Test/CBMC/proofs/lib/summarize.py | 143 | ||||
-rwxr-xr-x | FreeRTOS/Test/CBMC/proofs/run-cbmc-proofs.py | 7 |
4 files changed, 238 insertions, 4 deletions
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 = [ + "<table>", + '<tr><td colspan="2" style="font-weight: bold">Tool Versions</td></tr>', + ] + for tool, version in table.items(): + if version: + v_str = f'<code><pre style="margin: 0">{version}</pre></code>' + else: + v_str = '<em>not found</em>' + lines.append( + f'<tr><td style="font-weight: bold; padding-right: 1em; ' + f'text-align: right;">{tool}:</td>' + f'<td>{v_str}</td></tr>') + lines.append("</table>") + 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() |