Equality saturation is a technique for program optimization based on non-destructive rewriting and a form of program analysis called e-class analysis. The current form of e-class analysis is pessimistic and therefore ineffective at analyzing cyclic programs, such as those in SSA form. We propose an abstract interpretation algorithm that can precisely analyze cycles during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We instantiate this approach on a prototype abstract interpreter for SSA programs using a new semantics of SSA. Our prototype can analyze simple example programs more precisely than clang and gcc.

翻译：等式饱和是一种基于非破坏性重写和称为等价类分析的程序分析技术的程序优化方法。当前形式的等价类分析采用悲观策略，因此在分析循环程序（如SSA形式程序）时效率低下。我们提出了一种抽象解释算法，能够在等式饱和过程中精确分析循环结构。这形成了一种统一算法，可同时实现乐观分析和非破坏性重写。我们基于SSA新语义，在SSA程序的原型抽象解释器上实例化了该方法。实验表明，我们的原型系统在分析简单示例程序时比clang和gcc编译器具有更高的精确度。