Shape Analysis with Reference Set Dominance

Precise modeling of the structure of the heap and how objects are shared between various arrays or data structures is fundamental to understanding the behavior of a program. This paper introduces a novel higher order relation, reference set dominance, which subsumes the concept of aliasing and enables ex- isting shape analysis techniques to, efficiently and accura tely, model many types of containment properties without the use of explicit quantification or special- ized logics for containers/sets. We extend an existing shape analysis to model the concept of reference set dominance. This concept allows the analysis to track a number of important relations (must =, and must ⊆) between the sets of objects that are the targets of two given sets of references (variabl es or pointers). In combination with shape properties, an analysis that tracks reference domi- nance information can precisely reason about sharing properties on the heap (are the contents of one array a subset of another array?), and how sharing influences the results of destructive updates (does modifying all the o bjects in one array imply that all the objects in another array are modified as wel l?). Precisely and efficiently reasoning about these kinds of sharing properti es has been beyond the abilities of previous analyses. We show that shape analysis augmented with dom- inance information is able to precisely model sharing for a large range of data structures in real programs and in contrast to more expressive proposals based on logic languages (e.g., extensions of first-order predicate logic with transitive clo- sure), dominance properties can be efficiently implemented in a shape analyzer.