next up previous
Next: Node properties Up: Progressive Shape Analysis for Previous: Working example


Reference Shape Graph

First, we need to present the notation used to describe the different memory configurations that may arise when executing a program.

Definition 3.1   We call a collection of dynamic structures a memory configuration. These structures comprise several memory chunks, that we call memory locations, which are linked by references. Inside these memory locations there is room for data and for pointers to other memory locations. These pointers are called selectors.

We represent the memory configurations with the tuple $ M = (L, P, S,
PS, LS)$ where: L is the set of memory locations; P is the set of pointer variables (pvars) used in the program; S is the set of selectors declared in the data structures; PS is the set of references from pvars to memory locations, of the type $ <pvar, l>$, with $ pvar \in P$ and $ l \in L$; and LS is the set of links between memory locations, of the form $ <l_1, sel, l_2>$ where $ l_1 \in
L$ references $ l_2 \in L$ by selector $ sel \in S$. We will use L(m), P(m), S(m), PS(m), and LS(m) to refer to each one of these sets for a particular memory configuration, $ m$.$ \square$

Therefore, we can assume that the RSRSG of a program sentence is an approximation of all possible memory configurations, after the execution of this sentence. However, let us first describe the RSGs now that we know how a memory configuration is defined.

Definition 3.2   An RSG is a graph represented by the tuple $ RSG = (N, P, S, PL,$ $ NL)$ where: N: is the set of nodes. Each node can represent several memory locations if they fulfill certain common properties; P: is the set of pointer variables (pvars) used in the program; S: is the set of declared selectors; PL: is the set of references from pvars to nodes, of the type $ <pvar, n>$ with $ pvar \in P$ and $ n \in N$; and NL: is the set of links between nodes, of the type $ <n_1, sel, n_2>$ where $ n_1 \in N$ references $ n_2 \in N$ by selector $ sel \in S$. We will use N(rsg), P(rsg), S(rsg), PL(rsg), and NL(rsg) to refer to each one of these sets for a particular RSG, $ rsg$.$ \square$

To obtain the RSG which approximates a memory configuration, $ M$, an abstraction function is used, $ F:M \rightarrow RSG$. This function maps memory locations into nodes and references to memory locations into references to nodes at the same time. In other words, $ F$, translates the memory domain into the graph domain. This, function $ F$ comprises three functions: $ F_n :L \rightarrow N$ takes care of mapping memory locations into nodes; $ F_p : PS \rightarrow PL$ maps references from pvars to memory locations into references from pvars to nodes, and $ F_l : LS \rightarrow NL$ maps links between locations into links between nodes.

It is easy to see that: $ F_p(<pvar, l>) = <pvar, n>$ iif $ F_n(l) = n$ and $ F_l(<l_1, sel, l_2>) = <n_1, sel, n_2>$ iif $ F_n(l_1) = n_1 \wedge
F_n(l_2) = n_2$ which means that translating references to locations into references to nodes is trivial after mapping locations into nodes. This translates almost all the complexity involved in function $ F$ to function $ F_n$ which actually maps locations into nodes.



Subsections
next up previous
Next: Node properties Up: Progressive Shape Analysis for Previous: Working example
Rafael Asenjo Plaza 2002-02-19