Type qualifier inference for Java

Java’s type system provides programmers with strong guarantees of type and memory safety, but there are many important properties not captured by standard Java types. We describe JQual, a tool that adds user-defined type qualifiers to Java, allowing programmers to quickly and easily incorporate extra lightweight, application-specific type checking into their programs. JQual provides type qualifier inference, so that programmers need only add a few key qualifier annotations to their program, and then JQual infers any remaining qualifiers and checks their consistency. We explore two applications of JQual. First, we introduce opaque and enum qualifiers to track C pointers and enumerations that flow through Java code via the JNI. In our benchmarks we found that these C values are treated correctly, but there are some places where a client could potentially violate safety. Second, we introduce a readonly qualifier for annotating references that cannot be used to modify the objects they refer to. We found that JQual is able to automatically infer readonly in many places on method signatures. These results suggest that type qualifiers and type qualifier inference are a useful addition to Java. Categories and Subject Descriptors D.2.4 [Software Engineering]