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

[PRITI1999]

Fixes #3224;
The Value checker did not infer array length information from the arguments of Arrays.copyOf() method leading to false positives.

To avoid those false positives, check if the expression valueTree is a call to Arrays.copyOf() method in commonAssignmentCheck() of ValueVisitor.java and then add appropriate @ArrayLen annotations to the return value of Arrays.copyOf().

[kelloggm]

Thanks for this pull request :)

I think there are some things we can do to improve it. I noted two specific changes in my review, but I'm also somewhat unsure of the algorithm and want to discuss it.

Arrays.copyOf is guaranteed to return an array of length equal to its second argument, even if the input array is not that long: all of the various versions of it have text like this: "Copies the specified array, truncating or padding with nulls (if necessary) so the copy has the specified length." I think that this means that we don't need a special-case for when the second argument is the length of an array; in all cases, we should convert any IntVal annotations on the second argument to ArrayLen annotations on the result (and similarly with IntRange to ArrayLenRange. Because the length of an array with an ArrayLen annotation should have a corresponding IntVal annotation, the special-case should be taken care of by the other rules in the type system.

[kelloggm]

This only tests that the second argument is any array length access expression. The correct test needs to check that it is an array length access for the array that is the first argument. You can add a test case for this:

    public static void m4(String @MinLen(1) [] args, String[] otherArray) {
        // :: error: assignment.type.incompatible
        String @MinLen(1) [] args2 = Arrays.copyOf(args, otherArray.length);
    }

[PRITI1999]

Do we want to check this now? As suggested above I have added to valuetype any @IntVal or @IntRange annotation on the second argument. Suppose the user intends to have args2 of the same length as otherArray, then this check might lead to a false positive.

[kelloggm]

In the test case I suggested, that is a true positive: otherArray might not be @MinLen(1), even if the user hopes that it is - its length could be zero. I think you can add that test method verbatim into the existing test (except for changing the name).

[kelloggm]

Thanks for the improvements. I noticed a few other things we can improve, but I think we're getting close.

[kelloggm]

nit: in camel-case, this should be isArraysCopyOfMethodInvocation (that is, capitalize the "c" in "copy")

[kelloggm]

This test isn't strong enough - it will return true on any method named copyOf in a class named Arrays, even if it is not the one from the JDK.

You should look at how IndexMethodIdentifier in the Index Checker identifies specific methods; you should be able to use the same kind of code here to identify Arrays.copyOf with confidence.

(It would probably also be worthwhile to add an inner static class named "Arrays" with a static "copyOf" method to the tests and then ensure that your code is not invoked when that method is called.)

[kelloggm]

Please add a check here that the length of args is what you expect (i.e. 2) and throw a BugInCF otherwise

[kelloggm]

Rather than checking for IntVal and IntRange by hand, I suggest using ValueCheckerUtils.getPossibleValues, which returns a Range or null if the annotation isn't integral. It already has support for both IntVal and IntRange, and you should be able to just use its lower bound directly rather than doing the computations below. That will greatly simplify the code.

[kelloggm]

One minor comment, no need for me to review again. This can be merged once tests are passing.

Thanks for this contribution - it looks fantastic now!

[kelloggm]

range can be null here, but createArrayLenRange assumes its input in non-null. Can you add a null check and only do the type.replaceAnnotation(atypeFactory.createArrayLenRangeAnnotation(range)); if the range is non-null?