Merge branch 'master' into bugfix/wpi-loop-unknowninitialization

Author: erfan-arvan

checker-qual-android/build.gradle

@@ -19,7 +19,19 @@ task copySources(type: Copy) {
 
   into file(layout.buildDirectory.dir("generated/sources/main/java"))
 
-  fileMode(0555)
+  filePermissions {
+    user {
+      read = true
+      write = true
+      execute = true
+    }
+    group {
+      read = true
+      write = true
+      execute = true
+    }
+    other.read = true
+  }
 }
 
 sourceSets {

checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java

@@ -34,7 +34,7 @@
  * @checker_framework.manual #defaults Default qualifier for unannotated types
  */
 @Documented
-@Retention(RetentionPolicy.SOURCE)
+@Retention(RetentionPolicy.RUNTIME)
 @Target({
   ElementType.PACKAGE,
   ElementType.TYPE,

checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java

@@ -22,13 +22,15 @@
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.TreeUtils;
 
 /** The transfer function for the Optional Checker. */
 public class OptionalTransfer extends CFTransfer {
 
+  /** The {@link OptionalAnnotatedTypeFactory} instance for this transfer class. */
+  private final OptionalAnnotatedTypeFactory optionalTypeFactory;
+
   /** The @{@link Present} annotation. */
   private final AnnotationMirror PRESENT;
 
@@ -38,20 +40,17 @@ public class OptionalTransfer extends CFTransfer {
   /** The element for java.util.Optional.ifPresentOrElse(), or null. */
   private final @Nullable ExecutableElement optionalIfPresentOrElse;
 
-  /** The type factory associated with this transfer function. */
-  private final AnnotatedTypeFactory atypeFactory;
-
   /**
    * Create an OptionalTransfer.
    *
    * @param analysis the Optional Checker instance
    */
   public OptionalTransfer(CFAbstractAnalysis<CFValue, CFStore, CFTransfer> analysis) {
     super(analysis);
-    atypeFactory = analysis.getTypeFactory();
-    Elements elements = atypeFactory.getElementUtils();
+    optionalTypeFactory = (OptionalAnnotatedTypeFactory) analysis.getTypeFactory();
+    Elements elements = optionalTypeFactory.getElementUtils();
     PRESENT = AnnotationBuilder.fromClass(elements, Present.class);
-    ProcessingEnvironment env = atypeFactory.getProcessingEnv();
+    ProcessingEnvironment env = optionalTypeFactory.getProcessingEnv();
     optionalIfPresent = TreeUtils.getMethod("java.util.Optional", "ifPresent", 1, env);
     optionalIfPresentOrElse =
         TreeUtils.getMethodOrNull("java.util.Optional", "ifPresentOrElse", 2, env);
@@ -70,7 +69,7 @@ public CFStore initialStore(UnderlyingAST underlyingAST, List<LocalVariableNode>
       LambdaExpressionTree lambdaTree = cfgLambda.getLambdaTree();
       List<? extends VariableTree> lambdaParams = lambdaTree.getParameters();
       if (lambdaParams.size() == 1) {
-        TreePath lambdaPath = atypeFactory.getPath(lambdaTree);
+        TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree);
         Tree lambdaParent = lambdaPath.getParentPath().getLeaf();
         if (lambdaParent.getKind() == Tree.Kind.METHOD_INVOCATION) {
           MethodInvocationTree invok = (MethodInvocationTree) lambdaParent;

dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java

@@ -468,7 +468,10 @@ protected boolean updateNodeValues(Node node, TransferResult<V, S> transferResul
    * @param b the block to add to {@link #worklist}
    */
   protected void addToWorklist(Block b) {
-    // TODO: use a more efficient way to check if b is already present
+    // TODO: This costs linear (!) time.  Use a more efficient way to check if b is already present.
+    // Two possibilities:
+    //  * add unconditionally, and detect duplicates when removing from the queue.
+    //  * maintain a HashSet of the elements that are already in the queue.
     if (!worklist.contains(b)) {
       worklist.add(b);
     }

dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java

@@ -11,10 +11,10 @@
 /**
  * {@code TransferInput} is used as the input type of the individual transfer functions of a {@link
  * ForwardTransferFunction} or a {@link BackwardTransferFunction}. It also contains a reference to
- * the node for which the transfer function will be applied.
+ * the node to which the transfer function will be applied.
  *
  * <p>A {@code TransferInput} contains one or two stores. If two stores are present, one belongs to
- * 'then', and the other to 'else'.
+ * "then", and the other to "else".
  *
  * @param <V> type of the abstract value that is tracked
  * @param <S> the store type used in the analysis
@@ -36,12 +36,12 @@ public class TransferInput<V extends AbstractValue<V>, S extends Store<S>> imple
   protected final @Nullable S store;
 
   /**
-   * The 'then' result store (or {@code null} if none is present). See invariant at {@link #store}.
+   * The "then" result store (or {@code null} if none is present). See invariant at {@link #store}.
    */
   protected final @Nullable S thenStore;
 
   /**
-   * The 'else' result store (or {@code null} if none is present). See invariant at {@link #store}.
+   * The "else" result store (or {@code null} if none is present). See invariant at {@link #store}.
    */
   protected final @Nullable S elseStore;
 
@@ -64,8 +64,8 @@ public long getUid(@UnknownInitialization TransferInput<V, S> this) {
    *
    * @param node the corresponding node
    * @param store the regular result store, or {@code null} if none is present
-   * @param thenStore the 'then' result store, or {@code null} if none is present
-   * @param elseStore the 'else' result store, or {@code null} if none is present
+   * @param thenStore the "then" result store, or {@code null} if none is present
+   * @param elseStore the "else" result store, or {@code null} if none is present
    * @param analysis analysis the corresponding analysis class to get intermediate flow results
    */
   private TransferInput(
@@ -166,7 +166,7 @@ protected TransferInput(TransferInput<V, S> from) {
   }
 
   /**
-   * Returns the abstract value of node {@code n}, which is required to be a 'sub-node' (that is, a
+   * Returns the abstract value of node {@code n}, which is required to be a "sub-node" (that is, a
    * direct or indirect child) of the node this transfer input is associated with. Furthermore,
    * {@code n} cannot be a l-value node. Returns {@code null} if no value is available.
    *

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ExplicitThisNode.java

@@ -32,6 +32,10 @@ public <R, P> R accept(NodeVisitor<R, P> visitor, P p) {
 
   @Override
   public String toString() {
-    return "this";
+    if (Node.disambiguateOwner) {
+      return "this{owner=" + type + "}";
+    } else {
+      return "this";
+    }
   }
 }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java

@@ -3,6 +3,7 @@
 import com.sun.source.tree.IdentifierTree;
 import com.sun.source.tree.MemberSelectTree;
 import com.sun.source.tree.Tree;
+import com.sun.tools.javac.code.Symbol;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.Objects;
@@ -91,7 +92,11 @@ public <R, P> R accept(NodeVisitor<R, P> visitor, P p) {
 
   @Override
   public String toString() {
-    return getReceiver() + "." + field;
+    if (Node.disambiguateOwner) {
+      return getReceiver() + "." + field + "{owner=" + ((Symbol) element).owner + "}";
+    } else {
+      return getReceiver() + "." + field;
+    }
   }
 
   /**

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java

@@ -26,6 +26,10 @@ public <R, P> R accept(NodeVisitor<R, P> visitor, P p) {
   // used in an inner class context.
   @Override
   public String toString() {
-    return "(this)";
+    if (Node.disambiguateOwner) {
+      return "(this{owner=" + type + "})";
+    } else {
+      return "(this)";
+    }
   }
 }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java

@@ -35,6 +35,12 @@
  */
 public abstract class Node implements UniqueId {
 
+  /**
+   * If true, print the owner of each field and {@code this}, to disambiguate shadowing. This field
+   * is intended for debugging.
+   */
+  public static final boolean disambiguateOwner = false;
+
   /**
    * The basic block this node belongs to. If null, this object represents a method formal
    * parameter.

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SuperNode.java

@@ -13,6 +13,9 @@
  * <pre>
  *   <em>super</em>
  * </pre>
+ *
+ * Its {@link #type} field is the type of the class in which "super" appears, <em>not</em> the type
+ * to which the "super" identifier resolves.
  */
 public class SuperNode extends Node {
 
@@ -36,7 +39,11 @@ public <R, P> R accept(NodeVisitor<R, P> visitor, P p) {
 
   @Override
   public String toString() {
-    return "super";
+    if (Node.disambiguateOwner) {
+      return "super{owner=" + type + "}";
+    } else {
+      return "super";
+    }
   }
 
   @Override