# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0

import argparse
import json
import logging
import os
import sys


DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize
an execution of CBMC proofs."""


def get_args():
    """Parse arguments for summarize script."""
    parser = argparse.ArgumentParser(description=DESCRIPTION)
    for arg in [{
            "flags": ["--run-file"],
            "help": "path to the Litani run.json file",
            "required": True,
    }]:
        flags = arg.pop("flags")
        parser.add_argument(*flags, **arg)
    return parser.parse_args()


def _get_max_length_per_column_list(data):
    ret = [len(item) + 1 for item in data[0]]
    for row in data[1:]:
        for idx, item in enumerate(row):
            ret[idx] = max(ret[idx], len(item) + 1)
    return ret


def _get_table_header_separator(max_length_per_column_list):
    line_sep = ""
    for max_length_of_word_in_col in max_length_per_column_list:
        line_sep += "|" + "-" * (max_length_of_word_in_col + 1)
    line_sep += "|\n"
    return line_sep


def _get_entries(max_length_per_column_list, row_data):
    entries = []
    for row in row_data:
        entry = ""
        for idx, word in enumerate(row):
            max_length_of_word_in_col = max_length_per_column_list[idx]
            space_formatted_word = (max_length_of_word_in_col - len(word)) * " "
            entry += "| " + word + space_formatted_word
        entry += "|\n"
        entries.append(entry)
    return entries


def _get_rendered_table(data):
    table = []
    max_length_per_column_list = _get_max_length_per_column_list(data)
    entries = _get_entries(max_length_per_column_list, data)
    for idx, entry in enumerate(entries):
        if idx == 1:
            line_sep = _get_table_header_separator(max_length_per_column_list)
            table.append(line_sep)
        table.append(entry)
    table.append("\n")
    return "".join(table)


def _get_status_and_proof_summaries(run_dict):
    """Parse a dict representing a Litani run and create lists summarizing the
    proof results.

    Parameters
    ----------
    run_dict
        A dictionary representing a Litani run.


    Returns
    -------
    A list of 2 lists.
    The first sub-list maps a status to the number of proofs with that status.
    The second sub-list maps each proof to its function and status.
    """
    count_statuses = {}
    proofs = [["Function","Proof", "Status"]]
    for proof_pipeline in run_dict:
        status_pretty_name = proof_pipeline['status']
        try:
            count_statuses[status_pretty_name] += 1
        except KeyError:
            count_statuses[status_pretty_name] = 1
        proofs.append([proof_pipeline["sourceLocation"]["function"], proof_pipeline["property"], status_pretty_name])
    statuses = [["Status", "Count"]]
    for status, count in count_statuses.items():
        statuses.append([status, str(count)])
    return [statuses, proofs]


def print_proof_results(out_file):
    """
    Print 2 strings that summarize the proof results.
    When printing, each string will render as a GitHub flavored Markdown table.
    """
    output = "## Summary of CBMC proof results\n\n"
    with open(out_file, encoding='utf-8') as run_json:
        run_dict = json.load(run_json)

    """
    Iterate through the json output until we get to the proof results
    Before this is info about loop unwinding, etc, which is not relevant
    to the summary page
    """
    for proof_pipeline in run_dict:
        if ('result' not in proof_pipeline):
            continue
        else:
            #Set the run_dict to be only the proof results.
            run_dict = proof_pipeline['result']

    status_table, proof_table = _get_status_and_proof_summaries(run_dict)
    for summary in (status_table, proof_table):
        output += _get_rendered_table(summary)

    print(output)
    sys.stdout.flush()

    github_summary_file = os.getenv("GITHUB_STEP_SUMMARY")
    if github_summary_file:
        with open(github_summary_file, "a") as handle:
            print(output, file=handle)
            handle.flush()
    else:
        logging.warning(
            "$GITHUB_STEP_SUMMARY not set, not writing summary file")

    msg = (
        "Click the 'Summary' button to view a Markdown table "
        "summarizing all proof results")
    if run_dict["status"] != "success":
        logging.error("Not all proofs passed.")
        logging.error(msg)
        sys.exit(1)
    logging.info(msg)


if __name__ == '__main__':
    args = get_args()
    logging.basicConfig(format="%(levelname)s: %(message)s")
    try:
        print_proof_results(args.run_file)
    except Exception as ex: # pylint: disable=broad-except
        logging.critical("Could not print results. Exception: %s", str(ex))