# Contextual Equality Saturation

Alexandre Brewery, Thomas Jensen, David Pichardie

► To cite this version:

Alexandre Brewery, Thomas Jensen, David Pichardie. Contextual Equality Saturation. SAS 2025 - 32nd Static Analysis Symposium, Oct 2025, Singapore, Singapore. pp.1-26. hal-05226543

HAL Id: hal-05226543

https://inria.hal.science/hal-05226543v1

Submitted on 27 Aug 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Contextual Equality Saturation

Alexandre Brewery¹[0009-0008-6171-4492], Thomas
P. Jensen¹,³[0000-0002-4064-7170], and David Pichardie²[0000-0002-2504-1760]

¹ Inria, Université de Rennes

Corresponding: alexandre.drewery@inria.fr

² Meta

³ Dept. of Computer Science, University of Copenhagen

**Abstract.** Equality saturation is a semantics-based technique for automatically and efficiently proving that two programs are equivalent modulo a fixed set of equality axioms. In this paper, we extend the equality saturation technique with contextual reasoning in order to perform rewriting under assumptions that are locally valid inside a conditional branch. This is based on a new notion of cyclic e-graphs with contextual annotations. We experimentally validate the efficiency and scalability of this new technique by proving equivalence of several families of programs where contextual reasoning is required.

# 1 Introduction

Equality saturation [22] is a semantics-based technique for proving equivalence of programs based on efficient term rewriting. It has successfully been used to validate program optimisations [20]. In order to compare programs and prove that a given source program has been optimised into a target program, the technique first convert both programs into a term representation of their semantics called a PEG (Program Expression Graph) [22]. A PEG can be loaded in an *e-graphs*, a data structure originally developed for proving term equivalence in SMT solvers and recently crafted into a high-performance Rust library named *egg* [26]. Equality saturation then consists in applying a series of rewriting rules on *e-graphs* in order to prove that the two programs have equivalent semantics.

There is, however, a fundamental limitation to Equality Saturation: it does not perform *contextual reasoning*. To illustrate this limitation, consider proving equivalence between the two tests `i+1>n` and `i==n`. These two tests are in general not equivalent but they will be in certain contexts, e.g. if we also know that `(i<=n)==true` holds. For example, two terms `if (i<=n) then T[i+1>n] else U` and `if (i<=n) then T[i==n] else U` are equivalent, for any term `T[.]` which contain a contextual hole [*]. The inability of equality saturation to perform contextual reasoning prohibits certain program transformations. For example, a compiler might produce this loop construction

```cpp
var x = 1; if (1 <= n) {
    x = 2*x; for (int i = 1; i != n; i++) { x = 2*x; }
}
```
from the following for-loop

int x = 1; for (int i = 1; i <= n; i++) { x = 2*x; }

but, without context reasoning, equality saturation cannot prove that the resulting programs are equivalent.

The purpose of this paper is to extend the equality saturation approach with such contextual reasoning. Equality saturation is an otherwise efficient program equivalence technique. Its main strength is the ability to reduce intricate equality deductions as a local calculation on terms. Our goal is to keep this philosophy in our contextual extension via a system of incremental bookkeeping.

In this paper:

- we extend the notion of e-graph with a new mechanism of contextual annotation that can be efficiently queried to detect potential contextual reasoning;

- we also introduce a new notion of *contextual rewriting rule* to implement this contextual reasoning. We design the algorithmic framework needed to *e-match*<fnref n="4" /> and apply these rules;

- we provide an experimental evaluation of the efficiency of EQUIMATCH, a new OCaml library for contextual equality saturation that implements these algorithms.

## 2 Equality Saturation and e-graphs

Equality saturation aims to produce a set of equivalent terms given an initial term and some term rewriting rules that preserve equivalence. The general idea is to keep track of the set of all encountered terms and all equivalences between them. The rewriting rules are applied to sub-terms whenever possible, which enrich this set with new terms and new equivalences. To represent the equivalence classes of terms, equality saturation uses an efficient data structure called **equality graphs (e-graphs)** [8], a union-find data structure [21] enriched with a congruence closure [9] reasoning. Whenever a new equality between two terms $t_1$ and $t_2$ is discovered, the structure is also able to prove efficiently that $f(t_1)$ and $f(t_2)$ are equal, for any function symbol $f$. This data structure is the backbone of many SMT solvers [7].

Intuitively, an e-graph can be seen as a mix between term graphs and an union-find structure, representing both a sub-term relation and an equivalence relation. Whereas in a term graph a node represents a term, in an e-graph, an **e-node** represents a set of terms. E-nodes do not directly point towards other children e-nodes but rather towards **e-classes**, equivalence classes of e-nodes.

Figure 1 is an example of a small e-graph for the two arithmetic expression terms $(a \times 2)/2$ and $(2 \times a)/2$: e-classes are represented in dotted lines. The e-class $C_2$ contains two $\times$ e-nodes: it indicates that they represent sets of equivalent terms. The e-node in e-class $C_1$ represents all terms with function symbol $/$ and

<footnote n="4">⁴ Detecting an occurrence of a left hand side rewriting rule in an e-graph is called *e-matching* [6].</footnote>
sub-terms obtained by picking in the children e-classes. All instances of the term 2 as a sub-term are represented by the same e-class $C_4$ containing the 2 e-node: this **sharing** improves the memory performances of the structure.

<figure><img src="image_2.png" /><figcaption>Fig. 1: A simple e-graph.</figcaption></figure>

**Definition 1.** An **e-graph** is a defined by a set of e-nodes $\mathcal{N}$ and a set of e-classes $C$:

- each e-class $C \in \mathcal{C}$ is a subset of e-nodes and the set $C$ of all e-classes forms a disjoint set partition of all e-nodes $\mathcal{N}$;

- each e-node $n \in \mathcal{N}$ is characterized by a function symbol $f$ from the term language and some (potentially zero) ordered children e-classes $C_1, \dots, C_k \in \mathcal{C}$.

More formally, an e-class represents the set of terms represented by its e-nodes. An e-node of symbol $f$ and children e-classes $C_1, \dots, C_n$ represents all terms of root term symbol $f$ and direct subterms picked respectively from terms represented by $C_1, \dots, C_n$. We use $rep(C)$ and $rep(n)$ to denote these **sets of represented terms**:

