Graph pruning

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,
:

,

and

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