#!/usr/bin/env python3

# This file is part of CoVeriTeam, a tool for on-demand composition of cooperative verification systems:
# https://gitlab.com/sosy-lab/software/coveriteam
#
# SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
#
# SPDX-License-Identifier: Apache-2.0

import argparse
import glob
import os
import sys
from pathlib import Path

# Setup bundled dependencies
sys.dont_write_bytecode = True  # prevents writing .pyc files

script = Path(__file__).resolve()
project_dir = script.parent.parent
lib_dir = project_dir / "lib"
for wheel in glob.glob(os.path.join(lib_dir, "*.whl")):
    sys.path.insert(0, wheel)

sys.path.insert(0, str(project_dir))
sys.path.append(str(lib_dir))


from coveriteam.remote_client import exec_remotely
import yaml
from functools import cache
from dataclasses import dataclass
from typing import Dict, Union, List, Optional
import time
import threading

ACTOR_LOC = project_dir / "actors"
SPEC_LOC = project_dir / "examples" / "test-data" / "properties"
VERIFIER_C = project_dir / "examples" / "verifier-C.cvt"
VERIFIER_HTML = project_dir / "examples" / "verifierHTML.cvt"
BASE = Path(os.getcwd())


@dataclass(frozen=True)
class RemoteConfig:
    remote_url: Optional[str]
    input_file: str
    verbose: bool
    inputs: Dict[str, Union[str, List[str]]]


class Spinner:
    busy = False
    delay = 0.1

    @staticmethod
    def spinning_cursor():
        while 1:
            for cursor in "|/-\\":
                yield cursor

    def __init__(self, delay=None):
        self.spinner_generator = self.spinning_cursor()
        if delay and float(delay):
            self.delay = delay

    def spinner_task(self):
        while self.busy:
            sys.stdout.write(next(self.spinner_generator))
            sys.stdout.flush()
            time.sleep(self.delay)
            sys.stdout.write("\b")
            sys.stdout.flush()

    def __enter__(self):
        self.busy = True
        threading.Thread(target=self.spinner_task).start()

    def __exit__(self, exception, value, tb):
        self.busy = False
        time.sleep(self.delay)
        if exception is not None:
            return False


@cache
def verifier_choice_map():
    ignore = {
        "cpachecker-BASE.yml",
        "condtest.yml",
        "cst-transform.yml",
        "verifier_resource.yml",
        "verifier+validator-portfolio.yml",
    }

    actors = {
        actor_def.stem: actor_def
        for actor_def in ACTOR_LOC.iterdir()
        if actor_def.is_file()
        and ((name := actor_def.name).endswith(".yml") or name.endswith(".yaml"))
        and (not name in ignore)
    }

    return actors


@cache
def property_choice_map():
    return {
        spec_path.stem: spec_path
        for spec_path in SPEC_LOC.iterdir()
        if spec_path.is_file()
    }


def get_parser() -> argparse.ArgumentParser:
    parser = argparse.ArgumentParser("verify", description="Remotely verify C programs")
    parser.add_argument(
        "-t", "--tool", action="store", choices=verifier_choice_map().keys()
    )
    parser.add_argument(
        "-r", "--remote", action="store_true", help="Execute with CoVeriTeam Service"
    )
    parser.add_argument(
        "-v",
        "--version",
        action="store",
        help="The version of the tool to execute "
        "(as specified in the respective actor definition)",
    )

    parser.add_argument(
        "--html",
        action="store_true",
        help="Indicate that the tool exports an html report that should be kept",
    )

    parser.add_argument(
        "--data-model", action="store", choices=["ILP32", "LP64"], default="ILP32"
    )

    parser.add_argument(
        "-s",
        "--spec",
        action="store",
        choices=property_choice_map().keys(),
        default="unreach-call",
    )

    parser.add_argument(
        "--remote-url",
        action="store",
        help="Overrides the default coveriteam service endpoint",
        default=None,
    )

    parser.add_argument("program", action="store", help="The program to verify")

    return parser


def prepare_inputs(args: argparse.Namespace) -> RemoteConfig:
    cvt_file = VERIFIER_HTML if args.html else VERIFIER_C
    verifier = verifier_choice_map()[args.tool]
    spec = property_choice_map()[args.spec]

    files_needed = [spec, verifier, cvt_file, args.program]

    # The remote_client only allows relative paths, so we find
    # the common ancestor of all files and provide their relative
    # from this common ancestor
    cp = os.path.commonpath(list(map(os.path.abspath, files_needed)))

    inputs = {
        "program_path": str(Path(args.program).absolute().relative_to(cp)),
        "data_model": args.data_model,
        "version": args.version,
        "specification_path": str(spec.relative_to(cp)),
        "verifier_path": str(verifier.relative_to(cp)),
    }

    return RemoteConfig(
        remote_url=args.remote_url,
        input_file=str(cvt_file.relative_to(cp)),
        inputs=inputs,
        verbose=False,
    )


def main():
    parser = get_parser()
    args = parser.parse_args(sys.argv[1:])
    if not args.remote:
        print("Local Execution is not supported by this script at this time.")
        return

    config = prepare_inputs(args)
    print("Calling CoVeriTeam Service... ", end="")
    with Spinner():
        exec_remotely(config)


sys.exit(main())
