Transition System and Collecting Semantics

$v \in V$ - program counter values. Denoted $p_i$ (program point) or $v_i$ (vertex in CFG)

$s \in S$ - values of other variables

Transition system semantics:

state is set of pairs $(v,s) \in V \times S$
element of concrete lattice is a set of such pairs $c \subseteq V \times S$ , i.e. $c \in 2^{V \times S}$
post maps set of such pairs to an extended set of such pairs, $post : 2^{V \times S} \to 2^{V \times S}$

Collecting Semantics

Take $c \in 2^{V \times S}$ .

$c = \{ (v_0, s_0), (v_1,s_1), (v_1, s_2), (v_2, s_2), (v_2,s_3), (v_4, s_4) \ldots \}$

Because $c$ is an arbitrary set, for a given $v_i$ , there can be any number of $s_j$ such that $(v_i,s_j)$ is in $c$ (in fact, $c$ is a relation on $V \times S$ ).

We can equivalently represent this relation $c \in 2^{V \times S}$ as the following multi-valued function, by grouping all $s_j$ for a given $v_i$ :

$\begin{equation*} g \in \left(2^S\right)^V \end{equation*}$

$\begin{equation*} g : V \to 2^S \end{equation*}$

$\begin{equation*} g = \{ (v_0, \{s_0\}), (v_1, \{s_1,s_2\}), (v_2,\{s_2,s_3\}), \ldots \} \end{equation*}$

Collecting semantics simply works with $(2^S)^V$ instead of $2^{V \times S}$ , which is just notational change.

lattice element is a function $g \in (2^S)^V$ i.e. $g : V \to 2^S$
we have function $F : (2^S)^V \to (2^S)^V$ that transforms such functions and directly corresponds to $post$

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$

Compute the big relation on global states in terms of $E$ and $r(v,v')$ .

$\begin{equation*} R = \bigcup_{(v,v') \in E} \{ ((v,s),(v',s') \mid (s,s') \in r(v,v') \} \end{equation*}$

Then derive a nice expression for $sp(c,R)$ where $c \subseteq V \times S$ .

$\begin{equation*} sp(c,R) = \bigcup_{(v,v') \in E} sp(c,\{ ((v,s),(v',s') \mid (s,s') \in r(v,v') \}) \end{equation*}$

Now we come back to the definition of post, which was

$\begin{equation*} post(c) = Init \cup sp(c,R) \end{equation*}$

so we obtain

$\begin{equation*} post(c) = Init \cup \bigcup_{(v,v') \in E} sp(c,\{ ((v,s),(v',s') \mid (s,s') \in r(v,v') \}) \end{equation*}$

Now instead of $c \subseteq V \times S$ , consider $g : V \to 2^S$ , and define a new sp on such different representation. Then

$\begin{equation*} sp(g,R) = g' \end{equation*}$

where

$\begin{equation*} g'(v') = \bigcup_{(v,v') \in E} sp(g(v),r(v,v')) \end{equation*}$

We also represent $Init$ as $g_{init} : V \to 2^S$ , then we obtain function $F$ that corresponds to $post$ :

$\begin{equation*} F : (V \to 2^S) \to (V \to 2^S) \end{equation*}$

$\begin{equation*} F(g)(v') = g_{init}(v') \cup \bigcup_{(v,v') \in E} sp(g(v),r(v,v')) \end{equation*}$

Note that $g_{init}(v')$ will be $\emptyset$ except at the entry into our control-flow graph.

If we compute $lfp(F)$ , we obtain $g^* : V \to 2^S$ such that $g^*(v)$ gives precisely the set of all reachable states at a program point $v$ . Such $g^*$ is isomorphic to $sp(Init,R^*)$ .

We call this way of defining $g^*$ the collecting semantics of the program, because it collects all states for each program point. It will be convenient to define how abstract interpretation works.