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, and , can be joined in a single one if they are compatible. Thus, we define COMPATIBLE true if ALIAS ALIAS COMP_NODES . We see that two graphs, and , 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 is the set of alias relations, , in the graph, where each identifies all the pvars pointing to the same node :
ALIAS where if
- COMP_NODES 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, and , 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 true if C_NODES
where C_NODES true if (TYPE = TYPE (SHARED SHARED (SHSEL SHSEL (TOUCH TOUCH (C_REFPAT (C_SPATH .
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.