The Checker Framework Manual:
Custom pluggable types for Java

Chapter 26 Reflection resolution

A call to Method.invoke might reflectively invoke any method. That method might place requirements on its formal parameters, and it might return any value. To reflect these facts, the annotated JDK contains conservative annotations for Method.invoke. These conservative library annotations often cause a checker to issue false positive warnings when type-checking code that uses reflection.

If you supply the -AresolveReflection command-line option, the Checker Framework attempts to resolve reflection. At each call to Method.invoke or Constructor.newInstance, the Checker Framework first soundly estimates which methods might be invoked at run time. When type-checking the call, the Checker Framework uses the library annotations for the possibly-invoked methods, rather than the imprecise one for Method.invoke.

If the estimate of invoked methods is small, the checker issues fewer false positive warnings. If the estimate of invoked methods is large, the resulting types may be no better than the conservative library annotations.

Reflection resolution is disabled by default, because it increases the time to type-check a program. You should enable reflection resolution with the -AresolveReflection command-line option if, for some call site of Method.invoke or Constructor.newInstance in your program:

• 1. the conservative library annotations on Method.invoke or Constructor.newInstance cause false positive warnings,

• 2. the set of possibly-invoked methods or constructors can be known at compile time, and

• 3. the reflectively invoked methods/constructors are on the classpath at compile time.

Reflection resolution does not change your source code or generated code. In particular, it does not replace the Method.invoke or Constructor.newInstance calls.

The command-line option -AresolveReflection=debug outputs verbose information about the reflection resolution process, which may be useful for debugging.

