next up previous
Next: Graph union Up: Reduced Set of RSGs Previous: Graph division


Graph pruning

After graph division, there can be nodes or links which are not compliant with the new properties of these graphs. For example, if a node $ n$ belongs to an $ rsg_1$ (which results from the division of $ rsg$) in which SELIN $ (n, sel) = 1$ there should be a node $ n_i$ pointing to $ n$ by selector $ sel$ ( $ <n_i,sel,n> \in NL(rsg_1)$). If such a node, $ n_i$, cannot be found we know that node $ n$ does not belong to this $ rsg_1$ and therefore the node and all its links can be removed from this graph. Actually, this node $ n$ will be present in other RSGs resulting from the graph division and in some of these RSGs the node will fulfill the SELIN property.

In our previous example we can see how the two divided graphs of Fig. 1(b) are simplified into the graphs presented in Fig. 1(c). Note that $ rsg\prime\prime_1$ is obtained after the pruning of $ rsg\prime_1$, in which we can safely remove the link $ <n_3,prv,n_1>$ due to it not fulfilling the cycle link properties of node $ n_3$. This property states that subsequently following $ prv$ and $ nxt$ from node $ n_3$, this $ n_3$ should be reached, but this does not happen for the above-mentioned link. Regarding $ rsg\prime\prime_2$, note that the same happens for the link $ <n_2,prv,n_1>$. Besides this, because node $ n_3$ is not shared by selector $ nxt$ and we are sure that $ <n_1,nxt,n_3>$ exists, we can conclude that $ <n_2,nxt,n_3>$ should be removed. This implies the elimination of $ <n_3,prv,n_2>$ due to cycle link properties. After this elimination, node $ n_2$ cannot be reached and is therefore removed from $ rsg\prime\prime_2$. In our implementation, these latter steps actually take place during the node materialization included in the abstract interpretation. In any case, it is important to note that the false value in share attributes leads to a more aggressive pruning which simplifies the RSRSGs and greatly contributes to avoid an explosion in the number of nodes.

To formalize the pruning process, our method uses two Boolean functions to determine whether a node, N_PRUNE$ (n)$, or a link, NL_PRUNE $ (<n_1,sel,n_2>)$, fulfill the graph properties:

$ \bullet$ A certain node, $ n$, is removed from the graph only taking into account the reference pattern property. That is, if the SELIN/SELOUT functions assert that the node is referenced by selector $ sel$ or that this node references by $ sel$ to another node, these conditions should be hold. In other cases, the node should be eliminated from the graph. More formally

N_PRUNE(n) = true if $ (\exists
sel_i \in $SELOUTset $ (n) ~\wedge~ sel_i \notin $posSELOUTset $ (n) ~\wedge~ \nexists n_2 \in
N(rsg), <n, sel_i, n_2> \in NL(rsg))~\vee~$ $ (\exists
sel_i \in $SELINset $ (n) ~\wedge~ sel_i \notin $posSELINset $ (n) ~\wedge~ \nexists n_2 \in
N(rsg), <n_2, sel_i, n> \in NL(rsg))$.

$ \bullet$ On the other hand, the link restrictions arise due to the CYCLELINKS property. For example, let's assume a certain node, $ n$, has a set of CYCLELINKS which comprises this particular one: $ <sel_1, sel_2>$. This cycle link points out that the memory locations represented by the node points to others by selector $ sel_1$, and those ones point to the original locations by selector $ sel_2$. Therefore, in our example, if the node $ n_2$ pointed to by $ n_1$ does not point again to $ n_1$ using selectors $ sel_1$ and $ sel_2$, respectively, we can safely remove the link $ <n_1,sel_1,n_2>$. Formally

NL_PRUNE $ (<n_1, sel_i, n_2>) =$ true if $ \exists <sel_i, sel_j> \in $ CYCLELINKS $ (n_1) ~\vert~<n_2,
sel_j, n_1> \notin NL(rsg)$.

Additionally, we should note that this pruning is an iterative process, because after the elimination of some nodes or links there may appear more nodes or links which do not fulfill the rules and should be removed too. This way, the pruning process ends when all the nodes and links fulfill the graph properties. The whole process can be expressed as PRUNE $ (rsg) = rsg_n$. This iterative function starts with $ rsg_0 = rsg$. Next, $ \forall i = 1 .. n$:

$N(rsg_i) = N(rsg_{i-1}) \setminus \{n \in N(rsg_{i-1}) \vert
\text{\tt N\_PRUNE}(n) = 1\}$,

$PL(rsg_i) = PL(rsg_{i-1}) \setminus
\{<pvar, n> \in PL(rsg_{i-1}) \vert \text{\tt N\_PRUNE}(n) = 1\}$ and

$NL(rsg_i) = NL(rsg_{i-1}) \setminus \{<n_1, sel, n_2> \in
NL(rsg_{i-1}) \vert (...
...ext{\tt N\_PRUNE}(n_2) = 1) \vee (\text{\tt NL\_PRUNE}(<n_1, sel, n_2>) = 1) \}$

where for each iteration we remove the nodes and links for which functions N_PRUNE and NL_PRUNE return true. The process ends when we reach the graph $ rsg_n$ which holds $\forall n
\in N(rsg_n), \text{\tt N\_PRUNE}(n) = 0$ $ \wedge$ $\forall <n_1, sel, n_2> \in NL(rsg_n), \text{\tt NL\_PRUNE}(<n_1, sel,n_2>) = 0$


next up previous
Next: Graph union Up: Reduced Set of RSGs Previous: Graph division
Rafael Asenjo Plaza 2002-02-19