next up previous
Next: Graph division Up: Progressive Shape Analysis for Previous: Compression of graphs


Reduced Set of RSGs

We have already seen that an RSG describes a memory configuration by a finite graph. The execution of each sentence in the program can modify the memory configuration and thus the RSG. However, due to the control flow of the program, the same sentence could be reached by several control paths leading to several memory configurations depending on the path. This way, there could also be several RSGs for the same program sentence. In our method, we maintain the representation of all these RSGs with the Reduced Set of Reference Shape Graphs (RSRSG).

Therefore, each sentence in the program has an associated RSRSG which approximately describes all possible memory configurations that may arise after the execution of this sentence.

However, the number of RSGs stored in an RSRSG could be prohibitive if we do not apply some simplifications while keeping reasonable accuracy in the representation. Actually, this simplification consists in allowing the union of some of the RSGs which fulfill certain conditions. After the union, the resulting RSG should represent all the locations approximated by the original RSGs and the relevant shape information should be maintained.

More precisely, two graphs, $ rsg_1$ and $ rsg_2$, can be joined in a single one if they are compatible. Thus, we define COMPATIBLE $ (rsg_1, rsg_2) =$ true   if ALIAS$ (rsg_1) = $ ALIAS $ (rsg_2))~ \wedge ~ $COMP_NODES $ (rsg_1, rsg_2) =
1$. We see that two graphs, $ rsg_1$ and $ rsg_2$, are compatible if they fulfill two conditions: i) the alias relation between pvars of both graphs are the same; and ii) certain nodes in both graphs are compatible. This leads us to define the alias relation between pvars and the compatibility condition between certain nodes in the graphs:

- ALIAS$ (rsg)$ is the set of alias relations, $ alr_i$, in the $ rsg$ graph, where each $ alr_i$ identifies all the pvars pointing to the same node $ n_i$:

ALIAS $ (rsg) = \{alr_1, ..., alr_n\}$ where $ alr_i = \{pvar_1, .., pvar_m \in P\}$ if $ \exists n_i \in
N(rsg) \vert <pvar_1, n_i>, ..., <pvar_m, n_i> \in PL(rsg)$

- COMP_NODES $ (rsg_1, rsg_2)$ is a Boolean function which returns true if the nodes directly pointed to by the same pvar are compatible, which happens when they have similar properties (and therefore these nodes can be summarized). This function is formalized in two steps: the first one identifies the nodes from both RSGs, $ n_j
\in N(rsg_1)$ and $ n_k \in N(rsg_2)$, which are pointed to by the same pvar; the second step determines whether these nodes have similar properties using an additional Boolean function C_NODES:

COMP_NODES $ (rsg_1, rsg_2) =$ true if $ \forall pvar_i \in P, ~
<pvar_i, n_j> \in PL(rsg_1)$ $ \wedge <pvar_i, n_k> \in PL(rsg_2)
~\wedge $ C_NODES $ (n_j, n_k) = 1. $

where C_NODES $ (n_1, n_2) =$ true if (TYPE$ (n_1)$ = TYPE $ (n_2)) ~ \wedge ~$(SHARED$ (n_1) = $ SHARED $ (n_2)) ~ \wedge ~$ (SHSEL $ (n_1, sel_i) = $ SHSEL $ (n_2, sel_i) \forall
sel_i \in S) ~ \wedge ~$ (TOUCH$ (n_1) = $ TOUCH $ (n_2)) ~ \wedge ~$ (C_REFPAT $ (n_1, n_2) = 1) ~ \wedge ~$ (C_SPATH $ (n_1, n_2, m) = 1) $.

We can see here that C_NODES_RSG and C_NODES are quite similar, but they differ in that the latter does not check the STRUCTURE property. This is because of the excessive complexity involved in checking this property for all the nodes of two different RSGs. Let us note again that we only impose node compatibility on those nodes directly pointed to by the same pvar.

In the following subsections, we describe the operations that can be carried out with the RSGs of an RSRSG. In the worst case, the sequence of operations that the compiler carries out in order to symbolically execute a sentence, as we have seen in Fig. 2, are: graph division, graph prune, sentence symbolic execution (RSG modification), RSG compression, and RSG union to build the final RSRSG. In fact, the RSG compression has already been presented in Sect. 3.2, so we focus on the other operations.



Subsections
next up previous
Next: Graph division Up: Progressive Shape Analysis for Previous: Compression of graphs
Rafael Asenjo Plaza 2002-02-19