$$ 
\begin{gathered}
rep(C) = \bigcup_{n \in C} rep(n) \\
rep(f(C_1, \dots, C_n)) = \{f(t_1, \dots, t_n) \mid t_1 \in rep(C_1), \dots, t_n \in rep(C_n)\}
\end{gathered}
$$

The e-graph data structure supports the following operations:

- **adding new e-node** to the e-graph in a fresh e-class and connecting its children to the proper e-classes (the process can be iterated to add a complete new term),

- **merging two e-classes** to incorporate new equalities (it can start a cascade of merging because of the congruence closure reasoning)

- and **e-matching a term pattern** in the e-graph. A **pattern** is a term $p$ built from term function symbols and variables from a set of pattern variables $\mathcal{X}$. E-matching such a pattern is used to identify a left hand-side of a rewriting rules before applying this rule to the e-graph.
An **occurrence** of a pattern *p* is a pair (*C*, *σ* ) of an e-class *C* and a substitu-
tion σ ∈ S such that e-node σ(*p*) is in *C*, which we denote *p* ∈<sub>σ</sub> *C*. **E-matching**
is the operation that looks for all occurrences of a pattern in an e-graph. For
instance, e-matching the pattern *X* × *Y* in Figure 1 will yield two occurrences
in *C*₂: one with substitution *X* → *C*₃, *Y* → *C*₄ and one with substitution
*X* → *C*₄, *Y* → *C*₃.

A **rewriting rule** takes the form of two patterns $p_1 \rightsquigarrow p_2$, with the restriction that all variables that appear in $p_2$ also appear in $p_1$. Intuitively such a rule states that for any substitution $\sigma$, the e-node $\sigma(p_1)$ is equivalent to the e-node $\sigma(p_2)$. For instance, the rule $X \times 2 \rightsquigarrow X+X$ makes the term $a \times 2$ and $a+a$ equivalent.

Equality saturation exploits these mechanisms by iteratively **applying** rewriting rules to the e-graph: e-match for occurrences of the rules, add the rewritten term and indicate equivalence by merging the two e-classes. The e-graph is saturated when no rule application can yield a new term: for instance, the e-graph of Figure 1 is saturated for rule $X \times Y \rightsquigarrow Y \times X$. Equality saturation terminates when the e-graph is saturated for the whole rule set or when a timeout condition is reached.

3 Program Equivalence Proof by Equality Saturation

Equality saturation has been used to perform program equivalence checking ef-
ficiently, as demonstrated by Tate *et al.* [22]. The technique is based on an
advanced intermediate representation of program, PEG, which is a variant of e-
graphs and which share similarities with advanced intermediate representations
used in the modern compilers (like Gated-SSA [12] or Sea-of-nodes [17]). It has
been successfully used to validate difficult translation validation challenges [20]
posed by advanced compiler optimizations techniques (dead code elimination,
global value numbering, partial redundancy elimination, sparse conditional con-
stant propagation, loop-invariant code motion, loop deletion, loop unswitching,
dead store elimination, loop-induction variables). Their approach is composed
of 3 distinct steps:

1. Building a term representation of programs

2. Identifying a fixed set of equivalence axioms

3. Run a custom saturation solver

Each program is converted into a term representation name PEG (Program Expression Graph) that is a pure functional representation of a program. If the two terms are equivalent according to a fixed set of equivalence axioms (rewriting rules) then the two initial program are observably equivalent. Such a term encoding is not trivial. Several specific reserved function symbols are introduced to reason on control flow (conditionals, loops) and also memory. Because we are mainly interested in contextual reasoning that is possible inside a if-then-else branch, we will focus on the $\Phi$ operator that they introduce for this specific construction. $\Phi$ is a ternary symbol that represents a conditional. The first child sub-term is the conditional, the second child is a term that represents
the *then*-branch and the third child represents the *else*-branch. For instance, the term $\Phi(eq(x, 0), 2, 5)$ represents the conditional that evaluates to 2 is $x$ is equal to 0 and 5 otherwise. This operator is similar to the $\Phi$ operator used in Gated-SSA [12].

Tate et al. provides rewriting rules for standard arithmetic expressions as well as rules that manipulate the various control flow operators, including the $\Phi$ operator. Figure 2 shows the rewriting rules that interact with $\Phi$. Rule [PHI-NEG] switches the branches of a conditional by negating its condition. Rules [PHI-TRUE] and [PHI-FALSE] simplify a conditional with trivial condition. Rule [PHI-SAME] removes a condition if both branches are equivalent. Rules [PHI-BOOL] and [PHI-BOOL-NEG] turn a condition into a simpler boolean expression when both branches are equivalent to boolean literals. Rules [PHI-DEAD-THEN] and [PHI-DEAD-ELSE] remove dead branches when two nested conditional test equivalent conditions. Rule [PHI-DEAD-DEEP] simplifies a nested conditional at depth 3 when an equivalent test is performed at depth 1. This last rule demonstrates the lack of contextual reasoning that motivates the current paper.

<figure><img src="image_3.png" /><figcaption>Fig. 2: Rewriting rules on $\Phi$-terms used in PEGGY [22].</figcaption></figure>

Tate et al. designed their own saturation solver, specialized for reasoning on equivalences classes of PEGs. The most notable difference with standard e-graph solvers used in SMT (like Z3) is the special treatment of cyclic expressions. Once the two initial terms have been loaded into the solver, the equality saturation process starts applying rules and merging classes. New merged classes may generate new rewriting opportunities. The iterative process can be stopped as soon as the two classes representing the returned value of each program are merged. If no more rules can be applied or a timeout is reached, the checking is inconclusive.

They showed that the custom saturation engine is capable of performing successful program reasoning using equality saturation, by doing translation validation of Soot optimizations on Java program, and translation validation of LLVM optimizations on LLVM programs. The set of rules must be chosen carefully,
though, taking into account the expected differences and similarities between
inputs. Adding too many rules may increase the number of rewriting steps and
hence the risk of timeout before merging the two classes representing the return
value of each compared programs

In general, equality saturation comes with potential weaknesses that must be
taken into account when engineering a tool with it. The search exploration must
be kept bounded because of a risk of memory overflow, or even non-termination
and well-chosen heuristics are necessary. Finally, there is a fundamental limi-
tation that we have illustrated with the previous set of rewriting rules on Φ-
patterns: equality saturation does not represent well the scope of a Φ-test and
misses opportunities to merge equivalent program fragments. The rest of the
paper presents a novel technique that remove this limitation.

