[Mlir-commits] [mlir] [mlir][utils] Add script to verify canonicalizations against Alive2 (PR #91867)
Ivan Butygin
llvmlistbot at llvm.org
Mon May 13 06:49:51 PDT 2024
https://github.com/Hardcode84 updated https://github.com/llvm/llvm-project/pull/91867
>From 2124fa47ad8308dbc0070a88c25ff37d45bec6a2 Mon Sep 17 00:00:00 2001
From: Ivan Butygin <ivan.butygin at gmail.com>
Date: Sat, 11 May 2024 22:24:37 +0200
Subject: [PATCH 1/5] [mlir][utils] Add script to verify canonicalizations
agains Alive2
This script takes IR before and after canonicalization, translates it into llvm IR and converts to format suitablle for Alive2 https://alive2.llvm.org/ce/
This is primarily for arith canonicalizations verification, but technically it can be adapted for any dialect translatable to llvm.
Usage `python verify_canon.py canonicalize.mlir func1 func2 ...`
Example output: https://alive2.llvm.org/ce/z/KhQs4J
Initial discussion: https://github.com/llvm/llvm-project/pull/91646#pullrequestreview-2049342826
---
mlir/utils/verify-canon/verify_canon.py | 74 +++++++++++++++++++++++++
1 file changed, 74 insertions(+)
create mode 100644 mlir/utils/verify-canon/verify_canon.py
diff --git a/mlir/utils/verify-canon/verify_canon.py b/mlir/utils/verify-canon/verify_canon.py
new file mode 100644
index 0000000000000..1dae30757f220
--- /dev/null
+++ b/mlir/utils/verify-canon/verify_canon.py
@@ -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)
+
+ file = argv[1]
+ funcs = argv[2:]
+
+ orig_ir = Path(file).read_bytes()
+ orig_ir = filter_funcs(orig_ir, funcs)
+
+ to_llvm_args = [
+ "--convert-arith-to-llvm",
+ "--convert-func-to-llvm",
+ "--convert-ub-to-llvm",
+ "--convert-vector-to-llvm",
+ ]
+ orig_args = ["mlir-opt"] + to_llvm_args
+ canon_args = ["mlir-opt", "-canonicalize"] + to_llvm_args
+ translate_args = ["mlir-translate", "-mlir-to-llvmir"]
+
+ orig = subprocess.check_output(orig_args, input=orig_ir)
+ canonicalized = subprocess.check_output(canon_args, input=orig_ir)
+
+ orig = subprocess.check_output(translate_args, input=orig)
+ canonicalized = subprocess.check_output(translate_args, input=canonicalized)
+
+ enc = "utf-8"
+ orig = bytes(add_func_prefix(orig.decode(enc), "src_"), enc)
+ canonicalized = bytes(add_func_prefix(canonicalized.decode(enc), "tgt_"), enc)
+
+ res = merge_ir([orig, canonicalized])
+
+ print(res.decode(enc))
>From 719336566ddbfa1cb85dc55adbbf06e37302b25e Mon Sep 17 00:00:00 2001
From: Ivan Butygin <ivan.butygin at gmail.com>
Date: Sun, 12 May 2024 22:08:31 +0200
Subject: [PATCH 2/5] add example
---
mlir/utils/verify-canon/verify_canon.py | 1 +
1 file changed, 1 insertion(+)
diff --git a/mlir/utils/verify-canon/verify_canon.py b/mlir/utils/verify-canon/verify_canon.py
index 1dae30757f220..4198d996a8928 100644
--- a/mlir/utils/verify-canon/verify_canon.py
+++ b/mlir/utils/verify-canon/verify_canon.py
@@ -4,6 +4,7 @@
# Run canonicalization, convert IR to LLVM and convert to format suitable to
# verification against Alive2 https://alive2.llvm.org/ce/.
+# Example: `python verify_canon.py canonicalize.mlir func1 func2 func3`
import subprocess
import tempfile
>From 5085fcecca5c7253c9a8aad3474243d723958bd8 Mon Sep 17 00:00:00 2001
From: Ivan Butygin <ivan.butygin at gmail.com>
Date: Mon, 13 May 2024 13:22:19 +0200
Subject: [PATCH 3/5] --convert-to-llvm
---
mlir/utils/verify-canon/verify_canon.py | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/mlir/utils/verify-canon/verify_canon.py b/mlir/utils/verify-canon/verify_canon.py
index 4198d996a8928..eec029afe31ad 100644
--- a/mlir/utils/verify-canon/verify_canon.py
+++ b/mlir/utils/verify-canon/verify_canon.py
@@ -50,12 +50,7 @@ def merge_ir(chunks):
orig_ir = Path(file).read_bytes()
orig_ir = filter_funcs(orig_ir, funcs)
- to_llvm_args = [
- "--convert-arith-to-llvm",
- "--convert-func-to-llvm",
- "--convert-ub-to-llvm",
- "--convert-vector-to-llvm",
- ]
+ to_llvm_args = ["--convert-to-llvm"]
orig_args = ["mlir-opt"] + to_llvm_args
canon_args = ["mlir-opt", "-canonicalize"] + to_llvm_args
translate_args = ["mlir-translate", "-mlir-to-llvmir"]
>From cb4fd0bdd38ad3c9f79f3828237ca02168f88d2e Mon Sep 17 00:00:00 2001
From: Ivan Butygin <ivan.butygin at gmail.com>
Date: Mon, 13 May 2024 13:38:34 +0200
Subject: [PATCH 4/5] use argparse, update comment
---
mlir/utils/verify-canon/verify_canon.py | 25 ++++++++++++++++---------
1 file changed, 16 insertions(+), 9 deletions(-)
diff --git a/mlir/utils/verify-canon/verify_canon.py b/mlir/utils/verify-canon/verify_canon.py
index eec029afe31ad..ebf5a911c2e19 100644
--- a/mlir/utils/verify-canon/verify_canon.py
+++ b/mlir/utils/verify-canon/verify_canon.py
@@ -2,14 +2,21 @@
# 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/.
-# Example: `python verify_canon.py canonicalize.mlir func1 func2 func3`
+# This script is a helper to verify canonicalization patterns using Alive2
+# https://alive2.llvm.org/ce/.
+# It performs the following steps:
+# - Filters out the provided test functions.
+# - Runs the canonicalization pass on the remaining functions.
+# - Lowers both the original and the canonicalized functions to LLVM IR.
+# - Prints the canonicalized and the original function side-by-side in a format
+# that can be copied into Alive2 for verification.
+# Example: `python verify_canon.py canonicalize.mlir -f func1 func2 func3`
import subprocess
import tempfile
import sys
from pathlib import Path
+from argparse import ArgumentParser
def filter_funcs(ir, funcs):
@@ -39,13 +46,13 @@ def merge_ir(chunks):
if __name__ == "__main__":
- argv = sys.argv
- if len(argv) < 2:
- print(f"usage: {argv[0]} canonicalize.mlir [func1] [func2] ...")
- exit(0)
+ parser = ArgumentParser()
+ parser.add_argument("file")
+ parser.add_argument("-f", "--func-names", nargs="+", default=[])
+ args = parser.parse_args()
- file = argv[1]
- funcs = argv[2:]
+ file = args.file
+ funcs = args.func_names
orig_ir = Path(file).read_bytes()
orig_ir = filter_funcs(orig_ir, funcs)
>From 37b0e33a5924daa2af3035532a4f5a5e59eae815 Mon Sep 17 00:00:00 2001
From: Ivan Butygin <ivan.butygin at gmail.com>
Date: Mon, 13 May 2024 15:49:34 +0200
Subject: [PATCH 5/5] fix comment
---
mlir/utils/verify-canon/verify_canon.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/mlir/utils/verify-canon/verify_canon.py b/mlir/utils/verify-canon/verify_canon.py
index ebf5a911c2e19..bfddba9577b9a 100644
--- a/mlir/utils/verify-canon/verify_canon.py
+++ b/mlir/utils/verify-canon/verify_canon.py
@@ -8,7 +8,7 @@
# - Filters out the provided test functions.
# - Runs the canonicalization pass on the remaining functions.
# - Lowers both the original and the canonicalized functions to LLVM IR.
-# - Prints the canonicalized and the original function side-by-side in a format
+# - Prints the canonicalized and the original functions side-by-side in a format
# that can be copied into Alive2 for verification.
# Example: `python verify_canon.py canonicalize.mlir -f func1 func2 func3`
More information about the Mlir-commits
mailing list