Publication: Static Analysis of Accessed Regions in Recursive Data Structures
Date
Authors
Published Version
Journal Title
Journal ISSN
Volume Title
Publisher
Citation
Abstract
This paper presents an inter-procedural heap analysis that computes information about how programs access regions within recursive data structures, such as sublists within lists or subtrees within trees. The analysis is able to accu- rately compute heap access information for statements and procedures in recur- sive programs with destructive updates. We formulate our algorithm as a dataflow analysis which computes shape information and heap access information at each program point. We use an abstraction of the heap based on shape graphs, whose nodes represent heap regions and whose edges encode the reachability between these regions. Our analysis is able to summarize the effects of procedures: it com- putes the heap regions being accessed by each procedure in terms of the heap abstraction at the entry of the procedure. We use node labels to express the re- gions at program points inside procedures in terms of the regions at procedure entry points. The inter-procedural analysis uses a fixpoint algorithm to compute the heap regions accessed by the whole execution of each procedure, including all of the procedures it invokes. We demonstrate how our analysis computes precise heap region access information for a recursive quicksort program that sorts a list in-place, using destructive updates.