This article concerns the static analysis of programs that perform destructive 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 list and (2) when the input to the program is a tree, the output is also a tree. For example, the method can determine that ``listness'' is preserved 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 methods that use graphs to model the program's store are capable of determining that ``listness'' is preserved on these examples (or examples of similar complexity). In contrast with most previous work, our shape analysis 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.''

CR Categories and Subject Descriptors: D.2.5 [Software Engineering]: Testing and Debugging -- symbolic execution; D.3.3 [Programming Languages]: Language Constructs and Features -- data types and structures, dynamic storage management; D.3.4 [Programming Languages]: Processors -- optimization; E.1 [Data]: Data Structures -- graphs, lists, trees; E.2 [Data]: Data Storage Representations -- composite structures, linked representations; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs -- assertions, invariants; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs -- type structure

General Terms: Algorithms, Languages, Theory, Verification

Additional Key Words and Phrases: abstract interpretation, alias analysis, dataflow analysis, destructive updating, pointer analysis, shape analysis, shape graphs, static analysis

(Click here to access the paper: PostScript, PDF.)