| Abstract Ownership and uniqueness are important properties that improve local reasoning in complex software systems. Unique objects, which are those referred to by only one pointer, are by definition unaliased. Owned objects are completely encapsulated within another object, and hence their use is tightly controlled. In this paper we present a novel static analysis for automatically inferring ownership and uniqueness in Java programs. Our analysis requires no annotations, and combines an intraprocedural points-to analysis with an interprocedural, demand-driven predicate resolution algorithm to compute uniqueness and ownership. We have implemented our analysis as a tool called Uno and applied it to a variety of Java applications. Our experimental results show that Uno finds many uses of ownership and uniqueness in programs. As a result, we believe that Uno can be a valuable tool for discovering and checking ownership and uniqueness properties in Java programs. |