Warnings about loss of type refinement information

A relatively frequent question from users is why a type-checking error occurs, when it seems that type refinement should have made the Java construct legal. Oftentimes, the answer is that some call to an impure method cleared the type refinement information from the store.

Here is an example:

class TestString {
  int i;
  int[] arr;

  void flush_char() {
    if (i > 0) {
      help(i);
      int k = arr[i]; // warns here for @LowerBoundUnknown int i
    }
  }

  void help(@NonNegative int m) { ... }
}

The user might know that the help() method has no side effects, but the user forgot to specify this fact by annotating help() as @SideEffectFree.

I propose that the the type-checker should issue a warning about impure methods and merge points that have caused a loss of type refinement information.

Here is a rough design:

• The store records, for each expression, the most recent time that the expression's type was un-refined. This is new information, in addition to what is already recorded in the store. This new information will often be null, for an expression that has not had its type un-refined.

• Whenever an impure method call causes loss of type refinement information for an expression (the before and after types are non-equal), record in the store the line number and the original and final types. The final type is often the declared type. Likewise, at a merge point, record information whenever either of the two branches is not equal to the final type.

• Whenever a type is refined, null out its "lost refinement" information. In other words, only the most recent loss of refinement is recorded, even if the variable is repeatedly refined and unrefined. This is probably adequate in practice.

• Whenever a type error is reported, test whether the rhs expression (such as an actual argument) previously had a refined type that would have prevented this particular error message from appearing. If so, then the type-checker issues additional informational output, stating the line(s) that caused the loss of type refinement information. The informational output could also point at a section of the manual that lists workarounds, such as method postconditions, @SideEffectFree, and annotating the variable definition.

• How much path information should be kept about a given lost refinement? Relatedly, what should the CF do if an impure method call doesn't affect the type (it leaves the type unaffected)? This happens, for example, if there are two impure method calls in a row. If there hadn't been an unrefinement (the "lost refinement" information is null), there is nothing to do. If "lost refinement" information exists, here are two possibilities:

  • Don't overwrite the stored information. Only the first impure method call will be reported.
  • Append additional information without replacing the existing information. (Maybe in this case the CF would never overwrite, only append to, existing information in the store.) Multiple method calls and merge points may be reported.
    I don't have a feel for which of these would be better, but I lean toward the first for simplicity.

• The extra information in the store requires more memory and computation, yet for most methods no error is issued and so the information won't be used. So, instead do the following. By default, the information is not recorded. If an error message would be issued for a method, then re-start the analysis of that method from scratch, computing the information.

Start by tracing the type-checker's store, refinement handling, impure method calls, merge points, and type-error reporting described in the proposal. The work is complete when the checker can identify and report where relevant type refinement information was lost, while addressing the proposal's unresolved storage and path-information choices.