Differences
This shows you the differences between two versions of the page.
sav08:collecting_semantics [2008/05/08 12:37] vkuncak |
sav08:collecting_semantics [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ===== 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: | ||
- | \[ | ||
- | I \subseteq C(p_0) | ||
- | \] | ||
- | \[ | ||
- | \bigwedge_{(p_1,p_2) \in E} sp(C(p_1),r(p_1,p_2))) \subseteq C(p_2) | ||
- | \] | ||
- | over variables $C(p)$ for all of finitely many program points $p$. | ||
- | |||
- | The last condition is equivalent to | ||
- | \[ | ||
- | \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) | ||
- | \] | ||
- | |||
- | 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: | ||
- | |||
- | <code> | ||
- | i = 20; | ||
- | x = 2; | ||
- | while (i > 0) { | ||
- | x = x + 4; | ||
- | i = i - 1; | ||
- | } | ||
- | if (x==0) { | ||
- | error; | ||
- | } else { | ||
- | y = 1000/x; | ||
- | } | ||
- | </code> | ||
- | After the assignment of $x$ to 2, the set of reachable states $C$ is $C = \{ (x,2), (i,20), (y,t) \}$ | ||