4 Contextual Equality Saturation

We want our rewriting rules to be able to exploit information gained in the
conditionals. A basic example of such a rule is given in Figure 3: the Φ-node
checks if X and Y are different and this information can be used as a context in
the then-child to change a greater-or-equal check to a greater-than check.

<figure><img src="image_4.png" /><figcaption>Fig. 3: A conditional rewriting rule that exploits an inequality in a condition.</figcaption></figure>

However, as written, the rule of Figure 3 can only be used if e-node *gte(X, Y)* is in the immediate *then*-child e-class of the *Φ*-node. In practice this will rarely be the case in a term obtained from a real program: *gte(X, Y)* will often appear as a subcomputation in a bigger term, not right under the *Φ*-node. We are more often in the situation of Figure 4 where the instance of *gte(X, Y)* is further along the *then*-branch of the term. The dotted edge notation denotes the same term structure in both terms, except for the instance of *X* replaced by *Y*.
<figure><img src="image_5.png" /></figure>

[CONTEXTUAL-GTE-TO-GT]: neq(X, Y) ⊢ gte(X, Y) ⇝ gt(X, Y)

<caption>Fig. 4: Contextual version of the rule [GTE-TO-GT].</caption>

The main subtlety of the transition from the conditional rule of Figure 3 to the contextual rule of Figure 4 is that the two equivalent classes **are not those of gte(X, Y)** and **gt(X, Y)** but rather the classes of the $\Phi$-nodes (the checks are equivalent but only **under the condition that neq(X, Y) holds**). The rule must therefore encompass the $\Phi$-nodes. The pattern of the rule of Figure 4 cannot be explicitly specified using the standard pattern language since it must allow branches from $\Phi$ to gte(X, Y) that are of arbitrary length.

We introduce the new notation neq(X, Y) ⊢ gte(X, Y) ⇝ gt(X, Y) for the rule of Figure 4. This can be read as the rewriting of gte(X, Y) into gt(X, Y) where the context neq(X, Y) is known to be true. We call this new kind of rules that works on arbitrary $\Phi$-terms for **contextual rewriting rules**.

**Definition 2.** A contextual rewriting rule has the form

$$p_c \vdash p_1 \rightsquigarrow p_2$$

The pattern $p_c$ is called the **contextual requirement** of the rule and the $p_1 \rightsquigarrow p_2$ part is a standard rewriting rule. We call $p_1$ the **structural requirement** of the rule.

Intuitively, a contextual rule can be applied whenever we find an e-class C that matches the structural requirement $p_1$, in the **then-branch** of a $\Phi$-node $\Phi(C_c, C_t, C_e)$ such that $C_c$ matches the contextual requirement $p_c$. The fact that C is found in the **then-branch** denoted by $C_t$ is formally defined below.

**Definition 3.** A e-class $C_1$ is a **subclass** of an e-class $C_2$ (written $C_1 \preceq C_2$) if and only if there exists a term $t_1 \in \text{rep}(C_1)$ and a subterm $t_2 \in \text{rep}(C_2)$ such that $t_1$ is a subterm of $t_2$ (written $t_1 \preceq t_2$).

For example, on Figure 5, both $C_2 \preceq C_1$ and $C_x \preceq C_1$ hold.
<figure><img src="image_6.png" /><figcaption>Fig. 5: E-graph where the rule [CONTEXTUAL-GTE-TO-GT] can be used.</figcaption></figure>

**Definition 4.** *Given a contextual rule $p_c \vdash p_1 \rightsquigarrow p_2$, a contextual occurrence is a pair $(C, \sigma)$ of an e-class $C$ and a substitution $\sigma \in S$ such that:*

- the pair $(C, \sigma)$ is an occurrence of $p_1$ (written $p_1 \in_{\sigma} C$ in Section 2);

- there exists an e-node $\Phi(C_c, C_t, C_e)$ such that $p_c \in_{\sigma} C_c$ and $C \subseteq C_t$.

For instance, on Figure 5, there is a contextual occurrence in e-class $C_{\ge}$. This e-class represents the term $gte(x, y)$ and is in the *then*-branch of a conditional of condition $neq(x, y)$.

In the following subsections, we describe algorithms that use the notion of context to determine when a contextual rewriting rule can be applied and how the rule updates the e-graph. We first describe naive versions of the algorithms, before defining the efficient algorithms as optimized versions of the naive counterparts.

## 4.1 Naive Contextual Rewriting

The simplest way of looking for contextual occurrences of a contextual rule $p_c \vdash p_1 \rightsquigarrow p_2$ is to search for all $\Phi$-terms which condition matches $p_c$ and then explore the entire *then*-branch of these term in search for a match for $p_1$. We propose a pseudo-code for this process in Algorithm 1.

Once this algorithm finds occurrences for the contextual rule, they can be passed to the procedure of Algorithm 2 that will perform the rewriting.

The intuitive idea of this algorithm is, given an occurrence $(C, \sigma)$, to build a node $n'$ similar to $n = \Phi(C_c, C_t, C_e)$ (which is also passed as an argument), except that instances of e-class $C$ in e-nodes of the *then*-branch $C_t$ are replaced with a rewritten e-class. The e-classes of $n'$ and $n$ are then merged. The result of this procedure can be seen in Figure 6, in which the entire *then*-branch of the $\Phi$-node has been copied under a new $\Phi$-node, but with the e-class $C_{\ge}$ replaced by a new e-class for term $gt(x, y)$.
<caption>**Algorithm 1** Pseudo-code for a naive contextual e-matching procedure.</caption>

1: **function** CONTEMATCHINGNAIVE(contextual requirement $p_c$, structural requirement $p_1$)
2: &nbsp;&nbsp;&nbsp;&nbsp;**for** all e-nodes $\Phi(C_c, C_t, C_e)$ such that $\exists \sigma_c. p_c \in_{\sigma} C_c$ **do**
3: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;traverse downward the e-graph starting from $C_t$
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for** all met e-classes $C$ such that $C \preceq C_t$ and $\exists \sigma_1. p_1 \in_{\sigma_1 \circ \sigma_c} C$ **do**
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$(C, \sigma_1 \circ \sigma_c)$ is an occurrence
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**end for**
7: &nbsp;&nbsp;&nbsp;&nbsp;**end for**
8: **end function**

<caption>**Algorithm 2** Pseudo-code for a naive contextual rewriting procedure.</caption>

