LARA

Lecture 9 Skeleton

Recall formula propagation from Lecture 7. See correctness of formula propagation.

Static analysis as equation solving in a lattice

If instead of formulas as $\mbox{fact}(v)$ we have elements of some lattice, this condition becomes

\begin{equation*} sp(\gamma(\mbox{fact}(u)),c) \subseteq \gamma(\mbox{fact}(v)) \end{equation*}

(where sp in now denotes operator on states and not formulas).

By properties of Galois connection, this is equivalent to

\begin{equation*} \alpha(sp(\gamma(\mbox{fact}(u)),c)) \sqsubseteq \mbox{fact}(v) \end{equation*}

and we defined best transformer as $sp\#(a,c) = \alpha(sp(\gamma(a),c))$, so this condition is equivalent to

\begin{equation*} sp\#(\mbox{fact}(u),c) \sqsubseteq \mbox{fact}(v) \qquad\qquad (*) \end{equation*}

We conclude that finding an inductive invariant expressed using elements of a lattice corresponds to finding a solution to a system of inequations $(*)$ for all $(u,c,v) \in E$. We next examine the existence and computation of such solutions more generally.

Note that $sp\#(a,c)$ is a function monotonic in a. Why?

So, we are solving a conjunction of inequations

\begin{equation*} a^i \sqsupseteq f_k(a^j) \end{equation*}

where $a^1,\ldots,a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph).

From a system of equations to one equation

In lattice, we have that a conjunction of inequations

\begin{eqnarray*} x \sqsupseteq y_1 \\ \ldots \\ x \sqsupseteq y_n \end{eqnarray*}

is equivalent to $x = x \sqcup y_1 \sqcup \ldots \sqcup y_n$ ($x$ is least upper bound of them).

So we can write the conjunction of inequations in the previous section as a system of equations

\begin{eqnarray*} a^1 &=& g_1(a^1,\ldots,a^n) \\ \ \ \ldots \\ a^n &=& g_1(a^1,\ldots,a^n) \\ \end{eqnarray*}

Now, introduce a new product lattice $\bar A = A^n$ with order $(a^1,\ldots,a^n) \sqsubseteq (b^1,\ldots,b^n)$ iff $a^1 \squbseteq b^1$,\ldots, $a^n \sqsubseteq b^n$ all hold. Then we have reduced the problem to finding a solution to equation

\begin{equation*} x = G(x) \end{equation*}

where $G((a^1,\ldots,a^n)) = (g_1(a^1,\ldots,a^n),..., g_n(a^1,\ldots,a^n))$. Function $G$ is also monotonic.

The solution of equation of the form $x=G(x)$ is called a fixed point of function $G$, because $G$ leaves $x$ in place.

The iterative process that we described above corresponds to picking an initial element $x$ such that $x \sqsubseteq G(x)$ and then computing $G(G(x))$, \ldots, $G^n(x)$.

  • we have $G^n(x) \sqsubseteq G^{n+1}(x)$
  • we have $x \sqsubseteq G^n(x)$

If it stabilizes we have $G^{n+1}(x)=G^n(x)$, so $G^n(x)$ is a fixed point. This always happens if there are no infinite ascending chains.

What is we have arbitrary lattices? See, for example non-converging iteration in reals.

$\omega$-continuity in a complete lattice is a requirement that for every chain $x_1 \sqsubseteq x_2 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have

\begin{equation*} f(\bigsqcup_i x_i) = \bigsqcup_i f(x_i) \end{equation*}

(generalizes continuity in real numbers). For continuous functions, even if there are infinite ascending chains, the fixed point iteration converges in the limit.

In general, even without $\omega$-continuity we know that the fixed point exists, due to Tarski fixed point theorem.

See also lecture notes in SAV07 resource page, in particular notes by Michael Schwartzbach for the finite case and slides by David Schmidt for $\omega$-continuity. You can also check papers by Cousot & Cousot:

Widening

Narrowing

Reduced product