[Checkers] Declarative specification of qualifier hierarchy

Matt Papi mpapi at csail.mit.edu
Fri Mar 28 15:17:45 EDT 2008


> Yes, all checkers need to implement their own type checking.
> SimpleSubtypeRelation is not expressive enough for anything other than a 
> simple subtype relationship.

I think Mahmood may have meant that all checkers should *not* need to 
implement their own type checking. The point of GraphSubtypeRelation is 
that it's generalized: if you give it two annotations where one is a 
subtype of the other, it's essentially becomes SimpleSubtypeRelation; if 
you give it the IGJ or Javari relation graph, it handles those without 
having to do anything specially in the checkers. In particular, 
individual checkers won't have to worry about getting things like 
boxing, generics, etc. correct.

> I do think extending a Relation class for each checker is better than 
> expressing the hierarchy through meta-annotations. 

One benefit of meta-annotations versus specifying relations is that you 
get relationships for the annotations themselves -- you can easily ask 
if @NonNull and @Nullable can be written on the same type -- whereas 
isSubtype requires actually having the whole, annotated type present. I 
imagine this is useful for other things as well, but I don't have any 
concrete examples at the moment.

> To put it in other way, the differences between the desired functionality of SubtypeRelation and GraphSubtypeRelation are still not clear to me; and I think each checker could express its allowed assignments by extending some subclass of SubtypeRelation (including SubtypeRelation). 

With the graph relation, you need _only_ give it a type hierarchy (or 
not even that, if meta-annotations are used); with SubtypeRelation, it's 
hard to avoid having to re-implement difficult checks (for example, 
isSubtype(List<@ReadOnly Date>[], Object[])). They work the same in the 
end, but the graph relation holds information in a more flexible form 
(a set of edges rather than a black-box comparison method) that could be 
used elsewhere, and it seems like it will require much less code in the 
individual checkers.

Is your idea of the TypeRelation significantly different that what is 
there now? E.g., what would the code for the Javari relation ideally 
look like under that scheme? It might also help if Mahmood could share 
the work he's done on the graph relation so far (as I'd suggested in 
previous message) so you can get a better idea of what the that scheme 
would look like.


>> As a side-note, CustomChecker assumes that the 
>> negative annotation is a supertype of the positive annotation, which 
>> is false ("Plaintext/Encrypted", Trusted/Tained, etc).

That's not quite right. The CustomChecker supports two different 
schemes: a single annotation that is the subtype of the unannotated type 
(like Encrypted) or two annotations where one is the subtype of the 
other (like NonNull and Nullable), and giving two unrelated types is 
unsupported. The full type hierarchy for Encrypted is really { Encrypted 
<: Anytext, Plaintext <: Anytext }, so you can give the CustomChecker 
any of the following:
- Encrypted
- Plaintext
- Encrypted/Anytext
- Plaintext/Anytext
but not Plaintext/Encrypted (at least, not in this version). Positive 
and negative are not the best names (they come from the type notation 
sometimes seen for nullness where T+ = nonnull T and T- = nullable T), 
though I don't think they're used in any of our documentation.


- Matt



More information about the checkers mailing list