import argparse
import os
import subprocess

path = "TARGET-PRECISION"

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

    res_path = f"{path}/{oracle}-{domain}"
    os.makedirs(path, exist_ok=True)
    if os.path.exists(res_path):
        os.system(f"rm {res_path}/*/*.json")
        os.system(f"rmdir {res_path}/*")

    drivers_path = "../downloaded_benchmarks/drivers/"

    print(f"\n### Processing {oracle} oracle with {domain} domain ###\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
        print(f"{id}: processing {driver}")

        res_path = f"{path}/{oracle}-{domain}/{driver}/"
        os.makedirs(res_path, exist_ok=True)

        cmd = ["clam.py",
               "--inline",
               f"--crab-havoc-analysis={oracle}",
               f"--crab-dom={domain}",
               f"-ojson={res_path}/result.json",
               "--crab-print-invariants=true",
               "--crab-print-invariants-kind=loops",
               "--crab-print-ghost-variables=true",
               "--crab-disable-warnings",
               driver_path]

        result = subprocess.run(cmd, capture_output=True, text=True)

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)
