Reaching Definitions

For every variable \( v \), we track the most recent edges \((l, v = \mathtt{aexpr}, l') \in G\) that assign a value to \( v. \)

Abstract Domain: \( D = (C, (E, \sqsubseteq, \sqcup, \top), [[\cdot]]) \) with \( E \subseteq \mathit{Var} \times (\mathbb{L} \times \mathbb{L}) \).
Order Relation: \((l, S) \sqsubseteq_\mathbb{RD} (l', S')\) if \( l = l' \) or \( l' = \top_\mathbb{L} \) and \( S \subseteq S' \).
Merge Operator: \[ \mathsf{merge}\big((l, S), (l', S')\big) = \begin{cases} (l, S \cup S'), & \text{if } l = l' \\ (l', S'), & \text{otherwise.} \end{cases} \]
Stop Condition: \[ \mathsf{stop}(e, E_{\mathit{reached}}) = \exists e' \in E_{\mathit{reached}}: e \sqsubseteq e'. \]

Example:

Consider a simple program fragment with control flow labels:

l1: x := 10
l2: y := x + 2
l3: x := y - 3

At l1, the definition of x is established. When execution reaches l2, the definition \( (x, l1, l2 ) \) for \( x \) is still active and can be used for the arithmetic computation in \( y := x + 2 \). Then, at l3, the new assignment overwrites the previous definition of \( x \) by introducing a new definition \( (x, l3, l4 ) \). This tracking of which assignment “reaches” a given point in the program is the core idea behind reaching definitions.

Transfer Relation

The transfer relation is defined as: \[ (l, S) \rightsquigarrow_{RD} (l', S') \] if:

There exists a CFA edge \( g = (l, \mathit{op}, l') \in G \) such that: \[ S' = \begin{cases} \Bigl(S \setminus \{(x, k, k') \mid k, k' \in \mathbb{L}\}\Bigr) \cup \{(x, l, l')\}, & \text{if op is of the form } x := a; \\ S, & \text{otherwise.} \end{cases} \]
Additionally, if \( l = l' = \top_\mathbb{L} \), then \( S' = E \).

Here, \( a \) represents an arithmetic expression (\( \mathtt{aexpr} \)).

Example:

Suppose there is a CFA edge corresponding to the statement:

l1: x := 5

If the current reaching definitions state \( S \) contains one or more earlier definitions for \( x \), the transfer function removes all previous definitions of \( x \) (i.e., all elements of the form \((x, k, k')\)) and then adds the new definition \((x, l1, l2)\) (assuming the edge goes from \( l1 \) to \( l2 \)). This update ensures that only the most recent assignment is used in subsequent analyses.

In effect, the transfer relation models the way definitions “flow” through the program, discarding obsolete ones and retaining only those that are relevant at each program point.