The Checker Framework Manual:
Custom pluggable types for Java

Chapter 15 Format String Checker

The Format String Checker prevents use of incorrect format strings in format methods such as System.out.printf and String.format.

The Format String Checker warns you if you write an invalid format string, and it warns you if the other arguments are not consistent with the format string (in number of arguments or in their types). Here are examples of errors that the Format String Checker detects at compile time. Section 15.3 provides more details.

    String.format("%y", 7);            // error: invalid format string

    String.format("%d", "a string");   // error: invalid argument type for %d

    String.format("%d %s", 7);         // error: missing argument for %s
    String.format("%d", 7, 3);         // warning: unused argument 3
    String.format("{0}", 7);           // warning: unused argument 7, because {0} is wrong syntax

To run the Format String Checker, supply the -processor org.checkerframework.checker.formatter.FormatterChecker command-line option to javac.

The paper “A type system for format strings” [WKSE14] (ISSTA 2014, https://homes.cs.washington.edu/~mernst/pubs/format-string-issta2014-abstract.html) gives more details about the Format String Checker and the Internationalization Format String Checker (Chapter 16).

15.1 Formatting terminology

Printf-style formatting takes as an argument a format string and a list of arguments. It produces a new string in which each format specifier has been replaced by the corresponding argument. The format specifier determines how the format argument is converted to a string. A format specifier is introduced by a % character. For example, String.format("The %s is %d.","answer",42) yields "The answer is 42.". "The %s is %d." is the format string, "%s" and "%d" are the format specifiers; "answer" and 42 are format arguments.

15.2 Format String Checker annotations

The @Format qualifier on a string type indicates a valid format string. A programmer rarely writes the @Format annotation, as it is inferred for string literals. A programmer may need to write it on fields and on method signatures.

The @Format qualifier is parameterized with a list of conversion categories that impose restrictions on the format arguments. Conversion categories are explained in more detail in Section 15.2.1. The type qualifier for "%d %f" is, for example, @Format({INT, FLOAT}).

Consider the below printFloatAndInt method. Its parameter must be a format string that can be used in a format method, where the first format argument is “float-like” and the second format argument is “integer-like”. The type of its parameter, @Format({FLOAT, INT}) String, expresses that contract.

    void printFloatAndInt(@Format({FLOAT, INT}) String fs) {
        System.out.printf(fs, 3.1415, 42);
    }

    printFloatAndInt("Float %f, Number %d");   // OK
    printFloatAndInt("Float %f");              // error

Figure 15.1 shows all the type qualifiers. The annotations other than @Format are only used internally and cannot be written in your code. @InvalidFormat indicates an invalid format string — that is, a string that cannot be used as a format string. For example, the type of "%y" is @InvalidFormat String. @FormatBottom is the type of the null literal. @UnknownFormat is the default that is applied to strings that are not literals and on which the user has not written a @Format annotation.

There is also a @FormatMethod annotation; see Section 15.5.

15.2.1 Conversion categories

Given a format specifier, only certain format arguments are compatible with it, depending on its “conversion” — its last, or last two, characters. For example, in the format specifier "%d", the conversion d restricts the corresponding format argument to be “integer-like”:

      String.format("%d", 5);          // OK
      String.format("%d", "hello");    // error

Many conversions enforce the same restrictions. A set of restrictions is represented as a conversion category. The “integer-like” restriction is, for example, the conversion category INT. The following conversion categories are defined in the ConversionCategory enumeration:

GENERAL: imposes no restrictions on a format argument’s type. Applicable for conversions b, B, h, H, s, S.
CHAR: requires that a format argument represents a Unicode character. Specifically, char, Character, byte, Byte, short, and Short are allowed. int or Integer are allowed if Character.isValidCodePoint(argument) would return true for the format argument. (The Format String Checker permits any int or Integer without issuing a warning or error — see Section 15.3.2.) Applicable for conversions c, C.
INT: requires that a format argument represents an integral type. Specifically, byte, Byte, short, Short, int and Integer, long, Long, and BigInteger are allowed. Applicable for conversions d, o, x, X.
FLOAT: requires that a format argument represents a floating-point type. Specifically, float, Float, double, Double, and BigDecimal are allowed. Surprisingly, integer values are not allowed. Applicable for conversions e, E, f, g, G, a, A.
TIME: requires that a format argument represents a date or time. Specifically, long, Long, Calendar, and Date are allowed. Applicable for conversions t, T.
UNUSED: imposes no restrictions on a format argument. This is the case if a format argument is not used as replacement for any format specifier. "%2$s", for example, ignores the first format argument.

All conversion categories accept null. Furthermore, null is always a legal argument array, because it is treated as supplying null to each format specifier. For example, String.format("%d %f %s", (Object[]) null) evaluates to "null null null".

The same format argument may serve as a replacement for multiple format specifiers. Until now, we have assumed that the format specifiers simply consume format arguments left to right. But there are two other ways for a format specifier to select a format argument:

• n$ specifies a one-based index n. In the format string "%2$s", the format specifier selects the second format argument.
• The < flag references the format argument that was used by the previous format specifier. In the format string "%d %<d", for example, both format specifiers select the first format argument.

In the following example, the format argument must be compatible with both conversion categories, and can therefore be neither a Character nor a long.

    format("Char %1$c, Int %1$d", (int)42);                  // OK
    format("Char %1$c, Int %1$d", new Character(42));        // error
    format("Char %1$c, Int %1$d", (long)42);                 // error

Only three additional conversion categories are needed to represent all possible intersections of previously-mentioned conversion categories:

NULL: is used if no object of any type can be passed as parameter. In this case, the only legal value is null. For example, the format string "%1$f %1$c" requires that the first format argument be null. Passing either 4 or 4.2 would lead to an exception.
CHAR_AND_INT: is used if a format argument is restricted by a CHAR and a INT conversion category (CHAR ∩ INT).
INT_AND_TIME: is used if a format argument is restricted by an INT and a TIME conversion category (INT ∩ TIME).

All other intersections lead to already existing conversion categories. For example, GENERAL ∩ CHAR = CHAR and UNUSED ∩ GENERAL = GENERAL.

Figure 15.2 summarizes the subset relationship among all conversion categories.

15.2.2 Subtyping rules for `@Format`

Here are the subtyping rules among different @Format qualifiers. It is legal to:

• use a format string with a weaker (less restrictive) conversion category than required.
• use a format string with fewer format specifiers than required. Although this is legal, a warning is issued because most occurrences of this are due to programmer error.

The following example shows the subtyping rules in action:

    @Format({FLOAT, INT}) String f;

    f   =   "%f %d";      //   OK
    f   =   "%s %d";      //   OK, %s is weaker than %f
    f   =   "%f";         //   warning: last argument is ignored
    f   =   "%f %d %s";   //   error: too many arguments
    f   =   "%d %d";      //   error: %d is not weaker than %f

    String.format(f, 0.8, 42);

15.3 What the Format String Checker checks

If the Format String Checker issues no errors, it provides the following guarantees:

1. The following guarantees hold for every format method invocation:
- (a) The format method’s first argument (or second if a Locale is provided) is a valid format string (or null).
- (b) A warning is issued if one of the format string’s conversion categories is UNUSED.
- (c) None of the format string’s conversion categories is NULL.
2. If the format arguments are passed to the format method as varargs, the Format String Checker guarantees the following additional properties:
- (a) No fewer format arguments are passed than required by the format string.
- (b) A warning is issued if more format arguments are passed than required by the format string.
- (c) Every format argument’s type satisfies its conversion category’s restrictions.
3. If the format arguments are passed to the format method as an array, a warning is issued by the Format String Checker.

Following are examples of every guarantee:

    String.format("%d", 42);                       //   OK
    String.format(Locale.GERMAN, "%d", 42);        //   OK
    String.format(new Object());                   //   error (1a)
    String.format("%y");                           //   error (1a)
    String.format("%2$s", "unused", "used");       //   warning (1b)
    String.format("%1$d %1$f", 5.5);               //   error (1c)
    String.format("%1$d %1$f %d", null, 6);        //   error (1c)
    String.format("%s");                           //   error (2a)
    String.format("%s", "used", "ignored");        //   warning (2b)
    String.format("%c",4.2);                       //   error (2c)
    String.format("%c", (String)null);             //   error (2c)
    String.format("%1$d %1$f", new Object[]{1});   //   warning (3)
    String.format("%s", new Object[]{"hello"});    //   warning (3)

15.3.1 Possible false alarms

There are three cases in which the Format String Checker may issue a warning or error, even though the code cannot fail at run time. (These are in addition to the general conservatism of a type system: code may be correct because of application invariants that are not captured by the type system.) In each of these cases, you can rewrite the code, or you can manually check it and write a @SuppressWarnings annotation if you can reason that the code is correct.

Case 1b: Unused format arguments. It is legal to provide more arguments than are required by the format string; Java ignores the extras. However, this is an uncommon case. In practice, a mismatch between the number of format specifiers and the number of format arguments is usually an error.

Case 1c: Format arguments that can only be null. It is legal to write a format string that permits only null arguments and throws an exception for any other argument. An example is String.format("%1$d %1$f", null). The Format String Checker forbids such a format string. If you should ever need such a format string, simply replace the problematic format specifier with "null". For example, you would replace the call above by String.format("null null").

Case 3: Array format arguments. The Format String Checker performs no analysis of arrays, only of varargs invocations. It is better style to use varargs when possible.

15.3.2 Possible missed alarms

The Format String Checker helps prevent bugs by detecting, at compile time, which invocations of format methods will fail. While the Format String Checker finds most of these invocations, there are cases in which a format method call will fail even though the Format String Checker issued neither errors nor warnings. These cases are:

1. The format string is null. Use the Nullness Checker to prevent this.
2. A format argument’s toString method throws an exception.
3. A format argument implements the Formattable interface and throws an exception in the formatTo method.
4. A format argument’s conversion category is CHAR or CHAR_AND_INT, and the passed value is an int or Integer, and Character.isValidCodePoint(argument) returns false.

The following examples illustrate these limitations:

    class A {
        public String toString() {
            throw new Error();
        }
    }

    class B implements Formattable {
        public void formatTo(Formatter fmt, int f,
                int width, int precision) {
            throw new Error();
        }
    }

    // The checker issues no errors or warnings for the
    // following illegal invocations of format methods.
    String.format(null);          // NullPointerException (1)
    String.format("%s", new A()); // Error (2)
    String.format("%s", new B()); // Error (3)
    String.format("%c", (int)-1); // IllegalFormatCodePointException (4)

15.4 Implicit qualifiers

The Format String Checker adds implicit qualifiers, reducing the number of annotations that must appear in your code (see Section 33.4). The checker implicitly adds the @Format qualifier with the appropriate conversion categories to any String literal that is a valid format string.

15.5 @FormatMethod

Your project may contain methods that forward their arguments to a format method. Consider for example the following log method:

@FormatMethod
void log(String format, Object... args) {
    if (enabled) {
        logfile.print(indent_str);
        logfile.printf(format, args);
    }
}

You should annotate such a method with the @FormatMethod annotation, which indicates that the String argument is a format string for the remaining arguments.

15.6 Testing whether a format string is valid

The Format String Checker automatically determines whether each String literal is a valid format string or not. When a string is computed or is obtained from an external resource, then the string must be trusted or tested.

One way to test a string is to call the FormatUtil.asFormat method to check whether the format string is valid and its format specifiers match certain conversion categories. If this is not the case, asFormat raises an exception. Your code should catch this exception and handle it gracefully.

The following code examples may fail at run time, and therefore they do not type-check. The type-checking errors are indicated by comments.

Scanner s = new Scanner(System.in);
String fs = s.next();
System.out.printf(fs, "hello", 1337);   // error: fs is not known to be a format string

Scanner s = new Scanner(System.in);
@Format({GENERAL, INT}) String fs = s.next();       // error: fs is not known to have the given type
System.out.printf(fs, "hello", 1337);               // OK

The following variant does not throw a run-time error, and therefore passes the type-checker:

Scanner s = new Scanner(System.in);
String format = s.next();
try {
    format = FormatUtil.asFormat(format, GENERAL, INT);
} catch (IllegalFormatException e) {
    // Replace this by your own error handling.
    System.err.println("The user entered the following invalid format string: " + format);
    System.exit(2);
}
// `format` is now known to be of type: @Format({GENERAL, INT}) String
System.out.printf(format, "hello", 1337);

To use the FormatUtil class, the checker-util.jar file must be on the classpath at run time.

The Checker Framework Manual: Custom pluggable types for Java