MIR Definitions

Here we describe definitions of MIR concepts that are relevant to the PCG.

MIR Dataflow Analysis

At a high level, a MIR dataflow analysis is defined by the following elements:

• A domain $\mathcal{D}$
• A join operation $join:(\mathcal{D}\times \mathcal{D})\to \mathcal{D}$
• An empty state $d_{ϵ}\in \mathcal{D}$
• A transfer function $transfer:(\mathcal{D}\times Location)\to \mathcal{D}$

Performing the dataflow analysis on a MIR body $B$ computes a value of type $\mathcal{D}$ for every location in $B$. The analysis is performed (conceptually) as follows¹:

• The analysis defines a map $S$ that maps locations in $B$ to elements of $\mathcal{D}$.
• Each location in $S$ is initialized to $d_{ϵ}$
• The operation analyze(b) updates $S$ as follows:
  • $s[b[0]]\leftarrow transfer(s[b[0]],b[0])$
  • For $0<i⩽|b|:s[b[i]]\leftarrow transfer(s[b[i-1]],b[i])$
• The analysis defines a worklist $W=[b_0]$
• While $W$ is not empty:
  • Pop $b$ from $W$
  • Perform $analyze(b)$
  • Let $s_b^{exit}$ be the entry of the last location in $b$ in $s$
  • For each successor $b^{\prime }$ of $b$:
    • Let $s_{b^{\prime }}^{entry}=s[b^{\prime }[0]]$
    • Let $s_{b^{\prime }}^{join}=join(s_{b^{\prime }}^{entry},s_b^{exit})$
    • If $s_{b^{\prime }}^{join}\ne s_{b^{\prime }}^{entry}$:
      • $s[b^{\prime }[0]]\leftarrow s_{b^{\prime }}^{join}$
      • Add $b^{\prime }$ to $W$
• $S$ is the result

1. The current analysis implementation (defined in the rust compiler) is more efficient than what we describe because it tracks state per basic block rather than per-location, as the states for any location in a block can be computed by repeated application of the transfer function to the entry state. ↩