[Checkers] Questions about javari checker issues

[Mahmood Ali]

Hi Telmo,

I am writing this email without reviewing the code.  So the names  
might be off.  Unfortunately, I am behind in improving the  
documentation.  There is some lame documentation here and there.  You  
might like to review GraphSubtypeRelations and TypesRelations (and see  
how IGJ deals with it).  Improving the documentation is my top  
priority now.

> A. Mahmood pointed to me that as of the last release, the Javari  
> checker doesn't emit errors for an assignment of a type A<@Mutable  
> B> into a type A<@ReadOnly B>, which seems a high priority bug.  
> Implementation-wise, I think I should override more methods on  
> JavariChecker to behave differently once the assignment check is  
> being done on type parameters, instead of main types. Matt tells me  
> that Mahmood's GraphSubtypeRelation proposal might change that, and/ 
> or might change the way this must be fixed. Should I try to fix this  
> bug as it is now, try to change into GraphSubtypeRelation myself  
> (requiring catching up on its implementation), or wait for Mahmood  
> to perform the change?
I emailed you the batch earlier that deals with Javari.  It dealt with  
GraphSubtypeRelations.  I believe that you don't need to override  
anything in GraphSubtypeRelations, but you can simply specify the  
relations in the regular manner.

To override the behavior of type arguments subtyping, you just need to  
override compareTypeArguments in TypesRelations (check out the code in  
IGJ, in IGJChecker).

> B. When I run
>
> leek:~/research/to-annotate/jolden> javac -cp ~/checkers/ 
> checkers.jar -sourcepath ~/checkers/jdk/javari/src -typeprocessor  
> checkers.javari.JavariChecker bh/*.java
>
> I obtain checker errors caused by incomplete jdk annotations, for  
> example:
> [...]
> among other errors I need to fix (such as allowing annotations on  
> static method receivers for javari, that will then apply only to  
> static local fields, since the other fields cannot be referred to  
> according to regular java syntax, and possibly manual annotation  
> errors).
>
> ~/checkers/jdk/javari/src/java/lang/Object.java, however, is  
> properly annotated. Unfortunately, the annotations on String.java  
> are not as complete as they should be (for instance, equals doesn't  
> have a @ReadOnly receiver annotation). The checker doesn't complain  
> about it since the jdk is not being type-checked, but the bh test of  
> jolden doesn't pass. What should be done about this?

We have not implemented skipClasses in the framework.  We should have  
done it, but we didn't :(.  Thanks for the reminder.
As a side note, I thought that you couldn't annotate Object.java in  
source, because the compiler JVM actually needing java.lang.Object and  
using a stub would break it?!

Thanks,
Mahmood