1#!/usr/bin/env python3
2# SPDX-License-Identifier: BSD-3-Clause
3# SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
4#
5
6"""
7This script is used to compare the summary of the CBMC analysis with the
8baseline. The script prints an error message and returns error code if there is
9a parsing error, or the change in the summary is not compatible with the baseline.
10In the latter case, either the baseline should be updated, or the RMM code or the
11CBMC testbench needs to be fixed.
12
13The script assumes that the summary lines of the `analysis` and the `assert` modes
14have the same format and semantics
15"""
16
17import argparse
18import logging
19import ntpath
20import re
21import sys
22
23
24class ParseException(Exception):
25    """
26    An exception of this type is raised in case of parsing error
27    """
28
29
30class CompareException(Exception):
31    """
32    An exception of this type is raised when there is a difference in the
33    summaries that should be fixed.
34    """
35
36
37re_summary_prefix = re.compile(r"\|\s*([a-z_.]+)\s*\|\s*(\d+)\s+of\s+(\d+)")
38re_separator = re.compile(r"\+-+\+-+\+")
39re_header = re.compile(r"\|\s*[A-Z_]+\s*\|\s*([A-Z_]+)\s*\|")
40re_failed_analysis = re.compile(r"\|\s*([a-z_.]+)\s*\|\s*N\/A\s*\|")
41
42
43def parse_summary_file(summary_file_name):
44    """
45    Parse a single summary file.
46
47    Returns a tuple:
48    (summary type as a string, list of summaries)
49
50    Each element in the list of summaries is a tuple of three values:
51    (testbench name, first integer value, second integer value)
52    """
53    logging.debug(f"Parsing file {summary_file_name}")
54    with open(summary_file_name, "r", encoding="utf-8") as file:
55        lines = file.readlines()
56
57    summary_type = None
58    summary_list = []
59
60    for idx, line in enumerate(lines):
61        line = line.strip()
62        if not line:
63            continue
64        m_separator = re_separator.match(line)
65        if m_separator:
66            continue
67        m_summary_prefix = re_summary_prefix.match(line)
68        if m_summary_prefix:
69            logging.debug(f"    summary line '{line}'")
70            if not summary_type:
71                raise ParseException(
72                    f"Missing summary header in file {summary_file_name}"
73                )
74            summary_list.append(
75                (
76                    m_summary_prefix.group(1),
77                    int(m_summary_prefix.group(2)),
78                    int(m_summary_prefix.group(3)),
79                )
80            )
81            continue
82        m_header = re_header.match(line)
83        if m_header:
84            summary_type = m_header.group(1)
85            logging.debug(f"    header line '{line}'")
86            continue
87        m_failed_analysis = re_failed_analysis.match(line)
88        if m_failed_analysis:
89            logging.debug(f"    N/A line '{line}'")
90            raise ParseException(
91                f"CBMC Analysis failed in {summary_file_name} for {m_failed_analysis.group(1)} "
92                + "Please fix RMM/testbench code"
93            )
94        logging.debug(f"    Parse failed on line '{line}'")
95        raise ParseException(f"Invalid line in {summary_file_name} at line {idx+1}")
96
97    if not summary_list:
98        raise ParseException(f"No summary in file {summary_file_name}")
99
100    logging.info(f"Summary type of {summary_file_name} is {summary_type}")
101
102    return summary_type, summary_list
103
104
105def compare_coverage_summary(testbench_name, baseline_results, current_results):
106    """
107    Compare two coverage summary lines.
108
109    The results must be in the form of tuple:
110    (first integer value, second integer value)
111    """
112    logging.debug(
113        f"Comparing {baseline_results[0]} of {baseline_results[1]} against "
114        + f"{current_results[0]} of {current_results[1]}"
115    )
116    if baseline_results[0] < current_results[0]:
117        raise CompareException(
118            f"The coverage of {testbench_name} increased "
119            + f"({baseline_results[0]}->{current_results[0]}). "
120            + "Please update the baseline for later checks."
121        )
122    if baseline_results[0] > current_results[0]:
123        raise CompareException(
124            f"The coverage of {testbench_name} decreased "
125            + f"({baseline_results[0]}->{current_results[0]}). "
126            + "Please update the baseline if this is acceptable."
127        )
128    if baseline_results[1] != current_results[1]:
129        logging.warning(
130            f"The number of coverage tests in {testbench_name} changed. "
131            + f"({baseline_results[1]}->{current_results[1]}). "
132            + "Please consider updating the baseline."
133        )
134
135
136def compare_assert_summary(testbench_name, baseline_results, current_results):
137    """
138    Compare two assert summary lines.
139
140    The results must be in the form of tuple:
141    (first integer value, second integer value)
142    """
143    logging.debug(
144        f"Comparing {baseline_results[0]} of {baseline_results[1]} against "
145        + f"{current_results[0]} of {current_results[1]}"
146    )
147    if baseline_results[0] < current_results[0]:
148        raise CompareException(
149            f"The number of failed asserts in {testbench_name} increased "
150            + f"({baseline_results[0]}->{current_results[0]}). "
151            + "Please update the baseline if this is acceptable."
152        )
153    if baseline_results[0] > current_results[0]:
154        raise CompareException(
155            f"The number of failed asserts in {testbench_name} decreased "
156            + f"({baseline_results[0]}->{current_results[0]}). "
157            + "Please update the baseline for later checks."
158        )
159    # The number of asserts in the code can change frequently, so don't do a check on it.
160
161
162def compare_summary_lists(baseline_list, actual_list, comparator, testbench_list):
163    """
164    Compare two summary lists.
165
166    Arguments:
167    baseline_list -- List of testbench baseline results
168    actual_list -- List of testbench actual results
169    comparator -- A function that can compare 2 testbench result items
170    testbench_list -- A list of testbenches to be considered. If None, all
171                      testbenches are considered
172
173    baseline_list and  actual_list items are expected to be in the format of a
174    tuple: (testbench name, first integer value, second integer value)
175
176    """
177    # TODO: check for duplicated lines
178    baseline = {summary[0]: summary[1:] for summary in baseline_list}
179
180    # It is important to first check the common lines, and only report any
181    # missing or extra testbenches after that. This is to make sure that no
182    # coverage/assert change remains unnoticed due to an update of the baseline
183    # that was triggered by a tetsbench addition/deletion.
184    actual_extra = {}
185
186    if testbench_list is not None:
187        baseline = {k: v for k, v in baseline.items() if k in testbench_list}
188        actual_list = [e for e in actual_list if e[0] in testbench_list]
189
190    for summary in actual_list:
191        testbench_name = summary[0]
192        if testbench_name not in baseline.keys():
193            actual_extra[testbench_name] = summary[1:]
194            continue
195        comparator(testbench_name, baseline[testbench_name], summary[1:])
196        del baseline[testbench_name]
197    if baseline:
198        raise CompareException(
199            f"{next(iter(baseline))} is missing from the actual result. Please update baseline!"
200        )
201    if actual_extra:
202        raise CompareException(
203            f"{testbench_name} is missing from the baseline. Please update baseline!"
204        )
205
206
207def compare_summary_files(baseline_filename, actual_filename, testbench_list):
208    """
209    Compare two summary files.
210    """
211    base_type, base_summary_list = parse_summary_file(baseline_filename)
212    actual_type, actual_summary_list = parse_summary_file(actual_filename)
213
214    if base_type != actual_type:
215        raise ParseException(
216            f"{baseline_filename} and {actual_filename} have different summary type"
217        )
218
219    comparators = {
220        "COVERAGE": compare_coverage_summary,
221        "ANALYSIS": compare_assert_summary,
222        "ASSERT": compare_assert_summary,
223    }
224
225    if base_type not in comparators:
226        raise ParseException(f"Unknown summary type {base_type}")
227
228    compare_summary_lists(
229        base_summary_list, actual_summary_list, comparators[base_type], testbench_list
230    )
231
232
233def main():
234    """
235    main function of the script.
236    """
237    parser = argparse.ArgumentParser(description="compare CBMC summary siles")
238    parser.add_argument(
239        "--testbench-files",
240        type=str,
241        help="A semicolon (;) separated list of files to check in the summaries.",
242    )
243    parser.add_argument(
244        "baseline",
245        type=str,
246        help="The path of the baseline summary file.",
247    )
248    parser.add_argument(
249        "actual", type=str, help="The path of the current summary file."
250    )
251    args = parser.parse_args()
252
253    if args.testbench_files:
254        testbench_list = [ntpath.basename(p) for p in args.testbench_files.split(";")]
255    else:
256        testbench_list = None
257
258    try:
259        compare_summary_files(args.baseline, args.actual, testbench_list)
260    except ParseException as exc:
261        logging.error("Failed to compare summaries:")
262        logging.error(f"{str(exc)}")
263        sys.exit(1)
264    except CompareException as exc:
265        logging.error("The results contain significant differences:")
266        logging.error(f"{str(exc)}")
267        sys.exit(1)
268
269
270if __name__ == "__main__":
271    logging.basicConfig(format="%(message)s", level=logging.WARNING)
272    main()
273