# Solving shape-analysis problems in languages with destructive updating.

1. INTRODUCTIONThis article concerns the static analysis of programs that perform destructive updating on heap-allocated storage. It addresses problems that can be looked at - depending on one's point of view - as pointer analysis problems, alias analysis problems, sharing-analysis problems, storage analysis problems (also known as shape analysis problems), or typechecking problems. The information obtained is useful, for instance, for generating efficient sequential or parallel code.

Throughout most of the article, we emphasize the application of our work to shape-analysis problems. The goal of shape analysis is to give, for each program point, a conservative, finite characterization of the possible "shapes" that the program's heap-allocated data structures can have at that point. We illustrate our approach by means of a running example in which we apply the shape-analysis technique to a program that uses destructive-updating operations to reverse a list. This example also illustrates the connection between shape analysis and typechecking: it demonstrates how a sufficiently precise shape-analysis algorithm is able to verify that the destructive-reverse program does indeed return a list whenever its argument is a list. The application of our work to pointer-analysis and alias-analysis problems is discussed in Section 7.1.

This article presents a new shape-analysis algorithm. For certain programs - including ones in which a significant amount of destructive updating takes place - the algorithm is able to verify such shape-preservation properties as (1) when the input to the program is a list, the output is also a list and (2) when the input to the program is a tree, the output is also a tree. For instance, the method can determine that "listness" is preserved by (1) a list-reversal program that performs the reversal by destructively updating the input list and (2) a list-insert program that searches a list and splices a new element into the list. Furthermore, the shapeanalysis algorithm is even accurate for certain programs that update cyclic data structures; that is, it is sometimes able to show that when the input to the program is a circular list, the output is also a circular list. For example, the shape-analysis algorithm can determine that an insertion into a circular list preserves "circular listness."

These are rather surprising capabilities. None of the previously developed methods that use graphs to solve shape-analysis problems are capable of determining that "listness" is preserved on these examples (or examples of similar complexity) [Chase et al. 1990; Jones and Muchnick 1981; Larus and Hilfinger 1988; Stransky 1992; Plevyak et al. 1993]. Previous to this article, it was an open question whether such precision could ever be obtained by any method that uses graphs to model storage usage. Furthermore, as far as we know, no other shape-analysis/typechecking method (whether based on graphs or other principles [Choi et al. 1993; Deutsch 1992; Deutsch 1994; Ghiya and Hendren 1996; Hendren 1990; Hendren and Nicolau 1990; Landi and Ryder 1991]) has the ability to determine that "circular listness" is preserved by the list-insert program.

What does our method do that allows it to obtain such qualitatively better results on the above-mentioned programs than previous methods? A detailed examination of the differences between our algorithm and previous algorithms is deferred to Section 8; however, a brief characterization of some of the differences is as follows:

* Several previous methods have used allocation sites to name shape-nodes [Chase et al. 1990; Jones and Muchnick 1982; Plevyak et al. 1993]. Allocation-site information imposes a fixed partition on the memory. In contrast, our approach deliberately drops information about the concrete locations. There is only an indirect connection to the run-time locations: shape-graph nodes are named using a (possibly empty) set of variables. A shape-node named with variable-set X represents run-time locations that are simultaneously pointed to by all (and only) the variables in X.

* Like other shape-analysis methods, our method clusters collections of run-time locations into summary nodes. In our approach, run-time locations that are not pointed to by variables are clustered into a single summary node. [Chase et al. 1990, p.309] observed that their shape-analysis method cannot handle programs such as the list-reversal program because it lacks a way to materialize ("unsummarize") summary nodes at certain key points of the analysis. Our method materializes copies of the summary node (as nonsummary nodes) whenever a pointer variable is assigned a previously summarized run-time location.

* In the analysis of an assignment to a component, say x.cdr := nil, our method always removes x's cdr edges. Previous methods either never remove these edges [Stransky 1992] or use some heuristics to remove such edges only under limited conditions [Chase et al. 1990; Jones and Muchnick 1981; Larus and Hilfinger 1988; Plevyak et al. 1993]. (This unusual characteristic of our method is also a by-product of the node-naming scheme.)

* We use sharing information to increase the accuracy of the primitive operations used by our method. More specifically, we keep track of shape-nodes that represent cons-cells that may be the target of more than one pointer from fields of cons-cells.(1) (Sharing through variables - e.g., when two variables point to the same cons-cell - is represented directly by shape-graph edges.)

When an unshared list is traversed, say via a loop containing an assignment x := x.cdr, the sharing information is used to improve the precision of the materialization operation, which allows the algorithm to determine that x points to an unshared list on every iteration. The limited way in which sharing information is utilized in Chase et al.[1990] and Jones and Muchnick [1981] prevents the methods described in those articles from determining this fact.

* The shape-node names also provide information that sometimes permits the method to determine that a shared node becomes unshared (e.g., this occurs in the program that performs an insertion into a list). With the Chase-WegmanZadeck method, once a node is shared it remains shared forever thereafter. For programs that operate on lists and trees, the non-graph-based method of Hendren [1990] is sometimes able to determine that a shared node becomes unshared. However, Hendren's method does not handle data structures that contain cycles.

An experimental implementation of the shape-analysis method has been created. The examples presented in this article have been prepared with the aid of this implementation.

The remainder of the article is organized as follows. Section 2 provides an overview of the shape-analysis technique. Section 3 introduces the terminology and notation used in the rest of the article. Section 4 presents a concrete collecting semantics for a language with destructive updating, in terms of "shape-graphs" that represent memory states. Section 5 introduces an abstract domain of "static shape-graphs" and shows how they can be used to approximate the sets of shapegraphs that arise in the collecting semantics. Section 6 presents some elaborations and extensions of our basic approach. Section 7 concerns applications of the shapeanalysis method. Section 8 discusses related work. A proof of correctness, showing that the abstract semantics of static shape-graphs is safe with respect to the concrete semantics, is presented in the electronic appendix.

2. AN OVERVIEW OF THE METHOD

The shape-analysis algorithm is presented and proven correct using the framework of abstract interpretation [Cousot and Cousot 1977]. Because pointers, heapallocated storage, and destructive updating are all mechanisms that introduce aliasing, the formal treatment of shape analysis is notationally somewhat formidable. However, many aspects of the shape-analysis algorithm can be understood at an intuitive level. In this section, we give such an overview of the algorithm, using a program that performs a list reversal via destructive updating as a running example.

The list-reversal program is shown in Figure 1. Assuming that variable x initially points to an unshared list (i.e., a possibly empty, acyclic, singly linked list with no shared cons-cells), after each iteration, y points to the reversal of a successively longer prefix of the original list. The shape-analysis algorithm detects (among other things) that at the beginning of each iteration of the loop the following properties hold:

* Invariant (1). Variable x points to an unshared, acyclic, singly linked list.

* Invariant (2). Variable y points to an unshared, acyclic, singly linked list, and variable t may point to the second element of the y-list (if such an element exists).

* Invariant (3). The lists pointed to by x and y are disjoint.

2.1 Static Shape Graphs

The shape-analysis algorithm is based on an abstraction of memory, called a static shape graph (SSG). An SSG is a finite, labeled, directed graph that approximates the actual (or "concrete") stores that can arise during program execution. The shape-analysis algorithm itself is an iterative procedure that computes an SSG at every program point.

In contrast to concrete stores, each SSG in a program is a priori of bounded size. This is achieved by using a single shape-node to represent multiple cons-cells. In general, a shape-node in an SSG has the following properties:

(a) A shape-node [n.sub.Z], where Z [not equal to] [Phi], represents a unique cons-cell in any given concrete store: the cons-cell pointed to by exactly the variables in Z. However, across the collection of SSGs that are the abstractions of the (several different) concrete stores that arise on different loop iterations (or during entirely different executions of the program), [n.sub.Z] will, in general, denote different cons-cells. For example, column two of Figure 2 shows the concrete stores that arise at the beginning of the loop in the list-reversal program when input-list x is a fiveelement list; column three shows the corresponding SSGs. Shape-node [n.sub.{x}] represents the cons-cells [l.sub.1], [l.sub.2], [l.sub.3], [l.sub.4], and [l.sub.5] in the concrete stores that arise on iterations 0, 1, 2, 3, and 4, respectively.

(b) In contrast, shape-node [n.sub.[Phi]] can represent multiple cons-cells of a single concrete store. (Jocularly, we refer to [n.sub.[Phi]] as the "primordial soup.") For example, in the SSG in column three of the iteration-0 row, [n.sub.[Phi]] represents the cons-cells [l.sub.2], [l.sub.3], [l.sub.4], and [l.sub.5] of the concrete store in column two. In the SSG in column three of the iteration-5 row, [n.sub.[Phi]] represents the cons-cells [l.sub.3], [l.sub.2], and [l.sub.1].

(c) In different SSGs, the same cons-cell may be represented by different shapenodes. For instance, consider the SSGs in column three of Figure 2 in topto-bottom order. Cons-cell [l.sub.1] is represented by shape-nodes [n.sub.{x}], [n.sub.{y}], [n.sub.{t}], [n.sub.[Phi]], [n.sub.[Phi]], and [n.sub.[Phi]]; cons-cell [l.sub.3] is represented by [n.sub.[Phi]], [n.sub.[Phi]], [n.sub.{x}], [n.sub.{y}], [n.sub.{t}], and [n.sub.[Phi]]; cons-cell [l.sub.5] is represented by [n.sub.[Phi]], [n.sub.[Phi]], [n.sub.[Phi]], [n.sub.[Phi]], [n.sub.{x}], and [n.sub.{y}].

There is an important conclusion to draw from these properties: it is incorrect to think of a shape-node as representing a fixed partition of memory. Instead, the ideas to keep in mind are the following:

By going from stores to SSGs, we deliberately drop information about the concrete locations, but we keep "aliasing-configuration" information that characterizes cons-cells that are simultaneously pointed to by different sets of variables. A shape-node [n.sub.X] (i.e., with variable-set X) in the shape-graph for program-point p represents the cons-cells that are simultaneously pointed to by all (and only) the variables in X when control reaches p.

(The sets of variable names that represent alias configurations are reminiscent of the alias-configurations tracked by Myers in his algorithm for determining aliasing among (scalar) program variables [Myers 1981].)

2.2 An Explicit Representation of Sharing

An examination of the iteration-0 row of Figure 2 may lead the reader to think that acyclic structures are abstracted to cyclic structures (and hence that the abstraction cannot distinguish between cyclic and acyclic structures). In fact, although SSGs are "cyclic" - in the sense that there are nodes with paths to themselves - there is an additional component of SSGs that distinguishes the abstractions of cyclic concrete structures from the abstractions of acyclic concrete structures. In particular, each shape-node n in an SSG has an associated Boolean flag, denoted by [is.sup.[sharp]](n), that, when true, indicates that the cons-cells represented by n may be the target of pointers emanating from two or more distinct cons-cell fields ("[is.sup.[sharp]]" stands for "is-shared"). Edges from variables do not contribute to [is.sup.[sharp]] status: [is.sup.[sharp]] captures a notion of "heap shared"; sharing through variables is represented explicitly by edges from variables to shape-nodes.

The SSG in column three of the iteration-0 row of Figure 2 illustrates an important aspect of the abstraction from concrete stores to SSGs: because all nodes in the tail of an acyclic list are represented by summary-node [n.sub.[Phi]], the abstraction of a list (deliberately) loses information about the length of the list. In this way, we achieve a bounded-size abstract representation and hence a terminating abstract semantics.

The significance of [is.sup.[sharp]](n) = false is that if several car and cdr edges in an SSG point to n, they represent concrete edges that never point to the same cons-cell in any concrete store that the SSG represents. For example, in the SSG in column three of the iteration-0 row of Figure 2, because [is.sup.[sharp]]([n.sub.[Phi]]) = false, the two cdr edges from [n.sub.{x}] to [n.sub.[Phi]] and from [n.sub.[Phi]] to [n.sub.[Phi]] cannot represent edges that point to the same cons-cell in any concrete store that this SSG represents. Thus, despite the fact that this SSG contains a cycle, it only represents acyclic concrete stores.

An examination of the iteration-3 row of Figure 2 may lead the reader to think that disjoint lists are abstracted to shared lists (and hence that the abstraction cannot distinguish between disjoint lists and shared lists). However, the [is.sup.[sharp]] values come to the rescue here, too. Because [is.sup.[sharp]]([n.sub.[Phi]]) = false, we know that the two cdr edges from [n.sub.{x}] to [n.sub.[Phi]] and from [n.sub.{t}] to [n.sub.[Phi]] cannot point to the same cons-cell in any concrete store. Consequently, the abstraction captures the fact that at the beginning of iteration 3, the lists pointed to by x and t are disjoint. Thus, despite the fact that the tails of the x-list and the t-list are both represented by [n.sub.[Phi]], the SSG only represents concrete stores in which the x-list and the t-list do not share any cons-cells in common.

2.3 An Iterative Algorithm

The shape-analysis method is an iterative algorithm that computes an SSG for every point in the program. The algorithm operates over the domain of SSGs, with each statement in the program having an associated SSG-to-SSG transformer. The shape-analysis algorithm is conservative with respect to the collection of stores that can actually arise during any execution:

* The SSG computed for a program point by the algorithm may have more shapenodes and edges than the SSG obtained by abstracting the collection of stores that can actually arise during execution.

* The SSG for a program point p might have [is.sup.[sharp]](n) = true even though, in the concrete stores that arise at p, none of the cons-cells that n represents are the target of pointers emanating from two or more distinct cons-cell fields.

For the reverse program from Figure 1, the shape-analysis algorithm uses four iterations over the program to compute the final SSGs. The SSGs that arise at each program point during the analysis are shown in Figure 3. These will be used below, in Section 2.4, to explain how the algorithm is able to establish information about the possible "shapes" that heap-allocated structures in a program can take on. (For space reasons, only the SSGs for statements in the loop body are shown. In all of these SSGs, [is.sup.[sharp]] is false for all of the shape-nodes.)

2.4 What the Shape-Analysis Algorithm Achieves and Why

We now consider the main reasons why the shape-analysis algorithm is able to produce accurate information about the list-reversal program. In particular, we wish to give a feeling for why the algorithm is able to establish the three invariants mentioned at the beginning of Section 2.

