[Mlir-commits] [mlir] [mlir][utils] Add script to verify canonicalizations against Alive2 (PR #91867)

[Ivan Butygin]

================
@@ -0,0 +1,74 @@
+# Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+# See https://llvm.org/LICENSE.txt for license information.
+# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+# Run canonicalization, convert IR to LLVM and convert to format suitable to
+# verification against Alive2 https://alive2.llvm.org/ce/.
+
+import subprocess
+import tempfile
+import sys
+from pathlib import Path
+
+
+def filter_funcs(ir, funcs):
+    if not funcs:
+        return ir
+
+    funcs_str = ",".join(funcs)
+    return subprocess.check_output(
+        ["mlir-opt", f"--symbol-privatize=exclude={funcs_str}", "--symbol-dce"],
+        input=ir,
+    )
+
+
+def add_func_prefix(src, prefix):
+    return src.replace("@", "@" + prefix)
+
+
+def merge_ir(chunks):
+    files = []
+    for chunk in chunks:
+        tmp = tempfile.NamedTemporaryFile(suffix=".ll")
+        tmp.write(chunk)
+        tmp.flush()
+        files.append(tmp)
+
+    return subprocess.check_output(["llvm-link", "-S"] + [f.name for f in files])
+
+
+if __name__ == "__main__":
+    argv = sys.argv
+    if len(argv) < 2:
+        print(f"usage: {argv[0]} canonicalize.mlir [func1] [func2] ...")
+        exit(0)
----------------
Hardcode84 wrote:

done

https://github.com/llvm/llvm-project/pull/91867