|
| 1 | +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. |
| 2 | +# SPDX-License-Identifier: MIT-0 |
| 3 | + |
| 4 | +import argparse |
| 5 | +import json |
| 6 | +import logging |
| 7 | +import os |
| 8 | +import sys |
| 9 | + |
| 10 | + |
| 11 | +DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize |
| 12 | +an execution of CBMC proofs.""" |
| 13 | + |
| 14 | + |
| 15 | +def get_args(): |
| 16 | + """Parse arguments for summarize script.""" |
| 17 | + parser = argparse.ArgumentParser(description=DESCRIPTION) |
| 18 | + for arg in [{ |
| 19 | + "flags": ["--run-file"], |
| 20 | + "help": "path to the Litani run.json file", |
| 21 | + "required": True, |
| 22 | + }]: |
| 23 | + flags = arg.pop("flags") |
| 24 | + parser.add_argument(*flags, **arg) |
| 25 | + return parser.parse_args() |
| 26 | + |
| 27 | + |
| 28 | +def _get_max_length_per_column_list(data): |
| 29 | + ret = [len(item) + 1 for item in data[0]] |
| 30 | + for row in data[1:]: |
| 31 | + for idx, item in enumerate(row): |
| 32 | + ret[idx] = max(ret[idx], len(item) + 1) |
| 33 | + return ret |
| 34 | + |
| 35 | + |
| 36 | +def _get_table_header_separator(max_length_per_column_list): |
| 37 | + line_sep = "" |
| 38 | + for max_length_of_word_in_col in max_length_per_column_list: |
| 39 | + line_sep += "|" + "-" * (max_length_of_word_in_col + 1) |
| 40 | + line_sep += "|\n" |
| 41 | + return line_sep |
| 42 | + |
| 43 | + |
| 44 | +def _get_entries(max_length_per_column_list, row_data): |
| 45 | + entries = [] |
| 46 | + for row in row_data: |
| 47 | + entry = "" |
| 48 | + for idx, word in enumerate(row): |
| 49 | + max_length_of_word_in_col = max_length_per_column_list[idx] |
| 50 | + space_formatted_word = (max_length_of_word_in_col - len(word)) * " " |
| 51 | + entry += "| " + word + space_formatted_word |
| 52 | + entry += "|\n" |
| 53 | + entries.append(entry) |
| 54 | + return entries |
| 55 | + |
| 56 | + |
| 57 | +def _get_rendered_table(data): |
| 58 | + table = [] |
| 59 | + max_length_per_column_list = _get_max_length_per_column_list(data) |
| 60 | + entries = _get_entries(max_length_per_column_list, data) |
| 61 | + for idx, entry in enumerate(entries): |
| 62 | + if idx == 1: |
| 63 | + line_sep = _get_table_header_separator(max_length_per_column_list) |
| 64 | + table.append(line_sep) |
| 65 | + table.append(entry) |
| 66 | + table.append("\n") |
| 67 | + return "".join(table) |
| 68 | + |
| 69 | + |
| 70 | +def _get_status_and_proof_summaries(run_dict): |
| 71 | + """Parse a dict representing a Litani run and create lists summarizing the |
| 72 | + proof results. |
| 73 | +
|
| 74 | + Parameters |
| 75 | + ---------- |
| 76 | + run_dict |
| 77 | + A dictionary representing a Litani run. |
| 78 | +
|
| 79 | +
|
| 80 | + Returns |
| 81 | + ------- |
| 82 | + A list of 2 lists. |
| 83 | + The first sub-list maps a status to the number of proofs with that status. |
| 84 | + The second sub-list maps each proof to its status. |
| 85 | + """ |
| 86 | + count_statuses = {} |
| 87 | + proofs = [["Proof", "Status"]] |
| 88 | + for proof_pipeline in run_dict["pipelines"]: |
| 89 | + status_pretty_name = proof_pipeline["status"].title().replace("_", " ") |
| 90 | + try: |
| 91 | + count_statuses[status_pretty_name] += 1 |
| 92 | + except KeyError: |
| 93 | + count_statuses[status_pretty_name] = 1 |
| 94 | + if proof_pipeline["name"] == "print_tool_versions": |
| 95 | + continue |
| 96 | + proofs.append([proof_pipeline["name"], status_pretty_name]) |
| 97 | + statuses = [["Status", "Count"]] |
| 98 | + for status, count in count_statuses.items(): |
| 99 | + statuses.append([status, str(count)]) |
| 100 | + return [statuses, proofs] |
| 101 | + |
| 102 | + |
| 103 | +def print_proof_results(out_file): |
| 104 | + """ |
| 105 | + Print 2 strings that summarize the proof results. |
| 106 | + When printing, each string will render as a GitHub flavored Markdown table. |
| 107 | + """ |
| 108 | + output = "## Summary of CBMC proof results\n\n" |
| 109 | + with open(out_file, encoding='utf-8') as run_json: |
| 110 | + run_dict = json.load(run_json) |
| 111 | + status_table, proof_table = _get_status_and_proof_summaries(run_dict) |
| 112 | + for summary in (status_table, proof_table): |
| 113 | + output += _get_rendered_table(summary) |
| 114 | + |
| 115 | + print(output) |
| 116 | + sys.stdout.flush() |
| 117 | + |
| 118 | + github_summary_file = os.getenv("GITHUB_STEP_SUMMARY") |
| 119 | + if github_summary_file: |
| 120 | + with open(github_summary_file, "a") as handle: |
| 121 | + print(output, file=handle) |
| 122 | + handle.flush() |
| 123 | + else: |
| 124 | + logging.warning( |
| 125 | + "$GITHUB_STEP_SUMMARY not set, not writing summary file") |
| 126 | + |
| 127 | + msg = ( |
| 128 | + "Click the 'Summary' button to view a Markdown table " |
| 129 | + "summarizing all proof results") |
| 130 | + if run_dict["status"] != "success": |
| 131 | + logging.error("Not all proofs passed.") |
| 132 | + logging.error(msg) |
| 133 | + sys.exit(1) |
| 134 | + logging.info(msg) |
| 135 | + |
| 136 | + |
| 137 | +if __name__ == '__main__': |
| 138 | + args = get_args() |
| 139 | + logging.basicConfig(format="%(levelname)s: %(message)s") |
| 140 | + try: |
| 141 | + print_proof_results(args.run_file) |
| 142 | + except Exception as ex: # pylint: disable=broad-except |
| 143 | + logging.critical("Could not print results. Exception: %s", str(ex)) |
0 commit comments