1: **function** CONTREWRITINGNAIVE(contextual rule $p_c \vdash p_1 \rightsquigarrow p_2$, occurrence $(C, \sigma)$, e-node $n = \Phi(C_c, C_t, C_e)$ in its e-class $C_n$)
2: &nbsp;&nbsp;&nbsp;&nbsp;add e-node $\sigma(p_2)$ to the e-graph
3: &nbsp;&nbsp;&nbsp;&nbsp;let $t_2$ be a term of $\text{rep}(\sigma(p_2))$
4: &nbsp;&nbsp;&nbsp;&nbsp;**for** all terms $\Phi(t_c, t_t, t_e) \in \text{rep}(n)$ **do**
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $t_t$ has a subterm $t_1 \preceq t_t$ in $\text{rep}(\sigma(p_1))$ **then**
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;add term $t'_t = t_t[t_1 \to t_2]$ to the e-graph in an e-class $C'_t$
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;add e-node $n' = \Phi(C_c, C'_t, C_e)$ to e-graph and merge its e-class with $C_n$
8: &nbsp;&nbsp;&nbsp;&nbsp;**end if**
9: &nbsp;&nbsp;&nbsp;&nbsp;**end for**
10: **end function**

<figure><img src="image_7.png" /><figcaption>Fig. 6: E-graph of Figure 5 after contextual rewriting with $[\text{CONTEXTUAL-GTE-To-GT}]$.</figcaption></figure>

In this naive approach, we explicitly enumerate (and build) the new terms $t_t[t_1 \to t_2]^5$, which is unrealistic but explains the objective of this section. Another problem is that the naive e-matching algorithm has a quadratic complexity

<footnote n="5">⁵ This notation means that all occurrences of $t_1$ in $t_t$ have been simultaneously replaced by $t_2$.</footnote>
over the size of the e-graph in the worst case: it performs a graph traversal under every $\Phi$-node which condition matches. In practice, this is too inefficient for the process of contextual rewriting that may be run frequently every time a new contextual pattern is found. In the following subsections, we design a more efficient framework for contextual rewriting.

## 4.2 Context Annotations

One way to improve the complexity of this process is to ** annotate** all subclasses in the *then*-branch $C_t$ of an e-node $\Phi(C_c, C_t, C_e)$ with the information that they are in the context of $C_c$ being true. This allows for a local check of which *then*-branches a term is in, rather than having to do an exploration every time.

The kind of annotations we want is shown on a basic e-graph in the square boxes in Figure 7. Annotations are attached to e-classes and an e-class can have multiple annotations. All annotations are pairs $(C_c, e)$ with $C_c$ an e-class of boolean terms (the **context**) and $e$ an edge of the e-graph (the **source information**). Such a pair intuitively means that further upward edge $e$, there is at least one $\Phi$-node with condition $C_c$. An annotation for an e-class $C$ can contain several pairs for the same context $C_c$ if different paths lead to $C$ from $\Phi$-nodes with condition $C_c$. For example, in Figure 7, the e-graph represents a program with two conditionals with the same condition in two *then*-branches arranged sequentially. These multiple instances of the *then*-branch are associated with different paths in the e-graph, hence there are two annotations for the e-class of the `+`-node.

<figure><img src="image_8.png" /><figcaption>Fig. 7: E-graph annotation with different sources.</figcaption></figure>

**Definition 5.** Let $C_c$ be an e-class (the **context**) and $e$ an edge (the **source information**) in an e-graph. The pair $(C_c, e)$ is an **annotation** for e-class $C_c$ if the e-graph represents a term $\Phi(t_c, t_t, t_e)$ such that:
- $t_c \in \text{rep}(C_c)$ (i.e. $C_c$ represents $t_c$);

- e is an edge from a node n to the class $C_k$ (i.e. n is of the form $f(C_1, \dots, C_k, \dots)$);

- for some $t_k \in \text{rep}(C)$, there exists a subterm $f(t_1, \dots, t_k, \dots) \in \text{rep}(n)$ of $t_t$.

Annotations allow to check locally the context of an e-class. The source information in annotations allow to find the parents $\Phi$-nodes that generates these contexts. In the following subsections, we present how more efficient contextual rewriting is done in a fully annotated e-graph. We delay the description of the incremental annotation process until Section 4.5.

## 4.3 Efficient Contextual E-matching

Assuming an e-graph that is properly annotated, it is possible to efficiently e-match for occurrences of a contextual rule $p_c \vdash p_1 \rightsquigarrow p_2$ by e-matching (with a regular e-matching procedure) for the structural requirement $p_1$ and then, for each occurrence $(C, \sigma)$, use the annotation associated with $C$ to get some e-class candidates that we can try to match with the contextual requirement $p_c$. For instance, in Figure 8a, when trying to activate the rule [CONTEXTUAL-GTE-To-GT], the naive approach would first e-match for $neq(X, Y)$ and then naively traverse the full *then*-branch of the $\Phi$-node, searching for pattern *gte(X, Y)*. Instead, we can now immediately identify that the only possible occurrence of our structural pattern is in $C_\ge$ and immediately after, check that $C_\ge$ indeed have $C_c$ as a context in its annotations.

Algorithm 3 describes this procedure. A strength of Algorithm 3 is that it can rely on a regular, optimized e-matching procedure to identify matches for the structural requirement.

<caption>**Algorithm 3** Contextual e-matching algorithm that exploits the annotations.</caption>

1: **function** CONTEMATCHING(contextual requirement $p_c$, structural requirement $p_1$)
2: &nbsp;&nbsp;&nbsp;&nbsp;e-match for occurrences of $p_1$
3: &nbsp;&nbsp;&nbsp;&nbsp;**for** all such occurrences $(C, \sigma_1)$ **do**
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $C$ has an annotation $(C_c, e)$ such that $\exists \sigma_c. p_c \in_{\sigma_c \circ \sigma_1} C_c$ **then**
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$(C, \sigma_c \circ \sigma_1)$ is an occurrence
6: &nbsp;&nbsp;&nbsp;&nbsp;**end if**
7: &nbsp;&nbsp;&nbsp;&nbsp;**end for**
8: **end function**

## 4.4 Contextual Rewriting

