The Checker Framework Manual:
Custom pluggable types for Java

Chapter 24 Constant Value Checker

The Constant Value Checker is a constant propagation analysis: for each variable, it determines whether that variable’s value can be known at compile time.

There are two ways to run the Constant Value Checker.

• • Typically, it is automatically run by another type-checker.

• • Alternatively, you can run just the Constant Value Checker by supplying the following command-line option to javac: -processor org.checkerframework.common.value.ValueChecker

24.1 Annotations

The Constant Value Checker uses type annotations to indicate the value of an expression (Section 24.1.1), and it uses method annotations to indicate methods that the Constant Value Checker can execute at compile time (Section 24.2.2).

24.1.1 Type annotations

Typically, the programmer does not write any type annotations. Rather, the type annotations are inferred by the Constant Value Checker. The programmer is also permitted to write type annotations. This is only necessary in locations where the Constant Value Checker does not infer annotations: on fields and method signatures.

The main type annotations are @BoolVal, @IntVal, @IntRange, @DoubleVal, @StringVal, @MatchesRegex, @DoesNotMatchRegex, and @EnumVal. Additional type annotations for arrays and strings are @ArrayLen, @ArrayLenRange, and @MinLen. A polymorphic qualifier (@PolyValue) is also supported (see Section 32.2). In addition, there are separate checkers for @ClassVal and @MethodVal annotations (see Section 26.2).

Each *Val type annotation takes as an argument a set of values, and its meaning is that at run time, the expression evaluates to one of the values. For example, an expression of type @StringVal("a", "b") evaluates to one of the values "a", "b", or null. The set is limited to 10 entries; if a variable could have more than 10 different values, the Constant Value Checker gives up and its type becomes @IntRange for integral types, @ArrayLenRange for array types, @MatchesRegex, @DoesNotMatchRegex, @ArrayLen, or @ArrayLenRange for String, and @UnknownVal for all other types. The @ArrayLen annotation means that at run time, the expression evaluates to an array or a string whose length is one of the annotation’s arguments.

In the case of too many strings in @StringVal, the values are forgotten and just the lengths are used in @ArrayLen. If this would result in too many lengths, only the minimum and maximum lengths are used in @ArrayLenRange, giving a range of possible lengths of the string.

The @StringVal, @MatchesRegex, and @DoesNotMatchRegex annotations may be applied to char arrays. Although byte arrays are often converted to/from strings, these annotations may not be applied to them. This is because the conversion depends on the platform’s character set.

The @MatchesRegex and @DoesNotMatchRegex annotations use the standard Java regular expression syntax. @MatchesRegex(A) is only a subtype of @MatchesRegex(B) if the set of regular expressions A is a subset of the set of regular expressions B. An @StringVal annotation is a subtype of a @MatchesRegex annotation if each string matches at least one of the regular expressions. @DoesNotMatchRegex(A) is only a subtype of @DoesNotMatchRegex(B) if the set of regular expressions A is a superset of the set of regular expressions B. Matching is done via the java.lang.String#matches method, which matches against the entire string (it does not look for a matching substring).

The @EnumVal annotation’s argument is the names of the enum constants that the type might evaluate to. (Java syntax does not allow the enum constants themselves to be arguments.) @EnumVal is treated identically to @StringVal by the checker internally, so @StringVal may appear in error messages related to enums.

@IntRange takes two arguments — a lower bound and an upper bound. Its meaning is that at run time, the expression evaluates to a value between the bounds (inclusive). For example, an expression of type @IntRange(from=0, to=255) evaluates to 0, 1, 2, …, 254, or 255. An @IntVal annotation and an @IntRange annotation that represent the same set of values are semantically identical and interchangeable: they have exactly the same meaning, and using either one has the same effect. @ArrayLenRange has the same relationship to @ArrayLen that @IntRange has to @IntVal. The @MinLen annotation is an alias for @ArrayLenRange (meaning that every @MinLen annotation is automatically converted to an @ArrayLenRange annotation) that only takes one argument, which is the lower bound of the range. The upper bound of the range is the maximum integer value.

Figure 24.1 shows the subtyping relationship among the type annotations. For two annotations of the same type, subtypes have a smaller set of possible values, as also shown in the figure. Because int can be cast to double, an @IntVal annotation is a subtype of a @DoubleVal annotation with the same values.

Figure 24.2 illustrates how the Constant Value Checker infers type annotations (using flow-sensitive type qualifier refinement, Section 33.7).

public void flowSensitivityExample(boolean b) {
    int i = 1;     // i has type: @IntVal({1}) int
    if (b) {
        i = 2;     // i now has type: @IntVal({2}) int
    }
                   // i now has type: @IntVal({1,2}) int
    i = i + 1;     // i now has type: @IntVal({2,3}) int
}

24.2 Other constant value annotations

The Checker Framework’s constant value annotations are similar to annotations used elsewhere.

If your code is already annotated with a different constant value or range annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Constant Value Checker, as described in Figure 24.3. If the other annotation is a declaration annotation, it may be moved; see Section 40.6.10.

The Constant Value Checker trusts the @Positive, @NonNegative, and @GTENegativeOne annotations. If your code contains any of these annotations, then in order to guarantee soundness, you must run the Index Checker whenever you run the Constant Value Checker.

24.2.1 Compile-time execution of expressions

