Precise set sharing analysis for Java-style programs (and proofs)

Abstract

Finding useful sharing information between instances in object-oriented programs has recently been the focus of much research.
The applications of such static analysis are multiple: by knowing which
variables definitely do not share in memory we can apply conventional
compiler optimizations, find coarse-grained parallelism opportunities, or,
more importantly, verify certain correctness aspects of programs even
in the absence of annotations. In this paper we introduce a framework
for deriving precise sharing information based on abstract interpretation for a Java-like language. Our analysis achieves precision in various
ways, including supporting multivariance, which allows separating different contexts. We propose a combined Set Sharing + Nullity + Classes
domain which captures which instances do not share and which ones are
definitively null, and which uses the classes to refine the static information when inheritance is present. The use of a set sharing abstraction
allows a more precise representation of the existing sharings and is crucial in achieving precision during interprocedural analysis. Carrying the
domains in a combined way facilitates the interaction among them in the
presence of multivariance in the analysis. We show through examples and
experimentally that both the set sharing part of the domain as well as
the combined domain provide more accurate information than previous
work based on pair sharing domains, at reasonable cost.