Contextual rewriting can also exploit the annotations. The intuition is the same as in Section 4.1 but the path that connects a source e-node $\Phi(C_c, C_t, C_e)$ to an occurrence $(C, \sigma)$ can be built starting from $C$ and moving upwards using the clues provided by the annotations e-class encountered.
This process is illustrated in Figure 8. Starting from the initial configuration of Figure 8a, the structural part of the rewriting is performed to get to Figure 8b with a new >-node. The path information of the annotation of $C_\ge$ indicates to copy the structure above $e_2$: a ^-node. We add a new ^-node above the e-class of the >-node in Figure 8c. The same process then copies a $\Phi$-node to get to Figure 8d. Since this $\Phi$-node has condition $C_c$, the process ends here and the two e-classes of $\Phi$-nodes are merged (Figure 8e).

<caption>**Algorithm 4** Contextual e-matching algorithm that exploits the annotations.</caption>

1: **function** CONTEMATCHING(contextual rule $p_c \vdash p_1 \rightsquigarrow p_2$, occurrence $(C, \sigma)$)
2: &nbsp;&nbsp;&nbsp;&nbsp;add e-node $\sigma(p_2)$ to the e-graph, let $C'$ be its e-class
3: &nbsp;&nbsp;&nbsp;&nbsp;let $C_c$ be the e-class of $\sigma(p_c)$
4: &nbsp;&nbsp;&nbsp;&nbsp;call procedure RebuildPath($C, C', C_c$)
5: &nbsp;&nbsp;&nbsp;&nbsp;**end function**
1: **function** REBUILDPATH($C, C', C_c$)
2: &nbsp;&nbsp;&nbsp;&nbsp;**for** all annotations $(C_c, e)$ of $C$ **do**
3: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let e-node $n = f(..., C, ...)$ be the source of $e$ and $C_n$ the e-class of $n$
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;add e-node $n' = f(..., C', ...)$ to the e-graph, let $C'_n$ be its e-class
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $n = \Phi(C_c, C, C_e)$ **then**
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;merge $C_n$ and $C'_n$
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else**
8: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;call RebuildPath($C_n, C'_n, C_c$)
9: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**end if**
10: &nbsp;&nbsp;&nbsp;&nbsp;**end for**
11: **end function**

Algorithm 4 describes the procedure for this contextual rewriting. It is split in two: CONTEMATCHING will perform the structural part of the rewriting (creating a new e-node $\sigma(p_2)$), while REBUILDPATH iteratively inserts copies above the new e-node $\sigma(p_2)$ of the paths that lead from $\Phi$-nodes to $\sigma(p_1)$.

A subtlety of this algorithm is what happens when several possible parents propagate context $C_c$ to e-class $C$. For instance, this happens in the e-class of the +-node in Figure 7. In that case the rewriting process splits into two distinct rewritings on the fly: all rewritings associated with all paths are performed.

The contextual rewriting process may need to travel upward along an arbitrary path in the e-graph, so it is more costly than a standard rewriting (linear in the length of this path). However, thanks to the path informations of annotations, it visits exactly the e-nodes it needs to in order to rebuild a path from the $\Phi$-node to the occurrence.

## 4.5 Incremental E-graph Annotation

We have explained how the contextual annotations can be used to perform contextual rewriting. We will now explain how to compute these annotations. Because e-graph are progressively built by alternating the e-graph operations *add*
<figure><img src="image_9.png" /><figcaption>Fig. 8: Step-by-step contextual rewriting.</figcaption></figure>
and *merge*, we redefine these operations to incrementally build an annotated e-graph.

The general intuition of the annotation process is a downward propagation of context annotations along the edges of the e-graph whenever a new context appears. Both annotation-update procedures take the form of maintenance functions that must be called immediately after a *add* or *merge* has been performed.

The procedure for adding a new e-node *n* is described in Algorithm 5. If *n* is not a *Φ*-node, it does not add any new context. Otherwise, if *n* is a *Φ*-node *Φ*(*C*<sub>*c*</sub>, *C*<sub>*t*</sub>, *C*<sub>*e*</sub>) then a new context *C*<sub>*c*</sub> is iteratively propagated to its *then*-child e-class *C*<sub>*t*</sub>.

<caption>**Algorithm 5** Updating annotations whenever an e-node is added.</caption>

1: **function** UPDATEONADD(added e-node *n*, its e-class *C*)
2:     **if** *n* has the form *Φ*(*C*<sub>*c*</sub>, *C*<sub>*t*</sub>, *C*<sub>*e*</sub>) **then**
3:         **let** *e* be the edge outgoing of *n* to *C*<sub>*t*</sub>
4:         **Propagate**(*C*<sub>*t*</sub>, {*C*<sub>*c*</sub>}, *e*)
5:     **end if**
6: **end function**

When merging two e-classes $C_1$ and $C_2$, the context annotations must also be
merged. This is done with Algorithm 6. The paths leading to $C_1$ now also lead
to $C_2$ and vice versa so contexts are now shared. Since all e-nodes of the new
merged e-class have potentially new possible contexts, the propagation process
must be invoked on their children as well.

<caption>**Algorithm 6** Updating annotations whenever e-classes are merged.</caption>

1: **function** UPDATEONMERGE(merged e-classes $C_1$ and $C_2$, resulting e-class $C$)
2:     **let** $A_1$ and $A_2$ be the sets of annotations of $C_1$ and $C_2$
3:     ** annotate** $C$ with $A_1 \cup A_2$
4:     **let** the set of contexts $\mathcal{C}$ be $\{C_c|(C_c, e) \in A_1 \cup A_2\}$
5:     **for** all e-nodes $n \in C$ **do**
6:         **for** all outgoing edges $e'$ (pointing towards $C'$) of $n$ **do**
7:             **Propagate**($C', C, e'$)
8:         **end for**
9:     **end for**
10: **end function**

The propagation procedure is an e-graph traversal described in Algorithm 7. This traversal uses the incoming edges in order to annotate e-classes with the correct path information. This propagation plays a role similar to the e-graph traversal in the naive e-matching algorithm of Section 4.1, but it is called only once when needed, it is only performed on e-classes of the e-graph whose anno-
tations must be updated, and the process only uses information **local** to these e-classes.

<caption>**Algorithm 7** Propagation of annotations.</caption>

1: **function** PROPAGATE(e-class C, set of contexts C, incoming edge e)
2:   let A be the annotations of C
3:   **if** {⟨C_c, e⟩|C_c ∈ C} ⊆ A **then**
4:     do nothing
5:     **else**
6:       A ← {⟨C_c, e⟩|C_c ∈ C} ∪ A
7:       **for** all e-nodes n ∈ C **do**
8:         **for** all outgoing edges e' (pointing towards C') of n **do**
9:           Propagate(C', C, e')
10:         **end for**
11:     **end for**
12:   **end if**
13: **end function**

