LARA

Abstract Interpretation Recipe

Program Representation

Control-flow graph: $(V,E,r)$ where

  • $V = \{p_1,\ldots,p_n\}$ is set of program points
  • $E \subseteq V \times V$ are control-flow graph edges
  • $r : E \to 2^{PS \times PS}$, so each $r(p_1,p_2) \subseteq PS \times PS$ is relation describing the meaning of command between $p_1$ and $p_2$

We can define meaning of program in this form using Collecting Semantics.

Summary of key steps

  • design abstract domain $A$ that represents sets of program states
  • define $\gamma : A \to C$ giving meaning to elements of $A$
  • define lattice ordering $\sqsubseteq$ on $A$ such that $a_1 \le a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$
  • define $sp^\# : A \times R \to A$ that maps an abstract element and a CFG statement to new abstract element, such that $sp(\gamma(a),r) \subseteq \gamma ( sp^{\#} (a,r))$

(for example, by defining function $\alpha$ so that $(\alpha,\gamma)$ becomes a Galois Connection on Lattices)

  • extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$)

\begin{equation*}
   F^{\#}(g^{\#})(p') = g^{\#}(p') \sqcup \bigsqcup_{(p,p') \in E} sp^{\#}(g^{\#}(p),r(p,p'))
\end{equation*}

which is analogous to Collecting Semantics

  • compute $g^{\#}_* = lfp(F^\#)$ (this is easier than computing collecting semantics because lattice $A^n$ is simpler than $C^n$):

\begin{equation*}
   g^{\#}_* = \bigsqcup_{n \ge 0} (F^{\#})^{n}(\bot^{\#})
\end{equation*}

where $\bot^{\#}(p) = \bot_A$ for all $p \in V$