HEC: Equivalence Verification Checking for Code Transformation via Equality Saturation

TL;DR

HEC is a novel framework that uses equality saturation and e-graphs to verify the correctness of source-to-source code transformations in compilers, detecting bugs and ensuring functional equivalence.

Contribution

This paper introduces HEC, a new e-graph based framework that verifies the correctness of code transformations in compiler optimization pipelines using MLIR integration.

Findings

Successfully verified loop unrolling, tiling, and fusion transformations on benchmarks.

Detected critical compiler errors related to loop boundary checks and memory violations.

Processed over 100,000 lines of code in 40 minutes with predictable scaling.

Abstract

In modern computing systems, compilation employs numerous optimization techniques to enhance code performance. Source-to-source code transformations, which include control flow and datapath transformations, have been widely used in High-Level Synthesis (HLS) and compiler optimization. While researchers actively investigate methods to improve performance with source-to-source code transformations, they often overlook the significance of verifying their correctness. Current tools cannot provide a holistic verification of these transformations. This paper introduces HEC, a framework for equivalence checking that leverages the e-graph data structure to comprehensively verify functional equivalence between programs. HEC utilizes the MLIR as its frontend and integrates MLIR into the e-graph framework. Through the combination of dynamic and static e-graph rewriting, HEC facilitates the validation of comprehensive code transformations. We demonstrate effectiveness of HEC on PolyBenchC benchmarks, successfully verifying loop unrolling, tiling, and fusion transformations. HEC processes over 100,000 lines of MLIR code in 40 minutes with predictable runtime scaling. Importantly, HEC identified two critical compilation errors in mlir-opt: loop boundary check errors causing unintended executions during unrolling, and memory read-after-write violations in loop fusion that alter program semantics. These findings demonstrate HEC practical value in detecting real-world compiler bugs and highlight the importance of formal verification in optimization pipelines.