1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
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"]:
if proof_pipeline["name"] == "print_tool_versions":
continue
status_pretty_name = proof_pipeline["status"].title().replace("_", " ")
try:
count_statuses[status_pretty_name] += 1
except KeyError:
count_statuses[status_pretty_name] = 1
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))
|
