[Checkers] Questions about javari checker issues

[Mahmood Ali]

Hi Telmo again,

I made some simplified my previous answer.  So you can ignore the  
previous email and follow this one.

> 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?
You can apply the diff I sent you awhile ago to utilize TypesRelations  
and AnnotationRelations.  To handle QReadOnly, you can simply override  
TypesRelations.compareTypeArg():
    typesRelations = new TypesRelations(factory, env, annoRelations) {
       @Override
       protected boolean compareTypeArg(AnnotatedTypeMirror lhs,  
AnnotatedTypeMirror rhs) {
           return lhs.hasAnnotation(QREADONLY) ||  
super.compareTypeArg(lhs, rhs);
       }
    };


>
> 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:
>
I have finally implemented skipClasses.  You can supply - 
Dcheckers.skipClasses="^java\." as a java argument (you might need to  
modify the script itself).

P.S. I used regular expressions to adhere to the manual specification,  
but I think that using regexp is cumbersome.

> 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).
>
I think that the checker framework prevents you from annotating static  
method receivers, as they do not actually have receivers (i.e. cannot  
reference 'this' in them).  We might need to change the framework to  
support this.

> ~/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?
When I was annotating the JDK, I found it very helpful to type check  
the jdk stubs with the checker.  It informed of many missing  
annotations (because of the override relationship check).

Regards,
Mahmood