The PROPAGATE procedure holds most of the maintenance cost of the annotation framework. In the worst case, PROPAGATE is linear in the number of edges of the e-graph. This implementation is however minimal in the sense that it only visits the edges that propagate new contextual annotations. Some additional work could further improve the performance of contextual rewriting such as delaying the annotation maintenance, similar to the performance-improving approach of *egg* of delaying invariants maintenance in the e-graph [26].

The program term representation we use involves cyclic terms to represent loops. Although all definitions hold on cyclic terms, using a contextual rewriting rule on such a term may lead to rewrites inside the loop bodies that makes no sense regarding the initial program. We choose not to propagate context through loops operators to prevent this behaviour.

# 5 Evaluation

We aim to evaluate the scalability of the contextual equality saturation framework we propose, as the size of the e-graphs increases. To this end, we have generated three collections of pairs of equivalent programs. Proving their equivalence is based on the use of the contextual rule of Section 4:

$$[\text{CONTEXTUAL-GTE-To-GT}]: neq(X, Y) \vdash gte(X, Y) \rightsquigarrow gt(X, Y)$$

We task the equality saturation engine described in this paper, EQUIMATCH, with solving these problems. We compare its performances with three other rewriting strategies described in Section 5.1.
## 5.1 Experimental settings

**Naive swap-based non-contextual engine:** the first setting represents how state-of-the-art equality-saturation tools would simulate contextual rewriting at the cost of introducing extra *swapping* rules. In this setting we force EQUIMATCH to only perform regular non-contextual rewrites, but we feed the solver with the rule:

$$ [\text{GTE-To-GT}]: \vdash \Phi(\text{neq}(X, Y), \text{gte}(X, Y), Z) \rightsquigarrow \Phi(\text{neq}(X, Y), \text{gt}(X, Y), Z) $$

This rule encodes the same reasoning as the contextual one, but only for contextual requirement at distance 1 of the structural requirement. We complement this rule with swapping rules between $\Phi$-nodes and other types of nodes that appear in the problems, e.g. f-nodes:

$$ \vdash \Phi(X_c, f(X_t^1, X_t^2), f(X_e^1, X_e^2)) \rightsquigarrow f(\Phi(X_c, X_t^1, X_e^1), \Phi(X_c, X_t^2, X_e^2)) $$

These rules (one for each operator $f$) help recover the lack of specific contextual reasoning by pushing down the context-bearing $\Phi$-term or pushing up the structural point of application closer to each other. However, depending on the operator $f$, they can usually only be used in limited situations since $f$ has to appear on both sides of the $\Phi$ operator.

**Naive traversal-based contextual engine:** the second setting implements contextual equality saturation but using naive algorithmic approach. In this setting, we force EQUIMATCH to perform the expensive graph traversal presented in Algorithm 1 and 2 in Section 4.1, and we do not use the efficient incremental context annotation algorithms presented in Section 4.2, 4.3, 4.4 and 4.5.

**EquiMatch annotation-based contextual engine:** the third setting implements full contextual equality saturation based on the contextual annotation bookkeeping system of the current paper.

**Unsound rewriting setting:** the last setting is a non-contextual rewriting strategy that quickly solves the problems using the (unsound) rule:

$$ \vdash \text{gte}(X, Y) \rightsquigarrow \text{gt}(X, Y) $$

We introduce this setting to have a kind of baseline with respect to the e-matching phase. However this approach does not provide a strict baseline since it does not produce the exact same terms as the three sound previous settings. As an example, the two terms $\Phi(\text{neq}(X, Y), f_1(f_2(f_3(\text{gte}(X, Y)))), Z)$ and $\Phi(\text{neq}(X, Y), f_1(f_2(f_3(\text{gt}(X, Y)))), Z)$ will be merged by all four strategies but the unsound setting will also merge each pair of subterms $f_i(\dots(\text{gte}(X, Y)))$ and $f_i(\dots(\text{gt}(X, Y)))$ in specific classes.

Still this setting can be used as an estimate for the time EQUIMATCH takes to load the two PEG and to perform an ideal e-matching procedure.

## 5.2 Source-pattern distance benchmark

The first benchmark consists of pairs of programs that measure each method performance when the distance $N$ between a context source and a structural
pattern increases. All pairs have the following structure and vary only in the
number *N*:

```
if (x != y) {
    if (x >= y) {
        z = z + 1;
    }
    <N buffer instructions>
};
return z;
```

For a given number *N*, the only difference between the left and right programs is the condition of the inner conditional. Notice that, due to the way that the PEG is built, the buffer of size *N* that is added **after** the inner conditional will increase the distance between *Φ*-terms of the inner and the outer conditionals in the PEG associated with these programs as shown in Figure 16 in the Appendix B.

<figure><img src="image_10.png" /><figcaption>Fig. 10: Results for the Source-pattern distance benchmarks</figcaption></figure>

**Experimental results:** Figure 10 shows the time elapsed for equivalence proving with each experimental setting, for values of *N* up to 500.

This benchmark is very favorable to the naive traversal-based approach, which outperforms even the unsound rewriting. Indeed, contextual e-matching is called exactly once, performs a singular traversal of the (linear) *then*-branch of the left program. This traversal is light in memory-write accesses, and will
result in the merging of the outer $\Phi$-terms. In comparison, the unsound proof requires $N$ recursive e-class merging from the bottom of the e-graph.

Still the annotation-based approach behaves as well as the unsound rewriting. The difference in performance with the naive traversal-based approach is explained by the amount of memory-write accesses needed to setup the annotations. Note that this benchmark does not play to the strengths of the annotation framework as every problem is solved in one single contextual rewriting rule application.

Both contextual approaches perform better than the swap-based approach, validating the relevance of contextual reasoning.

## 5.3 Number of sources benchmark

**Experimental setup:** we evaluate how contextual equality saturation performs on programs with multiple contextual sources. This benchmark tests the path information part of the annotation framework: multiple paths from multiple sources lead to the structural pattern. We study a new family of pairs of programs that combines $N$ conditionals sharing some calculations in a large *then*-branch containing the structural pattern for the contextual rewriting rule:

