Abstract Interpretation Recipe

Program Representation

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

$V = \{v_1,\ldots,v_n\}$ is set of program points
$E \subseteq V \times V$ are control-flow graph edges
$r : E \to 2^{S \times S}$ , so each $r(v,v') \subseteq S \times S$ is relation describing the meaning of command between $v$ and $v'$

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 \sqsubseteq a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$
define $sp^\# : A \times 2^{S\times S} \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 and letting $sp^{\#} (a,r)=\alpha(sp(\gamma(a),r))$ )

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^{\#})(v') = Init(v') \sqcup \bigsqcup_{(v,v') \in E} sp^{\#}(g^{\#}(v),r(v,v')) \end{equation*}$

which is analogous to collecting semantics.

(Note the Equivalent Form of Abstract Interpretation Function.)

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^{\#}(v) = \bot_A$ for all $v \in V$ .