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