[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