
This script takes IR before and after canonicalization, translates it into llvm IR and converts it to format suitable 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 -f func1 func2 ...` Example output: https://alive2.llvm.org/ce/z/KhQs4J Initial discussion: https://github.com/llvm/llvm-project/pull/91646#pullrequestreview-2049342826
78 lines
2.4 KiB
Python
78 lines
2.4 KiB
Python
# 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
|
|
|
|
# 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 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`
|
|
|
|
import subprocess
|
|
import tempfile
|
|
import sys
|
|
from pathlib import Path
|
|
from argparse import ArgumentParser
|
|
|
|
|
|
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__":
|
|
parser = ArgumentParser()
|
|
parser.add_argument("file")
|
|
parser.add_argument("-f", "--func-names", nargs="+", default=[])
|
|
args = parser.parse_args()
|
|
|
|
file = args.file
|
|
funcs = args.func_names
|
|
|
|
orig_ir = Path(file).read_bytes()
|
|
orig_ir = filter_funcs(orig_ir, funcs)
|
|
|
|
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"]
|
|
|
|
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))
|