feat: add infrastructure for Alive tests (bv_bench) (#848)

bv-evaluation/collect-data-llvm-alive.py

@@ -0,0 +1,76 @@
+import matplotlib.pyplot as plt
+import numpy as np
+import pandas as pd
+import os 
+import re
+
+benchmark_dir = "../SSA/Projects/InstCombine/"
+res_dir = "results/alive-symbolic/"
+raw_data_dir = '../../paper-lean-bitvectors/raw-data/alive-symbolic/'
+reps = 1
+
+
+col = [
+"#a6cee3",
+"#1f78b4",
+"#b2df8a",
+"#33a02c",
+"#fb9a99",
+"#e31a1c"]
+
+
+
+def parse_tacbenches(file_name, raw):
+    # Regular expression to match TACBENCH entries
+    tac_bench_pattern = re.compile(
+        r"TACBENCH\s+(\w+)\s+(PASS|FAIL),\s+TIME_ELAPSED\s+([\d.]+)\s+ms,(?:\s*MSGSTART(.*?)MSGEND)?",
+        re.DOTALL
+    )
+    tac_block_pattern = re.compile(r"(TACSTART.*?TACEND)", re.DOTALL)
+    # Parsing the TACBENCH entries
+    guid = 0
+    out = []
+    for blk in tac_block_pattern.findall(raw):
+        guid += 1
+        new = []
+        for match in tac_bench_pattern.finditer(blk):
+            tactic_name = match.group(1)
+            status = match.group(2)
+            time_elapsed = float(match.group(3))
+            error_message = match.group(4).strip() if match.group(4) else None  # Only if MSGSTART-MSGEND present
+            new.append({
+                "filename" : file_name,
+                "guid":guid,
+                "name": tactic_name,
+                "status": status,
+                "time_elapsed": time_elapsed,
+                "error_message": error_message
+            })
+        print("==")
+        print(blk)
+        print("--")
+        for r in new: print(r)
+        out.extend(new)
+        print("==")
+    return out
+
+
+def run():
+    out = None
+    file = 'AliveStatements.lean'
+    with open(res_dir+file.split(".")[0]+"_r"+str("0")+".txt") as res_file:
+            results = parse_tacbenches(file.split(".")[0], res_file.read())
+
+    df = pd.DataFrame(results)
+    print(df)
+    if out is None:
+        out = df
+    else:
+        out = pd.concat([out, df])
+
+    print(out)
+    out.to_csv(raw_data_dir + 'alive_symbolic.csv')
+
+if __name__ == "__main__":
+    run()
+    pass

bv-evaluation/compare-leansat-vs-bitwuzla-alive.py

@@ -0,0 +1,62 @@
+import subprocess
+import os
+import concurrent.futures
+import argparse
+import shutil
+
+ROOT_DIR = subprocess.check_output(['git', 'rev-parse', '--show-toplevel']).decode('utf-8').strip()
+
+RESULTS_DIR = ROOT_DIR + '/bv-evaluation/results/alive-bench/'
+
+BENCHMARK_DIR = ROOT_DIR + '/SSA/Projects/InstCombine/'
+
+REPS = 1
+
+def clear_folder():
+    for file in os.listdir(RESULTS_DIR):
+        file_path = os.path.join(RESULTS_DIR, file)
+        try:
+            if os.path.isfile(file_path) or os.path.islink(file_path):
+                os.unlink(file_path)
+            elif os.path.isdir(file_path):
+                shutil.rmtree(file_path)
+        except Exception as e:
+            print('Failed to delete %s. Reason: %s' % (file_path, e))
+
+def run_file(file: str):
+    file_path = BENCHMARK_DIR + file
+    file_title = file.split('.')[0]
+    subprocess.Popen('sed -i -E \'s,try alive_auto,simp_alive_split,g\' ' + file_path, cwd=ROOT_DIR, shell=True).wait()
+    subprocess.Popen('sed -i -E \'s,all_goals sorry,bv_bench,g\' ' + file_path, cwd=ROOT_DIR, shell=True).wait()
+
+    for r in range(REPS):
+        log_file_path = RESULTS_DIR + file_title + '_' + 'r' + str(r) + '.txt'
+        with open(log_file_path, 'w') as log_file:
+            cmd = 'lake lean ' + file_path
+            print(cmd)
+            subprocess.Popen(cmd, cwd=ROOT_DIR, stdout=log_file, stderr=log_file, shell=True).wait()
+    subprocess.Popen('sed -i -E \'s,simp_alive_split,try alive_auto,g\' ' + file_path, cwd=ROOT_DIR, shell=True).wait()
+    subprocess.Popen('sed -i -E \'s,bv_bench,all_goals sorry,g\' ' + file_path, cwd=ROOT_DIR, shell=True).wait()
+
+
+def process(jobs: int):
+    os.makedirs(RESULTS_DIR, exist_ok=True)
+    tactic_auto_path = f'{ROOT_DIR}/SSA/Projects/InstCombine/TacticAuto.lean'
+
+    with concurrent.futures.ThreadPoolExecutor(max_workers=jobs) as executor:
+        futures = {}
+        file = 'AliveStatements.lean'
+        future = executor.submit(run_file, file)
+        futures[future] = file
+        total = len(futures)
+        for idx, future in enumerate(concurrent.futures.as_completed(futures)):
+            file = futures[future]
+            future.result()
+            percentage = ((idx + 1) / total) * 100
+            print(f'{file} completed, {percentage}%')
+
+parser = argparse.ArgumentParser(prog='compare-leansat-vs-bitwuzla-alive')
+parser.add_argument('-j', '--jobs', type=int, default=1)
+args = parser.parse_args()
+clear_folder()
+process(args.jobs)