Sync opprop pico with lnsun pico #1

.travis-build.sh

@@ -10,47 +10,29 @@ export CHECKERFRAMEWORK=$JSR308/checker-framework
 export PATH=$AFU/scripts:$JAVA_HOME/bin:$PATH
 
 #default value is opprop. REPO_SITE may be set to other value for travis test purpose.
-export REPO_SITE=topnessman
+export REPO_SITE=baoruiz
 
 echo "------ Downloading everthing from REPO_SITE: $REPO_SITE ------"
 
-# Clone annotation-tools (Annotation File Utilities)
-if [ -d $JSR308/annotation-tools ] ; then
-    (cd $JSR308/annotation-tools && git pull)
-else
-    (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/annotation-tools.git)
-fi
-
-# Clone stubparser
-if [ -d $JSR308/stubparser ] ; then
-    (cd $JSR308/stubparser && git pull)
-else
-    (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/stubparser.git)
-fi
 # Clone checker-framework
 if [ -d $JSR308/checker-framework ] ; then
-    (cd $JSR308/checker-framework && git checkout pico-dependant-copy && git pull)
+    (cd $JSR308/checker-framework && git checkout pull-pico-changes && git pull)
 else
-    # ViewpointAdapter changes are not yet merged to master, so we depend on pico-dependant branch
-    (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/checker-framework.git)
+    (cd $JSR308 && git clone -b pull-pico-changes --depth 1 https://github.com/"$REPO_SITE"/checker-framework.git)
 fi
 
 # Clone checker-framework-inference
 if [ -d $JSR308/checker-framework-inference ] ; then
-    (cd $JSR308/checker-framework-inference && git checkout pico-dependant-copy && git pull)
+    (cd $JSR308/checker-framework-inference && git checkout pull-pico-changes && git pull)
 else
-    # Again we depend on pico-dependant branch
-    (cd $JSR308 && git clone -b pico-dependant-copy --depth 1 https://github.com/"$REPO_SITE"/checker-framework-inference.git)
+    (cd $JSR308 && git clone -b pull-pico-changes --depth 1 https://github.com/"$REPO_SITE"/checker-framework-inference.git)
 fi
 
-# Build annotation-tools (and jsr308-langtools)
-(cd $JSR308/annotation-tools/ && ./.travis-build-without-test.sh)
-# Build stubparser
-(cd $JSR308/stubparser/ && mvn package -Dmaven.test.skip=true)
 # Build checker-framework, with downloaded jdk
-(cd $JSR308/checker-framework && ant -f checker/build.xml dist-downloadjdk)
+(cd $JSR308/checker-framework && ./.travis-build-without-test.sh downloadjdk)
+
 # Build checker-framework-inference
-(cd $JSR308/checker-framework-inference && gradle dist) # This step needs to be manually in $CFI executed due to path problems
+(cd $JSR308/checker-framework-inference && ./gradlew dist)
 
 # Build PICO
 (cd $JSR308/immutability && ./gradlew build)

check.sh

@@ -10,7 +10,8 @@ export JAVAC=$CF/checker/bin/javac
 export PICO=$(cd $(dirname "$0") && pwd)
 
 # Dependencies
-export CLASSPATH=$PICO/build/classes/java/main:$CFI/dist/checker-framework-inference.jar
+export CLASSPATH=$PICO/build/classes/java/main:$PICO/build/resources/main:\
+$PICO/build/libs/immutability.jar:$CFI/dist/checker-framework-inference.jar
 
 # Command
 DEBUG=""
@@ -35,9 +36,9 @@ done
 cmd=""
 
 if [ "$DEBUG" == "" ]; then
-	cmd="$JAVAC -cp "${CLASSPATH}" -processor "${CHECKER}" "${ARGS[@]}""
+    cmd="$JAVAC -cp "${CLASSPATH}" -processor "${CHECKER}" "${ARGS[@]}""
 else
-	cmd="$JAVAC "$DEBUG" -cp "${CLASSPATH}" -processor "${CHECKER}" -AatfDoNotCache "${ARGS[@]}""
+    cmd="$JAVAC "$DEBUG" -cp "${CLASSPATH}" -processor "${CHECKER}" -AatfDoNotCache "${ARGS[@]}""
 fi
 
 eval "$cmd"

src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java

@@ -20,15 +20,15 @@
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
-import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator;
+import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.TypeAnnotator;
 import org.checkerframework.javacutil.Pair;
 import org.checkerframework.javacutil.TreeUtils;
-import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator;
+import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator;
 import pico.typecheck.PICOTypeUtil;
 
 import javax.lang.model.element.AnnotationMirror;
@@ -62,17 +62,17 @@ public PICOInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, bool
     // be inserted results anyway).
     @Override
     public TreeAnnotator createTreeAnnotator() {
-        return new ListTreeAnnotator(new ImplicitsTreeAnnotator(this),
+        return new ListTreeAnnotator(new LiteralTreeAnnotator(this),
                 new PICOInferencePropagationTreeAnnotator(this),
                 new InferenceTreeAnnotator(this, realChecker, realTypeFactory, variableAnnotator, slotManager));
     }
 
     @Override
     protected TypeAnnotator createTypeAnnotator() {
-        // Reuse PICOImplicitsTypeAnnotator even in inference mode. Because the type annotator's implementation
+        // Reuse PICODefaultForTypeAnnotator even in inference mode. Because the type annotator's implementation
         // are the same. The only drawback is that naming is not good(doesn't include "Inference"), thus may be
         // hard to debug
-        return new ListTypeAnnotator(super.createTypeAnnotator(), new PICOImplicitsTypeAnnotator(this));
+        return new ListTypeAnnotator(super.createTypeAnnotator(), new PICODefaultForTypeAnnotator(this));
     }
 
     @Override
@@ -235,7 +235,7 @@ public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) {
             return super.visitTypeCast(node, type);
         }
 
-        /**Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are not guaranteed
+        /**Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are not guaranteed
          to always have immutable annotation. If this happens, we manually add immutable to type. */
         private void applyImmutableIfImplicitlyImmutable(AnnotatedTypeMirror type) {
             if (PICOTypeUtil.isImplicitlyImmutableType(type)) {

src/main/java/pico/inference/PICOInferenceRealTypeFactory.java

@@ -11,16 +11,15 @@
 import java.util.List;
 import java.util.Set;
 
-import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.qual.RelevantJavaTypes;
 import org.checkerframework.framework.type.AbstractViewpointAdapter;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
-import org.checkerframework.framework.type.treeannotator.ImplicitsTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
+import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.framework.type.typeannotator.IrrelevantTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator;
@@ -31,7 +30,8 @@
 
 import com.sun.source.tree.Tree;
 
-import pico.typecheck.PICOAnnotatedTypeFactory.PICOImplicitsTypeAnnotator;
+import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator;
+import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator;
 import pico.typecheck.PICOAnnotatedTypeFactory.PICOPropagationTreeAnnotator;
 import pico.typecheck.PICOAnnotatedTypeFactory.PICOTreeAnnotator;
 import pico.typecheck.PICOAnnotatedTypeFactory.PICOTypeAnnotator;
@@ -55,7 +55,9 @@ public class PICOInferenceRealTypeFactory extends BaseAnnotatedTypeFactory {
 
     public PICOInferenceRealTypeFactory(BaseTypeChecker checker, boolean useFlow) {
         super(checker, useFlow);
-        addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY);
+        if (READONLY != null) {
+            addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, READONLY);
+        }
         postInit();
     }
 
@@ -82,7 +84,7 @@ protected AbstractViewpointAdapter createViewpointAdapter() {
     protected TreeAnnotator createTreeAnnotator() {
         return new ListTreeAnnotator(
                 new PICOPropagationTreeAnnotator(this),
-                new ImplicitsTreeAnnotator(this),
+                new LiteralTreeAnnotator(this),
                 new PICOTreeAnnotator(this));
     }
 
@@ -107,7 +109,7 @@ protected TypeAnnotator createTypeAnnotator() {
         // method, so if one annotator already applied the annotations, the others won't apply twice at the
         // same location
         typeAnnotators.add(new PICOTypeAnnotator(this));
-        typeAnnotators.add(new PICOImplicitsTypeAnnotator(this));
+        typeAnnotators.add(new PICODefaultForTypeAnnotator(this));
         return new ListTypeAnnotator(typeAnnotators);
     }
 
@@ -125,21 +127,6 @@ public boolean getShouldDefaultTypeVarLocals() {
         return false;
     }
 
-    // Copied from PICOAnnotatedTypeFactory
-    @Override
-    protected void annotateInheritedFromClass(AnnotatedTypeMirror type, Set<AnnotationMirror> fromClass) {
-        // If interitted from class element is @Mutable or @Immutable, then apply this annotation to the usage type
-        if (fromClass.contains(MUTABLE) || fromClass.contains(IMMUTABLE)) {
-            super.annotateInheritedFromClass(type, fromClass);
-            return;
-        }
-        // If interitted from class element is @ReceiverDependantMutable, then don't apply and wait for @Mutable
-        // (default qualifier in hierarchy to be applied to the usage type). This is to avoid having @ReceiverDependantMutable
-        // on type usages as a default behaviour. By default, @Mutable is better used as the type for usages that
-        // don't have explicit annotation.
-        return;// Don't add annotations from class element
-    }
-
     @Override
     public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) {
         PICOTypeUtil.addDefaultForField(this, type, elt);

src/main/java/pico/inference/PICOInferenceVisitor.java

@@ -23,10 +23,11 @@
 
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.framework.source.Result;
-import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedMethodType;
+import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
+import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.framework.util.AnnotatedTypes;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
@@ -166,14 +167,6 @@ public boolean validateTypeOf(Tree tree) {
     // TODO This might not be correct for infer mode. Maybe returning as it is
     @Override
     public boolean validateType(Tree tree, AnnotatedTypeMirror type) {
-        // basic consistency checks
-        if (!AnnotatedTypes.isValidType(atypeFactory.getQualifierHierarchy(), type)) {
-            if (!infer) {
-                checker.report(
-                        Result.failure("type.invalid", type.getAnnotations(), type.toString()), tree);
-                return false;
-            }
-        }
 
         if (!typeValidator.isValid(type, tree)) {
             if (!infer) {
@@ -192,7 +185,7 @@ public boolean validateType(Tree tree, AnnotatedTypeMirror type) {
     }
 
     @Override
-    protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, AnnotatedExecutableType constructor, NewClassTree newClassTree) {
+    protected void checkConstructorInvocation(AnnotatedDeclaredType invocation, AnnotatedExecutableType constructor, NewClassTree newClassTree) {
         if (infer) {
             AnnotationMirror constructorReturn = extractVarAnnot(constructor.getReturnType());
             mainIsSubtype(invocation, constructorReturn, "constructor.invocation.invalid", newClassTree);
@@ -201,10 +194,10 @@ protected boolean checkConstructorInvocation(AnnotatedDeclaredType invocation, A
             if (!atypeFactory.getTypeHierarchy().isSubtype(invocation, returnType)) {
                 checker.report(Result.failure(
                         "constructor.invocation.invalid", invocation, returnType), newClassTree);
-                return false;
+                return;
             }
         }
-        return super.checkConstructorInvocation(invocation, constructor, newClassTree);
+        super.checkConstructorInvocation(invocation, constructor, newClassTree);
     }
 
     private AnnotationMirror extractVarAnnot(final AnnotatedTypeMirror atm) {
@@ -418,7 +411,7 @@ private boolean isCompatibleCastInInfer(AnnotatedTypeMirror castType, AnnotatedT
             return true;
         } else {
             // Default strategy - comparablecast
-            final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager();
+            final QualifierHierarchy qualHierarchy = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy();
             final SlotManager slotManager = InferenceMain.getInstance().getSlotManager();
             final Slot castSlot = slotManager.getVariableSlot(castType);
             final Slot exprSlot = slotManager.getVariableSlot(exprType);
@@ -429,7 +422,8 @@ private boolean isCompatibleCastInInfer(AnnotatedTypeMirror castType, AnnotatedT
                 // Special handling for case with two ConstantSlots: even though they may not be comparable,
                 // but to infer more program, let this case fall back to "anycast" silently and continue
                 // inference.
-                return constraintManager.getConstraintVerifier().areComparable(castCSSlot, exprCSSlot);
+                return qualHierarchy.isSubtype(castCSSlot.getValue(), exprCSSlot.getValue())
+                		|| qualHierarchy.isSubtype(exprCSSlot.getValue(), castCSSlot.getValue());
             } else {
                 // But if there is at least on VariableSlot, PICOInfer guarantees that solutions don't include
                 // incomparable casts.
@@ -541,7 +535,7 @@ private void reportFieldOrArrayWriteError(Tree node, ExpressionTree variable, An
      * 2) In constructor
      * 3) In instance method, declared receiver is @UnderInitialized
      *
-     * @param node assignment tree that might be initializing an object
+     * @param variable assignment tree that might be initializing an object
      * @return true if the assignment tree is initializing an object
      *
      * @see #hasUnderInitializationDeclaredReceiver(MethodTree)
@@ -559,7 +553,7 @@ private boolean isInitializingObject(ExpressionTree variable) {
         }
 
         MethodTree enclosingMethod = TreeUtils.enclosingMethod(treePath);
-        // No possibility of initialiazing object if the assignment is not within constructor or method(both MethodTree)
+        // No possibility of initializing object if the assignment is not within constructor or method(both MethodTree)
         if (enclosingMethod == null) return false;
         // At this point, we already know that this assignment is field assignment within a method
         if (TreeUtils.isConstructor(enclosingMethod) || hasUnderInitializationDeclaredReceiver(enclosingMethod)) {
@@ -620,14 +614,14 @@ private void checkNewInstanceCreation(Tree node) {
     @Override
     public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
         super.visitMethodInvocation(node, p);
-        ParameterizedMethodType mfuPair =
+        ParameterizedExecutableType mfuPair =
                 atypeFactory.methodFromUse(node);
-        AnnotatedExecutableType invokedMethod = mfuPair.methodType;
+        AnnotatedExecutableType invokedMethod = mfuPair.executableType;
         ExecutableElement invokedMethodElement = invokedMethod.getElement();
         // Only check invocability if it's super call, as non-super call is already checked
         // by super implementation(of course in both cases, invocability is not checked when
         // invoking static methods)
-        if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperCall(node)) {
+        if (!ElementUtils.isStatic(invokedMethodElement) && TreeUtils.isSuperConstructorCall(node)) {
             checkMethodInvocability(invokedMethod, node);
         }
         return null;
@@ -648,7 +642,7 @@ protected void checkMethodInvocability(AnnotatedExecutableType method, MethodInv
                 // , otherwise it will cause inference result not typecheck
                 checker.report(
                         Result.failure(
-                                "super.constructor.invocation.incompatible", subClassConstructorReturnType, superClassConstructorReturnType), node);
+                                "super.invocation.invalid", subClassConstructorReturnType, superClassConstructorReturnType), node);
             }
         }
         super.checkMethodInvocability(method, node);
@@ -817,8 +811,6 @@ protected void commonAssignmentCheck(
             return;
         }
 
-        checkAssignability(var, varTree);
-
         if (varTree instanceof VariableTree) {
             VariableElement element = TreeUtils.elementFromDeclaration((VariableTree) varTree);
             if (element.getKind() == ElementKind.FIELD && !ElementUtils.isStatic(element)) {

src/main/java/pico/inference/PICOVariableAnnotator.java

@@ -69,7 +69,7 @@ protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) {
 
         // Insert @Immutable VarAnnot directly to enum bound
         if (PICOTypeUtil.isEnumOrEnumConstant(bound)) {
-            boundSlot = createConstant(IMMUTABLE);
+            boundSlot = slotManager.createConstantSlot(IMMUTABLE);
             classType.addAnnotation(slotManager.getAnnotation(boundSlot));
             classDeclAnnos.put(classElement, boundSlot);
             return;
@@ -80,7 +80,7 @@ protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) {
             // Have source tree
             if (bound.isAnnotatedInHierarchy(READONLY)) {
                 // Have bound annotation -> convert to equivalent ConstantSlot
-                boundSlot = createConstant(bound.getAnnotationInHierarchy(READONLY));
+                boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY));
             } else {
                 // No existing annotation -> create new VariableSlot
                 boundSlot = createVariable(treeToLocation(classTree));
@@ -89,15 +89,15 @@ protected void handleClassDeclarationBound(AnnotatedDeclaredType classType) {
             // No source tree: bytecode classes
             if (bound.isAnnotatedInHierarchy(READONLY)) {
                 // Have bound annotation in stub file
-                boundSlot = createConstant(bound.getAnnotationInHierarchy(READONLY));
+                boundSlot = slotManager.createConstantSlot(bound.getAnnotationInHierarchy(READONLY));
             } else {
                 // No stub file
                 if (PICOTypeUtil.isImplicitlyImmutableType(classType)) {
                     // Implicitly immutable
-                    boundSlot = createConstant(IMMUTABLE);
+                    boundSlot = slotManager.createConstantSlot(IMMUTABLE);
                 } else {
                     // None of the above applies: use conservative @Mutable
-                    boundSlot = createConstant(MUTABLE);
+                    boundSlot = slotManager.createConstantSlot(MUTABLE);
                 }
             }
         }