#!/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())
