Merge from upstream.

.gitignore

@@ -41,6 +41,7 @@ checker/jdk/jdk*.jar
 checker/jdk/**/*.class
 *.pyc
 checker/build-temp
+checker/bin/.do-like-javac
 checker/bin-devel/.plume-scripts
 checker/bin-devel/.run-google-java-format
 checker/bin-devel/dockerdir
@@ -128,8 +129,10 @@ checker/jtreg/multipleexecutions/Main.class
 checker-qual/src
 checker-qual-android/src
 
-framework/tests/whole-program-inference/annotated/
-/framework/tests/returnsreceiverdelomboked/
+# Some tests produce output into the tests/ directory instead of the build/ directory.
+checker/tests/wpi-testchecker/annotated/
+checker/tests/wpi-testchecker/inference-output/
+framework/tests/returnsreceiverdelomboked/
 
 docs/tutorial/src/personalblog-demo/bin/net/eyde/personalblog/service/PersonalBlogService.class
 docs/tutorial/src/personalblog-demo/bin/net/eyde/personalblog/struts/action/ReadAction.class

LICENSE.txt

@@ -16,8 +16,9 @@ the parts that you might want to include with your own program.
    I18nFormatUtil.java, NullnessUtil.java, Opt.java, PurityUnqualified.java,
    RegexUtil.java, SignednessUtil.java, SignednessUtilExtra.java, and
    UnitsTools.java.  It also applies to the cleanroom implementations of
-   third-party annotations (in checker/src/testannotations/ and in
-   framework/src/main/java/org/jmlspecs/).
+   third-party annotations (in checker/src/testannotations/,
+   framework/src/main/java/org/jmlspecs/, and
+   framework/src/main/java/com/google/).
 
 The Checker Framework includes annotations for some libraries.  Those in
 .astub files use the MIT License.  Those in https://github.com/typetools/jdk

azure-pipelines.yml

@@ -131,8 +131,8 @@ jobs:
    - nonjunit_tests_jdk11
    - misc_jdk11
    - typecheck_jdk11
-## Reduce latency due to the "daikon_jdk11 -> daikon_jdk8" critical path.
-#   - daikon_jdk11
+   ## Reduce latency due to the "daikon_jdk11 -> daikon_jdk8" critical path.
+   # - daikon_jdk11
   pool:
     vmImage: 'ubuntu-latest'
   container: mdernst/cf-ubuntu-jdk8:latest

build.gradle

