typetools/checker-framework 3.40.0 release (#626)

Author: wmdietl

.gitignore

@@ -156,6 +156,7 @@ framework/tests/returnsreceiverdelomboked/
 
 dataflow/tests/busyexpr/Out.txt
 dataflow/tests/busyexpr/*.class
+dataflow/tests/cfgconstruction/*.class
 dataflow/tests/constant-propagation/Out.txt
 dataflow/tests/constant-propagation/*.class
 dataflow/tests/issue3447/Out.txt

.travis-build.sh

@@ -37,10 +37,10 @@ SCRIPTDIR=$ROOTDIR/checker/bin-devel/
 
 # For debugging
 (cd "$CHECKERFRAMEWORK" && ./gradlew getPlumeScripts)
-"${SCRIPTDIR}/plume-scripts/ci-info" typetools
-eval $("${SCRIPTDIR}/plume-scripts/ci-info" typetools)
+"${SCRIPTDIR}/plume-scripts/ci-info" eisop
+eval $("${SCRIPTDIR}/plume-scripts/ci-info" eisop)
 
-source "$SCRIPTDIR/build.sh"
+source "$SCRIPTDIR/clone-related.sh"
 
 ###
 ### Run the test

build.gradle

@@ -159,7 +159,7 @@ allprojects {
     //   * any new checkers have been added, or
     //   * backward-incompatible changes have been made to APIs or elsewhere.
     // To make a snapshot release: ./gradlew publish
-    version '3.39.0-eisop2-SNAPSHOT'
+    version '3.40.0'
 
     tasks.withType(JavaCompile).configureEach {
         options.fork = true
@@ -326,6 +326,11 @@ allprojects {
         }
     }
 
+    test {
+        minHeapSize = "256m" // initial heap size
+        maxHeapSize = "4g" // maximum heap size
+    }
+
     // After all the tasks have been created, modify some of them.
     afterEvaluate {
         configurations {
@@ -533,11 +538,6 @@ allprojects {
     } // end afterEvaluate
 } // end allProjects
 
-task cloneAndBuildDependencies(type: Exec, group: 'Build') {
-    description 'Clones (or updates) and builds all dependencies'
-    executable 'checker/bin-devel/build.sh'
-}
-
 task version(group: 'Documentation') {
     description 'Print Checker Framework version'
     doLast {
@@ -971,6 +971,9 @@ subprojects {
         createCheckTypeTask(project.name, 'Signature',
                 'org.checkerframework.checker.signature.SignatureChecker')
 
+        // The checkNullness task runs on all code, but it only *checks* the following code:
+        //  * All files outside the 'framework' and 'checker' subprojects.
+        //  * In the 'framework' and 'checker' subprojects, files with `@AnnotatedFor("nullness")`.
         if (project.name.is('framework') || project.name.is('checker')) {
             createCheckTypeTask(project.name, 'Nullness',
                     'org.checkerframework.checker.nullness.NullnessChecker',

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java

@@ -45,6 +45,7 @@
 @PostconditionAnnotation(qualifier = CalledMethods.class)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
 @Repeatable(EnsuresCalledMethods.List.class)
+@InheritedAnnotation
 public @interface EnsuresCalledMethods {
     /**
      * The Java expressions that will have methods called on them.
@@ -73,6 +74,7 @@
     @Retention(RetentionPolicy.RUNTIME)
     @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
     @InheritedAnnotation
+    @PostconditionAnnotation(qualifier = CalledMethods.class)
     public static @interface List {
         /**
          * Return the repeatable annotations.

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethodsIf.java

@@ -26,6 +26,13 @@
 @InheritedAnnotation
 @Repeatable(EnsuresCalledMethodsIf.List.class)
 public @interface EnsuresCalledMethodsIf {
+    /**
+     * Returns the return value of the method under which the postcondition holds.
+     *
+     * @return the return value of the method under which the postcondition holds
+     */
+    boolean result();
+
     /**
      * Returns Java expressions that have had the given methods called on them after the method
      * returns {@link #result}.
@@ -35,13 +42,6 @@
      */
     String[] expression();
 
-    /**
-     * Returns the return value of the method under which the postcondition holds.
-     *
-     * @return the return value of the method under which the postcondition holds
-     */
-    boolean result();
-
     /**
      * The methods guaranteed to be invoked on the expressions if the result of the method is {@link
      * #result}.

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/RequiresCalledMethods.java

@@ -5,6 +5,7 @@
 
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
+import java.lang.annotation.Repeatable;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
@@ -23,6 +24,7 @@
 @Retention(RetentionPolicy.RUNTIME)
 @PreconditionAnnotation(qualifier = CalledMethods.class)
 @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@Repeatable(RequiresCalledMethods.List.class)
 public @interface RequiresCalledMethods {
     /**
      * The Java expressions that must have had methods called on them.
@@ -49,6 +51,7 @@
      */
     @Documented
     @Retention(RetentionPolicy.RUNTIME)
+    @PreconditionAnnotation(qualifier = CalledMethods.class)
     @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
     public static @interface List {
         /**

checker-qual/src/main/java/org/checkerframework/checker/index/qual/EnsuresLTLengthOfIf.java

@@ -59,17 +59,23 @@
 @InheritedAnnotation
 @Repeatable(EnsuresLTLengthOfIf.List.class)
 public @interface EnsuresLTLengthOfIf {
+    /**
+     * The return value of the method that needs to hold for the postcondition to hold.
+     *
+     * @return the return value of the method that needs to hold for the postcondition to hold
+     */
+    boolean result();
+
     /**
      * Java expression(s) that are less than the length of the given sequences after the method
      * returns the given result.
      *
+     * @return Java expression(s) that are less than the length of the given sequences after the
+     *     method returns the given result
      * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
      */
     String[] expression();
 
-    /** The return value of the method that needs to hold for the postcondition to hold. */
-    boolean result();
-
     /**
      * Sequences, each of which is longer than each of the expressions' value after the method
      * returns the given result.

checker-qual/src/main/java/org/checkerframework/checker/lock/qual/EnsuresLockHeldIf.java

@@ -25,6 +25,13 @@
 @InheritedAnnotation
 @Repeatable(EnsuresLockHeldIf.List.class)
 public @interface EnsuresLockHeldIf {
+    /**
+     * Returns the return value of the method under which the postconditions hold.
+     *
+     * @return the return value of the method under which the postconditions hold
+     */
+    boolean result();
+
     /**
      * Returns Java expressions whose values are locks that are held after the method returns the
      * given result.
@@ -39,13 +46,6 @@
     // assumes that conditional postconditions have a field named "expression".
     String[] expression();
 
-    /**
-     * Returns the return value of the method under which the postconditions hold.
-     *
-     * @return the return value of the method under which the postconditions hold
-     */
-    boolean result();
-
     /**
      * A wrapper annotation that makes the {@link EnsuresLockHeldIf} annotation repeatable.
      *

checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/MustCallAlias.java

@@ -11,7 +11,9 @@
  * always be used in pairs. On a method, it is written on some formal parameter type and on the
  * method return type. On a constructor, it is written on some formal parameter type and on the
  * result type. Fulfilling the must-call obligation of one is equivalent to fulfilling the must-call
- * obligation of the other.
+ * obligation of the other. Beyond its impact as a polymorphic annotation on {@code MustCall} types,
+ * the Resource Leak Checker uses {@link MustCallAlias} annotations to more precisely determine when
+ * a must-call obligation has been satisfied.
  *
  * <p>This annotation is useful for wrapper objects. For example, consider the declaration of {@code
  * java.net.Socket#getOutputStream}:
@@ -25,6 +27,25 @@
  * Calling {@code close()} on the returned {@code OutputStream} will close the underlying socket,
  * but the Socket may also be closed directly, which has the same effect.
  *
+ * <h2>Type system semantics</h2>
+ *
+ * Within the Must Call Checker's type system, {@code @MustCallAlias} annotations have a semantics
+ * different from a standard polymorphic annotation, in that the relevant actual parameter type and
+ * return type at a call site are not equated in all cases. Given an actual parameter {@code p}
+ * passed in a {@code @MustCallAlias} position at a call site, the return type of the call is
+ * defined as follows:
+ *
+ * <ul>
+ *   <li>If the base return type has a non-empty {@code @InheritableMustCall("m")} annotation on its
+ *       declaration, and {@code p} has a non-empty {@code @MustCall} type, then the return type is
+ *       {@code @MustCall("m")}.
+ *   <li>In all other cases, the return type has the same {@code @MustCall} type as {@code p}.
+ * </ul>
+ *
+ * {@link PolyMustCall} has an identical type system semantics. This special treatment is required
+ * to allow for a wrapper object to have a must-call method with a different name than the must-call
+ * method name for the wrapped object.
+ *
  * <h2>Verifying {@code @MustCallAlias} annotations</h2>
  *
  * Suppose that {@code @MustCallAlias} is written on the type of formal parameter {@code p}.
@@ -47,7 +68,10 @@
  * </ul>
  *
  * When the -AnoResourceAliases command-line argument is passed to the checker, this annotation is
- * treated identically to {@link PolyMustCall}.
+ * treated identically to {@link PolyMustCall}. That is, the annotation still impacts {@link
+ * MustCall} types as a polymorphic annotation (see "Type system semantics" above), but it is not
+ * used by the Resource Leak Checker to more precisely reason about when obligations have been
+ * satisfied.
  *
  * @checker_framework.manual #resource-leak-checker Resource Leak Checker
  * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism

checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/PolyMustCall.java

@@ -9,7 +9,9 @@
 import java.lang.annotation.Target;
 
 /**
- * The polymorphic qualifier for the Must Call type system.
+ * The polymorphic qualifier for the Must Call type system. The semantics of this qualifier differ
+ * from that of a standard polymorphic qualifier; see {@link MustCallAlias} for documentation of its
+ * semantics.
  *
  * @checker_framework.manual #must-call-checker Must Call Checker
  * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism