| package org.checkerframework.framework.util.typeinference.constraint; |
| |
| import java.util.List; |
| import java.util.Set; |
| import javax.lang.model.type.TypeKind; |
| import org.checkerframework.framework.type.AnnotatedTypeFactory; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedIntersectionType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedNullType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedUnionType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; |
| import org.checkerframework.framework.type.visitor.AbstractAtmComboVisitor; |
| import org.checkerframework.framework.util.AnnotatedTypes; |
| import org.checkerframework.framework.util.typeinference.TypeArgInferenceUtil; |
| import org.checkerframework.javacutil.BugInCF; |
| import org.checkerframework.javacutil.TypesUtils; |
| import org.plumelib.util.StringsPlume; |
| |
| /** |
| * Takes a single step in reducing a AFConstraint. |
| * |
| * <p>The visit method will determine if the given constraint should either: |
| * |
| * <ul> |
| * <li>be discarded - in this case, the visitor just returns |
| * <li>reduced to a simpler constraint or set of constraints - in this case, the new constraint or |
| * set of constraints is added to newConstraints |
| * </ul> |
| * |
| * Sprinkled throughout this class are comments of the form: |
| * |
| * <pre>{@code |
| * // If F has the form G<..., Yk-1, ? super U, Yk+1, ...>, where U involves Tj |
| * }</pre> |
| * |
| * These are excerpts from the JLS, if you search for them you will find the corresponding JLS |
| * description of the case being covered. |
| */ |
| abstract class AFReducingVisitor extends AbstractAtmComboVisitor<Void, Set<AFConstraint>> { |
| |
| public final Class<? extends AFConstraint> reducerType; |
| public final AnnotatedTypeFactory typeFactory; |
| |
| protected AFReducingVisitor( |
| final Class<? extends AFConstraint> reducerType, final AnnotatedTypeFactory typeFactory) { |
| this.reducerType = reducerType; |
| this.typeFactory = typeFactory; |
| } |
| |
| public abstract AFConstraint makeConstraint( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype); |
| |
| public abstract AFConstraint makeInverseConstraint( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype); |
| |
| public abstract AFConstraint makeEqualityConstraint( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype); |
| |
| public void addConstraint( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype, Set<AFConstraint> constraints) { |
| constraints.add(makeConstraint(subtype, supertype)); |
| } |
| |
| public void addInverseConstraint( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype, Set<AFConstraint> constraints) { |
| constraints.add(makeInverseConstraint(subtype, supertype)); |
| } |
| |
| public void addEqualityConstraint( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype, Set<AFConstraint> constraints) { |
| constraints.add(makeEqualityConstraint(subtype, supertype)); |
| } |
| |
| /** |
| * Called when we encounter an AF constraint on a type combination that we did not think is |
| * possible. This either implies that the type combination is possible, we accidentally created an |
| * invalid A2F or F2A Constraint, or we called the visit method on two AnnotatedTypeMirrors that |
| * do not appear together in a constraint. |
| */ |
| @Override |
| protected String defaultErrorMessage( |
| AnnotatedTypeMirror subtype, AnnotatedTypeMirror supertype, Set<AFConstraint> constraints) { |
| return StringsPlume.joinLines( |
| "Unexpected " + reducerType.getSimpleName() + " + Combination:", |
| "subtype=" + subtype, |
| "supertype=" + supertype, |
| "constraints=[", |
| StringsPlume.join(", ", constraints), |
| "]"); |
| } |
| |
| // ------------------------------------------------------------------------ |
| // Arrays as arguments |
| // From the JLS: |
| // If F = U[], where the type U involves Tj, then if A is an array type V[], or a type |
| // variable with an upper bound that is an array type V[], where V is a reference type, this |
| // algorithm is applied recursively to the constraint V << U or U << V (depending on the |
| // constraint type). |
| |
| @Override |
| public Void visitArray_Array( |
| AnnotatedArrayType subtype, AnnotatedArrayType supertype, Set<AFConstraint> constraints) { |
| addConstraint(subtype.getComponentType(), supertype.getComponentType(), constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitArray_Declared( |
| AnnotatedArrayType subtype, AnnotatedDeclaredType supertype, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| @Override |
| public Void visitArray_Null( |
| AnnotatedArrayType subtype, AnnotatedNullType supertype, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| @Override |
| public Void visitArray_Wildcard( |
| AnnotatedArrayType subtype, AnnotatedWildcardType supertype, Set<AFConstraint> constraints) { |
| visitWildcardAsSuperType(subtype, supertype, constraints); |
| return null; |
| } |
| |
| // Despite the above the comment at the beginning of the "array as arguments" section, a type |
| // variable cannot actually have an array type as its upper bound (e.g. <T extends Integer[]> is |
| // not allowed). |
| // So the only cases in which we visitArray_Typevar would be cases in which either: |
| // 1) Typevar is a type parameter for which we are inferring an argument, in which case the |
| // combination is already irreducible and we would not pass it to this class. |
| // 2) Typevar is an outer scope type variable, in which case it could NOT reference any of the |
| // type parameters for which we are inferring arguments and therefore will not lead to any |
| // meaningful AFConstraints. |
| // public void visitArray_Typevar |
| |
| // ------------------------------------------------------------------------ |
| // Declared as argument |
| |
| /** |
| * I believe there should be only 1 way to have a constraint of this form: {@code visit (Array<T>, |
| * T [])} At this point, I don't think that's a valid argument for a formal parameter. If this |
| * occurs it is because of idiosyncrasies with the Checker Framework . We're going to skip this |
| * case for now. |
| */ |
| @Override |
| public Void visitDeclared_Array( |
| AnnotatedDeclaredType subtype, AnnotatedArrayType supertype, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| // From the JLS Spec: |
| // If F has the form G<..., Yk-1,U, Yk+1, ...>, where U involves Tj |
| @Override |
| public Void visitDeclared_Declared( |
| AnnotatedDeclaredType subtype, |
| AnnotatedDeclaredType supertype, |
| Set<AFConstraint> constraints) { |
| if (subtype.wasRaw() || supertype.wasRaw()) { |
| // The error will be caught in {@link DefaultTypeArgumentInference#infer} and |
| // inference will be aborted, but type-checking will continue. |
| throw new BugInCF("Can't infer type arguments when raw types are involved."); |
| } |
| |
| if (!TypesUtils.isErasedSubtype( |
| subtype.getUnderlyingType(), |
| supertype.getUnderlyingType(), |
| typeFactory.getChecker().getTypeUtils())) { |
| return null; |
| } |
| AnnotatedDeclaredType subAsSuper = |
| AnnotatedTypes.castedAsSuper(typeFactory, subtype, supertype); |
| |
| final List<AnnotatedTypeMirror> subTypeArgs = subAsSuper.getTypeArguments(); |
| final List<AnnotatedTypeMirror> superTypeArgs = supertype.getTypeArguments(); |
| for (int i = 0; i < subTypeArgs.size(); i++) { |
| final AnnotatedTypeMirror subTypeArg = subTypeArgs.get(i); |
| final AnnotatedTypeMirror superTypeArg = superTypeArgs.get(i); |
| |
| // If F has the form G<..., Yk-1, ? extends U, Yk+1, ...>, where U involves Tj |
| // If F has the form G<..., Yk-1, ? super U, Yk+1, ...>, where U involves Tj |
| // Since we always have both bounds in the checker framework we always compare both |
| if (superTypeArg.getKind() == TypeKind.WILDCARD) { |
| final AnnotatedWildcardType superWc = (AnnotatedWildcardType) superTypeArg; |
| |
| if (subTypeArg.getKind() == TypeKind.WILDCARD) { |
| final AnnotatedWildcardType subWc = (AnnotatedWildcardType) subTypeArg; |
| TypeArgInferenceUtil.checkForUninferredTypes(subWc); |
| addConstraint(subWc.getExtendsBound(), superWc.getExtendsBound(), constraints); |
| addInverseConstraint(superWc.getSuperBound(), subWc.getSuperBound(), constraints); |
| } else { |
| addConstraint(subTypeArg, superWc.getExtendsBound(), constraints); |
| addInverseConstraint(superWc.getSuperBound(), subTypeArg, constraints); |
| } |
| |
| } else { |
| // if F has the form G<..., Yk-1, U, Yk+1, ...>, where U is a type expression that involves |
| // Tj |
| addEqualityConstraint(subTypeArg, superTypeArg, constraints); |
| } |
| } |
| |
| return null; |
| } |
| |
| @Override |
| public Void visitDeclared_Intersection( |
| AnnotatedDeclaredType subtype, |
| AnnotatedIntersectionType supertype, |
| Set<AFConstraint> constraints) { |
| |
| // Note: AnnotatedIntersectionTypes cannot have a type variable as one of the direct |
| // parameters but a type variable may be the type subtype to an intersection bound <e.g. <T |
| // extends Serializable & Iterable<T>> |
| for (final AnnotatedTypeMirror intersectionBound : supertype.getBounds()) { |
| if (intersectionBound instanceof AnnotatedDeclaredType |
| && !((AnnotatedDeclaredType) intersectionBound).getTypeArguments().isEmpty()) { |
| addConstraint(subtype, supertype, constraints); |
| } |
| } |
| |
| return null; |
| } |
| |
| // Remember that NULL types can come from lower bounds |
| @Override |
| public Void visitDeclared_Null( |
| AnnotatedDeclaredType subtype, AnnotatedNullType supertype, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| // a primitive supertype provides us no information on the type of any type parameters for that |
| // method |
| @Override |
| public Void visitDeclared_Primitive( |
| AnnotatedDeclaredType subtype, |
| AnnotatedPrimitiveType supertype, |
| Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| @Override |
| public Void visitDeclared_Typevar( |
| AnnotatedDeclaredType subtype, |
| AnnotatedTypeVariable supertype, |
| Set<AFConstraint> constraints) { |
| // Note: We expect the A2F constraints where F == a targeted type supertype to already be |
| // removed. Therefore, supertype should NOT be a target. |
| addConstraint(subtype, supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitDeclared_Union( |
| AnnotatedDeclaredType subtype, AnnotatedUnionType supertype, Set<AFConstraint> constraints) { |
| return null; // TODO: NOT SUPPORTED AT THE MOMENT |
| } |
| |
| @Override |
| public Void visitDeclared_Wildcard( |
| AnnotatedDeclaredType subtype, |
| AnnotatedWildcardType supertype, |
| Set<AFConstraint> constraints) { |
| visitWildcardAsSuperType(subtype, supertype, constraints); |
| return null; |
| } |
| |
| // ------------------------------------------------------------------------ |
| // Intersection as subtype |
| @Override |
| public Void visitIntersection_Declared( |
| AnnotatedIntersectionType subtype, |
| AnnotatedDeclaredType supertype, |
| Set<AFConstraint> constraints) { |
| |
| // at least one of the intersection bound types must be convertible to the param type |
| final AnnotatedDeclaredType subtypeAsParam = |
| AnnotatedTypes.castedAsSuper(typeFactory, subtype, supertype); |
| if (subtypeAsParam != null && !subtypeAsParam.equals(supertype)) { |
| addConstraint(subtypeAsParam, supertype, constraints); |
| } |
| |
| return null; |
| } |
| |
| @Override |
| public Void visitIntersection_Intersection( |
| AnnotatedIntersectionType argument, |
| AnnotatedIntersectionType parameter, |
| Set<AFConstraint> constraints) { |
| return null; // TODO: NOT SUPPORTED AT THE MOMENT |
| } |
| |
| // provides no information as the AnnotatedNullType cannot refer to a type parameter |
| @Override |
| public Void visitIntersection_Null( |
| AnnotatedIntersectionType argument, |
| AnnotatedNullType parameter, |
| Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| // ------------------------------------------------------------------------ |
| // Null as argument |
| |
| /** |
| * NULL types only have primary annotations. A type parameter could only appear as a component of |
| * the parameter type and therefore has no relationship to these primary annotations |
| */ |
| @Override |
| public Void visitNull_Array( |
| AnnotatedNullType argument, AnnotatedArrayType parameter, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| /** |
| * NULL types only have primary annotations. A type parameter could only appear as a component of |
| * the parameter type and therefore has no relationship to these primary annotations |
| */ |
| @Override |
| public Void visitNull_Declared( |
| AnnotatedNullType argument, AnnotatedDeclaredType parameter, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| /** |
| * TODO: PERHAPS FOR ALL OF THESE WHERE WE COMPARE AGAINST THE LOWER BOUND, WE SHOULD INSTEAD |
| * COMPARE TODO: against the UPPER_BOUND with the LOWER_BOUND's PRIMARY ANNOTATIONS For captured |
| * types, the lower bound might be interesting so we compare against the lower bound but for most |
| * types the constraint added in this method is probably discarded in the next round of reduction |
| * (especially since we don't implement capture at the moment). |
| */ |
| @Override |
| public Void visitNull_Typevar( |
| AnnotatedNullType subtype, AnnotatedTypeVariable supertype, Set<AFConstraint> constraints) { |
| // Note: We would expect that parameter is not one of the targets or else it would already |
| // be removed. Therefore we compare NULL against its bound. |
| addConstraint(subtype, supertype.getLowerBound(), constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitNull_Wildcard( |
| AnnotatedNullType subtype, AnnotatedWildcardType supertype, Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(supertype); |
| // we don't use visitSupertype because Null types won't have interesting components |
| constraints.add(new A2F(subtype, supertype.getSuperBound())); |
| return null; |
| } |
| |
| @Override |
| public Void visitNull_Null( |
| AnnotatedNullType argument, AnnotatedNullType parameter, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| @Override |
| public Void visitNull_Union( |
| AnnotatedNullType argument, AnnotatedUnionType parameter, Set<AFConstraint> constraints) { |
| return null; // TODO: UNIONS ARE NOT YET SUPPORTED |
| } |
| |
| // Despite the fact that intersections are not yet supported, this is the right impelementation. |
| // NULL types only have primary annotations. Since type parameters cannot be a member of the |
| // intersection's bounds (though they can be component types), we do not need to do anything |
| // further. |
| @Override |
| public Void visitNull_Intersection( |
| AnnotatedNullType argument, |
| AnnotatedIntersectionType parameter, |
| Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| // Primitive parameter types tell us nothing about the type parameters |
| @Override |
| public Void visitNull_Primitive( |
| AnnotatedNullType argument, AnnotatedPrimitiveType parameter, Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| // ------------------------------------------------------------------------ |
| // Primitive as argument |
| |
| @Override |
| public Void visitPrimitive_Declared( |
| AnnotatedPrimitiveType subtype, |
| AnnotatedDeclaredType supertype, |
| Set<AFConstraint> constraints) { |
| // we may be able to eliminate this case, since I believe the corresponding constraint will |
| // just be discarded as the parameter must be a boxed primitive |
| addConstraint(typeFactory.getBoxedType(subtype), supertype, constraints); |
| return null; |
| } |
| |
| // Primitive parameter types tell us nothing about the type parameters |
| @Override |
| public Void visitPrimitive_Primitive( |
| AnnotatedPrimitiveType subtype, |
| AnnotatedPrimitiveType supertype, |
| Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| @Override |
| public Void visitPrimitive_Intersection( |
| AnnotatedPrimitiveType subtype, |
| AnnotatedIntersectionType supertype, |
| Set<AFConstraint> constraints) { |
| addConstraint(typeFactory.getBoxedType(subtype), supertype, constraints); |
| return null; |
| } |
| |
| // ------------------------------------------------------------------------ |
| // Union as argument |
| @Override |
| public Void visitUnion_Declared( |
| AnnotatedUnionType argument, AnnotatedDeclaredType parameter, Set<AFConstraint> constraints) { |
| return null; // TODO: UNIONS ARE NOT CURRENTLY SUPPORTED |
| } |
| |
| // ------------------------------------------------------------------------ |
| // typevar as argument |
| // If we've reached this point, the typevar is NOT one of the types we are inferring. |
| |
| @Override |
| public Void visitTypevar_Declared( |
| AnnotatedTypeVariable subtype, |
| AnnotatedDeclaredType supertype, |
| Set<AFConstraint> constraints) { |
| addConstraint(subtype.getUpperBound(), supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitTypevar_Typevar( |
| AnnotatedTypeVariable subtype, |
| AnnotatedTypeVariable supertype, |
| Set<AFConstraint> constraints) { |
| // if we've reached this point and the two are corresponding type variables, then they are |
| // NOT ones that may have a type variable we are inferring types for and therefore we can |
| // discard this constraint |
| if (!AnnotatedTypes.areCorrespondingTypeVariables( |
| typeFactory.getElementUtils(), subtype, supertype)) { |
| addConstraint(subtype.getUpperBound(), supertype.getLowerBound(), constraints); |
| } |
| |
| return null; |
| } |
| |
| @Override |
| public Void visitTypevar_Null( |
| AnnotatedTypeVariable subtype, AnnotatedNullType supertype, Set<AFConstraint> constraints) { |
| addConstraint(subtype.getUpperBound(), supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitTypevar_Wildcard( |
| AnnotatedTypeVariable subtype, |
| AnnotatedWildcardType supertype, |
| Set<AFConstraint> constraints) { |
| visitWildcardAsSuperType(subtype, supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitTypevar_Intersection( |
| AnnotatedTypeVariable subtype, |
| AnnotatedIntersectionType supertype, |
| Set<AFConstraint> constraints) { |
| addConstraint(subtype.getUpperBound(), supertype, constraints); |
| return null; |
| } |
| |
| // ------------------------------------------------------------------------ |
| // wildcard as subtype |
| @Override |
| public Void visitWildcard_Array( |
| AnnotatedWildcardType subtype, AnnotatedArrayType supertype, Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(subtype); |
| addConstraint(subtype.getExtendsBound(), supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitWildcard_Declared( |
| AnnotatedWildcardType subtype, |
| AnnotatedDeclaredType supertype, |
| Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(subtype); |
| addConstraint(subtype.getExtendsBound(), supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitWildcard_Intersection( |
| AnnotatedWildcardType subtype, |
| AnnotatedIntersectionType supertype, |
| Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(subtype); |
| addConstraint(subtype.getExtendsBound(), supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitWildcard_Primitive( |
| AnnotatedWildcardType subtype, |
| AnnotatedPrimitiveType supertype, |
| Set<AFConstraint> constraints) { |
| return null; |
| } |
| |
| @Override |
| public Void visitWildcard_Typevar( |
| AnnotatedWildcardType subtype, |
| AnnotatedTypeVariable supertype, |
| Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(subtype); |
| addConstraint(subtype.getExtendsBound(), supertype, constraints); |
| return null; |
| } |
| |
| @Override |
| public Void visitWildcard_Wildcard( |
| AnnotatedWildcardType subtype, |
| AnnotatedWildcardType supertype, |
| Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(subtype); |
| // since wildcards are handled in visitDeclared_Declared this could only occur if two |
| // wildcards were passed to type subtype inference at the top level. This can only occur |
| // because we do not implement capture conversion. |
| visitWildcardAsSuperType(subtype.getExtendsBound(), supertype, constraints); |
| return null; |
| } |
| |
| // should the same logic apply to typevars? |
| public void visitWildcardAsSuperType( |
| AnnotatedTypeMirror subtype, AnnotatedWildcardType supertype, Set<AFConstraint> constraints) { |
| TypeArgInferenceUtil.checkForUninferredTypes(supertype); |
| // this case occur only when supertype should actually be capture converted (which we don't |
| // do) because all other wildcard cases would be handled via Declared_Declared |
| addConstraint(subtype, supertype.getSuperBound(), constraints); |
| |
| // if type1 is below the superbound then it is necessarily below the extends bound |
| // BUT the extends bound may have interesting component types (like the array component) |
| // to which we also want to apply constraints |
| // e.g. visitArray_Wildcard(@I String[], ? extends @A String[]) |
| // if @I is an annotation we are trying to infer then we still want to infer that @I <: @A |
| // in fact |
| addInverseConstraint(subtype, supertype.getExtendsBound(), constraints); |
| } |
| } |