LARA

This is an old revision of the document!

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 $c(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, 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: \[ 

I \subseteq C(p_0)

\] \[ 

\bigwedge_{(p_1,p_2) \in E} sp(C(p),r(c(p_1,p_2)))) \subseteq C(p_2)

\] where $c(p_1,p_2)$ is command associated with edge $(p_1,p_2)$, and $r(c(p_1,p_2))$ is the relation giving semantics for this command.

Example