@@ -102,7 +102,7 @@ allprojects {
     //   * any new checkers have been added,
     //   * the patch level is 9 (keep the patch level as a single digit), or
     //   * backward-incompatible changes have been made to APIs or elsewhere.
-    version '3.8.0-SNAPSHOT'
+    version '3.9.0'
 
     repositories {
         mavenCentral()
@@ -211,8 +211,10 @@ allprojects {
             options.compilerArgs += [
                     '-g',
                     '-Werror',
-                    // To not get a warning about missing bootstrap classpath for Java 8 (once we use Java 9).
-                    "-Xlint:-options",
+                    // -options: To not get a warning about missing bootstrap classpath for Java 8 (once we use Java 9).
+                    // -fallthrough: Don't check fallthroughs.  Instead, use Error Prone.  Its
+                    // are suppressible warns with a "// fall through" comment.
+                    "-Xlint:-options,-fallthrough",
                     "-Xlint",
             ]
 
@@ -428,7 +430,7 @@ configurations {
     requireJavadoc
 }
 dependencies {
-    requireJavadoc "org.plumelib:require-javadoc:1.0.0"
+    requireJavadoc "org.plumelib:require-javadoc:1.0.1"
 }
 task requireJavadoc(type: JavaExec) {
     description = 'Ensures that Javadoc documentation exists.'
@@ -544,8 +546,8 @@ task getPlumeScripts() {
 }
 
 task pythonIsInstalled(type: Exec) {
-  description "Check that the python executable is installed."
-  executable = "python"
+  description "Check that the python3 executable is installed."
+  executable = "python3"
   args "--version"
 }
 
@@ -581,7 +583,7 @@ subprojects {
         description 'Check whether the source code is properly formatted'
         // checker-qual* projects have no source, so skip
         onlyIf {!project.name.startsWith('checker-qual') }
-        executable 'python'
+        executable 'python3'
 
         doFirst {
             args += "${formatScriptsHome}/check-google-java-format.py"
@@ -600,7 +602,7 @@ subprojects {
         description 'Format the Java source code'
         // checker-qual* projects have no source, so skip
         onlyIf { !project.name.startsWith('checker-qual') }
-        executable 'python'
+        executable 'python3'
         doFirst {
             args += "${formatScriptsHome}/run-google-java-format.py"
             args += "--aosp" // 4 space indentation
@@ -818,15 +820,19 @@ subprojects {
         // Create a nonJunitTests task per project
         tasks.create(name: 'nonJunitTests', group: 'Verification') {
             description 'Run all Checker Framework tests except for the Junit tests.'
+            if (project.name.is('framework') || project.name.is('checker')) {
+                dependsOn('jtregTests')
+            }
             if (project.name.is('framework')) {
-                dependsOn('wholeProgramInferenceTests', 'loaderTests')
+                dependsOn('loaderTests')
             }
 
             if (project.name.is('checker')) {
                 if (!isJava8) {
                     dependsOn('jtregJdk11Tests')
                 }
-                dependsOn('nullnessExtraTests', 'commandLineTests', 'tutorialTests')
+                dependsOn('nullnessExtraTests', 'commandLineTests', 'tutorialTests',
+                          'wholeProgramInferenceTests', 'wpiScriptsTests')
             }
 
             if (project.name.is('dataflow')) {
@@ -841,13 +847,10 @@ subprojects {
             description 'Run the Checker Framework on itself'
             dependsOn('checkInterning', 'checkPurity', 'checkSignature')
             if (project.name.is('framework') || project.name.is('checker')) {
-                dependsOn('checkNullnessOnlyAnnotatedFor')
+                dependsOn('checkNullnessOnlyAnnotatedFor', 'checkCompilerMessages')
             } else {
                 dependsOn('checkNullness')
             }
-            if (project.name.is('framework') || project.name.is('checker')) {
-                dependsOn('checkCompilerMessages', 'jtregTests')
-            }
         }
 
         // Create an allTests task per project.
@@ -910,6 +913,7 @@ task checkBasicStyle(group: 'Format') {
             'manual.html',
             'manual.html-e',
             'junit.*.properties',
+            'securerandom.*',
             'checker/dist/META-INF/maven/org.apache.bcel/bcel/pom.xml',
             'checker/dist/META-INF/maven/org.apache.commons/commons-text/pom.xml',
             'framework/src/main/resources/git.properties']

changelog.txt

@@ -1,19 +1,64 @@
+Version 3.9.0, December 21, 2020
+
+New scripts checker/bin/wpi.sh and checker/bin/wpi-many.sh run whole-program
+inference, without modifying the source code of the target program(s).
+
+The Called Methods Checker supports the -AdisableReturnsReceiver command-line option.
+
+The Format String Checker recognizes Error Prone's `@FormatMethod` annotation.
+
+Implementation details:
+
+Class renamings:
+ * `StubParser` => `AnnotationFileParser`
+ * `Receiver` => `JavaExpression`
+     *  also related class and method renamings
+ * In the Dataflow Framework:
+    * `ThisLiteralNode` => `ThisNode`
+    * `ExplicitThisLiteralNode` => `ExplicitThisNode`
+    * `ImplicitThisLiteralNode` => `ImplicitThisNode`
+
+Method deprecations:
+ * Deprecated `AnnotatedTypeFactory.addAliasedAnnotation`; use `addAliasedTypeAnnotation`
+
+Closed issues:
+#765, #2452, #2953, #3287, #3294, #3377, #3390, #3496, #3499, #3681, #3826,
+#3839, #3850, #3851, #3862, #3871, #3884, #3888, #3908, #3929, #3932,
+#3935, #3956, #3971, #3974, #3994, #4004, #4005, #4018.
+
+---------------------------------------------------------------------------
+
 Version 3.8.0, December 1, 2020
 
+The Initialized Fields Checker warns when a field is not initialized by a
+constructor.  This is more general than the Initialization Checker, which
+only checks that `@NonNull` fields are initialized.
+
 The manual describes how to modify an sbt build file to run the Checker
 Framework.
 
 The -AwarnUnneededSuppressions command-line option warns only about
 suppression strings that contain a checker name.
 
+The -AwarnUnneededSuppressionsExceptions=REGEX command-line option
+partially disables -AwarnUnneededSuppressions.  Most users don't need this.
+
 Implementation details:
 
 Added classes `SubtypeIsSubsetQualifierHierarchy` and
 `SubtypeIsSupersetQualifierHierarchy`.
 
+Moved the `contractsUtils` field from the visitor to the type factory.
+
+Class renamings:
+ * `ContractsUtils` => `ContractsFromMethod`
+
 Method renamings:
-  ElementUtils.getVerboseName => ElementUtils.getQualifiedName
-  ElementUtils.getSimpleName => ElementUtils.getSimpleSignature
+ * `ElementUtils.getVerboseName` => `ElementUtils.getQualifiedName`
+ * `ElementUtils.getSimpleName` => `ElementUtils.getSimpleSignature`
+
+Field renamings:
+ * `AnnotatedTypeMirror.actualType` => `AnnotatedTypeMirror.underlyingType`
 
 Added a formal parameter to methods in `MostlyNoElementQualifierHierarchy`:
  * `leastUpperBoundWithElements`
@@ -23,6 +68,15 @@ Removed a formal parameter from methods in `BaseTypeVisitor`:
  * `checkPostcondition`
  * `checkConditionalPostcondition`
 
+In `Analysis.runAnalysisFor()`, changed `boolean` parameter to enum `BeforeOrAfter`.
+
+Removed `org.checkerframework.framework.util.AnnotatedTypes#getIteratedType`; use
+`AnnotatedTypeFactory#getIterableElementType(ExpressionTree)` instead.
+
+Closed issues:
+#3287, #3390, #3681, #3839, #3850, #3851, #3862, #3871, #3884, #3888, #3908,
+#3929, #3932, #3935.
+
 ---------------------------------------------------------------------------
 
 Version 3.7.1, November 2, 2020

checker/bin-devel/Dockerfile-ubuntu-jdk11

@@ -31,17 +31,6 @@ RUN export DEBIAN_FRONTEND=noninteractive \
   unzip \
   wget
 
-# Ubuntu 18.04 has Maven 3.6.0, but 3.6.1 apparently has better retry
-# behavior to work around network problems.
-RUN export DEBIAN_FRONTEND=noninteractive \
-&& VER=3.6.3 \
-&& mkdir -p $HOME/bin/install \
-&& cd $HOME/bin/install \
-&& wget http://apache.mirrors.pair.com/maven/maven-3/${VER}/binaries/apache-maven-${VER}-bin.tar.gz \
-&& tar xzf apache-maven-${VER}-bin.tar.gz \
-&& (cd /usr/local/bin && ln -sf $HOME/bin/install/apache-maven-${VER}/bin/* .) \
-&& hash -r
-
 RUN export DEBIAN_FRONTEND=noninteractive \
 && apt-get clean \
 && rm -rf /var/lib/apt/lists/*

checker/bin-devel/Dockerfile-ubuntu-jdk11-plus

@@ -34,17 +34,6 @@ RUN export DEBIAN_FRONTEND=noninteractive \
   unzip \
   wget
 
-# Ubuntu 18.04 has Maven 3.6.0, but 3.6.1 apparently has better retry
-# behavior to work around network problems.
-RUN export DEBIAN_FRONTEND=noninteractive \
-&& VER=3.6.3 \
-&& mkdir -p $HOME/bin/install \
-&& cd $HOME/bin/install \
-&& wget http://apache.mirrors.pair.com/maven/maven-3/${VER}/binaries/apache-maven-${VER}-bin.tar.gz \
-&& tar xzf apache-maven-${VER}-bin.tar.gz \
-&& (cd /usr/local/bin && ln -sf $HOME/bin/install/apache-maven-${VER}/bin/* .) \
-&& hash -r
-
 RUN export DEBIAN_FRONTEND=noninteractive \
 && apt-get -qqy update \
 && apt-get -qqy install \

checker/bin-devel/Dockerfile-ubuntu-jdk8

@@ -32,17 +32,6 @@ RUN export DEBIAN_FRONTEND=noninteractive \
   unzip \
   wget
 
-# Ubuntu 18.04 has Maven 3.6.0, but 3.6.1 apparently has better retry
-# behavior to work around network problems.
-RUN export DEBIAN_FRONTEND=noninteractive \
-&& VER=3.6.3 \
-&& mkdir -p $HOME/bin/install \
-&& cd $HOME/bin/install \
-&& wget http://apache.mirrors.pair.com/maven/maven-3/${VER}/binaries/apache-maven-${VER}-bin.tar.gz \
-&& tar xzf apache-maven-${VER}-bin.tar.gz \
-&& (cd /usr/local/bin && ln -sf $HOME/bin/install/apache-maven-${VER}/bin/* .) \
-&& hash -r
-
 RUN export DEBIAN_FRONTEND=noninteractive \
 && apt-get clean \
 && rm -rf /var/lib/apt/lists/*

checker/bin-devel/Dockerfile-ubuntu-jdk8-plus

@@ -32,17 +32,6 @@ RUN export DEBIAN_FRONTEND=noninteractive \
   unzip \
   wget
 
-# Ubuntu 18.04 has Maven 3.6.0, but 3.6.1 apparently has better retry
-# behavior to work around network problems.
-RUN export DEBIAN_FRONTEND=noninteractive \
-&& VER=3.6.3 \
-&& mkdir -p $HOME/bin/install \
-&& cd $HOME/bin/install \
-&& wget http://apache.mirrors.pair.com/maven/maven-3/${VER}/binaries/apache-maven-${VER}-bin.tar.gz \
-&& tar xzf apache-maven-${VER}-bin.tar.gz \
-&& (cd /usr/local/bin && ln -sf $HOME/bin/install/apache-maven-${VER}/bin/* .) \
-&& hash -r
-
 RUN export DEBIAN_FRONTEND=noninteractive \
 && apt-get -qqy update \
 && apt-get -qqy install \

checker/bin-devel/Makefile

@@ -0,0 +1,19 @@
+remove-annotations.sh:
+	\rm -f remove-annotations.sh
+	echo "#!/bin/sh" >> remove-annotations.sh
+	echo "# Remove Checker Framework annotations (except ones that the checker trusts" >> remove-annotations.sh
+	echo "# rather than verifies) from all files under the current directory." >> remove-annotations.sh
+	echo "" >> remove-annotations.sh
+	echo 'PREPLACE="$$(dirname "$$(readlink -f "$$0")")"/.plume-scripts/preplace' >> remove-annotations.sh
+	echo "" >> remove-annotations.sh
+# Only remove imports for annotations that are removed.
+	echo '"$$PREPLACE"'" '^import org.checkerframework(?!.*InternedDistinct).*\\\n' ''" >> remove-annotations.sh
+# Remove declaration annotations that appear on their own line.
+	echo '"$$PREPLACE"'" '^ *\@(Deterministic|EnsuresNonNull|FormatMethod|Pure|RequiresNonNull|SideEffectFree)(\([^()]*\))?\\\n' ''" >> remove-annotations.sh
+# The `grep -v` removes trusted annotations.  This list of trusted annotations was generated by hand.
+# TODO: Maybe have two variants of the script, with and without special treatment of trusted annotations.
+# TODO: Don't remove annotations that are within the scope of @SuppressWarnings.  (That requires a real parser rather than this script that uses regexes.)
+	grep '^    "[^"]*",' .run-google-java-format/fixup-google-java-format.py | grep -v InternedDistinct | sed 's/^    "\(.*\)",/"$$PREPLACE" '"'"'\\@\1(\\([^()"]*("[^"]*"[^()"]*)*\\))? '"'"' '"''"'/' >> remove-annotations.sh
+	echo '"$$PREPLACE"'" '\([ \\\n]*[A-Za-z][A-Za-z0-9_]*(<[^<>]*>)? this\)' '()'" >> remove-annotations.sh
+	echo '"$$PREPLACE"'" '\([ \\\n]*[A-Za-z][A-Za-z0-9_]*(<[^<>]*>)? this,[ \\\t]*' '('" >> remove-annotations.sh
+	chmod +x remove-annotations.sh

checker/bin-devel/git.pre-commit

@@ -20,7 +20,7 @@ if [ -n "$CHANGED_JAVA_FILES" ]; then
     # echo "CHANGED_JAVA_FILES: ${CHANGED_JAVA_FILES}"
 
     # shellcheck disable=SC2086
-    python checker/bin-devel/.run-google-java-format/check-google-java-format.py --aosp ${CHANGED_JAVA_FILES} || (echo "Problem in pre-commit.  Try running: ./gradlew reformat" && /bin/false)
+    python3 checker/bin-devel/.run-google-java-format/check-google-java-format.py --aosp ${CHANGED_JAVA_FILES} || (echo "Problem in pre-commit.  Try running: ./gradlew reformat" && /bin/false)
 
     BRANCH=$(git rev-parse --abbrev-ref HEAD)
     if [ "$BRANCH" = "master" ]; then