refactor: Cleaned the InstCombine/scipts folder, added a config file …

…and a Readme, and re-ran the scripts. (#679)

Co-authored-by: Luisa Cicolini <[email protected]>

SSA/Projects/InstCombine/scripts/README.md

@@ -0,0 +1,12 @@
+These scripts are used to generate .lean files for bitblasting proofs.
+
+mlir-tool.py generates .lean files based on LLVM's test cases.
+
+types.py generates _proof.lean files from mlir-tool's output. These files contain theorems that should be solvable by bitblasting.
+
+To use:
+
+- Download and build llvm (with the mlir option) from [github](https://github.com/llvm/llvm-project)
+- Add llvm's built binaires to your path
+- Insert the path from lean-mlir to llvm-project in config.py
+- run run.sh from this directory

SSA/Projects/InstCombine/scripts/cfg.py

@@ -0,0 +1,6 @@
+llvm_path=""
+
+if len(llvm_path) == 0:
+    raise ValueError("You need to give the path to llvm in config.py")
+
+test_path="SSA/Projects/InstCombine/tests/LLVM"

SSA/Projects/InstCombine/scripts/mlir-tool.py

@@ -23,6 +23,7 @@
 from pathlib import Path
 from xdsl.printer import Printer
 from multiprocessing import Pool
+from cfg import *
 
 # Initialize the MLIR context and register the LLVM dialect
 ctx = MLContext(allow_unregistered=True)
@@ -106,25 +107,18 @@ def parse_module(module):
 def parse_from_file(file_name):
     return parse_module(read_file(file_name))
 
+rm_tests = "\nrm -r " + test_path + "/*\n"
 
-# subprocess.run("""
-# cd SSA/Projects/InstCombine/scripts &&
-# rm -rf ./llvm-project-main &&
-# curl -o llvm-project-main.zip https://codeload.github.com/llvm/llvm-project/zip/refs/heads/main &&
-# unzip llvm-project-main.zip
-# """, shell=True)
 
+llvm_test_path = llvm_path + "/llvm/test/Transforms/InstCombine"
 
-subprocess.run("""
-rm -f SSA/Projects/InstCombine/tests/LLVM/*
-""", shell=True)
+subprocess.run(rm_tests, shell=True)
 
 expensive_files = [
     "pr96012.ll"
 ]
-directory = os.fsencode(
-    "SSA/Projects/InstCombine/scripts/llvm-project-main/llvm/test/Transforms/InstCombine"
-)
+directory = os.fsencode(llvm_test_path)
+
 # for file in os.listdir(directory):
 def process_file(file):
     filename = os.fsdecode(file)
@@ -135,16 +129,16 @@ def process_file(file):
     stem = "g" + filename.split(".")[0].replace("-", "h")
     output = ""
 
-    # module1 = parse_from_file(os.path.join("../vcombined-mlir", filename))
-    full_name = f"SSA/Projects/InstCombine/scripts/llvm-project-main/llvm/test/Transforms/InstCombine/{filename}"
-    print(f"opt -passes=instcombine -S {full_name}  | mlir-translate -import-llvm | mlir-opt --mlir-print-op-generic")
+    full_name = f"{llvm_test_path}/{filename}"
+    run_process1 = f"opt -passes=instcombine -S {full_name}  | mlir-translate -import-llvm | mlir-opt --mlir-print-op-generic"
+    print(run_process1)
     process1 = subprocess.run(
-            f"opt -passes=instcombine -S {full_name} | mlir-translate -import-llvm | mlir-opt --mlir-print-op-generic",
+            run_process1,
             shell=True,
             capture_output=True,
             encoding="utf-8"
     )
-    # print(process1)
+
     module1 = parse_module(
        process1.stdout
     )
@@ -158,7 +152,7 @@ def process_file(file):
     )
     if module1 is None or module2 is None:
         return
-    # module2 = parse_from_file(os.path.join("../vbefore-mlir", filename))
+
     funcs = [
         func
         for func in module1.walk()
@@ -207,14 +201,7 @@ def {name}_after := [llvm|
   all_goals (try extract_goal ; sorry)
   ---END {name}\n\n\n"""
         print(o1)
-        write_file = os.path.join(
-            "SSA",
-            "Projects",
-            "InstCombine",
-            "tests",
-            "LLVM",
-            f"{stem}.lean",
-        )
+        write_file = f"{test_path}/{stem}.lean"
         with open(write_file, "a+") as f3:
             if os.stat(write_file).st_size == 0:
                 f3.write(
@@ -235,7 +222,6 @@ def {name}_after := [llvm|
                                                     """
                 )
             f3.write(o1)
-        # with open(write_file, "a+") as f3:
-        #     f3.write(f"end {stem}_statements")
+
 with Pool(7) as p:
     p.map(process_file, os.listdir(directory))

SSA/Projects/InstCombine/scripts/run.sh

@@ -0,0 +1,5 @@
+cd ../../../..
+
+python SSA/Projects/InstCombine/scripts/mlir-tool.py
+
+python SSA/Projects/InstCombine/scripts/types.py

SSA/Projects/InstCombine/scripts/types.py

@@ -3,7 +3,7 @@
 import os
 import subprocess
 from multiprocessing import Pool
-
+from cfg import *
 
 def get_lines(msg):
     # Define the regex pattern to match error messages with line numbers
@@ -72,7 +72,7 @@ def main():
     worklist = []
     for root, _, files in os.walk(directory):
         for lean_file in files:
-            if lean_file.endswith(".lean"):  # Assuming the files have a .lean extension
+            if lean_file.endswith(".lean") and not lean_file.endswith("_proof.lean"):  # Assuming the files have a .lean extension
                 file_path = os.path.join(root, lean_file)
                 print(file_path)
                 worklist.append(file_path)