Apply declaration bounds to string conversions and binary comparisons

checker/src/main/java/org/checkerframework/checker/lock/LockTreeAnnotator.java

@@ -3,13 +3,17 @@
 import com.sun.source.tree.BinaryTree;
 import com.sun.source.tree.CompoundAssignmentTree;
 import com.sun.source.tree.NewArrayTree;
-import com.sun.source.tree.Tree;
 
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
+import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypesUtils;
 
+/**
+ * A TreeAnnotator implementation to apply special type introduction rules to string concatenations,
+ * binary comparisons, and new array instantiations.
+ */
 public class LockTreeAnnotator extends TreeAnnotator {
 
     public LockTreeAnnotator(AnnotatedTypeFactory atypeFactory) {
@@ -26,8 +30,7 @@ public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
         // @GuardedBy({}) since for such operators, both operands are of type @GuardedBy({}) boolean
         // to begin with.
 
-        if (isBinaryComparisonOrInstanceOfOperator(node.getKind())
-                || TypesUtils.isString(type.getUnderlyingType())) {
+        if (TreeUtils.isBinaryComparison(node) || TypesUtils.isString(type.getUnderlyingType())) {
             // A boolean or String is always @GuardedBy({}). LockVisitor determines whether
             // the LHS and RHS of this operation can be legally dereferenced.
             type.replaceAnnotation(((LockAnnotatedTypeFactory) atypeFactory).GUARDEDBY);
@@ -38,31 +41,6 @@ public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
         return super.visitBinary(node, type);
     }
 
-    /**
-     * Indicates that the result of the operation is a boolean value.
-     *
-     * @param opKind the operation to check
-     * @return whether the result is boolean
-     */
-    private static boolean isBinaryComparisonOrInstanceOfOperator(Tree.Kind opKind) {
-        switch (opKind) {
-            case EQUAL_TO:
-            case NOT_EQUAL_TO:
-                // Technically, <=, <, > and >= are irrelevant for visitBinary, since currently
-                // boxed primitives cannot be annotated with @GuardedBy(...), but they are left here
-                // in case that rule changes.
-            case LESS_THAN:
-            case LESS_THAN_EQUAL:
-            case GREATER_THAN:
-            case GREATER_THAN_EQUAL:
-            case INSTANCE_OF:
-                return true;
-            default:
-        }
-
-        return false;
-    }
-
     @Override
     public Void visitCompoundAssignment(CompoundAssignmentTree node, AnnotatedTypeMirror type) {
         if (TypesUtils.isString(type.getUnderlyingType())) {

checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java

@@ -26,7 +26,7 @@
 
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
-import javax.lang.model.type.TypeKind;
+import javax.lang.model.type.TypeMirror;
 
 /**
  * The SignednessVisitor enforces the Signedness Checker rules. These rules are described in the
@@ -154,16 +154,21 @@ public Void visitBinary(BinaryTree node, Void p) {
                     AnnotationMirror rightAnno =
                             rightOpType.getEffectiveAnnotations().iterator().next();
 
-                    if (leftOpType.getKind() != TypeKind.CHAR
-                            && !TypesUtils.isDeclaredOfName(
-                                    leftOpType.getUnderlyingType(), "java.lang.Character")
+                    // Note that leftOpType.getUnderlyingType() and rightOpType.getUnderlyingType()
+                    // are always java.lang.String. Please refer to binaryTreeArgTypes for more
+                    // details.
+                    // Here, the original types of operands can be something different from string.
+                    // For example, "123" + obj is a string concatenation in which the original type
+                    // of the right operand is java.lang.Object.
+                    TypeMirror leftOpOriginalType = TreeUtils.typeOf(leftOp);
+                    TypeMirror rightOpOriginalType = TreeUtils.typeOf(rightOp);
+
+                    if (!TypesUtils.isCharType(leftOpOriginalType)
                             && !atypeFactory
                                     .getQualifierHierarchy()
                                     .isSubtype(leftAnno, atypeFactory.SIGNED)) {
                         checker.reportError(leftOp, "unsigned.concat");
-                    } else if (rightOpType.getKind() != TypeKind.CHAR
-                            && !TypesUtils.isDeclaredOfName(
-                                    rightOpType.getUnderlyingType(), "java.lang.Character")
+                    } else if (!TypesUtils.isCharType(rightOpOriginalType)
                             && !atypeFactory
                                     .getQualifierHierarchy()
                                     .isSubtype(rightAnno, atypeFactory.SIGNED)) {
@@ -341,9 +346,9 @@ public Void visitCompoundAssignment(CompoundAssignmentTree node, Void p) {
 
             case PLUS_ASSIGNMENT:
                 if (TreeUtils.isStringCompoundConcatenation(node)) {
-                    if (exprType.getKind() != TypeKind.CHAR
-                            && !TypesUtils.isDeclaredOfName(
-                                    exprType.getUnderlyingType(), "java.lang.Character")) {
+                    // Note that exprType.getUnderlyingType() is always java.lang.String.
+                    // Please refer to compoundAssignmentTreeArgTypes for more details.
+                    if (!TypesUtils.isCharType(TreeUtils.typeOf(expr))) {
                         AnnotationMirror anno =
                                 exprType.getEffectiveAnnotations().iterator().next();
                         if (!atypeFactory

docs/CHANGELOG.md

@@ -9,6 +9,15 @@ files and in .java files.
 
 **Implementation details:**
 
+In `PropagationTreeAnnotator.visitBinary`, we now consider the two cases where
+the resulting Java type of a binary operation can be different from the operands'
+types: string concatenation and binary comparison. We apply the declaration
+bounds of the resulting Java type to ensure annotations in the ATM are valid.
+
+Deprecated `AnnotatedTypeFactory.binaryTreeArgTypes(AnnotatedTypeMirror, AnnotatedTypeMirror)` in favor of
+`AnnotatedTypeFactory.binaryTreeArgTypes(BinaryTree)` and
+`AnnotatedTypeFactory.compoundAssignmentTreeArgTypes(CompoundAssignmentTree)`.
+
 **Closed issues:**
 
 typetools#3025, typetools#3030, typetools#3236.

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -1405,6 +1405,35 @@ public Set<AnnotationMirror> getTypeDeclarationBounds(TypeMirror type) {
         return qualifierUpperBounds.getBoundQualifiers(type);
     }
 
+    /**
+     * Compare the given {@code annos} with the declaration bounds of {@code type} and return the
+     * appropriate qualifiers. For each qualifier in {@code annos}, if it is a subtype of the
+     * declaration bound in the same hierarchy, it will be added to the result; otherwise, the
+     * declaration bound will be added to the result instead.
+     *
+     * @param type java type that specifies the qualifier upper bound
+     * @param annos a set of qualifiers to be compared with the declaration bounds of {@code type}
+     * @return the modified {@code annos} after applying the rules described above
+     */
+    public Set<AnnotationMirror> getAnnotationOrTypeDeclarationBound(
+            TypeMirror type, Set<? extends AnnotationMirror> annos) {
+        Set<AnnotationMirror> boundAnnos = getTypeDeclarationBounds(type);
+        Set<AnnotationMirror> results = AnnotationUtils.createAnnotationSet();
+
+        for (AnnotationMirror anno : annos) {
+            AnnotationMirror boundAnno =
+                    qualHierarchy.findAnnotationInSameHierarchy(boundAnnos, anno);
+            assert boundAnno != null;
+
+            if (!qualHierarchy.isSubtype(anno, boundAnno)) {
+                results.add(boundAnno);
+            } else {
+                results.add(anno);
+            }
+        }
+        return results;
+    }
+
     /**
      * Returns the set of qualifiers that are the upper bound for a type use if no other bound is
      * specified for the type.
@@ -3078,28 +3107,92 @@ public Set<AnnotationMirror> getWidenedAnnotations(
     }
 
     /**
-     * Returns the types of the two arguments to the BinaryTree, accounting for widening and
-     * unboxing if applicable.
+     * Returns the types of the two arguments to the BinaryTree. Please refer to {@link
+     * #binaryTreeArgTypes(TypeMirror, AnnotatedTypeMirror, AnnotatedTypeMirror)} )} for more
+     * details.
      *
      * @param node a binary tree
      * @return the types of the two arguments
      */
     public Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> binaryTreeArgTypes(BinaryTree node) {
         return binaryTreeArgTypes(
-                getAnnotatedType(node.getLeftOperand()), getAnnotatedType(node.getRightOperand()));
+                TreeUtils.typeOf(node),
+                getAnnotatedType(node.getLeftOperand()),
+                getAnnotatedType(node.getRightOperand()));
     }
 
     /**
-     * Returns the types of the two arguments to the CompoundAssignmentTree, accounting for widening
-     * and unboxing if applicable.
+     * Returns the types of the two arguments to the CompoundAssignmentTree. Please refer to {@link
+     * #binaryTreeArgTypes(TypeMirror, AnnotatedTypeMirror, AnnotatedTypeMirror)} ) for more
+     * details.
      *
      * @param node a compound assignment tree
      * @return the types of the two arguments
      */
     public Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> compoundAssignmentTreeArgTypes(
             CompoundAssignmentTree node) {
         return binaryTreeArgTypes(
-                getAnnotatedType(node.getVariable()), getAnnotatedType(node.getExpression()));
+                TreeUtils.typeOf(node.getVariable()),
+                getAnnotatedType(node.getVariable()),
+                getAnnotatedType(node.getExpression()));
+    }
+
+    /**
+     * Returns the types of the two arguments to a binary operation. There are two special cases:
+     *
+     * <p>1. If both operands have numeric type, widening and unboxing will be applied accordingly.
+     *
+     * <p>2. If we have a non-string operand in a string concatenation (i.e., result is a string),
+     * we will always return a string ATM for the operand. The resulting ATM will have the original
+     * annotations with the declaration bounds of string type applied. Please check {@link
+     * #getAnnotationOrTypeDeclarationBound} for more details.
+     *
+     * @param resultType the type of the result of a binary operation
+     * @param left the type of the left argument of a binary operation
+     * @param right the type of the right argument of a binary operation
+     * @return the types of the two arguments
+     */
+    protected Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> binaryTreeArgTypes(
+            TypeMirror resultType, AnnotatedTypeMirror left, AnnotatedTypeMirror right) {
+        TypeKind widenedNumericType =
+                TypeKindUtils.widenedNumericType(
+                        left.getUnderlyingType(), right.getUnderlyingType());
+        if (TypeKindUtils.isNumeric(widenedNumericType)) {
+            TypeMirror widenedNumericTypeMirror = types.getPrimitiveType(widenedNumericType);
+            AnnotatedPrimitiveType leftUnboxed = applyUnboxing(left);
+            AnnotatedPrimitiveType rightUnboxed = applyUnboxing(right);
+            AnnotatedPrimitiveType leftWidened =
+                    (leftUnboxed.getKind() == widenedNumericType
+                            ? leftUnboxed
+                            : getWidenedPrimitive(leftUnboxed, widenedNumericTypeMirror));
+            AnnotatedPrimitiveType rightWidened =
+                    (rightUnboxed.getKind() == widenedNumericType
+                            ? rightUnboxed
+                            : getWidenedPrimitive(rightUnboxed, widenedNumericTypeMirror));
+            return Pair.of(leftWidened, rightWidened);
+        } else if (TypesUtils.isString(resultType)) {
+            // the result of a binary operation is String iff it's string concatenation
+            AnnotatedTypeMirror leftStringConverted = left;
+            AnnotatedTypeMirror rightStringConverted = right;
+
+            if (!TypesUtils.isString(left.getUnderlyingType())) {
+                leftStringConverted = toAnnotatedType(resultType, false);
+                Set<AnnotationMirror> annos =
+                        getAnnotationOrTypeDeclarationBound(
+                                resultType, left.getEffectiveAnnotations());
+                leftStringConverted.addAnnotations(annos);
+            }
+            if (!TypesUtils.isString(right.getUnderlyingType())) {
+                rightStringConverted = toAnnotatedType(resultType, false);
+                Set<AnnotationMirror> annos =
+                        getAnnotationOrTypeDeclarationBound(
+                                resultType, right.getEffectiveAnnotations());
+                rightStringConverted.addAnnotations(annos);
+            }
+            return Pair.of(leftStringConverted, rightStringConverted);
+        }
+
+        return Pair.of(left, right);
     }
 
     /**
@@ -3109,7 +3202,10 @@ public Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> compoundAssignmentTreeArgT
      * @param left the type of the left argument of a binary operation
      * @param right the type of the right argument of a binary operation
      * @return the types of the two arguments
+     * @deprecated use {@link #binaryTreeArgTypes(BinaryTree)} or {@link
+     *     #compoundAssignmentTreeArgTypes(CompoundAssignmentTree)}
      */
+    @Deprecated // 2022-06-03
     public Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> binaryTreeArgTypes(
             AnnotatedTypeMirror left, AnnotatedTypeMirror right) {
         TypeKind resultTypeKind =

framework/src/main/java/org/checkerframework/framework/type/treeannotator/PropagationTreeAnnotator.java

@@ -18,10 +18,10 @@
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
 import org.checkerframework.framework.type.QualifierHierarchy;
-import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.CollectionUtils;
 import org.checkerframework.javacutil.Pair;
 import org.checkerframework.javacutil.TreePathUtil;
+import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypeKindUtils;
 
 import java.util.Map;
@@ -212,12 +212,15 @@ public Void visitCompoundAssignment(CompoundAssignmentTree node, AnnotatedTypeMi
             // propagated annotations won't be applied.  So don't compute them.
             return null;
         }
-        AnnotatedTypeMirror rhs = atypeFactory.getAnnotatedType(node.getExpression());
-        AnnotatedTypeMirror lhs = atypeFactory.getAnnotatedType(node.getVariable());
+
+        Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> argTypes =
+                atypeFactory.compoundAssignmentTreeArgTypes(node);
         Set<? extends AnnotationMirror> lubs =
                 qualHierarchy.leastUpperBounds(
-                        rhs.getEffectiveAnnotations(), lhs.getEffectiveAnnotations());
+                        argTypes.first.getEffectiveAnnotations(),
+                        argTypes.second.getEffectiveAnnotations());
         type.addMissingAnnotations(lubs);
+
         return null;
     }
 
@@ -237,6 +240,13 @@ public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) {
                 qualHierarchy.leastUpperBounds(
                         argTypes.first.getEffectiveAnnotations(),
                         argTypes.second.getEffectiveAnnotations());
+
+        if (TreeUtils.isBinaryComparison(node)) {
+            // When we have binary comparison, the result type (boolean) can be different
+            // from the operands' types. So we need to apply the bounds of boolean to the
+            // lubs.
+            lubs = atypeFactory.getAnnotationOrTypeDeclarationBound(type.getUnderlyingType(), lubs);
+        }
         type.addMissingAnnotations(lubs);
 
         return null;
@@ -337,16 +347,8 @@ private boolean hasPrimaryAnnotationInAllHierarchies(AnnotatedTypeMirror type) {
      * @param annos annotations to add to type
      */
     private void addAnnoOrBound(AnnotatedTypeMirror type, Set<? extends AnnotationMirror> annos) {
-        Set<AnnotationMirror> boundAnnos =
-                atypeFactory.getQualifierUpperBounds().getBoundQualifiers(type.getUnderlyingType());
-        Set<AnnotationMirror> annosToAdd = AnnotationUtils.createAnnotationSet();
-        for (AnnotationMirror boundAnno : boundAnnos) {
-            AnnotationMirror anno = qualHierarchy.findAnnotationInSameHierarchy(annos, boundAnno);
-            if (anno != null && !qualHierarchy.isSubtype(anno, boundAnno)) {
-                annosToAdd.add(boundAnno);
-            }
-        }
+        Set<AnnotationMirror> annosToAdd =
+                atypeFactory.getAnnotationOrTypeDeclarationBound(type.getUnderlyingType(), annos);
         type.addMissingAnnotations(annosToAdd);
-        type.addMissingAnnotations(annos);
     }
 }

framework/src/test/java/org/checkerframework/framework/test/junit/TypeDeclBoundsTest.java

@@ -0,0 +1,20 @@
+package org.checkerframework.framework.test.junit;
+
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.checkerframework.framework.testchecker.typedeclbounds.TypeDeclBoundsChecker;
+import org.junit.runners.Parameterized;
+
+import java.io.File;
+import java.util.List;
+
+public class TypeDeclBoundsTest extends CheckerFrameworkPerDirectoryTest {
+
+    public TypeDeclBoundsTest(List<File> testFiles) {
+        super(testFiles, TypeDeclBoundsChecker.class, "typedeclbounds");
+    }
+
+    @Parameterized.Parameters
+    public static String[] getTestDirs() {
+        return new String[] {"typedeclbounds"};
+    }
+}

framework/src/test/java/org/checkerframework/framework/testchecker/typedeclbounds/TypeDeclBoundsAnnotatedTypeFactory.java

@@ -0,0 +1,26 @@
+package org.checkerframework.framework.testchecker.typedeclbounds;
+
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.testchecker.typedeclbounds.quals.Bottom;
+import org.checkerframework.framework.testchecker.typedeclbounds.quals.S1;
+import org.checkerframework.framework.testchecker.typedeclbounds.quals.S2;
+import org.checkerframework.framework.testchecker.typedeclbounds.quals.Top;
+
+import java.lang.annotation.Annotation;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.Set;
+
+public class TypeDeclBoundsAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+    public TypeDeclBoundsAnnotatedTypeFactory(BaseTypeChecker checker) {
+        super(checker);
+        postInit();
+    }
+
+    @Override
+    protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
+        return new HashSet<>(Arrays.asList(Top.class, Bottom.class, S1.class, S2.class));
+    }
+}

framework/src/test/java/org/checkerframework/framework/testchecker/typedeclbounds/TypeDeclBoundsChecker.java

@@ -0,0 +1,5 @@
+package org.checkerframework.framework.testchecker.typedeclbounds;
+
+import org.checkerframework.common.basetype.BaseTypeChecker;
+
+public class TypeDeclBoundsChecker extends BaseTypeChecker {}