Shape Analysis with Reference Set Relations

11 years 10 months ago
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...
Mark Marron, Rupak Majumdar, Darko Stefanovic, Dee
Added 05 Mar 2010
Updated 08 Mar 2010
Type Conference
Year 2010
Authors Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur
Comments (0)