Optimism in Equality Saturation

TL;DR

This paper introduces an optimistic analysis approach for equality saturation that improves precision over traditional methods while maintaining comparable performance, addressing issues with cyclic program analysis.

Contribution

It proposes a novel abstract interpretation algorithm that enables optimistic analysis during equality saturation, enhancing precision without sacrificing efficiency.

Findings

The prototype tool shows improved analysis precision over existing methods.

Performance remains comparable to traditional abstract interpretation techniques.

The approach effectively handles cyclic SSA programs in equality saturation.

Abstract

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.