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 is obtained after the pruning of , in which we can safely remove the link due to it not fulfilling the cycle link properties of node . This property states that subsequently following and from node , this should be reached, but this does not happen for the above-mentioned link. Regarding , note that the same happens for the link . Besides this, because node is not shared by selector and we are sure that exists, we can conclude that should be removed. This implies the elimination of due to cycle link properties. After this elimination, node cannot be reached and is therefore removed from . 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, or a link, NL_PRUNE , fulfill the graph properties:
A certain node, , 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 or that this node references by 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 SELOUTset posSELOUTset SELINset posSELINset .
On the other hand, the link restrictions arise due to the CYCLELINKS property. For example, let's assume a certain node, , has a set of CYCLELINKS which comprises this particular one: . This cycle link points out that the memory locations represented by the node points to others by selector , and those ones point to the original locations by selector . Therefore, in our example, if the node pointed to by does not point again to using selectors and , respectively, we can safely remove the link . Formally
NL_PRUNE true if CYCLELINKS .
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 . This iterative function starts with . Next, :
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 which holds