Propagate length information from argument to return value of Arrays.copyOf()

checker/tests/index/Issue3224.java

@@ -0,0 +1,40 @@
+// Test case for https://tinyurl.com/cfissue/3224
+
+import java.util.Arrays;
+import org.checkerframework.common.value.qual.IntRange;
+import org.checkerframework.common.value.qual.MinLen;
+
+public class Issue3224 {
+    static class Arrays {
+        static String[] copyOf(String[] args, int length) {
+            return args;
+        }
+    }
+
+    public static void m1(String @MinLen(1) [] args) {
+        int i = 4;
+        String @MinLen(1) [] args2 = java.util.Arrays.copyOf(args, i);
+    }
+
+    public static void m2(String @MinLen(1) [] args) {
+        String @MinLen(1) [] args2 = java.util.Arrays.copyOf(args, args.length);
+    }
+
+    public static void m3(String @MinLen(1) ... args) {
+        String @MinLen(1) [] args2 = java.util.Arrays.copyOf(args, args.length);
+    }
+
+    public static void m4(String @MinLen(1) [] args, @IntRange(from = 10, to = 200) int len) {
+        String @MinLen(1) [] args2 = java.util.Arrays.copyOf(args, len);
+    }
+
+    public static void m5(String @MinLen(1) [] args, String[] otherArray) {
+        // :: error: assignment.type.incompatible
+        String @MinLen(1) [] args2 = java.util.Arrays.copyOf(args, otherArray.length);
+    }
+
+    public static void m6(String @MinLen(1) [] args) {
+        // :: error: assignment.type.incompatible
+        String @MinLen(1) [] args2 = Arrays.copyOf(args, args.length);
+    }
+}

framework/src/main/java/org/checkerframework/common/value/ValueMethodIdentifier.java

@@ -19,13 +19,21 @@ class ValueMethodIdentifier {
     private final List<ExecutableElement> mathMinMethod;
     /** The {@code java.lang.Math#max()} methods. */
     private final List<ExecutableElement> mathMaxMethod;
+    /** Arrays.copyOf() methods. */
+    private final List<ExecutableElement> copyOfMethod;
 
+    /**
+     * Initialize elements with methods that have special handling in the value checker
+     *
+     * @param processingEnv the processing environment
+     */
     public ValueMethodIdentifier(ProcessingEnvironment processingEnv) {
         lengthMethod = TreeUtils.getMethod("java.lang.String", "length", 0, processingEnv);
         startsWithMethod = TreeUtils.getMethod("java.lang.String", "startsWith", 1, processingEnv);
         endsWithMethod = TreeUtils.getMethod("java.lang.String", "endsWith", 1, processingEnv);
         mathMinMethod = TreeUtils.getMethods("java.lang.Math", "min", 2, processingEnv);
         mathMaxMethod = TreeUtils.getMethods("java.lang.Math", "max", 2, processingEnv);
+        copyOfMethod = TreeUtils.getMethods("java.util.Arrays", "copyOf", 2, processingEnv);
     }
 
     /** Returns true iff the argument is an invocation of Math.min. */
@@ -59,4 +67,15 @@ public boolean isEndsWithMethod(ExecutableElement method) {
         // equals (rather than ElementUtils.ismethod) because String.length cannot be overridden
         return method.equals(endsWithMethod);
     }
+
+    /**
+     * Determines whether a tree is an invocation of the {@code Arrays.copyOf()} method.
+     *
+     * @param tree tree to check
+     * @param processingEnv the processing environment
+     * @return true iff the argument is an invocation of {@code Arrays.copyOf()} method.
+     */
+    public boolean isArraysCopyOfInvocation(Tree tree, ProcessingEnvironment processingEnv) {
+        return TreeUtils.isMethodInvocation(tree, copyOfMethod, processingEnv);
+    }
 }

framework/src/main/java/org/checkerframework/common/value/ValueTreeAnnotator.java

@@ -17,6 +17,7 @@
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypesUtils;
@@ -398,6 +399,22 @@ public Void visitMethodInvocation(MethodInvocationTree tree, AnnotatedTypeMirror
             }
         }
 
+        if (atypeFactory
+                .getMethodIdentifier()
+                .isArraysCopyOfInvocation(tree, atypeFactory.getProcessingEnv())) {
+            List<? extends ExpressionTree> args = tree.getArguments();
+            if (args.size() != 2) {
+                throw new BugInCF(
+                        "Arrays.copyOf() should have 2 arguments. This point should not have reached");
+            }
+            Range range =
+                    ValueCheckerUtils.getPossibleValues(
+                            atypeFactory.getAnnotatedType(args.get(1)), atypeFactory);
+            if (range != null) {
+                type.replaceAnnotation(atypeFactory.createArrayLenRangeAnnotation(range));
+            }
+        }
+
         if (!methodIsStaticallyExecutable(TreeUtils.elementFromUse(tree))
                 || !handledByValueChecker(type)) {
             return null;