SOLVING SHAPE-ANALYSIS PROBLEMS IN LANGUAGES WITH DESTRUCTIVE UPDATING

This article concerns the static analysis of programs that perform des tructive updating on heap allocated storage. We give an algorithm that uses finite shape graphs to approximate conservatively the possible ' 'shapes'' that heap-allocated structures in a program can take on. For certain programs, our technique is able to determine such properties as (1) when the input to the program is a list, the output is also a l ist and (2) when the input to the program is a tree, the output is als o a tree. For example, the method can determine that ''listness'' is p reserved by (1) a program that performs list reversal via destructive updating of the input list and (2) a program that searches a list and splices a new element into the list. None of the previously known meth ods that use graphs to model the program's store are capable of determ ining that ''listness'' is preserved on these examples (or examples of similar complexity). In contrast with most previous work, our shape a nalysis algorithm is even accurate for certain programs that update cy clic 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 circ ular list. For example, the shape-analysis algorithm can determine tha t an insertion into a circular list preserves ''circular listness.''