Equality saturation is a technique for program optimization based on non-destructive rewriting and a form of abstract interpretation called e-class analysis. Existing e-class analyses are pessimistic and therefore ineffective at 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. To demonstrate the practicality of our approach, we implement a prototype abstract interpreter and equality saturation tool for SSA programs using a new semantics of SSA. 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语义，为SSA程序实现了一个原型抽象解释器和平等饱和工具。在示例程序上，我们的工具相比纯抽象解释（不含重写）和悲观e-class分析，在精度上有所提升。此外，其性能与现有的抽象解释和e-class分析技术相当。