Abstract:

This paper introduces egglog, a fixpoint reasoning system that unifies the capabilities of Datalog and equality saturation (EqSat). The system is motivated by the complementary weaknesses of the two paradigms: Datalog struggles with efficient equational reasoning, while EqSat lacks support for rich, compositional analyses. egglog addresses this by providing a Datalog-like language that incorporates a built-in, extensible notion of equality and uninterpreted functions. A key technical innovation is the use of merge expressions, a novel mechanism for resolving functional dependency violations that arise when terms are unified, enabling both congruence closure (like EqSat) and lattice-based reasoning (like advanced Datalog systems).

The authors evaluate egglog by reimplementing two real-world applications: a unification-based pointer analysis originally in Datalog and a floating-point optimizer (Herbie) based on EqSat. The results demonstrate that the egglog versions are significantly faster (e.g., a 4.96x speedup for the pointer analysis), are simpler to implement, and fix soundness bugs present in the original systems by enabling the sound application of conditional rewrite rules.

Better Together: A Unified System for Analysis and Optimization

• Page 125:1 - Central Problem: Standalone systems for program analysis (Datalog) and optimization (Equality Saturation, or EqSat) have limitations. Datalog is slow and complex for equational reasoning, while EqSat struggles to incorporate the rich semantic analyses needed to make rewrite rules sound.
• Page 125:2 - The egglog Solution: egglog is a new fixpoint reasoning system that unifies Datalog and EqSat. It combines Datalog's strengths—such as incremental execution and composable analyses—with EqSat's efficient term rewriting and congruence closure.
• Page 125:2 - Key Technical Innovation: The system introduces "merge expressions" for functions. When two terms are unified (made equal), and this creates a conflict where a function is mapped to two different outputs, the merge expression provides a user-defined way to resolve it (e.g., by unifying the outputs or taking their supremum in a lattice).
• Page 125:5 - Combining Unification and Logic: egglog allows users to declare uninterpreted sorts (types) and union values of these sorts. This operation, backed by a union-find data structure, makes two values indistinguishable to the system, forming the basis for all equational reasoning.
• Page 125:8 - Equality Saturation as Datalog Rules: Term rewriting in egglog is expressed as simple rules. A rewrite from one term to another is syntactic sugar for a rule that finds the first term and unions it with the second, effectively adding it to the same equivalence class.
• Page 125:12 - Optimized Implementation: egglog is implemented in Rust and leverages database optimizations. It uses a relational query engine with semi-naïve evaluation, an incremental technique from Datalog that avoids re-deriving old facts, leading to significant performance gains.
• Page 125:15 - Case Study 1: Points-to Analysis: A unification-based C/C++ points-to analysis (cclyzer++) was reimplemented in egglog.
  • Key Takeaway: The egglog version is 4.96x faster than the fastest sound Soufflé (Datalog) implementation and significantly simpler. It avoids inefficient "join modulo equivalence" operations and complex, bug-prone encodings that were necessary in the original Datalog version.
• Page 125:17 - Case Study 2: Sound Floating-Point Optimization (Herbie): The core of the Herbie tool, which uses EqSat to improve floating-point accuracy, was reimplemented in egglog.
  • Key Takeaway: egglog's support for rich, interacting analyses (e.g., interval analysis) allows Herbie to apply its rewrite rules soundly for the first time, for instance by proving that a denominator is non-zero before applying a division rule. The new version is faster overall and often finds more accurate results.