util/dvsim/FpvCfg.py - 3p/lowrisc/opentitan - Git at Google

 # 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 FpvCfg(OneShotCfg):
     """Derivative class for FPV purposes.
     """
     def __init__(self, flow_cfg_file, proj_root, args):
         super().__init__(flow_cfg_file, proj_root, args)
         self.header = ["name", "errors", "warnings", "proven", "cex", "undetermined",
                        "covered", "unreachable", "pass_rate", "cov_rate"]
         self.summary_header = ["name", "pass_rate", "stimuli_cov", "coi_cov", "prove_cov"]

     def __post_init__(self):
         super().__post_init__()
         self.results_title = self.name.upper() + " FPV 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_fpv_summary_results(self, result):
         summary = []
         fpv_summary = result.get("fpv_summary")
         if fpv_summary is None:
             results_str = "No fpv_summary found\n"
             summary.append("N/A")
         else:
             colalign = ("center", ) * len(self.header)
             table = [self.header]
             table.append([
                 self.name,
                 str(fpv_summary["errors"]) + " E ",
                 str(fpv_summary["warnings"]) + " W ",
                 str(fpv_summary["proven"]) + " G ",
                 str(fpv_summary["cex"]) + " E ",
                 str(fpv_summary["undetermined"]) + " W ",
                 str(fpv_summary["covered"]) + " G ",
                 str(fpv_summary["unreachable"]) + " E ",
                 fpv_summary["pass_rate"],
                 fpv_summary["cov_rate"]
             ])
             summary.append(fpv_summary["pass_rate"])
             if len(table) > 1:
                 results_str = tabulate(table, headers="firstrow", tablefmt="pipe",
                                        colalign=colalign)
             else:
                 results_str = "No content in fpv_summary\n"
                 summary.append("N/A")
         return results_str, summary

     def get_fpv_coverage_results(self, result):
         summary = []
         fpv_coverage = result.get("fpv_coverage")
         if fpv_coverage is None:
             results_str = "No fpv_coverage 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([
                 fpv_coverage["stimuli"],
                 fpv_coverage["coi"],
                 fpv_coverage["proof"]
             ])
             summary.append(fpv_coverage["stimuli"])
             summary.append(fpv_coverage["coi"])
             summary.append(fpv_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 fpv_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
         # The email_summary will contain all the information from results_md
         log.info("Create summary of FPV results")

         results_str = "## " + self.results_title + " (Summary)\n\n"
         results_str += "### " + self.timestamp_long + "\n\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)

         # Generate email results summary
         colalign = ("left", ) + ("center", ) * (len(self.header) - 1)
         email_table = [self.header]
         error_message = ""

         for cfg in self.cfgs:
             email_result = cfg.result.get("fpv_summary")
             if email_result is not None:
                 email_table.append([
                     cfg.name,
                     str(email_result["errors"]) + " E ",
                     str(email_result["warnings"]) + " W ",
                     str(email_result["proven"]) + " G ",
                     str(email_result["cex"]) + " E ",
                     str(email_result["undetermined"]) + " W ",
                     str(email_result["covered"]) + " G ",
                     str(email_result["unreachable"]) + " E ",
                     email_result["pass_rate"],
                     email_result["cov_rate"]
                 ])
             messages = cfg.result.get("messages")
             if messages is not None:
                 # TODO: temp disable printing out "fpv_warnings" in results_summary
                 # Will clean up FPV warnings first, then display "fpv_warnings"
                 error = self.parse_dict_to_str(messages, ["fpv_warnings"])
                 if error:
                     error_message += "\n#### " + cfg.name + "\n"
                     error_message += error

         if len(email_table) > 1:
             self.email_summary_md = results_str + tabulate(
                 email_table, headers="firstrow", tablefmt="pipe", colalign=colalign)
         self.email_summary_md += error_message

         return self.results_summary_md

     def _gen_results(self):
         # This function is called after the regression and looks for
         # results.hjson file with aggregated results from the FPV run.
         # The hjson file is required to follow this format:
         # {
         #   "messages": {
         #      "errors"      : []
         #      "warnings"    : []
         #      "cex"         : ["property1", "property2"...],
         #      "undetermined": [],
         #      "unreachable" : [],
         #   },
         #
         #   "fpv_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 FPV coverage. It will have the following format:
         #   "fpv_coverage": {
         #      stimuli: "90 %",
         #      coi    : "90 %",
         #      proof  : "80 %"
         #   }
         results_str = "## " + self.results_title + "\n\n"
         results_str += "### " + self.timestamp_long + "\n"
         results_str += "### FPV Tool: " + self.tool.upper() + "\n"
         results_str += "### LogFile dir: " + self.scratch_path + "/default\n\n"

         summary = [self.name]  # cfg summary for publish results

         if len(self.build_modes) != 1:
             mode_names = [mode.name for mode in self.build_modes]
             log.error("FPV only supports mode 'default', but found these modes: %s", mode_names)
         else:
             mode = self.build_modes[0]
             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],
                     }
                 }

             fpv_result_str, fpv_summary = self.get_fpv_summary_results(self.result)
             results_str += fpv_result_str
             summary += fpv_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_fpv_coverage_results(self.result)
                 results_str += cov_result_str
                 summary += cov_summary

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

         # Write results to the scratch area
         self.results_md = results_str
         results_file = self.scratch_path + "/results_" + self.timestamp + ".md"
         with open(results_file, 'w') as f:
             f.write(self.results_md)

         log.info("[results page]: [%s] [%s]", self.name, results_file)

         # Generate result summary
         if not self.cov:
             summary += ["N/A", "N/A", "N/A"]
         self.result_summary[self.name] = summary

         return self.results_md

     def _publish_results(self):
         '''This does nothing: detailed messages from FPV runs are not published

         Our agreement with tool vendors allows us to publish the summary
         results (as in gen_results_summary), but not anything more detailed.
         '''
         return
	# 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 FpvCfg(OneShotCfg):
	"""Derivative class for FPV purposes.
	"""
	def __init__(self, flow_cfg_file, proj_root, args):
	super().__init__(flow_cfg_file, proj_root, args)
	self.header = ["name", "errors", "warnings", "proven", "cex", "undetermined",
	"covered", "unreachable", "pass_rate", "cov_rate"]
	self.summary_header = ["name", "pass_rate", "stimuli_cov", "coi_cov", "prove_cov"]

	def __post_init__(self):
	super().__post_init__()
	self.results_title = self.name.upper() + " FPV 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_fpv_summary_results(self, result):
	summary = []
	fpv_summary = result.get("fpv_summary")
	if fpv_summary is None:
	results_str = "No fpv_summary found\n"
	summary.append("N/A")
	else:
	colalign = ("center", ) * len(self.header)
	table = [self.header]
	table.append([
	self.name,
	str(fpv_summary["errors"]) + " E ",
	str(fpv_summary["warnings"]) + " W ",
	str(fpv_summary["proven"]) + " G ",
	str(fpv_summary["cex"]) + " E ",
	str(fpv_summary["undetermined"]) + " W ",
	str(fpv_summary["covered"]) + " G ",
	str(fpv_summary["unreachable"]) + " E ",
	fpv_summary["pass_rate"],
	fpv_summary["cov_rate"]
	])
	summary.append(fpv_summary["pass_rate"])
	if len(table) > 1:
	results_str = tabulate(table, headers="firstrow", tablefmt="pipe",
	colalign=colalign)
	else:
	results_str = "No content in fpv_summary\n"
	summary.append("N/A")
	return results_str, summary

	def get_fpv_coverage_results(self, result):
	summary = []
	fpv_coverage = result.get("fpv_coverage")
	if fpv_coverage is None:
	results_str = "No fpv_coverage 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([
	fpv_coverage["stimuli"],
	fpv_coverage["coi"],
	fpv_coverage["proof"]
	])
	summary.append(fpv_coverage["stimuli"])
	summary.append(fpv_coverage["coi"])
	summary.append(fpv_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 fpv_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
	# The email_summary will contain all the information from results_md
	log.info("Create summary of FPV results")

	results_str = "## " + self.results_title + " (Summary)\n\n"
	results_str += "### " + self.timestamp_long + "\n\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)

	# Generate email results summary
	colalign = ("left", ) + ("center", ) * (len(self.header) - 1)
	email_table = [self.header]
	error_message = ""

	for cfg in self.cfgs:
	email_result = cfg.result.get("fpv_summary")
	if email_result is not None:
	email_table.append([
	cfg.name,
	str(email_result["errors"]) + " E ",
	str(email_result["warnings"]) + " W ",
	str(email_result["proven"]) + " G ",
	str(email_result["cex"]) + " E ",
	str(email_result["undetermined"]) + " W ",
	str(email_result["covered"]) + " G ",
	str(email_result["unreachable"]) + " E ",
	email_result["pass_rate"],
	email_result["cov_rate"]
	])
	messages = cfg.result.get("messages")
	if messages is not None:
	# TODO: temp disable printing out "fpv_warnings" in results_summary
	# Will clean up FPV warnings first, then display "fpv_warnings"
	error = self.parse_dict_to_str(messages, ["fpv_warnings"])
	if error:
	error_message += "\n#### " + cfg.name + "\n"
	error_message += error

	if len(email_table) > 1:
	self.email_summary_md = results_str + tabulate(
	email_table, headers="firstrow", tablefmt="pipe", colalign=colalign)
	self.email_summary_md += error_message

	return self.results_summary_md

	def _gen_results(self):
	# This function is called after the regression and looks for
	# results.hjson file with aggregated results from the FPV run.
	# The hjson file is required to follow this format:
	# {
	# "messages": {
	# "errors" : []
	# "warnings" : []
	# "cex" : ["property1", "property2"...],
	# "undetermined": [],
	# "unreachable" : [],
	# },
	#
	# "fpv_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 FPV coverage. It will have the following format:
	# "fpv_coverage": {
	# stimuli: "90 %",
	# coi : "90 %",
	# proof : "80 %"
	# }
	results_str = "## " + self.results_title + "\n\n"
	results_str += "### " + self.timestamp_long + "\n"
	results_str += "### FPV Tool: " + self.tool.upper() + "\n"
	results_str += "### LogFile dir: " + self.scratch_path + "/default\n\n"

	summary = [self.name] # cfg summary for publish results

	if len(self.build_modes) != 1:
	mode_names = [mode.name for mode in self.build_modes]
	log.error("FPV only supports mode 'default', but found these modes: %s", mode_names)
	else:
	mode = self.build_modes[0]
	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],
	}
	}

	fpv_result_str, fpv_summary = self.get_fpv_summary_results(self.result)
	results_str += fpv_result_str
	summary += fpv_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_fpv_coverage_results(self.result)
	results_str += cov_result_str
	summary += cov_summary

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

	# Write results to the scratch area
	self.results_md = results_str
	results_file = self.scratch_path + "/results_" + self.timestamp + ".md"
	with open(results_file, 'w') as f:
	f.write(self.results_md)

	log.info("[results page]: [%s] [%s]", self.name, results_file)

	# Generate result summary
	if not self.cov:
	summary += ["N/A", "N/A", "N/A"]
	self.result_summary[self.name] = summary

	return self.results_md

	def _publish_results(self):
	'''This does nothing: detailed messages from FPV runs are not published

	Our agreement with tool vendors allows us to publish the summary
	results (as in gen_results_summary), but not anything more detailed.
	'''
	return