LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:collecting_semantics [2008/05/08 12:36]
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) \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) \}$