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

[Tobias Gysi]

================
@@ -0,0 +1,75 @@
+# 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/.
----------------
gysit wrote:

I would probably go for an item list here to make it a bit less dense:

e.g.:
```
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 func1 func2 func3`
```

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