import argparse
import os
import subprocess
import statistics

path = "TARGET-EFFICIENCY"

def process(oracle, domain):
    assert oracle in ["none", "def-nonrel", "def-rel", "pos-nonrel", "pos-rel"]
    assert domain in ["int", "pk-ap-pplite"]

    outfile_name = f"{oracle}-{domain}.txt"

    os.makedirs(path, exist_ok=True)
    outfile_path = os.path.join(path, outfile_name)
    os.system(f"rm {outfile_path}")
    os.system(f"touch {outfile_path}")

    drivers_path = "../downloaded_benchmarks/drivers/"

    print(f"\n### Processing {oracle} oracle with {domain} domain ###")

    header = "driver ; id ; havoc ; target ; havoc+target ; clam.py"
    print(header)
    with open(outfile_path, "a") as f:
        f.write(f"{header}\n")

    id = 0
    for driver in sorted(os.listdir(drivers_path)):
        driver_path = os.path.join(drivers_path, driver)
        if not os.path.isfile(driver_path):
            continue
        id = id + 1

        cmd = ["clam.py",
               "--inline",
               f"--crab-havoc-analysis={oracle}",
               f"--crab-dom={domain}",
               "--crab-print-invariants=false",
               "--crab-disable-warnings",
               driver_path]

        result = subprocess.run(cmd, capture_output=True, text=True)
        all_lines = result.stdout.split("\n")
        havoc_lines = [x for x in all_lines
                       if ("Havoc analysis time" in x)
                       or ("Havoc propagation time" in x)]
        havoc = sum(
            float(x.split()[4].replace('s', '')) for x in havoc_lines
        )
        target_lines = [x for x in all_lines
                    if "Target analysis time" in x]
        target = sum(
            float(x.split()[4].replace('s', '')) for x in target_lines
        )
        both= havoc + target
        clam_lines = [x for x in all_lines
                      if "BRUNCH_STAT Clam " in x
                      or "BRUNCH_STAT ClamPP" in x
                      or "BRUNCH_STAT Clang" in x]
        clam = sum(
            float(x.split()[2]) for x in clam_lines
        )

        outline = f"{driver} ; d{id:2d} ; {havoc:.6f} ; {target:.6f} ; {both:.6f} ; {clam:.6f}"
        print(outline)
        with open(outfile_path, "a") as f:
            f.write(f"{outline}\n")

if __name__ == "__main__":
    argparser = argparse.ArgumentParser()
    argparser.add_argument("--oracle", help="oracle to use for havoc analysis", required=True)
    argparser.add_argument("--domain", help="domain to use for target analysis", required=True)
    args = argparser.parse_args()
    process(args.oracle, args.domain)
