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.pull/947/head
Kareem Khazem
2 years ago
committed by
GitHub
parent
9fa0fb7f0d
commit
408c3841ea
@ -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()
|
||||
@ -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))
|
||||
Loading…
Reference in New Issue