panacekcz / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
0 stars 0 forks source link

Refine minimum string length after startsWith and endsWith #6

Closed panacekcz closed 7 years ago

panacekcz commented 7 years ago

This is a part of the Bounded-size strings GSoC project, made in this fork to start a review process by @kelloggm. A PR with this feature will be opened in the main repository after typetools#1352 is merged.

With these changes, the minimum length of the receiver string in the then-branch is refined to the minimum length known for the argument (based on a stored annotation or the length of a string literal).

The purpose is to support code like:

if(str.startsWith("x")){
 String after = str.substring(1);
}

This pattern appears often in plume-lib and causes warnings from the index checker with support for strings (typetools#1413). With the added refinement, the checker will see that the string is at least as long as the prefix or suffix and so the index is valid for the string.

Unlike outlined in kelloggm#56, this PR does not use annotations, but adds special handling of String.startsWith(String) and String.endWith(String) to ValueTransfer.

panacekcz commented 7 years ago

@kelloggm, I have addressed the review comments.

panacekcz commented 7 years ago

Does not work in this method:

void m(String str) {
    int i = 0;
    while (str.endsWith("[]")) {
        @MinLen(2) String str2 = str;
        i++;
    }
}
error: [assignment.type.incompatible] incompatible types in assignment.
            @MinLen(2) String str2 = str;
                                     ^
  found   : @UnknownVal String
  required: @ArrayLenRange(from=2, to=2147483647) String

Removing the increment or using if instead of while makes it work.

panacekcz commented 7 years ago

Reopened as typetools#1432 in the main repository.