Section 26.1 gives an example of reflection resolution. Then, Section 26.2 describes the MethodVal and ClassVal Checkers, which reflection resolution uses internally. The paper “Static analysis of implicit control flow: Resolving Java reflection and Android intents” [BJM⁺15] (ASE 2015, https://homes.cs.washington.edu/~mernst/pubs/implicit-control-flow-ase2015-abstract.html) gives further details.

26.1 Reflection resolution example

Consider the following example, in which the Nullness Checker employs reflection resolution to avoid issuing a false positive warning.

public class LocationInfo {
    @NonNull Location getCurrentLocation() {    ...   }
}

public class Example {
    LocationInfo privateLocation = ... ;
    String getCurrentCity() throws Exception {
        Method getCurrentLocationObj = LocationInfo.class.getMethod("getCurrentLocation");
        Location currentLocation = (Location) getCurrentLocationObj.invoke(privateLocation);
        return currentLocation.nameOfCity();
    }
}

When reflection resolution is not enabled, the Nullness Checker uses conservative annotations on the Method.invoke method signature:

 @Nullable Object invoke(@NonNull Object recv, @NonNull Object ... args)

This causes the Nullness Checker to issue the following warning even though currentLocation cannot be null.

error: [dereference.of.nullable] dereference of possibly-null reference currentLocation
        return currentLocation.nameOfCity();
               ^
1 error

When reflection resolution is enabled, the MethodVal Checker infers that the @MethodVal annotation for getCurrentLocationObj is:

 @MethodVal(className="LocationInfo", methodName="getCurrentLocation", params=0)

Based on this @MethodVal annotation, the reflection resolver determines that the reflective method call represents a call to getCurrentLocation in class LocationInfo. The reflection resolver uses this information to provide the following precise procedure summary to the Nullness Checker, for this call site only:

 @NonNull Object invoke(@NonNull Object recv, @Nullable Object ... args)

Using this more precise signature, the Nullness Checker does not issue the false positive warning shown above.

26.2 MethodVal and ClassVal Checkers

The implementation of reflection resolution internally uses the ClassVal Checker (Section 26.2.1) and the MethodVal Checker (Section 26.2.2). They are similar to the Constant Value Checker (Chapter 24) in that their annotations estimate the run-time value of an expression.

In some cases, you may need to write annotations such as @ClassVal, @MethodVal, @StringVal, and @ArrayLen to aid in reflection resolution. Often, though, these annotations can be inferred (Section 26.2.3).

26.2.1 ClassVal Checker

The ClassVal Checker defines the following annotations:

@ClassVal(String[] value)

If an expression has @ClassVal type with a single argument, then its exact run-time value is known at compile time. For example, @ClassVal("java.util.HashMap") indicates that the Class object represents the java.util.HashMap class.

If multiple arguments are given, then the expression’s run-time value is known to be in that set.

Each argument is a “fully-qualified binary name” (@FqBinaryName): a primitive or binary name (JLS §13.1), possibly followed by array brackets.

@ClassBound(String[] value)

If an expression has @ClassBound type, then its run-time value is known to be upper-bounded by that type. For example, @ClassBound("java.util.HashMap") indicates that the Class object represents java.util.HashMap or a subclass of it.

If multiple arguments are given, then the run-time value is equal to or a subclass of some class in that set.

Each argument is a “fully-qualified binary name” (@FqBinaryName): a primitive or binary name (JLS §13.1), possibly followed by array brackets.

@UnknownClass

Indicates that there is no compile-time information about the run-time value of the class — or that the Java type is not Class. This is the default qualifier, and it may not be written in source code.

@ClassValBottom

Type given to the null literal. It may not be written in source code.

Subtyping rules

Figure 26.1 shows part of the type hierarchy of the ClassVal type system. @ClassVal(A) is a subtype of @ClassVal(B) if A is a subset of B. @ClassBound(A) is a subtype of @ClassBound(B) if A is a subset of B. @ClassVal(A) is a subtype of @ClassBound(B) if A is a subset of B.

26.2.2 MethodVal Checker

The MethodVal Checker defines the following annotations:

@MethodVal(String[] className, String[] methodName, int[] params)

Indicates that an expression of type Method or Constructor has a run-time value in a given set. If the set has size n, then each of @MethodVal’s arguments is an array of size n, and the ith method in the set is represented by { className[i], methodName[i], params[i] }. For a constructor, the method name is “<init>”.

Consider the following example:

@MethodVal(className={"java.util.HashMap", "java.util.HashMap"},
           methodName={"containsKey", "containsValue"},
           params={1, 1})

This @MethodVal annotation indicates that the Method is either HashMap.containsKey with 1 formal parameter or HashMap.containsValue with 1 formal parameter.

The @MethodVal type qualifier indicates the number of parameters that the method takes, but not their type. This means that the Checker Framework’s reflection resolution cannot distinguish among overloaded methods.

@UnknownMethod

Indicates that there is no compile-time information about the run-time value of the method — or that the Java type is not Method or Constructor. This is the default qualifier, and it may not be written in source code.

@MethodValBottom

Type given to the null literal. It may not be written in source code.

Subtyping rules

Figure 26.2 shows part of the type hierarchy of the MethodVal type system. @MethodVal(className=CA, methodName=MA, params=PA) is a subtype of @MethodVal(className=CB, methodName=MB, params=PB) if

where CA, MA, and PA are lists of equal size and CB, MB, and PB are lists of equal size.

26.2.3 MethodVal and ClassVal inference

The developer rarely has to write @ClassVal or @MethodVal annotations, because the Checker Framework infers them according to Figure 26.3. Most readers can skip this section, which explains the inference rules.

The ClassVal Checker infers the exact class name (@ClassVal) for a Class literal (C.class), and for a static method call (e.g., Class.forName(arg), ClassLoader.loadClass(arg), ...) if the argument is a statically computable expression. In contrast, it infers an upper bound (@ClassBound) for instance method calls (e.g., obj.getClass()).

The MethodVal Checker infers @MethodVal annotations for Method and Constructor types that have been created using a method call to Java’s Reflection API:

• • Class.getMethod(String name, Class<?>... paramTypes)

• • Class.getConstructor(Class<?>... paramTypes)

Note that an exact class name is necessary to precisely resolve reflectively-invoked constructors since a constructor in a subclass does not override a constructor in its superclass. This means that the MethodVal Checker does not infer a @MethodVal annotation for Class.getConstructor if the type of that class is @ClassBound. In contrast, either an exact class name or a bound is adequate to resolve reflectively-invoked methods because of the subtyping rules for overridden methods.