There are three key aspects of the algorithm that contribute to the successful outcome of the analysis of the list-reversal program. Each of them can be illustrated by the SSG transformations carried out by the algorithm during its third iteration over the program (see the iteration-3 column of Figure 3.)

2.4.1 Tracking of Aliasing Configurations. One aspect involves the tracking of aliasing configurations via the "names" attached to shape-nodes. This is illustrated by the SSG transformation carried out at the statements "t := y" and "y := x" during the third iteration, in particular, when the statement "t := y" is analyzed, thus producing the second SSG in column 3 of Figure 3 from the first SSG. There are two issues: (1) the "liquidization" of [n.sub.{t}] and (2) the "renaming" of [n.sub.{y}].

When "t := y" is encountered in the third iteration, t points to [n.sub.{t}], which is also pointed to by [n.sub.{y}].cdr. This represents a concrete store in which y is the only variable pointing to a cons-cell [l.sub.y], and [l.sub.y].cdr points to a cons-cell [l.sub.t], which is pointed to by t (and no other variable). After the assignment "t := y", [l.sub.t] is not pointed to by any variable, and both t and y point to [l.sub.y]. The appropriate SSG to represent this store is obtained by "liquidizing" [n.sub.{t}]: to model the fact that variable t no longer points to [l.sub.t], we remove t from the "name" of [n.sub.{t}]; because this turns the "name" of the shape-node into [Phi], it is merged with shape-node [n.sub.[Phi]], which already has the "name" [Phi]. (By this, [n.sub.{t}] is "liquidized" and falls into the primordial soup.)

In addition, to model the fact that variable t now points to [l.sub.y], we add t to the "name" of [n.sub.{y}], renaming [n.sub.{y}] to [n.sub.{t,y}]. Therefore, after statement "t := y" there is a cdr edge from [n.sub.{t,y}] to [n.sub.[Phi]] (and there is no longer any shape-node known as [n.sub.{y}]).

Executing the statement "t := y" cannot increase the amount of "sharing" in any concrete store. That is, it cannot increase the number of cons-cells that are the target of pointers emanating from two or more distinct cons-cell fields. This is reflected in the SSG by the fact that [is.sup.[sharp]] is still false for all shape-nodes in the new SSG. Thus, despite the fact that the tails of the x-list and y-list are both represented by [n.sub.[Phi]], the SSG captures the fact that the lists pointed to by y and x remain disjoint. (See Invariant (3) and the discussion in Section 2.2)

Similarly, when the statement "y := x" is processed (to produce the third SSG from the second SSG), [n.sub.{t,y}] is renamed to [n.sub.{t}], and [n.sub.{x}] is renamed to [n.sub.{y,x}]. (The use of sets of variables to name the nodes in SSGs can result in an exponential number of shape-nodes. Techniques to sidestep this problem are discussed in Section 6.2.)

2.4.2 "Materialization" of [n.sub.{x}] from [n.sub.[Phi]]. Equally important is the way the algorithm handles the advancement of x down the x-list by "x := x.cdr" (to produce the fourth SSG from the third SSG).

When "x := x.cdr" is encountered in the third iteration, x and y point to shapenode [n.sub.{y,x}], and the cdr field of [n.sub.{y,x}] points to summary-node [n.sub.[Phi]]. Because [is.sup.[sharp]]([n.sub.[Phi]]) = false, this represents a concrete store in which x and y point to a conscell [l.sub.0], and the cdr field of [l.sub.0] points to an unshared cons-cell [l.sub.1], which may, in turn, point to an unshared, acyclic, singly linked list (made up of [l.sub.2], [l.sub.3], etc.). After the assignment, only y points to [l.sub.0]; x points to [l.sub.1] (and [l.sub.2], [l.sub.3], etc. are still not pointed to by any variable). The appropriate SSG to represent this store has shape-nodes [n.sub.{y}], [n.sub.{x}], [n.sub.{t}], and [n.sub.[Phi]] as shown in the fourth SSG in column 3 of Figure 3.

The effect has been to "materialize" a new nonsummary shape-node [n.sub.{x}] from summary-node [n.sub.[Phi]]. (We say that "the operation 'x := x.cdr' ladles a node out of the primordial soup.")

Materialization creates an SSG that conservatively covers all the possible new configurations of storage. For example, had [is.sup.[sharp]]([n.sub.[Phi]]) been true in the third SSG, as it is in column two of Figure 4, then there would have been three additional cdr edges: from [n.sub.{x}] to [n.sub.{x}], from [n.sub.{t}] to [n.sub.{x}], and from [n.sub.[Phi]] to [n.sub.{x}]. (When we ladle a node from the primordial soup, and [is.sup.[sharp]]([n.sub.[Phi]]) = true, we refer to edges like these as "bits of algae" attached to [n.sub.{x}].)

2.4.3 Cutting the List. In the analysis of "y.cdr := t" (which produces the fifth SSG from the fourth SSG), the cdr edge of shape-node [n.sub.{y}] (which points to [n.sub.{x}] in the fourth SSG) is first removed. This cuts the y list at the head, separating the first element, [n.sub.{y}], from the tail, which x points to. A cdr edge from [n.sub.{y}] to [n.sub.{t}] is then added, which concatenates shape-node [n.sub.{y}] at the head of the list that t points to.

Other shape-analysis algorithms handle a statement of the form "y.cdr := t" much more conservatively: they do not, in general, remove the cdr edges emanating from the shape-nodes that y points to.(2) Instead, they retain the old edges and add cdr edges from the shape-node that y points to, to the shape-node that t points to.

The reason our shape-analysis algorithm is able to do a better job is because it conservatively tracks all the possible aliasing configurations via the "names" attached to shape-nodes: a shape-node [n.sub.Z] in the shape-graph for program-point p represents the cons-cells that are simultaneously pointed to by exactly the variables in Z when control reaches p. If y is in the name of shape-node [n.sub.Z] (i.e., if y [element of] Z), then [n.sub.Z] represents only concrete cons-cells whose cdr field will definitely be overwritten. Therefore, in the interpretation of "y.cdr := t," our method can always replace the cdr edges of all shape-nodes that y points to by edges to the shape-nodes that t points to. (In the fourth SSG in column 3 of Figure 3, there is only a single shape-node that y points to (namely [n.sub.{y}]), and a single shape-node that t points to (namely [n.sub.{t}]).)

In the shape analysis of the list-reversal program, there is a crucial interaction between these three aspects. Suppose, for example, that in the SSG transformation for "x := x.cdr," shape-node [n.sub.{x}] was not materialized out of [n.sub.[Phi]], but instead variable x was merely set to point to [n.sub.[Phi]]. (This is essentially what other shapeanalysis algorithms do, but expressed in our terminology.) At "y.cdr := t," the removal of y's cdr edge would still cut the y-list at the head, separating the node that y points to (i.e., [n.sub.{y}]) from the list pointed to by x (which in this case would be represented by [n.sub.[Phi]].). However, when the cdr edge from [n.sub.{y}] to [n.sub.{t}] is added to the SSG, this sets y's cdr field to t, whose cdr field points to [n.sub.[Phi]], which is what x points to. At this stage, the information that the x-list and the y-list are disjoint has been lost!

Note how differently things turn out when [n.sub.{x}] is materialized from [n.sub.[Phi]] at "x := x.cdr." At "y.cdr := t," x points to [n.sub.{x}], and thus when y's cdr field is set to [n.sub.{t}] (whose cdr field points to [n.sub.[Phi]]), x does not point to [n.sub.[Phi]]. Although [n.sub.[Phi]] occurs in both the tail of x and the tail of y, because [is.sup.[sharp]]([n.sub.[Phi]]) = false we know that the two lists do not share any cons-cells in common; that is, x and y must point to disjoint acyclic lists.

The operations discussed above - assigning a pointer to a pointer, advancing a pointer down a list, and cutting a list - are three of the five main operations of list-manipulation algorithms. The fourth and fifth common list-manipulation operations - splicing a new element into a list and removing an element from a list - can, in many cases, be handled accurately by our shape-analysis algorithm, even if shape-nodes temporarily become shared! (This is not illustrated by the list-reversal program, but is discussed in Section 5.5.) This points up the strength of our approach: our algorithm handles all five of the basic list-manipulation operations with a remarkable degree of precision, as well as similar tree- and circular-list-manipulation operations.

3. TERMINOLOGY AND NOTATION

A program is represented by a control-flow graph G = (V, A), where V is the set of vertices, and A [subset or equal to] V x V is the set of arcs. G has a unique start vertex, which we assume has no predecessors. The other vertices of the control-flow graph represent the statements and predicates of the program in the usual way; st(v) denotes the statement or predicate of vertex v.

To simplify the formulation of the analysis method, it will be stated for a single fixed (but arbitrary) program. The set of pointer variables in this program will be denoted by PVar.

3.1 Normalization Assumptions

For expository convenience, we will assume that programs have been normalized to meet the following conditions:

* Only one constructor or selector is applied per assignment statement.

* An expression cons(x, y) is executed in three steps: (1) an uninitialized cons cell is allocated, and its address is assigned into a new temporary variable (e.g., "temp := new"); (2) the car component of temp is initialized with the value of x ("temp.car := x"); (3) the cdr component of temp is initialized with the value of y ("temp. cdr := y").

* All allocation statements are of the form x := new, (as opposed to x.sel := new).

* In each assignment statement, the same variable does not occur on both the left-hand and right-hand side.

* Each assignment statement of the form lhs := rhs in which rhs [not equivalent to] nil is immediately preceded by an assignment statement of the form lhs := nil.

* An assignment statement of the form temp := nil is placed at the end of the program for each temporary variable temp introduced as part of normalization.

Thus, for every vertex v [element of] V in which a pointer manipulation is performed, st(v) has one of the following forms: x := nil, x.sel := nil, x := new, x := y, x := y.sel, or x.sel := y, where y [not equivalent to] x. (In our implementation, the work of putting a program into a form that meets these assumptions is carried out by a preprocessor.) Note that the number of temporary variables that are introduced to meet these restrictions is, in the worst case, linear in the size of the original program.

