Equality saturation is a program optimization technique based on non-destructive rewriting and a form of abstract interpretation called e-class analysis. Existing e-class analyses are pessimistic and therefore typically imprecise when analyzing cyclic programs, such as those in SSA form. We show that a straightforward optimistic variant of e-class analysis can result in unsoundness, due to a subtlety in how e-graphs represent programs. We propose an abstract interpretation algorithm that circumvents this issue and can optimistically analyze e-graphs during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We implement a prototype abstract interpreter and equality saturation tool for SSA programs. Our tool exhibits precision improvements over pure abstract interpretation (without rewriting) and pessimistic e-class analysis on example programs. Additionally, its performance is comparable to existing abstract interpretation and e-class analysis techniques.

翻译：平等饱和是一种基于非破坏性重写和称为e-class分析的抽象解释形式的程序优化技术。现有的e-class分析是悲观的，因此在分析循环程序（如SSA形式的程序）时通常不够精确。我们表明，由于e-graph表示程序的一个微妙问题，对e-class分析进行直接的乐观变体会导致不健全性。我们提出了一种抽象解释算法，该算法规避了此问题，并能在平等饱和期间对e-graph进行乐观分析。这产生了一种统一算法，用于乐观分析和非破坏性重写。我们为SSA程序实现了一个原型抽象解释器和平等饱和工具。在示例程序上，我们的工具相较于纯抽象解释（无重写）和悲观e-class分析表现出精度提升。此外，其性能与现有的抽象解释和e-class分析技术相当。