util/dvsim/FormalCfg.py

# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0

import logging as log
from pathlib import Path

import hjson
from tabulate import tabulate

from OneShotCfg import OneShotCfg
from utils import subst_wildcards


class FormalCfg(OneShotCfg):
    """Derivative class for running formal tools.
    """

    flow = 'formal'

    def __init__(self, flow_cfg_file, hjson_data, args, mk_config):
        # Options set from command line
        self.batch_mode_prefix = "" if args.gui else "-batch"

        super().__init__(flow_cfg_file, hjson_data, args, mk_config)
        self.header = ["name", "errors", "warnings", "proven", "cex", "undetermined",
                       "covered", "unreachable", "pass_rate", "cov_rate"]

        # Default not to publish child cfg results.
        if "publish_report" in hjson_data:
            self.publish_report = hjson_data["publish_report"]
        else:
            self.publish_report = False
        self.sub_flow = hjson_data['sub_flow']
        self.summary_header = ["name", "pass_rate", "stimuli_cov", "coi_cov", "prove_cov"]
        self.results_title = self.name.upper() + " Formal " + self.sub_flow.upper() + " Results"

    def parse_dict_to_str(self, input_dict, excl_keys = []):
        # This is a helper function to parse dictionary items into a string.
        # This function has an optional input "excl_keys" for user to exclude
        # printing out certain items according to their keys.
        # Note this function did not sort the input dictionary's key value
        # before printing the keys and items. If input dictionary is not an
        # OrderedDictionary, print out key order is not predictable.
        # This function works for Hjson lib outputs because the lib uses an
        # OrderDict when it reads dictionaries.
        # Example Input:
        # {
        #   "unreachable": ["prop1, prop2, prop3"],
        #   "cex"        : ["prop1"],
        # }
        # Example Output:
        # string = "unreachable:
        # ```
        # prop1
        # prop2
        # prop3
        # ```
        # cex:
        # ```
        # prop1
        # ```"
        output_str = ""
        for key, item in input_dict.items():
            if (key not in excl_keys) and item:
                output_str += "\n" + key + ":\n"
                output_str += "```\n"
                output_str += "\n".join(item)
                output_str += "\n```\n"
        return output_str

    def get_summary(self, result):
        summary = []
        formal_summary = result.get("summary")
        if formal_summary is None:
            results_str = "No summary information found\n"
            summary.append("N/A")
        else:
            colalign = ("center", ) * len(self.header)
            table = [self.header]
            table.append([
                self.name,
                str(formal_summary["errors"]) + " E ",
                str(formal_summary["warnings"]) + " W ",
                str(formal_summary["proven"]) + " G ",
                str(formal_summary["cex"]) + " E ",
                str(formal_summary["undetermined"]) + " W ",
                str(formal_summary["covered"]) + " G ",
                str(formal_summary["unreachable"]) + " E ",
                formal_summary["pass_rate"],
                formal_summary["cov_rate"]
            ])
            summary.append(formal_summary["pass_rate"])
            if len(table) > 1:
                results_str = tabulate(table, headers="firstrow", tablefmt="pipe",
                                       colalign=colalign)
            else:
                results_str = "No content in summary\n"
                summary.append("N/A")
        return results_str, summary

    def get_coverage(self, result):
        summary = []
        formal_coverage = result.get("coverage")
        if formal_coverage is None:
            results_str = "No coverage information found\n"
            summary = ["N/A", "N/A", "N/A"]
        else:
            cov_header = ["stimuli", "coi", "proof"]
            cov_colalign = ("center", ) * len(cov_header)
            cov_table = [cov_header]
            cov_table.append([
                formal_coverage["stimuli"],
                formal_coverage["coi"],
                formal_coverage["proof"]
            ])
            summary.append(formal_coverage["stimuli"])
            summary.append(formal_coverage["coi"])
            summary.append(formal_coverage["proof"])

            if len(cov_table) > 1:
                results_str = tabulate(cov_table, headers="firstrow",
                                       tablefmt="pipe", colalign=cov_colalign)

            else:
                results_str = "No content in formal_coverage\n"
                summary = ["N/A", "N/A", "N/A"]
        return results_str, summary

    def gen_results_summary(self):
        # Gathers the aggregated results from all sub configs
        # The results_summary will only contain the passing rate and
        # percentages of the stimuli, coi, and proven coverage
        results_str = "## " + self.results_title + " (Summary)\n\n"
        results_str += "### " + self.timestamp_long + "\n"
        if self.revision:
            results_str += "### " + self.revision + "\n"
        results_str += "### Branch: " + self.branch + "\n"
        results_str += "\n"

        colalign = ("center", ) * len(self.summary_header)
        table = [self.summary_header]
        for cfg in self.cfgs:
            try:
                table.append(cfg.result_summary[cfg.name])
            except KeyError as e:
                table.append([cfg.name, "ERROR", "N/A", "N/A", "N/A"])
                log.error("cfg: %s could not find generated results_summary: %s", cfg.name, e)
        if len(table) > 1:
            self.results_summary_md = results_str + tabulate(
                table, headers="firstrow", tablefmt="pipe", colalign=colalign)
        else:
            self.results_summary_md = results_str

        log.info("[result summary]: %s", self.results_summary_md)

        return self.results_summary_md

    def _gen_results(self, results):
        # This function is called after the regression and looks for
        # results.hjson file with aggregated results from the formal logfile.
        # The hjson file is required to follow this format:
        # {
        #   "messages": {
        #      "errors"      : []
        #      "warnings"    : []
        #      "cex"         : ["property1", "property2"...],
        #      "undetermined": [],
        #      "unreachable" : [],
        #   },
        #
        #   "summary": {
        #      "errors"      : 0
        #      "warnings"    : 2
        #      "proven"      : 20,
        #      "cex"         : 5,
        #      "covered"     : 18,
        #      "undetermined": 7,
        #      "unreachable" : 2,
        #      "pass_rate"   : "90 %",
        #      "cover_rate"  : "90 %"
        #   },
        # }
        # The categories for property results are: proven, cex, undetermined,
        # covered, and unreachable.
        #
        # If coverage was enabled then results.hjson will also have an item that
        # shows formal coverage. It will have the following format:
        #   "coverage": {
        #      stimuli: "90 %",
        #      coi    : "90 %",
        #      proof  : "80 %"
        #   }
        results_str = "## " + self.results_title + "\n\n"
        results_str += "### " + self.timestamp_long + "\n"
        if self.revision:
            results_str += "### " + self.revision + "\n"
        results_str += "### Branch: " + self.branch + "\n"
        results_str += "### Tool: " + self.tool.upper() + "\n"
        summary = [self.name]  # cfg summary for publish results

        assert len(self.deploy) == 1
        mode = self.deploy[0]

        if results[mode] == "P":
            result_data = Path(subst_wildcards(self.build_dir,
                                               {"build_mode": mode.name}),
                               'results.hjson')
            try:
                with open(result_data, "r") as results_file:
                    self.result = hjson.load(results_file, use_decimal=True)
            except IOError as err:
                log.warning("%s", err)
                self.result = {
                    "messages": {
                        "errors": ["IOError: %s" % err],
                    }
                }

        results_str += "\n\n## Formal " + self.sub_flow.upper() + " Results\n"
        formal_result_str, formal_summary = self.get_summary(self.result)
        results_str += formal_result_str
        summary += formal_summary

        if self.cov:
            results_str += "\n\n## Coverage Results\n"
            results_str += ("### Coverage html file dir: " +
                            self.scratch_path + "/default/formal-icarus\n\n")
            cov_result_str, cov_summary = self.get_coverage(self.result)
            results_str += cov_result_str
            summary += cov_summary
        else:
            summary += ["N/A", "N/A", "N/A"]

        if results[mode] != "P":
            results_str += "\n## List of Failures\n" + ''.join(
                mode.launcher.fail_msg.message)

        messages = self.result.get("messages")
        if messages is not None:
            results_str += self.parse_dict_to_str(messages)

        self.results_md = results_str

        # Generate result summary
        self.result_summary[self.name] = summary

        return self.results_md

    def _publish_results(self):
        ''' our agreement with tool vendors allows us to publish the summary
        results (as in gen_results_summary).

        In default this method does nothing: detailed messages from each child
        cfg will not be published.
        If the publish_report argument is set to true, this method will only
        publish a result summary of the child cfg.
        '''
        if self.publish_report:
            self.publish_results_md = self.gen_results_summary()
            super()._publish_results()
        else:
            return