LARA

Termination and Efficiency of Abstract Interpretation Analysis

Definition: A chain of length $n$ is a sequence $s_0, s_1, \ldots, s_n$ such that

\begin{equation*} s_0 \sqsubset s_1 \sqsubset s_2 \sqsubset \ldots \sqsubset s_n \end{equation*}

where $x \sqsubset y$ means, as usual, $x \sqsubseteq y \land x \neq y$

Definition: A partial order has a finite height $n$ if it has a chain of length $n$ and every chain is of length at most $n$.

A finite lattice is of finite height

Example: The constant propagation lattice $\mathbb{Z} \cup \{\bot, \top\}$ is an infinite lattice of height 2. One example chain of length 2 is

\begin{equation*} \bot \sqsubset 42 \sqsubset \top \end{equation*}

Here the $\gamma$ function is given by

  • $\gamma(k) = \ldots$ when $k \in \mathbb{Z}$
  • $\gamma(\top) = \ldots$
  • $\gamma(\bot) = \ldots$

The ordering is given by $a_1 \subseteq a_2$ iff $\gamma(a_1) \subseteq \gamma(a_2)$

Example: If a state of a (one-variable) program is given by an integer, then a concrete lattice element is a set of integers. This lattice has infinite height. There is a chain

\begin{equation*} \{ 0 \} \subset \{ 0, 1 \} \subset \{ 0, 1, 2 \} \subset \ldots \subset \{ 0, 1, 2, \ldots, n \} \end{equation*}

for every $n$.

Convergence in Lattices of Finite Heignth

Consider a finite-height lattice $(L, \sqsubseteq)$ of height $n$ and function

\begin{equation*} F : L \to L \end{equation*}

What is the maximum length of sequence $\bot, F(\bot), F^2(\bot), \ldots$ ?

Give an effectively computable expression for $lfp(F)$.

Computing the Height when Combining Lattices

Let $H(L,\leq)$ denote the height of the lattice $(L,\leq)$.

Product

Given lattices $(L_1,\sqsubeteq_1)$ and $(L_2,\sqsubeteq_2)$, consider product lattice with set $L_1 \times L_2$ and potwise order

\begin{equation*} (x_1,x_2) \sqsubseteq (x'_1, x'_2) \end{equation*}

iff $\ldots$

What is the height of the product lattice?

Exponent

Given lattice $(L, \sqsubeteq)$ and set $V$, consider the lattice $(L^V,\sqsubseteq')$ defined by

\begin{equation*} g \sqsubset' h \end{equation*}

iff $\forall v \in V. g(v) \sqsubseteq h(v)$.

What is the height of the exponent lattice?

Answer: height of $L$ times the cardinality of $V$.