CS6620 Compiler Note 3 Narrowing and Widening

Posted on In Disqus:

Interval analysis can be used in integer representation or array bound check. This would involve widening and narrowing.

A lattice of intervals is defined as $\text{Interval} \triangleq \text{lift}(\lbrace \lbrack l,h\rbrack \mid l,h\in\mathbb{Z} \wedge l \leq h\rbrace)$. The partial order is defined as $\lbrack l_1,h_1\rbrack \sqsubseteq \lbrack l_2,h_2\rbrack \iff l_2 \leq l_1 \wedge h_1 \le h_2$.

The top is defined to be $\lbrack -\infty,+\infty\rbrack$ and the bottom is defined as $\bot$, which means no integer. Since the chain of partial order can have infinite length, the lattice itself has infinite height.

The total lattice for a program point is $L = \text{Vars}\to \text{Interval}$, which provides bounds for each integer value.

The constraint rules are listed as
$$
\begin{aligned}
& & & JOIN(v) = \bigsqcup_{w\in pred(v)}\lbrack \lbrack w\rbrack \rbrack \newline
\lbrack\lbrack X = E\rbrack\rbrack &\phantom{:::} \lbrack\lbrack v\rbrack\rbrack &=& JOIN(v) \lbrack X \mapsto \text{eval}(JOIN(v), E)\rbrack\newline
& & & \text{eval}(\sigma, X) = \sigma(X)\newline
& & & \text{eval}(\sigma, I) = \lbrack I, I\rbrack\newline
& & & \text{eval}(\sigma, \text{input}) = \lbrack -\infty, \infty\rbrack\newline
& & & \text{eval}(\sigma, E_1\ op\ E_2) = \hat{op}(\text{eval}(\sigma, E_1), \text{eval}(\sigma, E_2))\newline
& & & \hat{op}(\lbrack l_1,r_1\rbrack, \lbrack l_2,r_2\rbrack) = \lbrack \min_{x\in \lbrack l_1,r_1\rbrack, y\in \lbrack l_2,r_2\rbrack} x\ op\ y, \max_{x\in \lbrack l_1,r_1\rbrack, y\in \lbrack l_2,r_2\rbrack }x\ op\ y\rbrack \newline
& \phantom{:::}\lbrack\lbrack v\rbrack\rbrack &=& JOIN(v)\newline
& \lbrack \lbrack exit\rbrack\rbrack &=& \varnothing
\end{aligned}
$$
The fixed-point problem we previously discussed is only restricted in lattice with finite height. New fixed-point algorithm is needed in practical space.

Widening and Narrowing

A widening function $\omega: L^n \to L^n$ is introduced by $(\omega \circ f)^i (\bot,\dots,\bot)$ is guaranteed to converge on a fixed-point that is larger or equal to the $f^i(\bot,\dots, \bot)$.

To ensure the convergence, the $\omega$ must monotone and extensive ($\forall x,x \sqsubseteq \omega(x)$), and $\omega(L) = \lbrace y \in L \mid \exists x \in L: y = \omega(x)\rbrace$ has finite height.

$\omega$ would coarsen the information sufficiently to ensure termination.

In this interval analysis, $\omega$ is defined pointwise on $L^n$. It operates relative to a fixed (parameterized to program) finite subset $\mathbb{B}\subset \mathbb{N}$ that must contain $\pm \infty$.

Typically $\mathbb{B}$ could seeded with all the integer constants occurring in the given program but other heuristic methods could be used.

$\omega’$ on single interval could be defined as $\omega’:\text{Interval}\to\text{Interval}$ by
$$
\omega’(\lbrack l,r\rbrack) = \lbrack \max\lbrace x \in \mathbb{B}\mid x \le l\rbrace, \min\lbrace x \in \mathbb{B}\mid x \ge r\rbrace\rbrack\
\omega’(\bot) = \bot
$$
Thus the new fixed-point algorithm is working on $L = (\text{Vars} \to \text{Interval})^n$ and $\omega:L\to L$ can be simply expand definition of $\omega’$ on each $L$ by
$$
\begin{aligned}
\omega(\sigma_1,\dots,\sigma_n) &= (\sigma_1’,\dots,\sigma_n’)\
\sigma_i’(X) &= \omega’(\sigma_i(X)), \forall X \in \text{Vars}, 1 \le i \le n
\end{aligned}
$$

Recap on the fixed-point and termination, the $\omega \circ f:\omega(L) \to\omega(L)$ is defined on a finite height lattice since $\omega(L)$ has finite height.

$fix = \bigsqcup f^i(\bot)$ and $fix\omega = \bigsqcup (\omega\circ f)^i(\bot)$, then we see $fix \sqsubseteq f\circ fix\omega \sqsubseteq (fix\omega = \omega \circ f \circ fix\omega)$.

This would lead to narrowing, which helps improve the result and still provide sound information.

More Sophisticated Widening

A new widening function can be defined as $\nabla: L\times L \to L$ that is extensive in both arguments and satisfies property:

  • $\forall z$ be increasing chains where $z_0 \sqsubseteq z_1 \sqsubseteq \dots$, the sequence $y_0 = z_0,\dots y_{i + 1} =y_i \nabla z_{i+1}$ converges.

Basic fixed-point solver can compute $x_0 = \bot, x_{i+1} = x_i \nabla F(x_i)$ until convergence.

If we let $\nabla = \sqcup$, then we see that fixed-point with widening is a special case of a fixed-point algorithm.

$\sqcup$ is a widening operator for a finite height $L$.

The idea of using infix binary $\nabla$ is that it allows us to combine abstract information from previous and current iteration fixed-point computation, and only coarsen values that are unstable.

A widening operator $\nabla’:\text{Interval}\to\text{Interval}$ is defined as
$$
\begin{aligned}
\bot \nabla’ y &= y\newline
x \nabla’ \bot &= x\newline
\lbrack l_1, h_1\rbrack \nabla’ \lbrack l_2,h_2\rbrack &= \lbrack l_3, r_3\rbrack\newline
l_3 &= \begin{cases}
l_1 &\text{if }l_1 \le l_2\newline
\max\lbrace i \in \mathbb{B} \mid i \le l_2\rbrace &\text{otherwise}
\end{cases}\newline
h_3 &=\begin{cases}
h_1 &\text{if }h_2 \le h_1\newline
\text{min}\lbrace i \in \mathbb{B} \mid h_2 \le i \rbrace&\text{otherwise}
\end{cases}
\end{aligned}
$$
$\nabla$ can then be expanded from definition of $\nabla’$ by
$$
\begin{aligned}
(\sigma_1,\dots,\sigma_n)\nabla (\sigma_1’, \dots, \sigma_n’) &= (\sigma_1’’,\dots,\sigma_n’’)\newline
\sigma_i’’(X)& = \sigma_i(X)\nabla’\sigma_i’(X), \forall X \in \text{Vars}, 1\le i \le n
\end{aligned}
$$