Whenever all the operands of an expression are compile-time constants (that is, their types have constant-value type annotations), the Constant Value Checker attempts to execute the expression. This is independent of any optimizations performed by the compiler and does not affect the code that is generated.

The Constant Value Checker statically executes (at compile time) operators that do not throw exceptions (e.g., +, -, <<, !=).

24.2.2 @StaticallyExecutable methods and the classpath

The Constant Value Checker statically executes (at compile time) methods annotated with @StaticallyExecutable.

@StaticallyExecutable @Pure
public static int myAdd(int a, int b) {
    return a + b;
}

public void   bar() {
    int a =   5;             // a has type:    @IntVal({5}) int
    int b =   4;             // b has type:    @IntVal({4}) int
    int c =   myAdd(a, b);   // c has type:    @IntVal({9}) int
}

The static execution feature has some requirements:

• • A @StaticallyExecutable method must be @Pure (side-effect-free and deterministic).

• • The Constant Value Checker must have an estimate for all the arguments at a call site.

  This means that @StaticallyExecutable is not applicable to user-written instance methods. It is only applicable to instance methods whose receiver is a compile-time constant, such as a primitive wrapper or an array.

• • The @StaticallyExecutable method and any method it calls must be on the same path (the classpath or the processorpath) as the Checker Framework. This is because the Constant Value Checker reflectively calls these methods at compile time.

  To use @StaticallyExecutable on methods in your own code, you should first compile the code without the Constant Value Checker and then add the location of the resulting .class files to the classpath or processorpath, whichever is appropriate. For example, the command-line arguments to the Checker Framework might include:

       -processor org.checkerframework.common.value.ValueChecker
       -classpath $CLASSPATH:MY_PROJECT/build/
  

  or

      -processor org.checkerframework.common.value.ValueChecker
      -processorpath ${CHECKERFRAMEWORK}/checker/build/libs/checker-4.2.1-SNAPSHOT.jar:MY_PROJECT/build/
  

24.3 Warnings

If the option -AreportEvalWarns is used, the Constant Value Checker issues a warning if it cannot load and run, at compile time, a method marked as @StaticallyExecutable. If it issues such a warning, then the return value of the method will be @UnknownVal instead of being resolved to a specific value annotation. Here are some examples:

• • [class.find.failed] Failed to find class named Test.

  The checker could not find the class specified for resolving a @StaticallyExecutable method. Typically this means that the path that contains the Checker Framework (the classpath or the processorpath) lacks the given classfile.

• • [method.find.failed] Failed to find a method named foo with argument types [@IntVal(3) int].

  The checker could not find the method foo(int) specified for resolving a @StaticallyExecutable method, but could find the class. This is usually due to providing an outdated version of the classfile that does not contain the method that was annotated as @StaticallyExecutable.

• • [method.evaluation.exception] Failed to evaluate method public static int Test.foo(int) because it threw an exception: java.lang.ArithmeticException: / by zero.

  An exception was thrown when trying to statically execute (at compile time) the method. In this case, it was a divide-by-zero exception. If the arguments to the method each only had one value in their annotations, then this exception will always occur when the program is actually run as well. If there are multiple possible values then the exception might not be thrown on every execution, depending on the run-time values.

There are some other situations in which the Constant Value Checker produces a warning message:

• • [too.many.values.given] The maximum number of arguments permitted is 10.

  The Constant Value Checker only tracks up to 10 possible values for an expression. If you write an annotation with more values than will be tracked, the annotation is replaced with @IntRange, @ArrayLen, @ArrayLenRange, or @UnknownVal.

24.4 Unsoundly ignoring overflow

The Constant Value Checker takes Java’s overflow rules into account when computing the possible values of expressions. The -AignoreRangeOverflow command-line option makes it ignore the possibility of overflow for range annotations @IntRange and @ArrayLenRange. Figure 24.5 gives an example of behavior with and without the -AignoreRangeOverflow command-line option.

    ...
    if (i > 5) {
      // i now has type: @IntRange(from=5, to=Integer.MAX_VALUE)
      i = i + 1;
      // If i started out as Integer.MAX_VALUE, then i is now Integer.MIN_VALUE.
      // i's type is now @IntRange(from=Integer.MIN_VALUE, to=Integer.MAX_VALUE).
      // When ignoring overflow, i's type is now @IntRange(from=6, to=Integer.MAX_VALUE).
    }

As with any unsound behavior in the Checker Framework, this option reduces the number of warnings and errors produced, and may reduce the number of @IntRange qualifiers that you need to write in the source code. However, it is possible that at run time, an expression might evaluate to a value that is not in its @IntRange qualifier. You should either accept that possibility, or verify the lack of overflow using some other tool or manual analysis.

24.5 Strings can be null in concatenations

By default, the Constant Value Checker is sound with respect to string concatenation and nullness. It assumes that, in a string concatenation, every non-primitive argument might be null, except for String literals and compile-time constants. It ignores Nullness Checker annotations. (This behavior is conservative but sound.)

Consider a variable declared as @StringVal("a", "b") String x;. At run time, x evaluates to one of the values "a", "b", or null. Therefore, the type of “x + "c"” is @StringVal("ac", "bc", "nullc") String.

The -AnonNullStringsConcatenation command-line option makes the Constant Value Checker unsoundly assume that no arguments in a string concatenation are null. With the command-line argument, the type of “x + "c"” is @StringVal("ac", "bc") String.