This chapter is about tools that infer annotations for your program’s method signatures and fields, before you run a type-checker. To learn about local type inference within a method body, see Section 33.7.
A typical workflow (Section 2.4) is for a programmer to first write annotations on method signatures and fields, then run a type-checker. Type inference performs the first step automatically for you. This saves time for programmers who would otherwise have to understand the code, then write annotations manually.
Type inference outputs type qualifiers that are consistent with your program’s source code. Your program still might not type-check if your program contains a bug or contains tricky code that is beyond the capabilities of the type-checker.
The qualifiers are output into an annotation file. They can be viewed and adjusted by the programmer, can be used by tools such as the type-checker, and can be inserted into the source code or the class file.
Inserting the inferred annotations into the program source code creates documentation in the form of type qualifiers, which can aid programmer understanding and may make type-checking warnings more comprehensible. Storing annotations in side-files is more desirable if the program’s source code cannot be modified for some reason, if the type-checking is “one-off” (type-checking will be done once and its results will be evaluated, but it will not be done repeatedly), or if the set of annotations is extremely voluminous and would clutter the code.
Type inference is most effective when you run it on a program rather than on a library — unless you also run it on an extensive test suite for the library. See Section 35.7 for an explanation.
Type inference is costly: it takes several times longer than type-checking does. However, it only needs to be run once, after which you can use and possibly modify the results.
This section lists tools that take a program and output a set of annotations for it. It first lists tools that work only for a single type system (but may do a more accurate job for that type system), then lists general tools that work for any type system.
Section 3.3.7 lists several tools that infer annotations for the Nullness Checker.
If you run the Checker Framework with the -AsuggestPureMethods command-line option, it will suggest methods that can be marked as @SideEffectFree, @Deterministic, or @Pure; see Section 33.7.5.
“Whole program inference”, or WPI, is distributed with the Checker Framework. See Section 35.2.
“Checker Framework Inference”, or CFI, is a type inference framework built on a variant of the Checker Framework. You need to slightly rewrite your type system to work with CFI. The CFI repository contains rewritten versions of some of the type systems that are distributed with the Checker Framework.
Cascade [VPEJ15] is an Eclipse plugin that implements interactive type qualifier inference. Cascade is interactive rather than fully-automated: it makes it easier for a developer to insert annotations. Cascade starts with an unannotated program and runs a type-checker. For each warning it suggests multiple fixes, the developer chooses a fix, and Cascade applies it. Cascade works with any checker built on the Checker Framework. You can find installation instructions and a video tutorial at https://github.com/reprogrammer/cascade. Cascade was last updated in November 2014, so it might or might not work for you.
Except for one of the nullness inference tools, all these type inference tools are static analyses. They analyze your program’s source code, but they do not run your program.
Whole-program inference infers types for fields, method parameters, and method return types that do not have a user-written qualifier (for the given type system). The inferred type qualifiers are output into annotation files. The inferred type is the most specific type that is compatible with all the uses in the program. For example, the inferred type for a field is the least upper bound of the types of all the expressions that are assigned into the field.
There are four scripts that you can use to run whole-program inference. Each has advantages and disadvantages, discussed below:
• To run whole-program inference on a single project, with a few changes to its buildfile but no changes to its source code, use the wpi2.sh script (Section 35.3).
• To run whole-program inference on a single project without modifying either its buildfile or its source code, use the wpi.sh script (Section 35.4). This script can automatically understand many Ant, Maven, and Gradle build files, so
it requires little manual configuration. However, it is based on a no-longer-maintained project, dljc, so it is not guaranteed to work.
• To run whole-program inference on many projects without modifying their source code (say, when running it on projects from GitHub), use the wpi-many.sh script (Section 35.5). This script can understand the same build files as
wpi.sh.
• If you want to insert the inferred annotations directly into a single project’s source code, use the infer-and-annotate.sh script (Section 35.6).
These type inference scripts appear in the checker/bin/ directory. The remainder of this chapter describes them (Sections 35.3–35.6), then concludes with discussion
that applies to all of them.
You need to edit your buildfile, then run the wpi2.sh script.
First, set up your buildfile to run the Checker Framework. If you use the Checker Framework Gradle plugin, then there is nothing to do.
Otherwise, add these command-line arguments:
• -Ainfer=ajava
• -AinferOutputDirectory=.../whole-program-inference-new
• -Aajava=.../whole-program-inference-output
• -Awarns
and remove or comment out -Werror and -AinferOutputOriginal. Here is a Gradle example:
checkerFramework {
extraJavacArgs = [
"-Ainfer=ajava",
"-AinferOutputDirectory=" + project.rootDir + "/whole-program-inference-new",
"-Aajava=" + project.rootDir + "/whole-program-inference-output",
"-Awarns",
// "-Werror", // remove or comment out any occurrence of "-Werror".
// "-AinferOutputOriginal" // remove or comment out any occurrence.
...
]
...
}
The two directories must be named whole-program-inference-new and whole-program-inference-output and must be absolute paths. They must also be the same for every subproject of a multi-project build, which is why the example uses project.rootDir rather
than project.projectDir.
Put the directories at the top level of your project. Do not put either directory under your build system’s output directory, such as build/ or target/. Your build system’s clean task would delete the inference output, possibly in the middle of a build.
wpi2.sh
Run wpi2.sh from your project’s top-level directory — the same directory that contains the whole-program-inference-* directories that you configured your buildfile to use.
The arguments to wpi2.sh are a command that runs the Checker Framework. Here is a typical invocation (if you use the Checker Framework Gradle plugin).
$CHECKERFRAMEWORK/checker/bin/wpi2.sh ./gradlew -Pwpi2 clean assemble
The clean task is needed because wpi2.sh runs the Checker Framework repeatedly, and Gradle does nothing if the old (but still up-to-date) compilation output is present. If the given command does not recompile every source file, then wpi2.sh halts with an error.
The output of wpi2.sh is a top-level directory whole-program-inference-output. For each of your project’s source files for which the Checker Framework inferred an annotation, it contains a file
package/ClassName-checkername.ajava, where checkername is the fully-qualified name of the checker that ran. A source file for which nothing was inferred has no .ajava file. wpi2.sh uses three other top-level
directories: whole-program-inference-new, which the compiler writes each iteration’s results to and which wpi2.sh removes when inference converges; whole-program-inference-diffs, which contains one diff file per iteration (iteration-1.diff,
iteration-2.diff, etc.) for diagnostic purposes; and whole-program-inference-previous, which exists only while each iteration’s results replace the previous iteration’s. You may wish to add whole-program-inference-* to your .gitignore file.
wpi2.sh exits with status 0 if inference converged, and with a nonzero status otherwise. In particular, it exits with status 1 if the Checker Framework inferred no annotations at all — most often because the buildfile is misconfigured, but also if your project is already fully annotated.
If wpi2.sh fails — for example, because the Checker Framework crashed or your buildfile is misconfigured — then a subsequent run of wpi2.sh continues from the annotations that it inferred so far in whole-program-inference-output. To start inference from scratch,
remove whole-program-inference-output before running wpi2.sh.
wpi2.sh runs the command at most 10 times. Set the WPI2_MAX_ITERATIONS environment variable to an integer 2 or greater to change the bound.
A typical invocation of wpi.sh is
$CHECKERFRAMEWORK/checker/bin/wpi.sh -- --checker nullness
The result is a set of log files placed in the dljc-out/ folder of the target project. See Section 35.4.1 for an explanation of the log files generated by an invocation of wpi.sh. The inferred annotations appear in
.ajava files in a temporary directory whose name appears in the dljc-out/wpi-stdout.log file; you can find their location by examining the -Aajava argument to the last javac command that was run. The annotation files generated in each round of
inference appear in directories labeled iteration0, iteration1, etc.
The wpi.sh script is most useful when analyzing projects that follow the standard conventions of their build system for single-module projects. When analyzing a project that requires non-standard build system commands, use the -c and -b options to override the defaults
used by wpi.sh. For example, suppose that you wanted to use wpi.sh to infer annotations for the Resource Leak Checker on Apache ZooKeeper’s zookeeper-server module only.
Without wpi.sh, one might use the following command: mvn -B --projects zookeeper-server --also-make install -DskipTests. To use this command via wpi.sh, use the following: sh wpi.sh -b "-B --projects zookeeper-server
--also-make" -c "install -DskipTests" -- --checker resourceleak.
The full syntax for invoking wpi.sh is
wpi.sh [-d PROJECTDIR] [-t TIMEOUT] [-c COMPILATION_TARGET] [-b EXTRA_BUILD_ARGS] [-g GRADLECACHEDIR] -- [DLJC-ARGS]
Arguments in square brackets are optional. Here is an explanation of the arguments:
The top-level directory of the project. It must contain an Ant, Gradle, or Maven buildfile. The default is the current working directory.
The timeout for running the checker, in seconds.
The name(s) of the build system target(s) used to compile the target project. The default is chosen based on the build system (e.g., compileJava for Gradle, compile for Maven, etc.). This argument is passed directly to the build system when compiling the target project, so it can also
include command-line arguments that only apply to the compilation targets (and not other targets like clean); for general command-line arguments that apply to all targets, use the -b option instead. When running WPI on a single module of a multi-module project, you might want to use
this option (possibly in combination with -b, below), depending on the setup of the target project. The argument may contain spaces and is re-tokenized by the shell.
Extra arguments to pass to the build script invocation. This argument will be passed to compilation tasks, such as ant compile, gradle compileJava, or mvn compile. The main difference between this option and -c is that the values of the -b
option are also passed to other, non-compilation build system commands, such as ant clean, gradle clean, or mvn clean. The argument may contain spaces and is re-tokenized by the shell.
The directory to use for the -g option to Gradle (the Gradle home directory). This option is ignored if the target project does not build with Gradle. The default is .gradle relative to the target project (i.e., each target project has its own Gradle home). This default is motivated by Gradle issue #1319.
Arguments that are passed directly to do-like-javac’s dljc program without modification. One argument is required: --checker, which indicates what type-checker(s) to run (in the format
described in Section 2.2.4).
The documentation of do-like-javac describes the other commands that its WPI tool supports. Notably, to pass checker-specific arguments to invocations of javac, use the --extraJavacArgs
argument to dljc. For example, to use the -AignoreRangeOverflow option for the Constant Value Checker (Chapter 24) when running inference, you would add
--extraJavacArgs=’-AignoreRangeOverflow’ anywhere after the -- argument to wpi.sh.
You may need to wait a few minutes for the command to complete.
The results of invoking wpi.sh are log files stored in the dljc-out/ folder of the target project. The dljc-out/ folder contains:
• typecheck.out: The final error messages produced by javac, comprising the results of type-checking obtained with the latest iteration of WPI (i.e., using the most precise, consistent set of annotations).
• build_output.txt: Logs collected from compiling the target project without the Checker Framework, using the build file found at the top-level directory.
• wpi-stdout.log: The results of type-checking with each candidate set of annotations, concatenated together in the order in which the annotations were inferred. The final results (i.e., those obtained using the most precise, consistent set of annotations) will appear at the end of this file.
• wpi-stdout-*: These files are separate from the logs in wpi-stdout.log. They may be useful in the case where dljc is not working as expected.
• toplevel.log: The log of the command executed at the top-level of the target directory to invoke whole-program inference.
• javac.json: The list of all .java files for which inference was attempted by wpi.sh, and the options passed to javac.
• stats.json: Statistics from the invocation of wpi.sh on the target project, including build time, the number of built .jar files, the number of executable .jar files, the number of javac invocations, and the number of source files.
The requirements to run wpi.sh and wpi-many.sh are the same:
• The project on which inference is run must contain an Ant, Gradle, or Maven buildfile that compiles the project.
• At least one of the JAVA_HOME, JAVA8_HOME, JAVA11_HOME, JAVA17_HOME, JAVA21_HOME, JAVA24_HOME, JAVA25_HOME, or JAVA26_HOME environment variables must be set.
• If set, the JAVA_HOME environment variable must point to a Java JDK.
• If set, the JAVA8_HOME environment variable must point to a Java 8 JDK.
• If set, the JAVA11_HOME environment variable must point to a Java 11 JDK.
• If set, the JAVA17_HOME environment variable must point to a Java 17 JDK.
• If set, the JAVA21_HOME environment variable must point to a Java 21 JDK.
• If set, the JAVA24_HOME environment variable must point to a Java 24 JDK.
• If set, the JAVA25_HOME environment variable must point to a Java 25 JDK.
• If set, the JAVA26_HOME environment variable must point to a Java 26 JDK.
• The CHECKERFRAMEWORK environment variable must point to a built copy of the Checker Framework.
• If set, the DLJC environment variable must point to a copy of the dljc script from do-like-javac. (If this variable is not set, the WPI scripts will download this dependency
automatically.)
• Other dependencies: ant, awk, curl, git, gradle, mvn, python3 (for dljc), wget.
Python 2.7 modules: subprocess32.
The requirements to run wpi.sh and wpi-many.sh are the same. See Section 35.4.2 for the list of requirements.
To run an experiment on many projects:
1. Use query-github.sh to search GitHub for candidate repositories. File docs/examples/wpi-many/securerandom.query is an example query, and file docs/examples/wpi-many/securerandom.list is the standard output created by running
query-github.sh securerandom.query 100. If you do not want to use GitHub, construct a file yourself that matches the format of the file securerandom.list.
2. Use wpi-many.sh to run whole-program inference on multiple Ant, Gradle, or Maven projects. You provide it a file in which each line is “GitHub repository URL” “git hash” (with no quotes, and with whitespace between them).
• If you are using a checker that is distributed with the Checker Framework, use wpi-many.sh directly.
• If you are using a checker that is not distributed with the Checker Framework (also known as a “custom checker”), file docs/examples/wpi-many/wpi-many-custom-checker-example.sh is a no-arguments script that serves as an example of how to use wpi-many.sh.
Log files are copied into a results directory. For a failed run, the log file indicates the reason that WPI could not be run to completion on the project. For a successful run, the log file indicates whether the project was verified (i.e., no errors were reported), or whether the checker issued warnings (which might be true positive or false positive warnings).
3. Use wpi-summary.sh to summarize the logs in the output results directory. Use its output to guide your analysis of the results of running wpi-many.sh: you should manually examine the log files for the projects that appear in the “results available” list it produces. This list is the list of
every project that the script was able to successfully run WPI on. (This does not mean that the project type-checks without errors afterward, or even type-checks at all — just that the Checker Framework attempted to type-check the project and some output was produced.)
4. (Optional) Add annotations that WPI does not infer, to eliminate false positive warnings. There are two ways you can add annotations to a target program:
• Fork the project and add the annotations directly to the project’s source code, and add a dependency on org.checkerframework:checker-qual to the project’s build system. This approach is the most difficult, but has the advantage that the checker will attempt to verify any annotations you add.
• Add the annotations in a stub file, creating the .astub file as a copy of the .java file. When you run the checker, supply the -AmergeStubsWithSource and -Astubs=... command-line arguments.
A typical invocation is
wpi-many.sh -o outdir -i /path/to/repo.list -t 7200 -- --checker optional
The wpi-many.sh script takes the following command-line arguments. The -o and -i arguments are mandatory. An invocation should also include -- [DLJC-ARGS] at the end; DLJC-ARGS is documented in Section 35.4.
Run the experiment in the outdir directory, and place the results in the outdir-results directory. Both will be created if they do not exist. The directory may be specified as an absolute or relative path.
Read the list of repositories to use from the file infile. The file must be specified as an absolute, not relative, path. Each line should have 2 elements, separated by whitespace:
1. The URL of the git repository on GitHub. The URL must be of the form https://github.com/username/repository . The script is reliant on the number of slashes, so excluding “https://” is an error.
2. The commit hash to use.
The timeout for running the checker on each project, in seconds.
The directory to use for the -g option to Gradle (the Gradle home directory). This option is ignored if the target project does not build with Gradle. The default is .gradle relative to the target project (i.e., each target project has its own Gradle home). This default is motivated by Gradle issue #1319.
If this flag is present, then projects that are not buildable — for which no supported build file is present or for which running the standard build commands fails — are skipped on future runs but are not deleted immediately (such projects are deleted immediately if this flag is not present). This flag is useful
if you intend to run wpi-many.sh several times on the same set of repositories (for example, during checker development), to avoid re-downloading unusable projects.
To obtain the locations of the annotation files generated by an invocation of wpi-many.sh, you can run wpi-annotation-paths.sh on the result directory, e.g., outdir-results.
A typical invocation is
wpi-annotation-paths.sh outdir-results
Here, the results of wpi-many.sh are located in outdir-results.
To use this version of whole-program inference, make sure that insert-annotations-to-source, from the Annotation File Utilities project, is on your path (for example, its directory is in the $PATH environment variable). Then, run the script
checker-framework/checker/bin/infer-and-annotate.sh. Its command-line arguments are:
1. Optional: Command-line arguments to insert-annotations-to-source.
2. Processor’s name.
3. Target program’s classpath. This argument is required; pass "" if it is empty.
4. Optional: Extra processor arguments which will be passed to the checker, if any. You may supply any number of such arguments, or none. Each such argument must start with a hyphen.
5. Optional: Paths to .jaif files used as input in the inference process.
6. Paths to .java files in the program.
For example, to add annotations to the plume-lib project:
git clone https://github.com/mernst/plume-lib.git
cd plume-lib
make jar
$CHECKERFRAMEWORK/checker/bin/infer-and-annotate.sh \
"LockChecker,NullnessChecker" java/plume.jar:java/lib/junit-4.12.jar:$JAVA_HOME/lib/tools.jar \
$(find java/src/plume/ -name "*.java")
# View the results
git diff
You may need to wait a few minutes for the command to complete. You can ignore warnings that the command outputs while it tries different annotations in your code.
It is recommended that you run infer-and-annotate.sh on a copy of your code, so that you can see what changes it made and so that it does not change your only copy. One way to do this is to work in a clone of your repository that has no uncommitted changes.
Type inference outputs the most specific type qualifiers that are consistent with all the source code it is given. (Section 35.7.1 explains when type inference ignores some code.) This may be different than the specification the programmer had in mind when writing the code. If the program uses a method or field in a limited way, then the inferred annotations will be legal for the program as currently written but may not be as general as possible and may not accommodate future program changes.
Here are some examples:
• Suppose that your program (or test suite) currently calls method m1 only with non-null arguments. The tool will infer that m1’s parameter has @NonNull type. If you had intended the method to be able to take null as an argument and you later add such a call,
the type-checker will issue a warning because the inferred @NonNull annotation is inconsistent with the new call.
• If your program (or test suite) passes only null as an argument, the inferred type will be the bottom type, such as @GuardedByBottom.
• Suppose that method m2 has no body, because it is defined in an interface or abstract class. Type inference can still infer types for its signature, based on the overriding implementations. If all the methods that override m2 return a non-null value, type inference will infer that
m2’s return type has @NonNull type, even if some other overriding method is allowed to return null.
If the program contains erroneous calls, the inferred annotations may reflect those errors. Suppose you intend method m3 to be called with non-null arguments, but your program contains an error and one of the calls to m3 passes null as the argument. Then the tool will infer
that m3’s parameter has @Nullable type.
If you run whole-program inference on a library that contains mutually recursive routines, and there are no non-recursive calls to the routines, then whole-program inference may run a long time and eventually produce incorrect results. In this case, write type annotations on the formal parameters of one of the routines.
Whole-program inference is a “forward analysis”. It determines a method parameter’s type annotation based on what arguments are passed to the method but not on how the parameter is used within the method body. It determines a method’s return type based on code in the method body but not on uses of the method return value in client code.
Whole-program inference ignores code within the scope of a @SuppressWarnings annotation with an appropriate key (Section 34.1). In particular, uses within the scope do not contribute to the
inferred type, and declarations within the scope are not changed. You should remove @SuppressWarnings annotations from the class declaration of any class you wish to infer types for.
As noted above, whole-program inference generalizes from invocations of methods and assignments to fields. If a field is set via reflection (such as via injection), there are no explicit assignments to it for type inference to generalize from, and type inference will produce an inaccurate result. There are two ways to
make whole-program inference ignore such a field. (1) You probably have an annotation such as @Inject or @Option that indicates such fields. Meta-annotate the declaration of the Inject or Option annotation with @IgnoreInWholeProgramInference. (2) Annotate the field to be ignored with @IgnoreInWholeProgramInference.
Whole-program inference, for a type-checker other than the Nullness Checker, ignores assignments and pseudo-assignments where the right-hand side is the null literal.
With any type inference tool, it is a good idea to manually examine the results. This can help you find bugs in your code or places where type inference inferred an overly-precise result. You can correct the inferred results manually, or you can add tests that pass additional values and then re-run inference.
When arguments or assignments are literals, whole-program inference commonly infers overly precise type annotations, such as @Interned and @Regex annotations when the analyzed code only uses a constant string.
When an annotation is inferred for a use of a type variable, you may wish to move the annotation to the corresponding upper bounds of the type variable declaration.
This section explains how the wpi.sh and infer-and-annotate.sh scripts work. If you merely want to run the scripts and you are not encountering trouble, you can skip this section.
Each script repeatedly runs the checker with an -Ainfer= command-line option to infer types for fields and method signatures. The output of this step is a .jaif (for infer-and-annotate.sh) or .ajava (for wpi.sh) file that records the
inferred types. Each script adds the inferred annotations to the next run, so that the checker takes them into account (and checks them). wpi.sh does this by updating the set of .ajava files that are passed to the checker via the -Aajava command-line argument;
infer-and-annotate.sh inserts the inferred annotations in the program using the Annotation File Utilities.
On each iteration through the process, there may be new annotations in the .jaif or .ajava files, and some type-checking errors may be eliminated (though others might be introduced). The process halts when there are no more changes to the inference results, that is, the
.jaif or .ajava files are unchanged between two runs.
When the type-checker is run on the program with the final annotations inserted, there might still be errors. This may be because the tool did not infer enough annotations, or because your program cannot type-check (either because it contains a defect, or because it contains subtle code that is beyond the capabilities of the type system). However, each of the inferred annotations is sound, and this reduces your manual effort in annotating the program.
The iterative process is required because type-checking is modular: it processes each class and each method only once, independently. Modularity enables you to run type-checking on only part of your program, and it makes type-checking fast. However, it has some disadvantages:
• The first run of the type-checker cannot take advantage of whole-program inference results because whole-program inference is only complete at the end of type-checking, and modular type-checking does not revisit any already-processed classes.
• Revisiting an already-processed class may result in a better estimate.
There exist monolithic whole-program analyses that run without requiring any annotations in the source code. An advantage of such a tool is that the programmer never needs to write any type annotations.
Running a whole-program inference tool, then running a type-checker, has some benefits:
• The type qualifiers act as machine-checked documentation, which can aid programmer understanding.
• Error messages may be more comprehensible. With a monolithic whole-program analysis, error messages can be obscure, because the analysis has already inferred (possibly incorrect) types for a number of variables.
• Errors are localized. A change to one part of the program does not lead to an error message in a far-removed part of the program.
• Type-checking is modular, which can be faster than re-doing a whole-program analysis every time the program changes.