Recent algorithmic advances have made equality saturation an appealing approach to program optimization because it avoids the phase-ordering problem. Existing work uses external equality saturation libraries, or custom implementations that are deeply tied to the specific application. However, these works only apply equality saturation at a single level of abstraction, or discard the discovered equalities when code is transformed by other compiler passes. We propose an alternative approach that represents an e-graph natively in the compiler's intermediate representation, facilitating the application of constructive compiler passes that maintain the e-graph state throughout the compilation flow. We build on a Python-based MLIR framework, xDSL, and introduce a new MLIR dialect, eqsat, that represents e-graphs in MLIR code. We show that this representation expands the scope of equality saturation in the compiler, allowing us to interleave pattern rewriting with other compiler transformations. The eqsat dialect provides a unified abstraction for compilers to utilize equality saturation across various levels of intermediate representations concurrently within the same MLIR flow.

翻译：近期算法进展使等式饱和成为极具吸引力的程序优化方法，因其避免了阶段排序问题。现有研究采用外部等式饱和库，或与特定应用深度绑定的定制实现。然而，这些工作仅在单一抽象层级应用等式饱和，或在代码被其他编译器过程转换时丢弃已发现的等式。我们提出一种创新方法，将e-graph原生表示于编译器的中间表示中，从而支持在完整编译流程中保持e-graph状态的构造性编译器过程。基于Python版MLIR框架xDSL，我们引入了新型MLIR方言eqsat，用于在MLIR代码中表征e-graph。研究表明，该表征方式拓展了等式中和在编译器中的应用范围，实现了模式重写与其他编译器转换的交错执行。eqsat方言为编译器提供了统一抽象，使其能够在同一MLIR流程中跨多级中间表示并发运用等式饱和技术。