Optimism in Equality Saturation
This work addresses a specific issue in program optimization for compilers or formal methods, offering an incremental improvement over pessimistic e-class analysis.
The paper tackled the problem of analyzing cyclic programs like those in SSA form using equality saturation, by proposing an optimistic abstract interpretation algorithm that avoids unsoundness and improves precision over existing methods, with comparable performance.
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.