[Checkers] @Raw in the nullness type qualifier hierarchy

Mahmood Ali mahmood at MIT.EDU
Sun May 24 23:31:07 EDT 2009


Greetings,

> I would have expected rawness to be orthogonal to nullness -- and in  
> fact
> for field types to act a bit like our dependent types, in that the  
> field is
> nullable exactly if the containing object is @Raw.  Is there a  
> benefit to
> making this all one type hierarchy?
We approached this problem from a typical subtype contract rules view  
rather than through intellectual examination:

- The Nonnull contract is stronger than Raw contract
   Any NonNull reference can be used as a Raw reference
     We can call Raw methods on NonNull reference.
     i.e. the assignment of the NonNull reference to the Raw receiver  
is valid
   Not visa-versa:
     Cannot call NonNull method on a Raw method (e.g. in constructor).

- Raw contract is stronger than Nullable contract
   Any Raw reference can be used as a Nullable one
     Obvious, Nullable is the root
   Not the other way around
     You can always dereference a Raw object to access fields and Raw  
methods safely, while you cannot on a Nullable reference.

Can you think of a case when this is not true?

> Is there a benefit to making this all one type hierarchy?  (I see  
> that it enables one to cast away rawness by casting to @NonNull, but  
> that seems like a slightly obscure
> way to cast away rawness.)
The main conceptual benefit is simplicity, I would argue.  It's easier  
to think of them as one type system when thinking of issues related to  
casts and flow.

The main benefit as a whole is an implementation benefit, as the  
decision simplifies the Nullness code significantly.  This choice  
makes the nullness checker require only adding Raw annotation  
implicitly to constructor receivers for it to handle Raw properly:
   - No special code to handle subtyping rules and interaction between  
type systems.
   - No special code to handle flow, e.g. cases like:
     void method() @Raw {
       Object ref = this;
       ref.nonRawMethod();   // invalid
       ref = new ThisClass();
       ref.nonRawMethod();   // valid
     }

Note: we ended up writing a bit more code to handle inference of  
NonNull qualifier of a constructor receiver when all the fields have  
been initialized.

Regards,
Mahmood




More information about the checkers mailing list