```
if (x != y) {
    if (x >= y) {
        z = z + 1;
    }
    <fixed buffer code>
};

a = a + z;
<... above code is copied N times>
return a;
```

```
if (x != y) {
    if (x > y) {
        z = z + 1;
    }
    <fixed buffer code>
};

a = a + z;
<... above code is copied N times>
return a;
```

The associated PEG structure of the left program can be found in Figure 17 in the Appendix B.

**Experimental results:** Figure 12 shows the time elapsed for equivalence proving with each experimental setting, for values of $N$ up to 500.

The naive traversal-based contextual approach has the worst performance on these benchmark. Each contextual source leads to another *then*-branch traversal during contextual e-matching which naturally lowers the performances of the approach.

Annotation-based contextual equality saturation performs better than all other sound approaches. The annotation bookkeeping framework is efficient here, as it is only computed once on shared parts of an e-graph.

## 5.4 Complex equivalence task benchmark

**Experimental setup:** in this last benchmark we propose a last family of pairs of programs where $N$ rewriting rules must be performed in the *then*-branch before
<figure><img src="image_11.png" /><figcaption>Fig. 12: Results for the number of sources benchmarks</figcaption></figure>

the contextual pattern appears. This benchmark tests the contextual e-matching and the incremental annotation parts of the annotation framework: it requires detecting when the contextual pattern appears, and updating annotations when rewriting are performed in a *then*-branch. The family we study is similar to the previous one, except that *N* now controls both the number of conditionals and the complexity of some patterns <p1(N)> and <p2(N)> in the condition of the conditionals:

```
if (x != <p2(N)>) {
    if (x >= <p1(N)>) {
        z = z + 1;
    }
    <fixed buffer code>
};

a = a + z;
<... above code is copied N times>
return a;
```

```
if (x != <p2(N)>) {
    if (x > <p1(N)>) {
        z = z + 1;
    }
    <fixed buffer code>
};

a = a + z;
<... above code is copied N times>
return a;
```

The pattern <p1(N)> can be shown equivalent to <p2(N)> in *N* standard rule applications. As *N* grows, these programs simulate increasingly complex equivalence tasks in both number of conditionals in the program and proof substeps. The associated PEG structure of the left program can be found in Figure 18 in the Appendix B.
<figure><img src="image_12.png" /><figcaption>Fig. 14: Results for the complex equivalence task benchmark</figcaption></figure>

**Experimental results:** Figure 12 shows the time elapsed for equivalence proving with each experimental setting, for values of *N* up to 120 (due to quadratic size of associated *PEG*).

The ranking of approach remains the same as for the previous task. Annotation-based contextual rewriting performs around 30% better than the non-contextual approach.

The naive traversal-based contextual approach performs worse than on the previous task. Some traversals will be performed despite the contextual pattern not being present in the e-graph prior to the rewriting of <p1(N)> to <p2(N)>.

As a conclusion, we observe that the swap-based approach is not practical when the size of e-graph grows and it is always outperformed by the annotation-based contextual rewriting we propose. The naive traversal-based rewriting is doing well only on the first benchmark and behaves badly on the others, which validates the pertinence of the incremental annotation we propose. Overall, in the three experiments the incremental annotation-based contextual rewriting has the best scalability properties.

# 6 Related Work

Equality saturation was initially introduced [22] as an optimization technique: the program to be optimized is turned into a PEG and a collection of rewriting rules is applied on the resulting e-graph to obtain an implicit representation of multiple optimized version of the original input. Heuristics pick the optimized candidate and decompile it from PEG to a real program. The approach was later
used to perform translation of advanced compiler optimizations techniques for the LLVM compiler [20]. Premtoon et al. [18] later showed how to adapt the equality saturation technique to perform semantic search of programming pattern. Semantic search has many applications, including bugfinding and program simplification (for example by detecting opportunities to use calls to library functions). The open-source Rust project Egg [26] represents the state-of-the-art in equality saturation. It has been used recently in several application areas [23, 27, 16, 25].

Relational Hoare logic [3] is an axiomatic approach to program comparison. It is a variant of Hoare logic that aims to reason about two programs at once. As it studies two programs rather than one, it needs to track and compare the states of two executions. It comes with an extensible proof system of inference rules. Building an automatic verifier with this approach requires to design a good proof system together with a strategy for applying them. Benton [4] has built such an automated semantic difference finder in order to compare the code produced by two compilers for the Hack programming language [11], a typed PHP variant. Both compilers generate HHVM bytecode<fnref n="6" />. The semantic core of the tool uses relational Hoare logic and performs a semantic comparison of the instructions at intraprocedural level for functions of the same name.

In [14], Lahiri et al. present SymDiff, a tool capable of checking equivalence and displaying semantic differences between imperative programs regardless of the programming language used. They rely on the Boogie intermediate verification language, which can be obtained via translations from multiple source languages such as C, C#, and x86. The tool works by first composing versions of the two programs to be compared, then building a *product program* [28, 2], and generating verification conditions to be discharged by the Z3 SMT solver. Barthe et al. explores a similar approach [1] in the context of the CompCert verified compiler project [15] where they use a custom solver to increase control over the expected differences between the two program inputs. Another custom program equivalence verifier was also introduced by Rideau and Leroy [19] in order to validate register allocation algorithms in CompCert. Building a suitable product program is not an easy task. To make sure the companion program verifier succeeds, the product needs to be properly *aligned*. Churchill et al [5] proposed advanced techniques to perform such a product.

Some work focuses on equivalence checking technique for translation validation of advanced loop transformations on affine programs [24, 10]. The proof is performed by combining the dependence graphs of both input programs and infer an *equivalence tree* of the product by abstract interpretation. Such a tree explores the various possible alignments between loop bodies on each side.

<footnote n="6">⁶ HHVM [13] is an open-source virtual machine designed for executing programs written in Hack.</footnote>
# 7 Conclusion

In this paper we introduce *contextual* equality saturation, a novel extension to equality saturation that adds support for contextual rewriting rules. Contextual equality saturation makes it possible to propagate information obtained from the boolean test in conditional statements when proving the equivalence of programs. This extends the capability of equality saturation beyond existing non-contextual techniques. We present a new annotation system for e-graphs which can be incrementally updated after each standard e-graph updates. These annotations are an essential part in the design of algorithms for efficient equality saturation of contextual rules. We have implemented a prototype tool for evaluating the effectiveness of our contextual equality saturation algorithms, using a set of benchmark programs which confirm the added precision and the scalability of the method

