Shape Analysis with Reference Set Relations

Tracking subset relations between the contents containers on the heap is fundamental to modeling the semantics of many common programing idioms such as applying a function to a subset of objects and maintaining multiple views of the same set of objects. We introduce a relation, must reference sets, which subsumes the concept of must-aliasing and enables existing shape analysis techniques to efficiently and accurately model many types of containment properties without the use of explicit quantification or specialized logics for containers/sets. We extend an existing shape analysis to model the concept of reference sets. Reference sets allow the analysis to efficiently track a number of important relations (must-=, and must-) between objects that are the targets of sets of references (variables or pointers). We show that shape analysis augmented with reference set information is able to precisely model sharing for a range of data structures in real programs that cannot be expressed using...

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur
• Keywords: Reference Sets, Shape Analysis, Shape Analysis Techniques, Software Engineering, VMCAI 2010