blob: 551af6ac320d27785afbf92fbf447048a4e34a56 [file] [log] [blame]
#!/usr/bin/env python3
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
import argparse
import logging as log
import re
from pathlib import Path
from collections import OrderedDict
import sys
import hjson
def extract_messages(str_buffer, patterns):
'''Extract messages matching patterns from str_buffer as a dictionary.
The patterns argument is a list of pairs, (key, pattern). Each pattern is a regex
and all matches in str_buffer are stored in a dictionary under the paired key.
'''
results = OrderedDict()
for key, pattern in patterns:
val = results.setdefault(key, [])
val += re.findall(pattern, str_buffer, flags=re.MULTILINE)
return results
def extract_messages_count(str_buffer, patterns):
'''Extract messages matching patterns from full_file as a dictionary.
The patterns argument is a list of pairs, (key, pattern). Each pattern is a regex
and the total count of all matches in str_buffer are stored in a dictionary under
the paired key.
'''
results = OrderedDict()
for key, pattern in patterns:
results.setdefault(key, 0)
results[key] += len(re.findall(pattern, str_buffer, flags=re.MULTILINE))
return results
def format_percentage(good, bad):
'''Return a percentage of good / (good + bad) with a format `100.00 %`.'''
denom = good + bad
pc = 100 * good / denom if denom else 0
return '{0:.2f} %'.format(round(pc, 2))
def parse_message(str_buffer):
'''Parse error, warnings, and failed properties from the log file'''
err_warn_patterns = [("errors", r"^Error.*"),
("errors", r"^\[Error.*"),
("warnings", r"^Warning.*"),
("warnings", r"^\[Warning.*"),
("cex", r"^\d+,assert,falsified,.*"),
("cex", r"^\d+,assert,vacuous,.*"),
("undetermined", r"^\d+,assert,inconclusive,.*"),
("unreachable", r"^\d+,cover,uncoverable,.*"),
("undetermined", r"^\d+,cover,inconclusive,.*")]
return extract_messages(str_buffer, err_warn_patterns)
def get_summary(str_buffer):
'''Count errors, warnings, and property status from the log file'''
message_patterns = [("errors", r"^Error.*"),
("errors", r"^\[Error.*"),
("warnings", r"^Warning.*"),
("warnings", r"^\[Warning.*"),
("proven", r"^\d+,assert,proven,.*"),
("cex", r"^\d+,assert,falsified,.*"),
("cex", r"^\d+,assert,vacuous,.*"),
("undetermined", r"^\d+,assert,inconclusive,.*"),
("covered", r"^\d+,cover,covered,.*"),
("unreachable", r"^\d+,cover,uncoverable,.*"),
("undetermined", r"^\d+,cover,inconclusive,.*")]
summary = extract_messages_count(str_buffer, message_patterns)
summary["pass_rate"] = format_percentage(summary["proven"],
summary["cex"] + summary["undetermined"])
summary["cov_rate"] = format_percentage(summary["covered"],
summary["unreachable"])
return summary
def get_results(logpath):
'''Parse log file and extract info to a dictionary'''
try:
with Path(logpath).open() as f:
results = OrderedDict()
full_file = f.read()
results["messages"] = parse_message(full_file)
summary = get_summary(full_file)
if summary:
results["summary"] = summary
return results
except IOError as err:
err_msg = 'IOError {}'.format(err)
log.error("[get_results] IOError %s", err)
return {'messages': {'errors': err_msg}}
return results
def get_cov_results(logpath, dut_name):
'''Parse coverage information from the log file'''
try:
with Path(logpath).open() as f:
full_file = f.read()
cov_pattern = r"\s*\|\d*.\d\d%\s\(\d*\/\d*\)" # cov pattern: 100.00% (5/5)
pattern_match = r"\s*\|(\d*.\d\d)%\s\(\d*\/\d*\)" # extract percentage in cov_pattern
coverage_patterns = \
[("stimuli", r"^\|" + dut_name + pattern_match + cov_pattern + cov_pattern),
("coi", r"^\|" + dut_name + cov_pattern + pattern_match + cov_pattern),
("proof", r"^\|" + dut_name + cov_pattern + cov_pattern + pattern_match)]
cov_results = extract_messages(full_file, coverage_patterns)
for key, item in cov_results.items():
if len(item) == 1:
cov_results[key] = item[0] + " %"
else:
cov_results[key] = "N/A"
log.warning("Parse %s coverage error. Expect one matching value, get %s",
key, item)
return cov_results
except IOError as err:
log.error("[get_cov_results] IOError %s", err)
return None
def main():
parser = argparse.ArgumentParser(
description=
'''This script parses the output log to extract below information.
"messages": {
"errors" : []
"warnings" : []
"cex" : ["property1", "property2"...],
"vacuous" : ["property5", "property6"...],
"undetermined": [],
"unreachable" : [],
},
"summary": {
"errors" : 0
"warnings" : 2
"proven" : 40,
"cex" : 5,
"vacuous" : 3,
"covered" : 18,
"undetermined": 2,
"unreachable" : 2,
"pass_rate" : "80 %",
"cover_rate" : "90 %"
},
If coverage is enabled, this script will also parse the coverage result:
"coverage": {
stimuli: "90 %",
coi : "90 %",
proof : "80 %"
}
The script returns nonzero status if any errors or property failures including
"cex, undetermined, unreachable" are presented.
Note this script is compatible with VC Formal version 2020.12-SP2.
''')
parser.add_argument('--logpath',
type=str,
help=('The path of the formal log file that will be parsed.'))
parser.add_argument('--reppath',
type=str,
default="results.hjson",
help=('Parsed output hjson file path. Defaults to '
'`results.hjson` under the current script directory.'))
parser.add_argument('--cov',
type=int,
default=0,
help=('Enable parsing coverage data. '
'By default, coverage parsing is disabled.'))
parser.add_argument('--dut',
type=str,
default=None,
help=('Tesbench name. '
'By default is empty, used for coverage parsing.'))
args = parser.parse_args()
results = get_results(args.logpath)
if args.cov:
results["coverage"] = get_cov_results(args.logpath, args.dut)
with Path(args.reppath).open("w") as results_file:
hjson.dump(results,
results_file,
ensure_ascii=False,
for_json=True,
use_decimal=True)
# return nonzero status if any errors or property failures are present
# TODO: currently allow warnings
err_msgs = results["messages"]
n_errors = len(err_msgs["errors"])
n_failures = (len(err_msgs.get("cex")) + len(err_msgs.get("undetermined")) +
len(err_msgs.get("unreachable")))
if n_errors > 0 or n_failures > 0:
log.info("Found %d errors, %d failures", n_errors, n_failures)
log.info("Formal logfile parsed succesfully")
return 0
if __name__ == "__main__":
sys.exit(main())