As we explained in Sect. 2 the code analysis implies symbolically executing each sentence applying the abstract semantics associated with this sentence. This symbolic execution modifies the RSGs included in the input RSRSG. This way, these graphs may contain new nodes representing new memory locations and/or the properties for certain nodes may have changed. In other words, after the symbolic execution of a sentence over an input RSRSG, the resulting RSRSG may contain RSGs with redundant information, which can be removed due to node summarization or compression of the RSG.
In order to do this, after the symbolic execution of a sentence, the method applies the COMPRESS function over the just modified RSGs. However, before explaining this COMPRESS function, we need to define the C_NODES_RSG one, which identifies the compatible nodes that will later be summarized. This Boolean function just has to check whether or not the first six properties previously described are the same for both nodes (as we said in the previous subsection, the CYCLELINKS property does not affect the compatibility of two nodes). This way
if (TYPE =
(STRUCTURE = STRUCTURE
(SHARED = SHARED (SHSEL = SHSEL (TOUCH = TOUCH
There is a similar function which returns true when two memory locations are compatible. With this, we can finally define as the function which maps all the compatible memory locations into the same node, which happens when they have the same TYPE, STRUCTURE, SHARED and TOUCH properties, and compatible REFPAT, and SPATH properties.
Now, compatible nodes of the same RSG are summarized by the function COMPRESS which does not change the set of pvars, , nor the set of selectors, , in the new . However, the other sets involved in the new composition are:
The set of nodes of the compressed RSG, , will contain the nodes which cannot be summarized with any other plus the nodes resulting from the summarization of compatible nodes. We use the MERGE_COMP_NODES function to generate a summary node from a group of compatible nodes, as we will see later. Formally:
The new set of pvar references, , is basically the same set of the uncompressed RSG, , but which maps all the nodes into the new ones. This is done with the MAP_RSG function which maps the old node into the new node :
The same idea applies to the set of references for the compressed graph:
Regarding the MERGE_COMP_NODES function used for the summarization of several compatible nodes, we define: MERGE_COMP_NODES
takes care of the summarization of nodes and
into node . The properties of this new node, , are set in order
to preserve the description of the data structures represented by the
original nodes. This way, MERGE_NODES
|TYPE = TYPE = TYPE||PosSELOUTset = PosSELOUTset PosSELOUTset|
|SHARED = SHARED = SHARED||PosSELINset = PosSELINset PosSELINset|
|TOUCH = TOUCH = TOUCH||SHSEL = SHSEL = SHSEL|
|SELINset = SELINset SELINset||SELOUTset = SELOUTset SELOUTset|
This means that the new node will have the same TYPE, SHARED, SHSEL, and TOUCH properties which actually should be the same in and to allow the summarization of both nodes. However, the new reference pattern information behaves conservatively. If is an input/output selector in both nodes, and , then it will remain as an input/output selector in the resulting summarized node, . The same happens if is not an input/output selector in both nodes. However, if we are not sure about the selector in one of the original nodes, then the same uncertainty exists regarding the resulting summarized node.
Finally, regarding the CYCLELINKS sets, the resulting node keeps the common cycle links sets from the original nodes, and . In addition, a cycle link, , from one of the nodes, for example, , is also included in the cycle link set of the node if the first selector is not a link selector in the other node, .