Uniqueness Inference for Object-Oriented Languages

Abstract. Sharing and mutability are inherent in object-oriented languages, but they make precise typestate analysis difficult: state changes made via one alias need to be reflected in other aliases. Therefore, typestate analysis requires alias information and uniqueness has proven to be essential for accuracy of analysis. Present alias analyses either require programmer annotations or are unable to infer uniqueness in the presence of lending, whereby a unique reference is tem-porarily passed to a method. In this paper, we propose a modular method to infer uniqueness properties for object-oriented languages. We advocate a restricted form of lending, which we call lent-once, to ensure exclusive access to the referenced object and thus al-low state changes to be captured. Furthermore, unlike previous alias type systems which rely on destructive read for object fields to guarantee uniqueness, we do not impose any such change on the semantics of the underlying language. We achieve this by maintaining a set of consumed uniqueness that is tracked in a flow-sensitive manner, with each field’s uniqueness assured at method boundary.