One promising application of contextual equality saturation is as a general technique for the validation of code re-factoring and code migration. We intend to develop and evaluate a validator for the Java-to-Kotlin code migrator, as implemented in the IntelliJ tool, which transforms a Java program into its Kotlin equivalent. Both programs can be compiled into Java bytecode representations and be semantically compared with equality saturation. Our first experiments show that state-of-the-art equivalence checkers based on equality saturation cannot handle some common loops patterns while our approach makes this checking feasible. This is a strong indication that contextual equality saturation is an important step towards building a full-fledged validation tool.

Another avenue for further work is to investigate how information coming from other program analyses can be integrated into the e-graph framework, so as to help proving more program equivalences. The annotations that we have defined in this paper represent information that comes from boolean tests in the program. Other sources of data flow information can provide complementary information which would enable more rules to apply, and our annotations provides the infrastructure for integrating such data flow information.

Finally, in order to address the migration of larger code bases, it is also necessary to design a methodology for modularising the use of equality saturation, so that local equivalences can be extended to more global equivalences without having to build e-graphs for an entire procedure (which is likely to be prohibitive in terms of computational complexity). For this strand of research, the techniques presented by of Churchill et al. [5] on semantic program alignment seem especially pertinent.

# References

1. Barthe, G., Blazy, S., Laporte, V., Pichardie, D., Trieu, A.: Verified translation validation of static analyses. In: Proc. of CSF’2017 IEEE 30th CSF. IEEE Computer Society (2017)

2. Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Log. Algebraic Methods Program. 85(5) (2016)
3. Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proc. of POPL'2004. ACM (2004)

4. Benton, N.: Semantic equivalence checking for HHVM bytecode. In: Proc. of PPDP'2018. ACM (2018)

5. Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: Proc. of PLDI'2019. ACM

6. De Moura, L.M., Bjørner, N.S.: Efficient e-matching for SMT solvers. In: Proc. of CADE'2021. LNCS, vol. 4603. Springer (2007)

7. De Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Proc. of TACAS'2008. LNCS, vol. 4963. Springer (2008)

8. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3) (2005)

9. Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4) (1980)

10. Dutta, S., Sarkar, D., Rawat, A., Singh, K.: Validation of loop parallelization and loop vectorization transformations. In: Proc. of ENASE'2016. SciTePress (2016)

11. Hack documentation. https://hacklang.org, accessed: 2024-04-01

12. Havlak, P.: Construction of thinned gated single-assignment form. In: Proc. of LCPC'1993. LNCS, vol. 768. Springer (1993)

13. HHVM documentation. https://hhvm.com, accessed: 2024-04-01

14. Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In: Proc. of CAV'2012. LNCS, vol. 7358. Springer (2012)

15. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7) (2009)

16. Nandi, C., Willsey, M., Anderson, A., Wilcox, J.R., Darulova, E., Grossman, D., Tatlock, Z.: Synthesizing structured CAD models with equality saturation and inverse transformations. In: Proc. of PLDI'2020. pp. 31–44. ACM (2020)

17. Paleczny, M., Vick, C.A., Click, C.: The java hotspot server compiler. In: Proc. of Java Virtual Machine Research and Technology Symposium. USENIX (2001)

18. Premtoon, V., Koppel, J., Solar-Lezama, A.: Semantic code search via equational reasoning. In: Proc. of PLDI'2020. ACM (2020)

19. Rideau, S., Leroy, X.: Validating register allocation and spilling. In: Proc. of CC'2010. LNCS, vol. 6011. Springer (2010)

20. Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Proc. of CAV'2011. LNCS, vol. 6806. Springer (2011)

21. Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2) (1975)

22. Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: A new approach to optimization. Log. Methods Comput. Sci. 7(1) (2011)

23. VanHattum, A., Nigam, R., Lee, V.T., Bornholt, J., Sampson, A.: Vectorization for digital signal processors via equality saturation. In: Proc. of ASPLOS'2021. pp. 874–886. ACM (2021)

24. Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3) (2012)

25. Wang, Y.R., Hutchison, S., Suciu, D., Howe, B., Leang, J.: SPORES: sum-product optimization via relational equality saturation for large scale linear algebra. Proc. of VLDB Endow. 13(11) (2020)

26. Willsey, M., Nandi, C., Wang, Y., Flatt, O., Tatlock, Z., Panchekha, P.: egg: Fast and extensible equality saturation. In: Proc. of POPL'2021. ACM (2021)
27. Yang, Y., Phothilimthana, P.M., Wang, Y.R., Willsey, M., Roy, S., Pienaar, J.: Equality saturation for tensor graph superoptimization. In: Proc. of MLSys 2021 (2021)

28. Zaks, A., Pnueli, A.: Covac: Compiler validation by program analysis of the cross-product. In: Proc. of FM'2008. LNCS, vol. 5014. Springer (2008)

A Symbols used in the text

<table><caption>Fig. 15: Notation used in this paper.</caption><tr><td>Function symbols for our terms</td><td>F &#8800; f | g | h | ...</td></tr><tr><td>Constant symbols for our terms</td><td>a | x | y | ...</td></tr><tr><td>Variable placeholders for terms</td><td>V &#8800; X | Y | Z | ...</td></tr><tr><td>Terms</td><td>T &#8800; t | t' | ...</td></tr><tr><td>Patterns</td><td>p | p' | ...</td></tr><tr><td>Substitutions</td><td>S &#8800; &sigma; | &sigma;' | ...</td></tr><tr><td>E-nodes</td><td>N &#8800; m | n | n' | ...</td></tr><tr><td>Edges</td><td>E &#8800; e | e' | ...</td></tr><tr><td>E-classes</td><td>C &#8800; C | C<sub>1</sub> | C<sub>2</sub> | ...</td></tr></table>
B Benchmarks PEG structures

<figure><img src="image_13.png" /><figcaption>Fig. 16: PEG structure of the left programs of the source-pattern distance benchmark</figcaption></figure>
<figure><img src="image_14.png" /><figcaption>Fig. 17: PEG structure of the left programs of the number of sources benchmark</figcaption></figure>
<figure><img src="image_15.png" /><figcaption>Fig. 18: PEG structure of the left programs of the complex equivalence task benchmark</figcaption></figure>