LARA

Describing Reachable States using Collecting Semantics

Main question: What values can variables of the program take at different program points?

We can represent programs by control-flow graphs (CFG).

Definition: Control flow-graph is a graph with nodes $V$, edges $E \subseteq V\times V$ and for each edge $e \in E$ a command given by relation $r(e)$, with initial $init$ and final node $final$

Program points are CFG nodes. Statements are labels on CFG edges.

We look at a particular way of representing and computing sets of reachable states, splitting states by program counter (control-flow graph node): collecting semantics.

$PS$ - states describing values of program variables (not including program counter).

For each program point $p$, we have the set of reachable states $C(p) \subseteq PS$.

The set of all reachable states of the program is $\{(p,s) \mid s \in C(p) \}$.

Let $p_0$ be initial program counter and $I$ the set of values of program variables in $p_0$.

The set of reachable states is defined as the least solution of constraints:

\begin{equation*} I \subseteq C(p_0) \end{equation*}

\begin{equation*} \bigwedge_{(p_1,p_2) \in E} sp(C(p_1),r(p_1,p_2))) \subseteq C(p_2) \end{equation*}

over variables $C(p)$ for all of finitely many program points $p$.

The last condition is equivalent to

\begin{equation*} \bigwedge_{p_2 \in V}\ \left( C(p_2) = C(p_2) \cup \bigcup_{(p_1,p_2) \in E} sp(C(p_1),r(p_1,p_2))) \right) \end{equation*}

Here $r(p_1,p_2)$ is the relation giving semantics for the command associated with edge $(p_1,p_2)$.

Set of recursive inequations in the lattice of products of sets. Note $e_1 \subseteq e_2$ is equivalent to $e_2 = e_1 \cup e_2$, so we have equations in lattice.

They specify function $G$ from pairs of sets of states to pairs of sets of states which is $\cup$-morphism (and therefore monotonic).

Least fixpoint of $G$ is $\bigcup_{i \ge 0} G^i(\emptyset)$.

Example

Sets of states at selected points: 

i = 20;
x = 2;
while (i > 0) {
  x = x + 4;
  i = i - 1;
}
if (x==0) {
  error;
} else {
  y = 1000/x;
}

After the assignment of $x$ to 2, the set of reachable states $C$ is $C = \{ (x,2), (i,20), (y,t) \}$