Static Analysis of Accessed Regions in Recursive Data Structures

Abstract

This paper presents a heap analysis algorithm that characterizes how programs access regions within recursive data structures, such as sublists within lists or subtrees within trees. The analysis precisely computes cyclicity, reachability, and heap access region information for programs with destructive updates.

The algorithm uses a shape graph abstraction of the heap that identifies connected, single-entry heap regions, whose entries are directly accessible from the stack. The edges of the shape graphs encode reachability information. This yields a more compact heap representation compared to the existing abstractions, making the analysis more efficient. Furthermore, the algorithm expresses heap access information using labels on the nodes of the shape graphs. The labels characterize the concrete locations that abstract nodes represent and make it possible to compare the sets of concrete locations modeled by nodes in different shape graphs. The labels allow the analysis to express the heap access information with respect to the nodes at a particular program point, for instance at the beginning of the current procedure. Our analysis is able to precisely and efficiently compute heap access region information for complex heap manipulations such as a recursive quicksort program that sorts a list in-place, using destructive updates.