xref: /llvm-project/mlir/utils/verify-canon/verify_canon.py (revision ca051dfe9f0996e7fdad8fde5817e5b6ce758ab9)
1*ca051dfeSIvan Butygin# Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
2*ca051dfeSIvan Butygin# See https://llvm.org/LICENSE.txt for license information.
3*ca051dfeSIvan Butygin# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
4*ca051dfeSIvan Butygin
5*ca051dfeSIvan Butygin# This script is a helper to verify canonicalization patterns using Alive2
6*ca051dfeSIvan Butygin# https://alive2.llvm.org/ce/.
7*ca051dfeSIvan Butygin# It performs the following steps:
8*ca051dfeSIvan Butygin# - Filters out the provided test functions.
9*ca051dfeSIvan Butygin# - Runs the canonicalization pass on the remaining functions.
10*ca051dfeSIvan Butygin# - Lowers both the original and the canonicalized functions to LLVM IR.
11*ca051dfeSIvan Butygin# - Prints the canonicalized and the original functions side-by-side in a format
12*ca051dfeSIvan Butygin#   that can be copied into Alive2 for verification.
13*ca051dfeSIvan Butygin# Example: `python verify_canon.py canonicalize.mlir -f func1 func2 func3`
14*ca051dfeSIvan Butygin
15*ca051dfeSIvan Butyginimport subprocess
16*ca051dfeSIvan Butyginimport tempfile
17*ca051dfeSIvan Butyginimport sys
18*ca051dfeSIvan Butyginfrom pathlib import Path
19*ca051dfeSIvan Butyginfrom argparse import ArgumentParser
20*ca051dfeSIvan Butygin
21*ca051dfeSIvan Butygin
22*ca051dfeSIvan Butygindef filter_funcs(ir, funcs):
23*ca051dfeSIvan Butygin    if not funcs:
24*ca051dfeSIvan Butygin        return ir
25*ca051dfeSIvan Butygin
26*ca051dfeSIvan Butygin    funcs_str = ",".join(funcs)
27*ca051dfeSIvan Butygin    return subprocess.check_output(
28*ca051dfeSIvan Butygin        ["mlir-opt", f"--symbol-privatize=exclude={funcs_str}", "--symbol-dce"],
29*ca051dfeSIvan Butygin        input=ir,
30*ca051dfeSIvan Butygin    )
31*ca051dfeSIvan Butygin
32*ca051dfeSIvan Butygin
33*ca051dfeSIvan Butygindef add_func_prefix(src, prefix):
34*ca051dfeSIvan Butygin    return src.replace("@", "@" + prefix)
35*ca051dfeSIvan Butygin
36*ca051dfeSIvan Butygin
37*ca051dfeSIvan Butygindef merge_ir(chunks):
38*ca051dfeSIvan Butygin    files = []
39*ca051dfeSIvan Butygin    for chunk in chunks:
40*ca051dfeSIvan Butygin        tmp = tempfile.NamedTemporaryFile(suffix=".ll")
41*ca051dfeSIvan Butygin        tmp.write(chunk)
42*ca051dfeSIvan Butygin        tmp.flush()
43*ca051dfeSIvan Butygin        files.append(tmp)
44*ca051dfeSIvan Butygin
45*ca051dfeSIvan Butygin    return subprocess.check_output(["llvm-link", "-S"] + [f.name for f in files])
46*ca051dfeSIvan Butygin
47*ca051dfeSIvan Butygin
48*ca051dfeSIvan Butyginif __name__ == "__main__":
49*ca051dfeSIvan Butygin    parser = ArgumentParser()
50*ca051dfeSIvan Butygin    parser.add_argument("file")
51*ca051dfeSIvan Butygin    parser.add_argument("-f", "--func-names", nargs="+", default=[])
52*ca051dfeSIvan Butygin    args = parser.parse_args()
53*ca051dfeSIvan Butygin
54*ca051dfeSIvan Butygin    file = args.file
55*ca051dfeSIvan Butygin    funcs = args.func_names
56*ca051dfeSIvan Butygin
57*ca051dfeSIvan Butygin    orig_ir = Path(file).read_bytes()
58*ca051dfeSIvan Butygin    orig_ir = filter_funcs(orig_ir, funcs)
59*ca051dfeSIvan Butygin
60*ca051dfeSIvan Butygin    to_llvm_args = ["--convert-to-llvm"]
61*ca051dfeSIvan Butygin    orig_args = ["mlir-opt"] + to_llvm_args
62*ca051dfeSIvan Butygin    canon_args = ["mlir-opt", "-canonicalize"] + to_llvm_args
63*ca051dfeSIvan Butygin    translate_args = ["mlir-translate", "-mlir-to-llvmir"]
64*ca051dfeSIvan Butygin
65*ca051dfeSIvan Butygin    orig = subprocess.check_output(orig_args, input=orig_ir)
66*ca051dfeSIvan Butygin    canonicalized = subprocess.check_output(canon_args, input=orig_ir)
67*ca051dfeSIvan Butygin
68*ca051dfeSIvan Butygin    orig = subprocess.check_output(translate_args, input=orig)
69*ca051dfeSIvan Butygin    canonicalized = subprocess.check_output(translate_args, input=canonicalized)
70*ca051dfeSIvan Butygin
71*ca051dfeSIvan Butygin    enc = "utf-8"
72*ca051dfeSIvan Butygin    orig = bytes(add_func_prefix(orig.decode(enc), "src_"), enc)
73*ca051dfeSIvan Butygin    canonicalized = bytes(add_func_prefix(canonicalized.decode(enc), "tgt_"), enc)
74*ca051dfeSIvan Butygin
75*ca051dfeSIvan Butygin    res = merge_ir([orig, canonicalized])
76*ca051dfeSIvan Butygin
77*ca051dfeSIvan Butygin    print(res.decode(enc))
78