Type checking exception parameters and throws clauses

[Suzanne Millstein]

All,

Currently, any type-qualifier annotation can be written on an exception parameter, but there is no enforcement that a caught exception will be of that qualified type.  For example:

try{

  @A Throwable t = ...;

  throw t;  // no warning even if @B <: @A

} catch( @B Throwable e){

}

Related, type-qualifier annotation on types in a throws clause are not checked.  For example,

void foo() throws @B Throwable {

    @A Throwable t = ...;

     throw t; // no warning even if  @B <: @A

}

If an exception parameter or type in a throws clause is an unchecked exception, a type checker* cannot verify these qualified typed. So, qualifiers in these locations must be top. 

If an exception parameter or type in a throws clause is a checked exception, a type checker could verify these qualifiers.  This would be a bit complicated because each throws statement could match more than one exception parameter or type in a throws clause.  (It would probably take a week or two to get the design and implementation correct.) 

I propose, for now, we treat checked exceptions conservatively -- force qualifiers in these locations to be top.  Then perhaps during the bug fix release next year, we add more precise checking for checked exceptions.

Thoughts?

-Suzanne

* In the case of the Nullness Checker, both exception parameters and types in throws clauses can be @NonNull because a null pointer exception is thrown if null would be thrown.  In general, the Nullness Checker will need to override checking of exceptions parameters and types in throws clauses.

[Suzanne Millstein]

I've implemented the conservative approach for exception parameters -- that is they must be top. (The Nullness Checker overrides this behavior.)  The test pass for all checkers except for the Fenum, IGJ, OIGJ, Javari and Gui Effects Checkers.  I explain the issue with each checker and propose a possible solution below.  

Fenum Checker:

The top qualifier @FenumTop may not be written, so if exception parameters are top, they can only be assigned to local variables or re-thrown. So, this causes unannotated code to not type checker. 

Exceptions should not be fake enums, so I propose that the annotation on exception parameters must be @FenumUnqualified.  

IGJ, OIGJ, and Javari Checkers:

If exception parameters are forced to be @ReadOnly, then unannotated code might not type check.  For example:

  catch( @ReadOnly Exception e) {

      Exception e2 = e;  // incompatible types, expected @Mutable

      throw new RuntimeException("message'", e) // incompatible types, expected @Mutable

   }

One alternative design is to force exception parameters to be at least @Mutable and only allow @Mutable exceptions to be thrown.

GUI Effect Checker:

@UI is the top type qualifier, @AlwaysSafe is bottom and the default.  Is it safe to assume that exceptions never access UI elements? 

Are these proposals reasonable?

Thanks,

Suzanne