Value Checker sometimes infers too-wide IntRange annotations

[kelloggm]

I added a test case on this branch, which has two examples of the problem (both from plume-util): https:/kelloggm/checker-framework/tree/number-format-exception. You can run the test with ./gradlew ainferIndexAjavaTest. Here is one example:

  public static int count(String s, int ch) {
    int result = 0;
    int pos = s.indexOf(ch);
    while (pos > -1) {
      result++;
      pos = s.indexOf(ch, pos + 1);
    }
    return result;
  }

The symptom is a NumberFormatException: WPI infers an @IntRange annotation that is larger than the bounds of the underlying type (i.e., an @IntRange on an int whose to element is only representable as a long; in the above case, the offending annotation is ``) for the method's return type. When the second round attempts to read the resulting ajava file, the parser crashes. (After running the test, you can see the malformed .ajava file in inference-output sibling directory to the test case.)

I think the parser crashing is expected behavior, and that the underlying problem is somewhere in the Value Checker's local type refinement: it is non-sensical to have an IntRange annotation that is larger than the underlying type's possible range. This isn't a problem during normal Value Checker operation, because any range is a subtype of @UnknownVal.

I've attempted without success to locate the cause of the too-wide local refinement. My best guess is that ValueAnnotatedTypeFactory#getRange is mis-used somewhere where there is a bound on only one side (e.g., only a from value in the range) instead of both bounds being present, and the Long.MAX_VALUE is sneaking in that way. But, I can't seem to find where the actual problem is.

I also attempted to deal with this on the WPI side by checking all return types for too-wide ranges before printing them to the ajava file, but this doesn't work: the resulting code isn't verifiable, because the annotation is more precise than the inferred range, and so the checker issues a return error. So, we need to find and fix the cause of the imprecision rather than stop it at the WPI level. Another possible idea that I had is to try to add WPI-specific logic to ValueTransfer#visitReturn at return nodes to convert ranges in return expressions so that they fit in the return type, but I wasn't able to get the declared return type from the return node (possibly because I don't remember how to use the API).

@smillst do you have any idea what might be causing this and/or how we can work around it?

[kelloggm]

Update: I've written a version of the test case that doesn't rely on WPI, which is in framework/tests/value/TooWideRanges.java on the same branch I mentioned in the previous comment. To write that test, I just added a full integer range to each return type and demonstrated that it isn't verifiable (i.e., the same reason that modifying WPI not to produce too-wide ranges didn't work).