The normalization assumptions are not essential, but simplify the presentation. For example, the next-to-last assumption allows the semantics to treat the "kill" aspects of a statement (e.g., x := nil) separately from the "gen" aspects (e.g., x := y.sel, assuming that x's value is nil). [ILLUSTRATION FOR FIGURES 6, 8, AND 9 OMITTED].

Example 3.1.1. Figure 5 shows (a) the normalized version of the list-reversal program and (b) the control-flow graph of the program in normalized form.

3.2 Shape-Graphs

Both the concrete and abstract semantics are defined in terms of a single unified concept of "shape-graph," which is defined as follows:

Definition 3.2.1. A shape-graph is a finite directed graph that consists of two kinds of nodes - variables (i.e., PVar) and shape-nodes - and two kinds of edges - variable-edges and selector-edges. A shape-graph is represented by a pair of edge sets, <[E.sub.v], [E.sub.s]>, where

* [E.sub.v] is the graph's set of variable-edges, each of which is denoted by a pair of the form [x, n], where x [element of] PVar and n is a shape-node.

* [E.sub.s] is the graph's set of selector-edges, each of which is denoted by a triple of the form <s, sel, t>, where s and t are shape-nodes, and sel [element of] {car, cdr}.

We overload the symbol [E.sub.v] to also mean the function that, when applied to a variable x, returns x's [E.sub.v] successors. That is, for x [element of] [P.sub.Var], we define [E.sub.v](x) to be [Mathematical Expression Omitted]. Similarly, for a shape-node s and sel [element of] {car, cdr}, we define [E.sub.s](s, set) to be [Mathematical Expression Omitted]. (The intended meaning of a use of [E.sub.v] or [E.sub.s] will always be clear, according to whether arguments are supplied or not.) Given SG = <[E.sub.v],[E.sub.s]>, we define shape_nodes(SG) as follows: [Mathematical Expression Omitted]. The class of shape-graphs is denoted by SG.

Note that for a given shape-graph SG, shape_nodes(SG) is uniquely defined: it consists of the set of nonisolated nodes in SG (i.e., the nodes that are touched by at least one edge). It is for this reason that we do not explicitly list the node set when specifying a shape-graph. (For the sake of simplicity, we choose not to work with a definition of shape_nodes(SG) that removes unreachable nodes.)

Remark. We will systematically use the terms "nodes" and "edges" when referring to elements of shape-graphs, and "vertices" and "arcs" when referring to elements of control-flow graphs. In general, properties of (or operations on) the shape-graphs used to define the abstract semantics will be superscripted with [sharp]; those used to define the concrete semantics have no superscript.

The shape-graphs that arise in the concrete semantics for the language have somewhat different characteristics from the ones that arise in the abstract semantics. However, the fact that both are defined from a shared root concept (namely, Definition 3.2.1) helps in defining the abstraction relation that relates them (see Definition 5.2.1).

In the concrete semantics, which is given in Section 4, the result of an execution sequence is a shape-graph that represents the state of heap-allocated storage in memory. In this case, each shape-node represents a unique cons-cell, and for each variable x, either [E.sub.v](x) is a singleton set (say {n}), or it is empty. Furthermore, [E.sub.s](n, car) and [E.sub.s] (n, cdr), which represent the cons-cells pointed to by the car and cdr fields of n, are also either singleton sets or empty (depending on whether these fields point to allocated cons-cells or not). Such properties are captured in the following definition:

Definition 3.2.2 (Deterministic Shape-Graphs). A shape-graph is deterministic if (1) for every x [element of] PVar, [absolute value of [E.sub.v](x)] [less than or equal to] 1, and (2) for every shape-node n and sel [element of] {car, cdr}, [absolute value of [E.sub.s](n, sel)] [less than or equal to] 1. The class of deterministic shape-graphs is denoted by DSG.

The concrete semantics will treat statements as "deterministic-shape-graph transformers." In contrast, in Section 5.3, the abstract semantics will use nondeterministic shape-graphs to model (conservatively) the state of heap-allocated storage. In nondeterministic shape-graphs, quantities such as [E.sub.v] (x), [E.sub.s] (n, car), and [E.sub.s] (n, cdr) may each yield a set with more than one shape-node.

4. THE CONCRETE SEMANTICS

In this section, we present a concrete semantics in which deterministic shape-graphs are used to represent the state of memory and in which the meaning of an assignment statement is a deterministic-shape-graph transformer. This concrete semantics is used to define a concrete collecting semantics that associates a set of possible concrete stores with each point in the program.

Figure 6 contains the semantic equations of the concrete semantics. The meaning of a statement st is a function [[st]]:DSG [approaches] DSG. (When examining the last four equations in Figure 6, bear in mind that, because of the Normalization Assumptions of Section 3.1, before each of the statements executes it is known that the value of the left-hand side is nil. Thus, the last four equations need only handle the "gen" aspects of the statements' semantics. The "kill" aspects are handled by the first two equations of Figure 6.) The DSG transformers listed in Figure 6 cover the six kinds of pointer-manipulation statements; all the other DSG transformers - for predicates and for assignment statements that do not perform any pointer manipulations - are the identity function.

By design, the "concrete" semantics is somewhat nonstandard in the following ways:

* The only parts of the store that the concrete semantics keeps track of are the pointer variables and the cons-cells of heap-allocated storage.

* Rather than causing an "abnormal termination" of the program, dereferences of nil pointers and uninitialized pointers are treated as no-ops.(3)

* The concrete semantics does not interpret predicates, read statements, and assignment statements that do not perform pointer manipulations.

These assumptions build a small amount of abstraction into the "concrete" semantics. The consequence of these assumptions is that the collecting semantics may associate a control-flow-graph vertex with more concrete stores (i.e., DSGs) than would be the case were we to start with a conventional concrete semantics. (These assumptions are patently safe, so we will not take the space here to justify them further.)

We now turn to the collecting semantics. For a control-flow-graph vertex v [element of] V, let pathsTo(v) be the set of paths in the control-flow graph from start to predecessors of v.

Definition 4.1. The collecting semantics cs: V [approaches] [2.sup.DSG] is defined as follows:

[Mathematical Expression Omitted]

The value of cs(v) represents (a superset of) the concrete stores that could arise just before vertex v is executed.

Equationally, the collecting semantics can be defined as the least fixed point (under set inclusion) of the following system of equations in [CS.sub.v], for v [element of] V:

[Mathematical Expression Omitted] (1)

5. THE ABSTRACT SEMANTICS

In this section, we present a shape-analysis technique that uses a restricted subset of shape-graphs to characterize the possible shapes that heap-allocated storage can take on.

Static shape-graphs (or SSGs, for short) are defined in Section 5.1; the abstraction function is defined in Section 5.2; and the abstract semantics is given in Section 5.3. The reverse program is used as a running example in these sections. Section 5.4 discusses an interesting aspect of how the abstract semantics treats statements of the form "x.sel := nil." Section 5.5 considers a second example program - a list-insertion program that may insert a cons-cell at an arbitrary point in a linked list - and shows that the shape-analysis method is capable of determining that when the argument is an unshared acyclic list, the result is also an unshared acyclic list.

5.1 Static Shape-Graphs

Unlike the concrete stores of the collecting semantics (i.e., DSGs), the SSGs of the abstract semantics are nondeterministic: [E.sub.v](x), [E.sub.s](n, car), and [E.sub.s](n, cdr) may each yield a set with more than one shape-node. In addition, and again in contrast with DSGs, the SSGs for a given program are a priori of bounded size. This is achieved by our naming scheme for shape-nodes: the name of a shape-node is a (possibly empty) set of program variables. In general, the abstraction function clusters infinitely many concrete cons-cells (from an infinite set of finite DSGs) into a single SSG shape-node.

Definition 5.1.1. A static shape-graph is a pair <[SG.sup.[sharp]], [is.sup.[sharp]]>, where

* [SG.sup.[sharp]] is a shape-graph,

* the set shape_nodes([SG.sup.[sharp]]) is a subset of {[n.sub.X] [where] X [subset or equal to] PVar}, and

* [is.sup.[sharp]] is a function of type shape_nodes([SG.sup.[sharp]]) [approaches] {false, true}.

The class of static shape-graphs is denoted by SSG.

In the following definition, we impose an order on SSGs where [Mathematical Expression Omitted] if [Mathematical Expression Omitted] contains at least the edges of [Mathematical Expression Omitted]:

Definition 5.1.2. Let [Mathematical Expression Omitted] and [Mathematical Expression Omitted]. We define the following ordering on SSG: [Mathematical Expression Omitted] if and only if all of the following conditions hold:

* [Mathematical Expression Omitted]

* [Mathematical Expression Omitted]

* For every n [element of] shape-nodes([SG.sup.[sharp]]), [Mathematical Expression Omitted].

The domain SSG is a complete join semi-lattice with a join operator [union] defined by

[Mathematical Expression Omitted].

5.2 The Abstraction Function

Our task in this section is to define the abstraction function that relates the domains [2.sup.DSG] and SSG. The abstraction function [Alpha] is defined in Definition 5.2.1; [Alpha] is defined in terms of the auxiliary functions [Pi], which establishes the relationship between the nodes of a DSG and their corresponding nodes in the SSG, and [Beta], which is an overloaded symbol denoting a family of functions defined inductively on the structure of elements that make up a DSG.

Definition 5.2.1 (The Abstraction Function). Let SG = <[E.sub.v], [E.sub.s> be a shape-graph in DSG, and let l, [l.sub.1], and [l.sub.2] be shape-nodes in shape_nodes(SG). The function [Pi][[E.sub.v]](l), from shape_nodes(SG) to [2.sup.PVar], identifies the set of variables that point to a given cons-cell l. It is defined as follows:

[Mathematical Expression Omitted].

(When [E.sub.v] is understood, we will write [Pi][[E.sub.v]](l) as [Pi](l).)

The function iis[[E.sub.s]](l), from shape_nodes(SG) to {false, true}, checks whether a cons-cell l is the target of pointers emanating from two or more distinct cons-cell fields ("iis" stands for "induced-is-shared"). It is defined as follows:

[Mathematical Expression Omitted].

(When [E.sub.s] is understood, we will write iis[[E.sub.s]](l) as iis(l).)

The collection of functions [Beta][[E.sub.v]] (abbreviated as [Beta] in all but the last case below) is defined as follows:

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

The abstraction function [Alpha]: [2.sup.DSG] [approaches] SSG is defined by

[Mathematical Expression Omitted].

The core components of Definition 5.2.1 are the operations [Pi][[E.sub.v]](l) and [Beta](l) = [n.sub.[Pi]][[E.sub.v]](l). The function [Pi][[E.sub.v]](l) establishes the relationship between a DSG shape-node l and the name of the SSG shape-node that represents l. For example, consider the iteration-0 row of Figure 2. In column two, DSG node [l.sub.1] is pointed to by variable x and is mapped by [Beta] to SSG node [Beta]([l.sub.1]) = [n.sub.[Pi][[E.sub.v]]([l.sub.1])] = [n.sub.{x}] (see column three). DSG nodes [l.sub.2], [l.sub.3], [l.sub.4], and [l.sub.5], which are not pointed to (directly) by any variables, are mapped by [Beta] to SSG node [n.sub.[Phi]]. In general, [Pi][[E.sub.v]] generates a finite set of SSG node names from the a priori unbounded number of DSG nodes in the DSGs in S. Auxiliary function [Beta] then collapses SG onto the smaller set of nodes, while preserving many aspects of SG's structure. We say that an SSG shape-node n represents a DSG shape-node l in SG = <[E.sub.v], [E.sub.s]> if [Beta][[E.sub.v]](l) = n.

The function iis[[E.sub.s]](l) checks whether a cons-cell l is the target of pointers emanating from two or more distinct cons-cell fields. Because of the indexed-or performed with respect to the set of cons-cells that [Beta] maps to [n.sub.X], [is.sup.[sharp]]([n.sub.X]) is true if any of the cons-cells in SG that [n.sub.X] represents is the target of pointers emanating from two or more distinct cons-cell fields in SG. (This aspect of [Beta] and [Pi][[E.sub.v]] is not illustrated by the SSGs that appear in Figure 2.) On the other hand, if [Beta] sets [is.sup.[sharp]]([n.sub.X]) to false, this means that the cons-cell (or cells) that [n.sub.X] represents all have at most one predecessor. For example, consider the iteration-0 row of Figure 2. In the SSG in column three, [n.sub.[Phi]] represents the cons-cells [l.sub.2], [l.sub.3], [l.sub.4], and [l.sub.5], each of which has exactly one predecessor in the DSG shown in column two. Consequently, [is.sup.[sharp]]([n.sub.[Phi]]) = false.

In Section 5.3 and the electronic appendix, it is convenient to work with an alternative, but equivalent, definition of iis[[E.sub.s]]:

Definition 5.2.2.

[Mathematical Expression Omitted]

It may not be immediately apparent why sharing information is represented explicitly in SSGs. The reason is that only very conservative information about sharing could be inferred directly from an SSG if there was no explicit [is.sup.[sharp]] function. For example, without the [is.sup.[sharp]] function, it would not be possible to distinguish acyclic lists from cyclic lists. Suppose that [SG.sup.[sharp]] is an SSG that arises from an application of abstraction-function [Alpha] to DSG SG, and suppose that n is a shape-node of [SG.sup.[sharp]] that represents a shared shape-node 1 of SG. Not only is [is.sup.[sharp]](n) = true, but one or more of the following conditions must hold in [SG.sup.[sharp]]:

* There exists a selector-edge from [n.sub.[Phi]] to n. This reflects the fact that [n.sub.[Phi]] can represent multiple cons-cells, and thus the single SSG edge <[n.sub.[Phi]], sel, n> can represent two or more selector-edges in SG.

* There exist two selector-edges to n from different SSG shape-nodes, say, [n.sub.[Z.sub.1]] and [n.sub.[Z.sub.2]], where [Z.sub.1] [intersection] [Z.sub.2] = [Phi]. In this case, the two SSG edges represent two different selector-edges to l in SG - one from the cons-cell pointed to by the set of variables [Z.sub.1] and one from the cons-cell pointed to by the set of variables [Z.sub.2].

* There exist two selector-edges to n, with different selectors, from a single shapenode in [SG.sup.[sharp]]. In this case, the two SSG edges represent two different selectoredges in SG.

The reason why explicit sharing information is maintained in SSGs is that the converse of the above observation need not hold. For example, in the SSG in column three of the iteration-0 row of Figure 2, there exist two selector-edges to [n.sub.[Phi]] from different shape-nodes, [n.sub.[Phi]] (i.e., [n.sub.[Z.sub.1]]) and [n.sub.{x}] (i.e., [n.sub.[Z.sub.2]]) such that [Z.sub.1] [intersection] [Z.sub.2] = [Phi] [intersection] {x} = [Phi]. However, the value of [is.sup.[sharp]]([n.sub.[Phi]]) is false. (The fact that [is.sup.[sharp]]([n.sub.[Phi]]) = false is what indicates that [n.sub.[Phi]]'s incoming edges represent edges that never point to the same cons-cell in any concrete store.)

As defined in Definition 5.2.1, the abstraction of a set of DSGs S results in a single SSG, [Alpha](S). Even though abstraction function [Alpha] combines information from several applications of [Beta], we can sometimes recognize that particular pairs of elements in an SSG represent features that can only come from different DSGs. In particular, a shape-node [n.sub.Z] represents cons-cells that are simultaneously pointed to by all (and only) the variables in Z. In a given DSG, each program variable points to at most one cons-cell. Therefore, two different shape-nodes [n.sub.X] and [n.sub.Y], such that X [not equal to] Y and X [intersection] Y [Phi], represent incompatible configurations of variables: they cannot possibly represent cons-cells that are in the same DSG. This means that the following structural property holds for an SSG [Mathematical Expression Omitted] that arises from an application of abstraction function [Alpha]:

Compatibility of Edge End-Points: For all [Mathematical Expression Omitted], either X = Y or X [intersection] Y = [Phi].

Example 5.2.3. For example, in the SSG at the top of column two in Figure 11, the selector-edge <[n.sub.{y}], cdr, [n.sub.{t}]> satisfies {y} [intersection] {t} = [Phi]. This SSG could not contain any of the following selector-edges: <[n.sub.{x}], car, [n.sub.{x,[t.sub.1]}]>, <[n.sub.{x}], cdr, [n.sub.{x,[t.sub.1]}]>, <[n.sub.{x,[t.sub.1]}]>, car, [n.sub.{x}]>, and <[n.sub.{x,[t.sub.1]}], cdr, [n.sub.{x}]>.

The SSG transformers of the abstract semantics make use of several properties similar to the "compatibility-of-edge-end-points" property to determine that certain combinations of shape-node elements cannot possibly coexist in the same concrete store [ILLUSTRATION FOR FIGURES 10 AND 12 OMITTED]. This is one of the key reasons why our shape-analysis method is able to carry out accurate "node materialization" on many programs (and consequently why it is more precise than competing methods on many of these programs).

Because abstraction function [Alpha] distributes over [union] (i.e., union of sets of DSGs), the unique concretization function [Gamma] such that [Alpha] and [Gamma] form a Galois connection can be defined as follows:

Definition 5.2.4 (The Concretization Function). Let [SG.sup.[sharp]] be a shape-graph in SSG. Concretization function [Gamma]:SSG [approaches] [2.sup.DSG] is defined as follows:

[Mathematical Expression Omitted].

A data type is a collection of DSGs. Definition 5.2.4 provides a way for certain data types, including linked lists, trees, and arbitrary graphs, to be characterized by SSGs:

Definition 5.2.5. Let [SG.sup.[sharp]] be a shape-graph in SSG. [SG.sup.[sharp]] characterizes the data type [Gamma]([SG.sup.[sharp]]).

Example 5.2.6. Figures 7(a)-(e) show the shape-graphs that characterize five kinds of data types.

The shape-analysis algorithm is conservative with respect to the concrete semantics, and thus the shape-graphs produced may have superfluous edges. Therefore, when the shape-analysis algorithm reports that a variable points to a circular list, it may actually point to a noncircular list; however, when the algorithm reports that a variable points to a noncircular list, it will never point to a circular list. This kind of conservative approximation is appropriate for use, for example, in parallelizing compilers [Hendren and Gao 1992; Hendren et al. 1992]. (An extension of our basic technique allows SSGs to characterize some kinds of definitely circular data types, including definitely circular lists. See Section 6.3.)

Remark. The reader may wonder why we do not use an abstraction function that uses a set of SSGs to represent the set of stores that can arise at a control-flow-graph vertex, such as

[Mathematical Expression Omitted].

Using such an abstraction function would have certain advantages:

* In general, it would lead to a shape-analysis algorithm that is more accurate than the method described in this article.

* It would allow us to give simpler definitions for the transfer functions of the abstract semantics [ILLUSTRATION FOR FIGURES 8 AND 9 OMITTED]. In particular, there would be no need to use the compatibility-of-edge-end-points property.

However, our belief is that an approach based on a set of SSGs per control-flowgraph vertex is not likely to be feasible in practice. The number of shape-nodes associated with a single control-flow-graph vertex can grow to be very large - in the worst case, doubly exponential in the number of program variables (i.e., [2.sup.2[absolute value of PVar]]). Using a single SSG per control-flow-graph vertex avoids the space blowup.(4) In addition, the operations needed by a fixed-point-finding algorithm - join of SSGs, equality of SSGs, and applications of the transfer functions of the abstract semantics - can usually be carried out more efficiently for a method based on one SSG per vertex. For these reasons, we believe that the use of a single SSG per vertex is more likely to provide a practical shape-analysis algorithm and that the additional notational complexity required to define the transformers of the abstract semantics is warranted.

5.3 The Abstract Interpretation

The abstract meaning function [[[]].sup.[sharp]: SSG [approaches] SSG for the pointer-manipulation statements is given in Figures 8 and 9. The operations presented in Figures 8 and 9 manipulate variable-edges, selector-edges, and sharing information, as well as the alias information that is maintained in the shape-node names of SSGs. As we shall see, this meaning function is conservative with respect to the concrete semantics defined in Figure 6 (see Theorems 5.3.6 and 5.3.7).

The key property of the abstract semantics is that each abstract assignment operation creates an SSG that conservatively covers all the possible new configurations of variable sets whose members all point to the same cons-cell (i.e., DSG shapenode). The formal definition of the abstract semantics, given in Figures 8 and 9, uses two basic mechanisms:

* In many of the cases, the "names" of SSG shape-nodes are adjusted by performing operations on the variable sets that "name" SSG shape-nodes, e.g., [n.sub.Z] becomes [n.sub.Z[union]{x}] or [n.sub.Z-{x}].

* The cases of the abstract semantics use "abstract predicates" over SSG shapegraph elements. These provide safe tests for corresponding "concrete predicates" on DSG shape-graphs.

Figure 10 lists four of the abstract predicates that are used in the abstract semantics and the corresponding concrete predicates.

Each of the abstract predicates [p.sup.[sharp]] in Figure 10 has the property that if the concrete property p holds on the elements of a given DSG SG, then [p.sup.[sharp]] holds on the corresponding elements of [Beta](SG). Therefore, the abstract semantics can use [p.sup.[sharp]] = false as a safe test of whether p holds on the corresponding elements in any of the DSGs in [Gamma]([SG.sup.[sharp]]): if [p.sup.[sharp]] equals false (on specific elements of an SSG [SG.sup.[sharp]]), then p does not hold on the corresponding elements in any of the DSGs in [Gamma]([SG.sup.[sharp]]). For example, when [Mathematical Expression Omitted] does not hold, we conclude that iis[[E.sub.s]] does not hold on any of the cons-cells represented by [n.sub.X] (i.e., none of the cons-cells represented by [n.sub.X] are shared). In the SSG transformer for a statement of the form "x.sel := nil," which removes the selector-edges emanating from all shape-nodes [n.sub.X] with x in their name, the abstract semantics can determine whether it is safe to set [is.sup.[sharp]]([n.sub.X]) to false by testing the value of [iis.sup.[sharp]]([n.sub.X]).

This relationship is captured by the following lemma about the properties listed in Figure 10:

LEMMA 5.3.1. Let SG = <[E.sub.v],[E.sub.s]> be some DSG in DSG; let l, [l.sub.1], [l.sub.2], . . ., [l.sub.n] be shape-nodes in shape_nodes(<[E.sub.v],[E.sub.s]>); and let [Beta] denote [Beta][[E.sub.v]].

(1) compatible([l.sub.1], . . ., [l.sub.n]) [implies] [compatible.sup.[sharp]]([Beta]([l.sub.1]), . . ., [Beta]([l.sub.n])).

(2) [l.sub.1] = [l.sub.2] [implies] [Beta]([l.sub.1] = [sharp] [Beta]([l.sub.2])

(3) [l.sub.1] [not equal to] [l.sub.2] [implies] [Beta]([l.sub.1]) [not equal to] [sharp] [Beta]([l.sub.2])

(4) iis[[E.sub.s]](l) [implies] [iis.sup.[sharp]][[Beta]([E.sub.s])]([Beta](l))

PROOF. The abstract properties are derived from the concrete ones using the following observations:

(1) A shape-node [n.sub.Z] represents cons-cells that are simultaneously pointed to by all (and only) the variables in Z. In a given DSG, each program variable points to at most one cons-cell. Consequently, two different shape-nodes [n.sub.[Z.sub.i]], and [n.sub.[Z.sub.j]], such that [Z.sub.i] [intersection] [Z.sub.j] [not equal to] [Phi], represent incompatible configurations of variables: they cannot possibly represent cons-cells that are in the same DSG. Therefore, two different SSG shape-nodes [n.sub.[Z.sub.i]] and [n.sub.[Z.sub.j]] can represent cons-cells in the same DSG only if [Z.sub.i] [intersection] [Z.sub.j] = [Phi].

(2) A given cons-cell in SG is represented by a unique SSG shape-node in [Beta](SG). Therefore, predicate [n.sub.[Z.sub.1]] [not equal to] [sharp] [n.sub.[Z.sub.2]] tests whether [n.sub.[Z.sub.1]] and [n.sub.[Z.sub.2]] are the same.

(3) Different cons-cells in SG are either represented in [Beta](SG) by different SSG shape-nodes, or else both are represented by summary node [n.sub.[Phi]].

(4) Let [l.sub.1], [l.sub.2], [sel.sub.1], and [sel.sub.2] be elements of SG that satisfy the conditions of the existential quantifiers in column two of the case for iis[[E.sub.s]](l) in Figure 10. We have

true [implies] compatible ([l.sub.1], [l.sub.2], l) Figure 10

[implies] [compatible.sup.[sharp]([Beta]([l.sub.1]),[Beta]([l.sub.2]),[Beta](l)) Case (1) above

<[l.sub.1], [sel.sub.1], l> [element of] [E.sub.s] <[Beta]([l.sub.1]),[sel.sub.1],[Beta](l)> [element of] [Beta]([E.sub.s])

[and] <[l.sub.2], [sel.sub.2], l> [element of] [E.sub.s] [implies] [and] <[Beta]([l.sub.2]),[sel.sub.2],[Beta](l)> [element of] [Beta]([E.sub.s]) Definition 5.2.1

[and] ([l.sub.1] [not equal to] [l.sub.2] [or] [sel.sub.1] [not equal to] [sel.sub.2]) [and] ([l.sub.1] [not equal to] [l.sub.2] [or] [sel.sub.1] [not equal to] [sel.sub.2])

<[Beta]([l.sub.1]),[sel.sub.1],[Beta](l)> [element of] [Beta]([E.sub.s])

[implies] [and] <[Beta]([l.sub.2]),[sel.sub.2],[Beta](l)> [element of] [Beta]([E.sub.s]) Case (3) above

[and] ([Beta]([l.sub.1]) [not equal to] [sharp][Beta]([l.sub.2]) [or] [sel.sub.1] [not equal to] [sel.sub.2])

This shows that there exist elements [Beta]([l.sub.1]), [Beta]([l.sub.2]), [sel.sub.1], and [sel.sub.2] in [Beta](SG) such that

[compatible.sup.[sharp]]([Beta]([l.sub.1]),[Beta]([l.sub.2]),[Beta](l)) [and] <[Beta]([l.sub.1]),[sel.sub.1],[Beta](l)> [element of] [Beta]([E.sub.s])

[and] <[Beta]([l.sub.2]),[sel.sub.2],[Beta](l)> [element of] [Beta]([E.sub.s]) [and] ([Beta]([l.sub.1]) [not equal to] [sharp] [Beta]([l.sub.2]) [or] [sel.sub.1] [not equal to] [sel.sub.2]).

Therefore, [Mathematical Expression Omitted] holds.

The above four predicates are examples of a more general principle:

Definition 5.3.2. Let p be any predicate on various DSG components (i.e., shape-nodes, variable-edges, selector-edges, etc.). Similarly, let [p.sup.[sharp]] be a predicate on the corresponding kinds of SSG components. We say that [p.sup.[sharp]] is a safe approximation of p (denoted by p [[implies].sub.[Beta]][p.sup.[sharp]]) if we have for every <[E.sub.v],[E.sub.s]> [element of] DSG and components A, B, . . . of <[E.sub.v], [E.sub.s]>

p(A, B, . . .) [implies] [p.sup.[sharp]]([Beta][[E.sub.v]](A),[Beta][[E.sub.v]](B), . . .).

The case of the abstract semantics that handles statements of the form "x := y.sel" make use of three additional abstract predicates: [compat_in.sup.[sharp]], [compat_self.sup.[sharp]], and [compat_out.sup.[sharp]]. These will be discussed in detail later in the section.

We now discuss the individual cases of the abstract meaning function [ILLUSTRATION FOR FIGURES 8 AND 9 OMITTED], illustrating the most important features using Figure 11, which shows the final SSGs computed for each program point by abstract interpretation of the destructive list-reversal program. Each block of Figure 11 indicates the shape of memory just before the program-point label that appears at the bottom of the block. The set listed at the top of each block indicates the vertex (or vertices) in the control-flow graph and the action(s) taken there. For example, the block labeled [v.sub.15] (see the lower right-hand corner of [ILLUSTRATION FOR FIGURE 11 OMITTED]) indicates that vertex [v.sub.15]'s one predecessor is the statement [t.sub.1] := nil at [v.sub.14].

* For an assignment statement of the form x := nil, x is "liquidized" from all shape-nodes that have variable x in their "name." That is, x is removed from the name of all such shape-node names, which may cause what were formerly distinct shape-nodes to be merged.

Example. In the transition between block [v.sub.7] and block [v.sub.8] of Figure 11, the assignment [t.sub.1] := nil causes [t.sub.1] to be removed from the "name" of shape-node [n.sub.{y,x,[t.sub.1]}]. Shape-nodes [n.sub.{y,x,[t.sub.1]}] and [n.sub.{y,x}] are then merged.

* For an assignment statement of the form x.sel := nil, the SSG transformer given in Figure 8 removes all of the sel selector-edges in shape-nodes that have x in their "name." This is safe because the variable set of a shape-node in the SSG for a program-point consists of variables that all point to the same cons-cell; therefore, all shape-nodes that have x in their name represent cons-cells whose sel field will be overwritten. (Conversely, if it is possible for a concrete cons-cell l that is not pointed to by variable x to arise at this statement, then l's sel field will not be overwritten; I will be represented in the SSG by a shape-node that does not have x in its "name.") See also the discussion of "strong nullification" in Section 5.4.

Example. In Figure 11, the transition between [v.sub.11] and [v.sub.12] removes selector-edge <[n.sub.{y}], cdr, [n.sub.{x,[t.sub.1]}]>.

The other important aspect of the SSG transformer for x.sel := nil is the way information in shape-node names is used to reset sharing information. This is based on the observation that it is safe to reset [is.sup.[sharp]](n) to false whenever [iis.sub.[sharp]](n) is false. (The resetting of sharing information by the SSG transformer is not illustrated by the list-reversal program, since [is.sup.[sharp]] is false for all shape-nodes in all shape-graphs that arise. The issue of resetting sharing information to false is discussed in detail in Section 5.5.)

* For an assignment statement of the form x := new, a new unshared node [n.sub.{x}] is created. All other shape-nodes are unaffected.

* For an assignment statement of the form x := y, the shape-node names are changed to reflect the fact that whatever y was pointing to before is now also pointed to by x. In addition, new variable-edges are added to reflect the assignment of y to x.

Example. See the transition between block [v.sub.6] and block [v.sub.7] of Figure 11.

* For an assignment statement of the form x.sel := y, sel selector-edges are added between shape-nodes pointed to by x and compatible shape-nodes pointed to by y.

Example. See the transition between block [v.sub.12] and block [v.sub.2] of Figure 11.

In addition, shape-nodes that are pointed to by y may have their [is.sup.[sharp]] values adjusted if the concrete cons-cells they represent could have become shared.

* The SSG transformer for an assignment statement of the form x := y.sel is the most elaborate operation [ILLUSTRATION FOR FIGURE 9 OMITTED]. The reason for this is that the SSG transformer has to create an SSG that conservatively covers all the possible new configurations of variable sets whose members all point to the same conscell after the assignment: in particular, if y.sel points to [n.sub.Z], then a copy of [n.sub.Z] is "materialized" - producing a "new" node [n.sub.Z[union]{x}] from "old" node [n.sub.Z]. In defining the materialization operation, the goal is to cover conservatively all the possibilities, yet at the same time not introduce too many superfluous edges that prevent the abstract semantics from being able to verify interesting properties.

Example. See the transition between block [v.sub.8] and block [v.sub.9] of Figure 11, in which the assignment [t.sub.1] := x.cdr causes node [n.sub.{[t.sub.1]}] to be materialized from [n.sub.[Phi]].

The other important aspect of the SSG transformer for x.sel := nil is the way information in shape-node names is used to reset sharing information. This is based on the observation that it is safe to reset [is.sup.[sharp]](n) to false whenever [iis.sup.[sharp]](n) is false. (The resetting of sharing information by the SSG transformer is not illustrated by the list-reversal program, since [is.sup.[sharp]] is false for all shape-nodes in all shape-graphs that arise. The issue of resetting sharing information to false is discussed in detail in Section 5.5.)

* For an assignment statement of the form x := new, a new unshared node [n.sub.{x}] is created. All other shape-nodes are unaffected.

* For an assignment statement of the form x := y, the shape-node names are changed to reflect the fact that whatever y was pointing to before is now also pointed to by x. In addition, new variable-edges are added to reflect the assignment of y to x.

Example. See the transition between block [v.sub.6] and block [v.sub.7] of Figure 11.

* For an assignment statement of the form x.sel := y, sel selector-edges are added between shape-nodes pointed to by x and compatible shape-nodes pointed to by y.

Example. See the transition between block [v.sub.12] and block [v.sub.2] of Figure 11.

In what follows, let [n.sub.Y] be a shape-node that y points to, and let [n.sub.Z] be one of the shape-nodes that y.sel points to (i.e., there is a selector-edge <[n.sub.Y], sel, [n.sub.Z]>). Bear in mind that

* y.sel may have selector-edges to many shape-nodes and

* y.sel may have a selector-edge to [n.sub.[Phi]], which in general represents many concrete cons-cells in a single DSG.

For every node [n.sub.Z] pointed to by y.sel, we materialize a new node [n.sub.Z[union]{x}] and direct the following variable-edges to [n.sub.Z[union]{x}]:

* Old variable-edges that point to [n.sub.Z] before the assignment. (This does notoccur in the transition between block [v.sub.8] and block [v.sub.9] of Figure 11.)

* A new variable-edge from x. (See variable-edge [[t.sub.1],[n.sub.{[t.sub.1]}]] in block [v.sub.9] of Figure 11.)

In Figure 9, the process of determining the selector-edges that are to be directed to and from [n.sub.Z[union]{x}] is divided into three cases, based on three additional abstract predicates, [compat_in.sup.[sharp]], [compat-self.sup.[sharp]], and [compat_out.sup.[sharp]], defined in columns three and four of Figure 12.

* The property [compat_in.sup.[sharp]] describes when two selector-edges whose targets are both [n.sub.Z] can possibly represent edges that coexist in the same concrete store. In particular, if an edge <[n.sub.W], sel[prime], [n.sub.Z]> is compatible with <[n.sub.Y], sel, [n.sub.Z]>, the abstract semantics for x := y.sel generates an old [right arrow] new selector-edge from the old node [n.sub.W] into the new node [n.sub.Z[union]{x}].

Example. Selector-edge <[n.sub.{y,x}], cdr, [n.sub.[Phi]]> in block [v.sub.8] of Figure 11 is a compatible incoming edge with respect to itself. This generates edge <[n.sub.{y,x}], cdr, [n.sub.{[t.sub.1]}]> in block [v.sub.9].

Note that if [is.sup.[sharp]]([n.sub.Z]) = false, then all of [n.sub.Z]'s incoming edges - other than <[n.sub.Y], sel, [n.sub.Z]> itself - are incompatible with <[n.sub.Y], sel, [n.sub.Z]>. In this case, the only old [right arrow] new edge generated is <[n.sub.Y], sel, [n.sub.Z[union]{x}]>. (This situation is illustrated by the above example.)

When y.sel points to [n.sub.[Phi]], if [n.sub.[Phi]] has a direct cycle of the form <[n.sub.[Phi]], sel[prime], [n.sub.[Phi]]>, this also counts as an "incoming" edge of [n.sub.[Phi]]. If [is.sup.[sharp]([n.sub.[Phi]]) = true, such an edge will be "materialized" in two ways: as an edge <[n.sub.[Phi]], sel[prime], [n.sub.{x}]) and as a direct cycle <[n.sub.{x}], sel[prime], [n.sub.{x}]). (The latter is handled by the set former that uses predicate [compat_self.sup.[sharp]]; see the discussion below.)

Example. In block [v.sub.8] of Figure 11, [is.sup.[sharp]]([n.sub.[Phi]]) = false, so the direct cycle <[n.sub.[Phi]], cdr, [n.sub.[Phi]]> is incompatible with <[n.sub.{y,x}], cdr, [n.sub.[Phi]]>. Consequently, a selector-edge <[n.sub.[Phi]], cdr, [n.sub.{[t.sub.1]}]> is not generated when [n.sub.{[t.sub.1]}] is materialized from [n.sub.[Phi]] in the transition from block [v.sub.8] to block [v.sub.9].

* The property [compat_self.sup.[sharp]] is used to define when a direct cycle <[n.sub.Z], sel[prime], [n.sub.Z]> is materialized as a direct cycle <[n.sub.Z[union]{x}], sel[prime], [n.sub.Z[union]{x}]>. If the edges <[n.sub.Z], sel[prime], [n.sub.Z]> and <[n.sub.Y], sel, [n.sub.Z]> represent a direct cycle and an edge that can possibly coexist in the same concrete store, the abstract semantics for x := y.sel generates a new [right arrow] new selector-edge from the new node [n.sub.Z[union]{x}] to [n.sub.Z[union]{x}]. Note that if [is.sup.[sharp]]([n.sub.Z]) = false, all of [n.sub.Z]'s incoming self edges are incompatible with <[n.sub.Y], sel, [n.sub.Z]>, unless [n.sub.Y] and [n.sub.Z] are the same shape-node and sel[prime] = sel.

Example. Selector-edge <[n.sub.[Phi]], cdr, [n.sub.[Phi]]> in block [v.sub.8] of Figure 11 is an incompatible self edge with respect to edge <[n.sub.{y,x}], cdr, [n.sub.[Phi]]>, and hence a selector-edge <[n.sub.{[t.sub.1]}], cdr, [n.sub.{[t.sub.1]}]> is not generated when [n.sub.{[t.sub.1]}] is materialized from [n.sub.[Phi]] in the transition from block [v.sub.8] to block [v.sub.9].

* The property [compat_out.sup.[sharp]] is used to define when an outgoing selector-edge <[n.sub.Z], sel[prime], [n.sub.W]> of [n.sub.Z] represents an edge that can possibly coexist in the same concrete store with an edge represented by selector-edge <[n.sub.Y], sel, [n.sub.Z]>. If <[n.sub.Z], sel[prime], [n.sub.W]> and <[n.sub.Y], sel, [n.sub.Z]> are compatible, the abstract semantics for x := y.sel generates a new [right arrow] old selector-edge from the new node [n.sub.Z[union]{x}] to the old node [n.sub.W].

Example. Selector-edge <[n.sub.[Phi]], cdr, [n.sub.[Phi]]> in block [v.sub.8] of Figure 11 is a compatible outgoing edge of [n.sub.[Phi]] with respect to edge <[n{y,x}], cdr, [n.sub.[Phi]]>, and hence a selector-edge <[n.sub.{[t.sub.1]}], cdr, [n.sub.[Phi]]> is generated when [n.sub.{[t.sub.1]}] is materialized from [n.sub.[Phi]] in the transition from block [v.sub.8] to block [v.sub.9].

Because each field of a concrete cons-cell can have only a single outgoing edge, if [n.sub.Y] = [n.sub.Z], then sel[prime] [not equal to] sel (or equivalently, [n.sub.Y] [not equal to] [n.sub.Z] [or] sel[prime] [not equal to] sel).

Note that all of the operations of the abstract semantics preserve the "compatibility" property for the variable-set names of selector-edge end-points described in Section 5.2.

The shape-analysis algorithm itself is an iterative procedure that computes an SSG, [Mathematical Expression Omitted], for each control-flow graph v, as the least fixed point (under the ordering defined in Definition 5.1.2) of the following system of equations in [Mathematical Expression Omitted]:

[Mathematical Expression Omitted] (2)

The iteration starts from the initial assignment [Mathematical Expression Omitted] for each control-flow-graph vertex w.

Example 5.3.3. The final abstract values for all of the control-flow-graph vertices of the normalized list-reversal program are shown in Figure 11. Among other things, this information tells us that if x's value is a list at the beginning of the program (see block [v.sub.1]) then y's value is a list at the end of the program (see block [v.sub.15]).

Block [v.sub.2] of Figure 11 shows the final SSG computed for vertex [v.sub.2] of the listreversal program. The elements of this graph can be interpreted as follows:

* There are two shape-nodes that represent the head of the list that x points to: [n.sub.{x}] and [n.sub.{x,[t.sub.1]}]. Shape-node [n.sub.{x}] represents the situation where x is the only variable pointing to the head of the list (which only happens before the first iteration of the loop). Shape-node [n.sub.{x,[t.sub.1]}] represents the situation where x and [t.sub.1] both point to the head of the list. Shape-node [n.sub.{y}] represents the head of the reversed list that y points to. Shape-node [n.sub.{t}] represents the head of the list that t points to, which is a sublist of the list that y points to. Shape-node [n.sub.[Phi]] represents all of the cons-cells in the tails of the lists that x, [t.sub.1], and t point to.

* For each of the shape-nodes in the graph, the value of [is.sup.[sharp]] is false. The fact that [is.sup.[sharp]]([n.sub.[Phi]]) = false tells us a number of interesting things about the memory state produced by any execution sequence that ends at vertex [v.sub.2]: (1) it implies that the cdr-edges from the cons-cells that x and t point to cannot point to the same cons-cell (and consequently the tails of the x-list and the t-list cannot share any cons-cells in common) and (2) similarly, for every pair of different cons-cells in the tail of x (respectively, t), the cdr-edges from these cons-cells cannot point to the same cons-cell. Consequently, the x-list (respectively, t-list) is an acyclic list.

Example 5.3.4. It is instructive to consider the algorithm's behavior when working with a program that uses the convention that the end of a linked list is represented by an element whose cdr field points to itself (e.g., see Sedgewick [1988, p.17-20]). This termination node would be represented in the SSG by a shape-node for which [is.sup.[sharp]] is true. However, if the convention is that there is a single copy of this node - shared by multiple lists - that is pointed to by a global variable, say nil, then the termination node [n.sub.{nil}] is distinct from summary-node [n.sub.[Phi]] in the SSG, and list-manipulation programs are analyzed as precisely as before.

Alternatively, suppose there are multiple termination nodes - one for each list - and that each linked-list object is represented using a pair of pointer variables, one pointing to the head of the list and one to the termination node. Again, the termination node will be distinct from summary-node [n.sub.[Phi]] in the SSG, and list-manipulation programs are analyzed as precisely as before.

If no pointer to the termination node is maintained, then [is.sup.[sharp]]([n.sub.[Phi]]) will be true. Therefore, techniques such as the ones discussed in Section 6.1 need to be used, or else much of the precision of the analysis will be lost.

Termination and safety of the shape-analysis algorithm are argued in the standard manner [Cousot and Cousot 1977]. For a given program P, we work with the domain of SSGs in which P Var consists of the program variables in P. This domain is finite and hence of finite height. Termination is assured because the semantic equations of Figures 8 and 9 are monotonic:

PROPOSITION 5.3.5 (MONOTONICITY OF [[]][sharp]). For all assignment statements st, and for each pair of SSGs, [Mathematical Expression Omitted] and [Mathematical Expression Omitted] such that [Mathematical Expression Omitted], we have [Mathematical Expression Omitted].

The heart of the safety argument involves showing that each semantic equation of the abstract semantics is conservative with respect to the corresponding equation of the concrete semantics:

THEOREM 5.3.6 (LOCAL SAFETY THEOREM). For each assignment statement st, and for every SG [element of] DSG, we have [Beta]([[st]](SG)) [subset or equal to] [[[st]].sup.[sharp]]([Beta](SG)).

PROOF. See the electronic appendix.

Finally, we have the following

THEOREM 5.3.7 (GLOBAL SAFETY THEOREM). For each control-flow-graph vertex v, we have [Mathematical Expression Omitted].

PROOF. Immediate from Proposition 5.3.5 (Monotonicity) and Theorem 5.3.6 (Local Safety), using Theorem T2 of Cousot and Cousot [1977, p.252].

5.4 Strong Nullification

The key property of the abstract semantics is that each abstract assignment operation creates an SSG that conservatively covers all the possible new configurations of variable sets whose members all point to the same cons-cell. This permits statements of the form x.sel : = nil to be treated in an unusual manner - unusual for a static-analysis algorithm, that is. When the algorithm processes such a statement, it always removes the sel edges emanating from the shape-nodes that x points to (i.e., the shape nodes [n.sub.X] such that x [element of] X). We call this operation strong nullification.

Example 5.4.1. Figure 13 shows a simple example that illustrates why strong nullification is possible. After the statement x : = y in the then-branch of the conditional, x and y point to the same cons-cell, and z points to a different cons-cell. Similarly, after the statement x : = z in the else,branch of the conditional, x and z point to the same cons-cell, and y points to a different cons-cell. Thus, in the SSG after the conditional statement, x and y both point to shape-node [n.sub.{x,y}], and z points to [n.sub.{z}] (reflecting the state of memory after the then-branch is executed); in addition, x and z both point to shape-node [n.sub.{x,z}], and y points to [n.sub.{y}] (reflecting the state of memory after the else-branch is executed).

The abstract semantics for the statement x.cdr : = nil eliminates the edges <[n.sub.{x,y}], cdr, [n.sub.[Phi]]> and <[n.sub.{x,z}], cdr, [n.sub.[Phi]]). This is safe because [n.sub.{x,y}] represents only cons-cells that are pointed to by both x and y (which occurs only on some execution sequences), and [n.sub.{x,z}] represents only cons-cells that are pointed to by both x and z (which also occurs only on some execution sequences).

The abstract semantics for x.cdr : = nil retains the edges <[n.sub.{z}], cdr, [n.sub.[Phi]]> and <[n.sub.{y}], cdr, [n.sub.[Phi]]). This correctly captures the fact that in the collecting semantics after x.cdr : = nil, there is a DSG that contains a cons-cell pointed to by y alone with an outgoing cdr-edge (to [l.sub.3]), as well as a DSG that contains a cons-cell pointed to by z alone with an outgoing cdr-edge (to [l.sub.4]).

Other shape-analysis algorithms do not perform strong nullification for a statement of the form "x.sel : = nil," except under very limited circumstances [Chase et al. 1990; Jones and Muchnick 1981; Larus 1989; Larus and Hilfinger 1988; Plevyak et al. 1993]. The reason for this is that, after the conditional statement in Example 5.4.1, they perform actions that (in our terminology) are equivalent to merging [n.sub.{y}] and [n.sub.{x,y}] into one shape-node. When this is done, it is not safe to perform strong nullification - i.e., to remove the shape-node's outgoing cdr edge because it would lose the information that y can, in fact, point to a cons-cell that has an outgoing cdr-edge.

In contrast, our shape-analysis algorithm always performs strong nullification. However, we are not claiming that our method is somehow "able to treat all statements precisely." With our method, the place where precision is lost (i.e., when it is lost) occurs in the treatment of statements of the form "x : = y.sel," rather than in statements of the form "x.sel : = nil." In particular, this is a problem when y's sel field points to [n.sub.[Phi]] and [is.sup.[sharp]]([n.sub.[Phi]]) = true. In the SSG transformer for x : = y.sel, node materialization creates shape-nodes that conservatively cover all the possible new configurations of variable sets whose members could all point to the same cons-cell. (See the treatment of the statement "x : = x.cdr" in Figure 4(b).)

On the other hand, in comparing the capabilities of our method with those of other graph-based shape-analysis algorithms, it would be wrong to think that we have just shifted the place where imprecision is introduced from the treatment of statements of the form "x.sel : = nil" to statements of the form "x : = y.sel." Not only do other shape-analysis algorithms use less precise SSG transformers for x.sel : = nil (i.e., performing strong nullification only under very limited circumstances), they also use less precise SSG transformers for statements of the form x : = y.sel; namely, they merely advance x to point to whatever shape-node (or shape-nodes) y.sel points to. In the case where y.sel points to [n.sub.[Phi]], this advances x into the primordial soup!

5.5 Insertion into a List

Whereas the previous sections have all considered the actions of the shape-analysis algorithm on the list-reversal program, this section considers a second example program, the list-insertion program shown in Figure 14, which may insert a cons-cell at an arbitrary point in a linked list. For this program, the shape-analysis algorithm is able to establish the following properties:

- "Listness" is preserved by the list-insert program. That is, when the initial value of variable x is an unshared acyclic list, the value of y at the end of the program is also an unshared acyclic list.

- "Circular listness" is also preserved by the list-insert program. More precisely, if at the beginning of the list-insert program x is a possibly cyclic list of length [greater than or equal to] 1 [ILLUSTRATION FOR FIGURE 7(E) OMITTED], then at the end of the program, x is a possibly cyclic list of length [greater than or equal to] 2 [ILLUSTRATION FOR FIGURE 7(D) OMITTED]. (For details, see Sagiv et al. [1995, Appendix B].)

The list-insert program also illustrates an interesting capability of the shape-analysis algorithm that does not arise with the list-reversal program: in certain circumstances, information in shape-node names can be used to reset a shape-node's sharing information from true to false. In the case of the list-insert program, this feature plays a crucial role in the ability of the shape-analysis algorithm to determine that the program preserves both "listness" and "circular listness."

Assume that at the beginning of the list-insert program, x points to an unshared list of length 1 or more and that e points to the new element to be inserted. The key SSGs are those that arise at vertices [v.sub.11], [v.sub.12], and [v.sub.13] of the control-flow graph, where the new element is spliced into the list. The crucial step is the transition from [v.sub.12] : y.cdr : = nil to [v.sub.13] In the immediately preceding transition, from [v.sub.11] to [v.sub.12] e.cdr is assigned the value t, which adds a new selector-edge into [n.sub.{t}] and causes [is.sup.[sharp]]([n.sub.{t}]) to be set to true in the shape-graph for [v.sub.12].

The strong nullification performed in the transition from [v.sub.12] to [v.sub.13] removes the selector-edges <[n.sub.{z,y}], cdr, [n.sub.{t}]> and <[n.sub.{x,y}], cdr, [n.sub.{t}]>. Thus, in the SSG for vertex [v.sub.13], shape-node [n.sub.{t}] retains only a single incoming selector-edge, namely <[n.sub.{e}], cdr, [n.sub.{t}]>. In the SSG transformer given in Figure 8 that covers the assignment y.cdr : = nil, the fact that predicate [iis.sup.[sharp]] is a safe approximation to iis is used to reset sharing information. In this case, because the value of [Mathematical Expression Omitted] at [v.sub.12] is false, the SSG transformer for the control-flow graph arc from [v.sub.12] to [v.sub.13] determines that it is safe to set [is.sup.[sharp]]([n.sup.{t}]) to false in the SSG for vertex [v.sub.13]. (See the third row of Figure 15.)

Remark. It is interesting to note that if the assignment at [v.sub.12] were e.cdr : = nil, rather than y.cdr : = nil, [is.sup.[sharp]]([n.sub.{t}]) would still be set to false at [v.sub.13], even though there would be two incoming selector-edges to shape-node [n.sub.{t}]: <[n.sub.{z,y}], cdr, [n.sub.{t}]> and <[n.sub.{x,y}], cdr, [n.sub.{t}]>. Because these two edges are incompatible they do not represent edges that can simultaneously coexist in a single concrete store - the value of [Mathematical Expression Omitted] would again be false at vertex [v.sub.12], and so [is.sup.[sharp]]([n.sub.{t}]) would be false at vertex [v.sub.13].

6. EXTENSIONS

This section discusses several variations on the basic method that has been presented above. Due to space limitations, they will only be sketched out below.

6.1 More Summary Shape-Nodes

The major source of inaccuracy in our method is attributable to the fact that, in general, summary shape-node [n.sub.[Phi]] represents a number of unrelated cons-cells. This is particularly a problem when [is.sup.[sharp]]([n.sub.[Phi]]) = true. For example, in a program that uses both a list and a graph, the tail of the list is abstracted to the same summary node as (most of) the graph's nodes. Consequently, the shape-analysis algorithm imprecisely identifies both structures as graphs: variables that actually point into the list appear to point to some kind of shared graph structure.

There are several simple ways to improve the accuracy of shape analysis by introducing more summary nodes, including the following:

* Using two separate summary nodes: One in which [is.sup.[sharp]]([n.sub.[Phi]]) = false, representing all nodes not pointed to by any variable and pointed to by at most one distinct cons-cell field, and one in which [is.sup.[sharp]]([n.sub.[Phi]]) = true, representing all nodes not pointed to by any variable and pointed to by two or more distinct cons-cell fields.

* Using allocation-sites to identify shape-nodes [Chase et al. 1990; Jones and Muchnick 1982]: This can be incorporated into our method as an "orthogonal dimension" of shape-node names - e.g., shape-nodes would have names such as [n.sub.s,X], where s is an allocation site, and X is a set of program variables. [n.sub.[Phi]]

* Using some type information: For example having one [n.sub.[Phi]] node for every declared data type.

However, even these extensions do not help solve the following kind of accuracy problem:

Example 6.1.1. At vertex [v.sub.11] of the list-insert program, the shape-graph computed by our shape-analysis algorithm indicates that variables y and z can point to a cyclic list ([ILLUSTRATION FOR FIGURE 15 OMITTED], the [v.sub.11] row). Note that during an execution of the program, at [v.sub.11] variables y and z point into the middle of the (acyclic) list that x points to. The reason for the inaccuracy in the structure reported at [v.sub.11] by the shape-analysis algorithm is that [n.sub.[Phi]] does double duty: (1) it represents the segment of the list in between x and y (cf. the selector-edges <[n.sub.{x}], cdr, [n.sub.[Phi]]> and <[n.sub.[Phi]], cdr, [n.sub.{z,y}]>); (2) it also represents the segment of the list beyond what y points to (cf. the selector-edges <[n.sub.{z,y}], cdr, [n.sub.{t}]> and <[n.sub.{t}], cdr, [n.sub.[Phi]]>). This, combined with the fact that [is.sup.[sharp]]([n.sub.{t}]) = true, causes it to appear that y and z may be pointing to a cyclic list.

In the case of the insert program, this temporary inaccuracy does not cause our algorithm any problems. In going from the second to the third row of Figure 15, the (apparent) cycle is broken, and thus the algorithm is still able to determine that at the end of the program x points to an acyclic list. However, for other programs we are not so fortunate. For example, in Lindstrom scanning of a tree [Lindstrom 1973] (also known as the Deutsch-Schorr-Waite algorithm for traversing a tree without a stack [Knuth 1973, p.417]) this kind of inaccuracy prevents us from finding that, after traversing a tree, we still have a tree.

It is possible to avoid this sort of inaccuracy by introducing additional summary nodes (with an appropriate naming scheme) to discriminate between cons-cells that are transitively pointed to by different collections of variables or via different selectors. We have developed several alternative abstract semantics based on this idea.

6.2 Reducing the Number of Shape-Nodes

The number of shape-nodes in an SSG is bounded by [2.sup.[absolute value of PVar]]. Unfortunately, for some pathological programs the number of shape-nodes can actually grow to be this large. For example, the number of shape-nodes in the SSG that arises at the end of the program shown in Figure 16 is [2.sup.n]. Our limited experience to date suggests that this is unlikely to arise in practice, the main reason being that the number of possible aliasing configurations is normally small.

It is possible to change the shape-analysis algorithm to use widening to eliminate the possibility of exponential blow-up and to guarantee that a conservative solution to Eq. (2) of Section 5.3 can be found in polynomial time. The basic idea is to reduce the number of shape-nodes that can arise, by discarding an arbitrary amount of "simultaneously-points-to" information at certain shape-nodes, thereby trading off accuracy for efficiency. For instance, at various points in the shape-analysis algorithm (e.g., at loops) we can widen an SSG into a less precise, but usually more compact, SSG by merging shape-nodes, say [n.sub.[Z.sub.1]] and [n.sub.[Z.sub.2]], into [n.sub.[Z.sub.1]][intersection][Z.sub.2] and giving [n.sub.[Z.sub.1]][intersection][Z.sub.2] all the variable- and selector-edges that were incident on [n.sub.[Z.sub.1]] and [n.sub.[Z.sub.2]].

Formalizing this notion involves changing the SSG domain by weakening what has (up to now) been a fundamental condition on variable-sets in shape-node names. In particular, we now allow the name of a shape-node to be any subset of the variables pointing to it:

As before, the SSG for program point p represents, in general, a number of DSGs. An SSG shape node [n.sub.Z], where Z [not equal to] [Phi], represents the (at most one) cons-cell in each DSG that is simultaneously pointed to by all the variables in Z. In addition, if w is a variable not in Z, but the SSG has a variable-edge [w, [n.sub.Z]], then variable w may or may not point to that same cons-cell.

For SSGs that are in the image of abstraction-function [Alpha] (Definition 5.2.1), we have the following property:

For every x [element of] PVar and [n.sub.X] [element of] shape-nodes([SG.sup.[sharp]]), x [element of] X if and only if [x, [n.sub.X]] [element of] [E.sub.v].

For SSGs on which widening has been performed, we have the weaker property:

For every x [element of] PVar and [n.sub.X] [element of] shape-nodes([SG.sup.[sharp]]), if x [element of] X then [x, [n.sub.X]] [element of] [E.sub.v].

The relation [subset or equal to][prime] on the extended domain of SSGs captures the fact that the widened SSGs are less accurate than the original SSGs, i.e., a widened SSG denotes more DSGs than the original SSG. Formally, [subset or equal to][prime] is a preordering on the extended domain of SSGs, defined as follows:

Definition 6.2.1. Let [Mathematical Expression Omitted] and [Mathematical Expression Omitted]. Then [Mathematical Expression Omitted] if and only if there exists a mapping r:[2.sup.PVar] [approaches] [2.sup.PVar] such that for all X [subset or equal to] PVar, r(X) [subset or equal to] X, and

* for every [Mathematical Expression Omitted], [Mathematical Expression Omitted],

* for every [Mathematical Expression Omitted], [Mathematical Expression Omitted], and

* for every [Mathematical Expression Omitted], [Mathematical Expression Omitted].

In Definition 6.2.1, function r has the ability to discard an arbitrary amount of "simultaneously-points-to" information at any shape-node. Note that we can still use graph union as a confluence operator.

We have been careful to write the abstract semantics given in Figures 8 and 9 so that it does not have to be changed when widening is employed. For example, x.sel : = nil removes x's sel selector-edges from a shape-node [n.sub.Z] only when x [element of] Z. Thus, if [x, [n.sub.Z]] [element of] [E.sub.v] but x [not element of] Z, the abstract semantics does not remove [n.sub.Z]'s outgoing sel edges: this would not be safe because we do not know that [n.sub.Z] represents a cons-cell that x must point to. Note that we still do perform a strong nullification of [n.sub.Z]'s outgoing sel edges for assignments of the form z.sel : = nil, where z [element of] Z, because [n.sub.Z] represents only cons-cells whose sel field will definitely be overwritten. (In Section 6.2.2, we define an operation that can be used to materialize shape-nodes in order to guarantee that if [x, [n.sub.Z]] [element of] [E.sub.v] then x [element of] Z. By applying this operation prior to nullification, we can still always perform strong nullification, even if the shape-analysis algorithm performs widening.)

This observation is captured in the following proposition:

PROPOSITION 6.2.2 (GENERALIZED MONOTONICITY OF [[]][sharp]). For each assignment statement st, and for each pair of SSGs [Mathematical Expression Omitted] and [Mathematical Expression Omitted] such that [Mathematical Expression Omitted], [Mathematical Expression Omitted].

The following generalization of Theorem 5.3.6 is an immediate corollary:

COROLLARY 6.2.3. For all assignment statements st, for every SG [element of] DSG, and for every [SG.sup.[sharp]] such that [Beta](SG) [subset or equal to][prime] [SG.sup.[sharp]], [Beta]([[st]](SG)) [subset or equal to][prime] [[[st]].sup.[sharp]] ([SG.sup.[sharp]]).

PROOF. [Beta]([[st]](SG)) [subset or equal to] [[[st]].sup.[sharp]] ([Beta](SG)) [subset or equal to][prime] [[[st]].sup.[sharp]] ([SG.sup.[sharp]]).

6.2.1 Strategies for Merging Nodes. There are many possible strategies for reducing the number of shape-nodes through widening. Different widening policies may lead to shape-analysis algorithms that differ in accuracy and efficiency. For example, we may decide to forget an arbitrary variable z [element of] PVar by widening

[Mathematical Expression Omitted] into [Mathematical Expression Omitted] where

[f.sub.z]([n.sub.W]) = [n.sub.W - {z}]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[is.sup.[sharp][prime]] ([n.sub.W]) = [is.sup.[sharp]]([n.sub.W]) [or] [is.sup.[sharp]] ([n.sub.W[union]{z}])

By definition, [Mathematical Expression Omitted]. It is possible to use this widening operator to guarantee that a conservative solution to Eq. (2) of Section 5.3 can be found in polynomial time. It simply has to be applied whenever necessary to limit the cardinality of shape-node name sets to some chosen constant. (This is similar in spirit to k-limiting [Jones and Muchnick 1981], but it is likely to produce much better results because limiting the cardinality of name sets still preserves most of the structural information about the graph.)

Example 6.2.1.1. In the SSG shown in the [v.sub.2] box of Figure 11, we can eliminate [t.sub.1] from the name sets to get the SSG shown in Figure 17. In this case, widening amounts to not distinguishing between the store that arises just before the first iteration and the stores that arise on each succeeding iteration. Because [t.sub.1] is not live at [v.sub.2], and because there are no structural differences between the store that arises just before the first iteration and the ones that arise subsequently, widening does not lead to a loss of accuracy in this case.

As mentioned earlier, another possible widening strategy is to merge shape-nodes [n.sub.Y] and [n.sub.Z] into a shape-node [n.sub.(Y[intersection]Z)]. This would seem to make the most sense when Y and Z have many variables in common.

Experimentation is necessary to determine what kind of widening works best in practice.

6.2.2 Materializing Shape Nodes via Narrowing. It is interesting to note that if widening has been performed we can also narrow an SSG into one that denotes the same DSGs but in some sense is more "precise." This operation may be employed gainfully just before the interpretation of statements of the form x.sel : = nil to allow the abstract semantics to always be able to perform strong nullification (i.e., to always remove x's sel selector-edges), even if the shape-analysis algorithm has widened the SSG with respect to variable x. The narrowing operation converts an SSG [Mathematical Expression Omitted] into an SSG [Mathematical Expression Omitted] defined by the following:

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

[Mathematical Expression Omitted]

The narrowing operation materializes at most [absolute value of [E.sub.v](x)] shape-nodes and guarantees that x is in the name of all the shape-nodes that x points to. This permits the interpretation of x.sel : = nil to nullify the sel field of all shape-nodes that x points to.

Example 6.2.2.1. Applying this narrowing operation to the SSG from Example 6.2.1.1 yields back the SSG shown in the [v.sub.2] box of Figure 11. In general, however, narrowing a widened graph may yield an SSG that is less precise than the original SSG.

6.3 Refining the Concrete Semantics

In this article, we have tried to simplify the presentation of our ideas both by choosing a small programming language and by using a "concrete semantics" that has a small amount of abstraction built into it already. The following are some possible refinements of the concrete semantics that would lead to slightly different abstract semantics (with somewhat different powers):

* Shape-nodes that are not reachable from variables are not removed by the operational semantics shown in Figure 6. For certain programs, this may lead to loss of accuracy. This can be overcome by working with concrete and abstract semantics that incorporate garbage-collection operations (see Sagiv et al. [1995]).

* In the way shape graphs were defined in Section 3.2, there are no shape-graph elements that represent uninitialized fields of cons-cells or fields whose value is either an atom or nil. One consequence of this is that the shape-analysis algorithm is only able determine rather weak data-type properties. As pointed out in Example 5.2.6, when the algorithm reports that a variable points to a circular list, it may actually point only to a noncircular list. That is, the type "circular list" really means "possibly circular list."

By introducing three additional nodes, [n.sub.atom], [n.sub.nil], and [n.sub.uninit], much more accurate type properties can be obtained in many cases. We impose the invariant on shape-graphs that all fields of shape-nodes have at least one outgoing selector-edge (possibly to [n.sub.atom], [n.sub.nil], or [n.sub.uninit]). This modified domain of SSGs is capable of characterizing some definitely cyclic data structures.

For example, with this extended definition of shape-graphs, the SSG shown in Figure 7(d) characterizes the definitely cyclic lists of length [greater than or equal to] 2 (modulo the absence of edges from the car fields to [n.sub.atom] in the two shape-nodes); Figure 7(e) characterizes the definitely cyclic lists of length [greater than or equal to] 1. The possibly cyclic lists of length [greater than or equal to] 1 are characterized by the following SSG:

6.4 Interprocedural Analysis

The shape-analysis algorithm can also be extended to handle procedure calls. Two fundamental problems need to be resolved:

(1) Representing multiple occurrences of the same local variable in (mutually) recursive procedures.

(2) Accounting for the different calling contexts in which a procedure can occur.

To approximate the local variables of recursive calls, we introduce an extra variable [Mathematical Expression Omitted] for every local variable x. Variable [Mathematical Expression Omitted] is used as a representative for all copies of x in other scopes. Shape-nodes whose name sets contain only barred variables are a new kind of "summary node." Like [n.sub.[Phi]], they can represent multiple cons-cells of a single concrete store. Using these ideas, we have extended the abstract semantics to handle procedure calls and returns.

The second problem can be resolved using one of the known interprocedural techniques of Sharir and Pnueli [1981]. For example, a simple conservative solution is to consider a procedure call as a goto to the called procedure and a return from a procedure P as a goto to all the statements that follow an invocation of P. A more accurate solution can be determined by tabulating a "shape-graph-transformation" function for each procedure.

An alternative is to use Hendren's tabulation method for interprocedural analysis [Hendren 1990].

7. APPLICATIONS

The algorithm developed in Section 5 produces an SSG [Mathematical Expression Omitted] for every program point v. This SSG provides an approximation to the set of stores (DSGs) that can possibly occur in any execution of the program that ends at v. Therefore, many interesting questions about the stores at v can be answered (conservatively) by investigating [Mathematical Expression Omitted]. In this section, we present two such applications of SSGs. The information that these techniques provide is useful both in optimizing compilers and in software engineering tools.

7.1 Finding May-Aliases

We say that two access paths, [e.sub.1] and [e.sub.2], are may-aliases at a program point v if there exists an execution sequence leading to v that produces a store in which both [e.sub.1] and [e.sub.2] point to the same cons-cell. The may-alias problem is a fundamental problem in optimizing compilers generating code for scalar, superscalar, and parallel architectures. It is also useful in software engineering tools.

A special case of the may-alias problem concerns whether two pointer variables x and y are may-aliases just before a given program point v. It is possible to use the results of our shape-analysis algorithm to give a conservative answer to this question by testing whether x and y point to a common shape-node in the SSG [Mathematical Expression Omitted]. If x and y do not point to a common shape-node, we conclude that they cannot be may-aliases; otherwise, we conservatively conclude that there may exist an execution sequence in which they point to the same cons-cell.(5)

The more general complex question is whether two access paths [e.sub.1] and [e.sub.2] are may-aliases. There are several different possible tests:

* A simple test is to check if there are common shape-nodes accessible from both [e.sub.1] and [e.sub.2]. If there are no such nodes, we can conclude that [e.sub.1] and [e.sub.2] are definitely not may-aliases. Otherwise, we conservatively conclude that [e.sub.1] and [e.sub.2] are may-aliases.

Example. In the [v.sub.2] box of Figure 11, this test yields that x.cdr and y.cdr are may-aliases. This is obviously a superfluous may-aliases because [n.sub.[Phi]] is not shared.

* Sharing information can be used to reduce the number of superfluous may-aliases reported for two given access paths. The main idea is that directed paths in [Mathematical Expression Omitted] that lead to unshared nodes do not create aliases. To test whether [e.sub.1] and [e.sub.2] are may-aliases just before program-point v, we test whether there exist two (possibly empty) directed selector-paths [[Pi].sub.1] and [[Pi].sub.2] in [Mathematical Expression Omitted] leading to a common SSG node such that the following conditions hold:

(1) For every node [n.sub.X] that appears more than once along [[Pi].sub.1] (resp., [[Pi].sub.2]), either X = [Phi] or is([n.sub.X]).

(2) There exists a possibly empty common suffix [Delta] of [e.sub.1] and [e.sub.2] (i.e., [e.sub.1] = [e[prime].sub.1][Delta] and [e.sub.2] = [e[prime].sub.2][Delta]) such that [e[prime].sub.1] and [e[prime].sub.2] lead to a common node n and either (1) [e[prime].sub.1] and [e[prime].sub.2] is a simple variable or (2) is(n) = true.

Example. In the [v.sub.2] box of Figure 11, none of the shape nodes are shared. Therefore, the only detected may-aliases are the ones induced by variables, e.g., y.cdr.cdr and t.cdr are may-aliases.

* The node-compatibility conditions can be used to trim out some additional superfluous aliases. The main idea is that directed paths that go through different shape-nodes that have common variables in their name can only come from different DSGs. Therefore, we can safely say that these kind of paths do not indicate may-aliases.

7.2 Detecting Shared Data Structures

SSGs can also be used to determine if there is possible sharing between components of two heap-allocated data structures, which is precisely the kind of information needed to be able to compile programs to take advantage of coarse-grained parallelism. The sharing problem is a natural generalization of the may-aliases problem in which we quantify over access paths. Therefore, the three aforementioned approaches can be adapted to provide a solution to the sharing problem. For example, the second approach implies that if all shape-nodes n accessible from both x and y have the value [is.sup.[sharp]](n) = false, there cannot possibly be any sharing between the data structures pointed to by x and y.

8. RELATED WORK

The shape-analysis problem was first investigated by Reynolds [1968], who studied it in the context of a Lisp-like language with no destructive updating. Reynolds treated the problem as one of simplifying a collection of set equations. A similar shape-analysis problem, but for an imperative language supporting nondestructive manipulation of heap-allocated objects, was formulated independently by Jones and Muchnick, who treated the problem as one of solving (i.e., finding the least fixed point of) a collection of equations using regular tree grammars [Jones and Muchnick 1981]. Follow-on work on this kind of shape-analysis problem includes Mogensen [1988; 1989], Heintze [1992], and Reps [1995].

Jones and Muchnick [1981], also began the study of shape analysis for languages with destructive updating. To handle such languages, they formulated an analysis method that associates program points with sets of finite shape-graphs.(6) To guarantee that the analysis terminates for programs containing loops, the Jones-Muchnick approach limits the length of acyclic selector paths by some chosen parameter k. All nodes beyond the "k-horizon" are clustered into a summary node. The Jones-Muchnick formulation has two drawbacks:

(1) The analysis yields poor results for programs that manipulate cons-cells beyond the k-horizon. For example, in the list-reversal program of Figure 5, little useful information is obtained. The analysis algorithm must model what happens when the program is applied to lists of length greater than k. However, the tail of such a list is treated conservatively, as an arbitrary, and possibly cyclic, data structure.

(2) The analysis may be extremely costly because the number of possible shape-graphs is doubly exponential in k.

In addition to Jones and Muchnick's work, k-limiting has also been used in a number of subsequent papers (e.g., Horwitz et al.[1989]).

Whereas Jones and Muchnick [1981] use sets of shape-graphs, our work follows Jones and Muchnick [1982], Larus [1989], Larus and Hilfinger [1988], Chase et al. [1990], and Stransky [1992] who developed shape-analysis methods that associate each program point with a single shape-graph. The use of a single shape-graph is possibly less accurate than a method based on sets of graphs, and, compared with a method that uses sets of graphs, working with a single graph complicates the abstract semantics. However, for reasons mentioned in Section 5.2, the use of a single graph seems necessary for the pragmatic reason that it is more likely to lead to a practical shape-analysis algorithm.

Jones and Muchnick [1982], Chase at el. [1990], and Stransky [1992] present similar methods in which the shape-nodes correspond to a program's allocation sites. These methods are more efficient than the methods discussed earlier, both from a theoretical perspective [Chase et al. 1990] and from an implementation perspective [Assmann and Weinhardt 1993].

The algorithm presented by Chase et al. [1990] is based on the following ideas:

* Sharing information, in the form of abstract heap reference counts (0, 1, and [infinity]),is used to characterize shape-graphs that represent list structures.(7)

* Several heuristics are introduced to allow several shape-nodes to be maintained for each allocation site.

* For an assignment to x.sel, when the shape-node that x points to represents only concrete cons-cells that will definitely be overwritten, the sel field of the shape-node that x points to can be overwritten (a so-called "strong update").

The Chase-Wegman-Zadeck algorithm is able to identify list-preservation properties in some cases; for instance, it can determine that a program that appends a list to a list preserves "listness." However, as noted by Chase et al. [1990], allocation-site information alone is insufficient to determine interesting facts in many programs. For example, it cannot determine that "listness" is preserved for either the list-reversal program or the list-insert program. In particular, in the list-reversal program, the Chase-Wegman-Zadeck algorithm reports that y points to a possibly cyclic structure and that the structures that x and y point to might share cons-cells in common.

There are three major technical differences between our algorithm and the Chase-Wegman-Zadeck algorithm that lead to the improvements in accuracy obtained by our algorithm:

(1) Tracking of aliasing configurations. The sets of variable names attached to shape-nodes track possible aliasing configurations. A shape-node [n.sub.Z] represents cons-cells that are simultaneously pointed to by exactly the variables in Z. The abstract semantics tracks possible aliasing configurations by performing operations on the variable sets that name SSG shape-nodes.

(2) "Strong nullification." For an assignment of the form x.sel : = y, the Chase-Wegman-Zadeck method ordinarily performs a "weak update" (i.e., selector-edges emanating from the shape-nodes that x points to are accumulated). It performs a strong update only under certain specialized conditions.

In our algorithm, because of the Normalization Assumptions of Section 3.1, an assignment statement x.sel : = y is transformed into two statements: x.sel : = nil, followed immediately by x.sel : = y. When our algorithm processes the first of these statements, it (always) removes the sel edges emanating from the shape-nodes that x points to. We have called this operation "strong nullification," by analogy with "strong update." When the algorithm processes the second statement, it introduces sel edges that emanate from the shape-nodes that x points to. With these taken together, the effect is to overwrite the sel edges emanating from the shape-nodes that x points to. In other words, for a statement in the original program of the form x.sel : = y, our algorithm always performs a strong update, even when x does not point to a unique SSG shape-node.

(3) Materialization. In an assignment statement of the form x : = y.sel, our algorithm materializes new shape-nodes that conservatively cover all the possible new configurations of variable sets whose members all point to the same cons-cell. For example, when y.sel points to [n.sub.[Phi]], our algorithm materializes a new node [n.sub.{x}] out of [n.sub.[Phi]]. Furthermore, if [is.sup.[sharp]]([n.sub.[Phi]]) = false, this information is used to exclude both of the two possible selector-edges from [n.sub.[Phi]] to [n.sub.{x}], as well as both of the two possible selector-edges from [n.sub.{x}] to [n.sub.{x}]. In programs that use a loop containing an assignment x : = x.cdr to traverse an unshared linked list, this technique permits our method to determine that x points to an unshared list element on every iteration.

The Chase-Wegman-Zadeck algorithm lacks a node-materialization operation (although they did recognize that the lack of one was a stumbling block to the accuracy of their method [Chase et al. 1990, p. 309]).

Chase, Wegman, and Zadeck use reference-count values 0, 1, and [infinity], whereas we use a Boolean-valued function [is.sup.[sharp]]. However, this does not represent a significant difference because in our SSGs the selector-edges allow recovering the distinction between 0 (no incoming edges) and 1 (at least one incoming selector-edge, but [is.sup.[sharp]](n) = false).

Our method has been presented within the framework of abstract interpretation, which allows us to prove that the algorithm obtained is conservative with respect to the concrete semantics. Chase, Wegman, and Zadeck give only informal arguments about the correctness of their algorithm. Because of several ad hoc features of the Chase-Wegman-Zadeck method, several changes would be necessary to reformulate it as an abstract interpretation. For instance, the rules they give for the "join" operation are complicated by the fact that the result of "joining" two shape-graphs depends on the program point at which the operation is applied. (For this reason, "join" is a misnomer in the lattice-theoretic sense.) In contrast, our join operation, which is essentially graph union, is the join operation in the lattice of SSGs defined in Section 5.1.

Plevyak et al. [1993] describe a shape-analysis algorithm that is similar to the Chase-Wegman-Zadeck method. Their algorithm inherits most of the drawbacks of the original Chase-Wegman-Zadeck algorithm.

Larus and Hilfinger [Larus 1989; Larus and Hilfinger 1988] devised a shape-analysis algorithm that is based on somewhat different principles from the aforementioned work. As with our algorithm, shape-nodes are labeled with some auxiliary information. At first glance, their node-labeling scheme appears to be more general than ours: whereas we use a set of variables to label each node, they use a regular expression (limited to be no longer than some chosen constant k) representing pointer-access paths that may lead to an instance of the node. However, their shape-node labels do not add any information to their representation because the pointer-access expressions can always be reconstructed from the graph stripped of node labels. In contrast, our labels - which in some sense represent degenerate regular expressions of length 1 - do contribute essential information to our representation: when x is in the variable-set of shape-node [n.sub.X], we know that a strong nullification (and hence a strong update) can be performed on the selector-edges emanating from [n.sub.X].

It would possibly be worthwhile to extend our technique to use more complicated shape-node names of the kind that Larus and Hilfinger use. However, on many interesting examples, even with our "length-1 labels," our algorithm achieves greater accuracy than the Larus-Hilfinger algorithm does, no matter what value of k is chosen: for example, the Larus-Hilfinger algorithm is not able to determine that programs such as the list-reversal and list-insert programs preserve "listness."

There are also several algorithms that are not based on shape-graphs for finding may-alias information for pointer variables. The most sophisticated ones are those of Landi and Ryder [1991] and Deutsch [1994]. Deutsch's algorithm is particularly interesting because, for certain programs that manipulate lists, it offers a way of representing the exact (infinite set of) may aliases in a compact way. It can be shown that, for the list-reversal program, Deutsch's algorithm yields may-alias information that is equivalent to that produced by the algorithm of Section 5.1. However, both the Landi-Ryder and Deutsch algorithms do not determine that either "listness" or "circular listness" is preserved by the insert program of Figure 15. The reason is that, due to the lack of a strong-nullification operation, these algorithms cannot infer that the assignment y.cdr : = nil in the program shown in Figure 14(b) cuts the list pointed to by x ([ILLUSTRATION FOR FIGURE 15 OMITTED], the second and the third rows)). (We do not mean to imply that our method always dominates the Landi-Ryder and Deutsch algorithms; we know of at least one program for which Deutsch's algorithm is more accurate than our algorithm.)

A different approach was taken by Hendren and Nicolau, who designed an algorithm that handles only acyclic data structures [Hendren 1990; Hendren and Nicolau 1990]. Because of the decision to work with programs that only manipulate acyclic structures, the algorithm does not have to have a way of representing cycles, even conservatively. For this alias-analysis problem, they have given an efficient algorithm that manipulates matrices that record access paths that are aliases.

To the best of our knowledge, the Hendren-Nicolau algorithm is the only algorithm besides ours that can detect that insertion of an element into a list (respectively, tree) preserves the list (tree) structure. However, by design, their algorithm cannot determine such structure-preservation properties for programs that handle cyclic lists.

Myers [1981] presented an algorithm for interprocedural bit-vector problems that accounts for aliasing. Like our shape-analysis algorithm, his algorithm also keeps track of sets of aliased variables. He conjectured that in practice the sizes of the alias sets remain small. However, Myers's work does not handle heap-allocated storage and destructive updating. Therefore, his algorithm is significantly simpler, and he is even able to show that it is precise. In contrast, it is undecidable to give a precise solution to our problem, even in the absence of procedure calls [Landi 1992; Ramalingam 1994].

ONLINE-ONLY APPENDIX

A. PROOF OF THREE SAFE-APPROXIMATION PROPERTIES

B. LOCAL SAFETY OF THE ABSTRACT SEMANTICS

Appendices A-B are available only online. You should be able to get the online-only appendices from the citation page for this article:

http://www.acm.org/pubs/citations/journals/toplas/1998-20-1/p1-sagiv/

Alternative instructions on how to obtain online-only appendices are given on the back inside cover of current issues of ACM TOPLAS or on the ACM TOPLAS web page:

http://www.acm.org/toplas

Fig. 1. A program to reverse a list.

program reverse(x, y) begin /* x points to an unshared, acyclic, singly linked list */ y := nil while, x [not equal to] nil do t := y y := x x := x.cdr y.cdr := t od t := nil end

ACKNOWLEDGMENTS

We are grateful for the helpful comments of Martin Alt, Alain Deutsch, Christian Fecht, John Field, Neil Jones, Yishay Mansour, Florian Martin, Mike O'Donnell, G. Ramalingam, and Michael Rodeh. Laurie Hendren provided us with extensive and very helpful information about the capabilities of her shape-analysis technique.

We used two logic-programming systems - Coral [Ramakrishnan et al. 1993] and XSB [Warren 1992] - to experiment with implementations of the shape-analysis algorithm. We are indebted to Raghu Ramakrishnan and Praveen Seshadri for help with Coral and to C.R. Ramakrishnan for porting the Coral implementation to XSB.

1 Throughout the article, the presentation is couched in terms of the Lisp primitives for manipulating heap-allocated storage (i.e., nil, cons, car, and cdr). However, this is not due to any basic limitation of the work; the algorithm extends readily to the case of pointers to user-defined types that have more than two fields. We assume that we are working with an imperative language that meets the following general description. A program consists of assignment statements, conditional statements, loops (while, for, repeat), read statements, write statements, and goto statements. (The treatment of procedures is discussed in Section 6.4.) The language provides atomic data (e.g., integer, real, boolean, etc.) and constructor and selector operations (e.g., nil, cons, car, and cdr), together with appropriate predicates (equal, atom, and null). We assume that a read statement reads just an atom and not an entire list, tree, or graph.

2 In some algorithms, cdr edges emanating from a shape-node that y points to are removed in very limited circumstances.

3 An alternative semantics that returns a special value [perpendicular to] if a nil pointer or uninitialized pointer is dereferenced was used in Sagiv et al. [1995]. The present formulation has the advantage of being simpler.

4 The number of shape-nodes in a single SSG is bounded by [2.sup.[absolute value of PVar]]. Although with our shape-analysis algorithm, the number of shape-nodes can actually grow to be this large for some pathological programs, our limited experience to date suggests that this is unlikely to arise in practice. The blow-up problem can also be mitigated by using widening (see Section 6.2).

5 Similarly, it is possible to use the results of our shape-analysis algorithm to give a conservative answer to the question of whether two pointer variables x and y are must-aliases just before a given program point v: if every shape-node with x in its name also has y in its name, and vice versa, then we conclude that they are must-aliases.

6 In this section, we use the term "shape-graph" in the generic sense, meaning any finite graph structure used to approximate the shapes of run-time data structures.

7 The idea of augmenting shape-graphs with sharing information also appears in the earlier work of Jones and Muchnick [1981].

REFERENCES

ASSMANN, U. AND WEINHARDT, M. 1993. Interprocedural heap analysis for parallelizing imperative programs. In Programming Models For Massively Parallel Computers, W. K. Giloi, S. Jahnichen, and B. D. Shriver, Eds. IEEE Computer Society, Washington, D.C., 74-82.

CHASE, D., WEGMAN, M., AND ZADECK, F. 1990. Analysis of pointers and structures. In SIGPLAN Conference on Programming Languages Design and Implementation. ACM Press, New York, 296-310.

CHOI, J.-D., BURKE, M., AND CARINI, P. 1993. Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side-effects. In Proceedings of the A CM Symposium on Principles of Programming Languages. ACM Press, New York, 232-245.

COUSOT, P. AND COUSOT, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York, 238-252.

DEUTSCH, A. 1992. A storeless model for aliasing and its abstractions using finite representations of right-regular equivalence relations. In Proceedings of the IEEE International Conference on Computer Languages. IEEE Computer Society, Washington, D.C., 2-13.

DEUTSCH, A. 1994. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In SIGPLAN Conference on Programming Languages Design and Implementation. ACM Press, New York, 230-241.

GHIYA, R. AND HENDREN, L. 1996. Is it a tree, a dag, or a cyclic graph? In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York. Available via ftp://ftp-acaps.cs.mcgill.ca/pub/doc/papers/POPL96.ps.gz.

HEINTZE, N. 1992. Set-based program analysis. Ph.D. thesis, School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa.

HENDREN, L. 1990. Parallelizing programs with recursive data structures. Ph.D. thesis, Cornell Univ., Ithaca, N.Y.

HENDREN, L. AND GAO, G. 1992. Designing programming languages for analyzability: A fresh look at pointer data structures. In Proceedings of the International Conference on Computer Languages. IEEE Computer Society, Washington, D.C., 242-251.

HENDREN, L., HUMMEL, J., AND NICOLAU, A. 1992. Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs. In SIGPLAN Conference on Programming Languages Design and Implementation. ACM Press, New York, 249-260.

HENDREN, L. AND NICOLAU, A. 1990. Parallelizing programs with recursive data structures. IEEE Trans. Parallel Distrib. Syst. 1, 1 (Jan.), 35-47.

HORWITZ, S., PFEIFFER, P., AND REPS, T. 1989. Dependence analysis for pointer variables. In SIGPLAN Conference on Programming Languages Design and Implementation. ACM Press, New York, 28-40.

JONES, N. AND MUCHNICK, S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, N.J., Chapter 4, 102-131.

JONES, N. AND MUCHNICK, S. 1982. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York, 66-74.

KNUTH, D. E. 1973. The Art of Computer Programming. Vol. 1, Fundamental Algorithms. 2nd. ed. Addison-Wesley, Reading, Mass.

LANDI, W. 1992. Undecidability of static analysis. ACM Lett. Program. Lang. Syst. 1, 4, 323-337.

LANDI, W. AND RYDER, B. 1991. Pointer induced aliasing: A problem classification. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York, 93103.

LARUS, J. 1989. Restructuring symbolic programs for concurrent execution on multiprocessors. Ph.D. thesis, Univ. of California, Berkeley, Calif.

LARUS, J. AND HILFINGER, P. 1988. Detecting conflicts between structure accesses. In SIGPLAN Conference on Programming Languages Design and Implementation. ACM Press, New York, 21-34.

LINDSTROM, G. 1973. Scanning list structures without stacks or tag bits. Inf. Process. Lett. 2, 2 (June), 47-51.

MOGENSEN, T. 1988. Partially static structures in a self-applicable partial evaluator. In Partial Evaluation and Mixed Computation: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation (Gammel Avernaes, Denmark, Oct 18-24, 1987). North-Holland, Amsterdam, 325-347.

MOGENSEN, T. 1989. Separating binding times in language specifications. In Proceedings of the 4th International Conference on Functional Programming and Computer Architecture. ACM Press, New York, 12-25.

MYERS, E. 1981. A precise inter-procedural data flow algorithm. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, New York, 219-230.

PLEVYAK, J., CHIEN, A., AND KARAMCHETI, V. 1993. Analysis of dynamic structures for efficient parallel execution. In Languages and Compilers for Parallel Computing, U. Banerjee, D. Gelernter, A. Nicolau, and D. Padua, Eds. Lecture Notes in Computer Science, vol. 768. Springer-Verlag, Berlin, 37-57.

RAMAKRISHNAN, R., SESHADRI, P., SRIVASTAVA, D., AND SUDARSHAN, S. 1993. Implementation of the CORAL deductive database system. In Proceedings of the A CM SIGMOD 93 Conference. ACM Press, New York, 167-176.

RAMALINGAM, G. 1994. The undecidability of aliasing. ACM Trans. Program. Lang. Syst. 16, 5, 1467-1471.

REPS, T. 1995. Shape analysis as a generalized path problem. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM'95. ACM Press, New York, 1-11.

REYNOLDS, J. 1968. Automatic computation of data set definitions. In Information Processing 68: Proceedings of the IFIP Congress. North-Holland, Amsterdam, 456-461.

SAGIV, M., REPS, T., AND WILHELM, R. 1995. Solving shape-analysis problems in languages with destructive updating. Tech. Rep. TR-1276, Computer Sciences Dept., Univ. of Wisconsin, Madison, Wisc. July. Available via http://www.cs.wisc.edu/trs.html.

SEDGEWICK, R. 1988. Algorithms. 2nd ed. Addison-Wesley, Reading, Mass.

SHARIR, M. AND PNUELI, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, N.J., 189-234.

STRANSKY, J. 1992. A lattice for abstract interpretation of dynamic (Lisp-like) structures. Inf. Comput. 101, 1 (Nov.), 70-102.

WARREN, D. 1992. Memoing for logic programs. Commun. ACM 35, 3 (Mar.), 93-111.

Printer friendly Cite/link Email Feedback | |

Author: | Sagiv, Mooly; Reps, Thomas; Wilhelm, Reinhard |
---|---|

Publication: | ACM Transactions on Programming Languages & Systems |

Date: | Jan 1, 1998 |

Words: | 20896 |

Previous Article: | A note on "On the Conversion of Indirect to Direct Recursion." (response to Owen Kaser and others, ACM Letters on Programming Languages, vol. 2, p.... |

Next Article: | Synthesis of concurrent systems with many similar processes. |

Topics: |