[Checkers] most recent Javari bug

[Telmo]

I also thought it would be a JDK problem, but Map.java currently is:

package java.util;
import checkers.javari.quals.*;

public interface Map<K,V> {
     int size() @ReadOnly;
     boolean isEmpty() @ReadOnly;
     boolean containsKey(@ReadOnly Object key);
     boolean containsValue(@ReadOnly Object value) @ReadOnly;
     V get(@ReadOnly Object key) @ReadOnly;
     V put(K key, V value);
     V remove(@ReadOnly Object key);
     void putAll(@ReadOnly Map<? extends K, ? extends V> m);
     void clear();
     @PolyRead Set<K> keySet() @PolyRead;
     @PolyRead Collection<V> values() @PolyRead;
     @PolyRead Set<@PolyRead Map.Entry<K, V>> entrySet() @PolyRead;
     interface Entry<K,V> {
         K getKey() @ReadOnly;
         V getValue() @ReadOnly;
         V setValue(V value);
         boolean equals(@ReadOnly Object o) @ReadOnly;
         int hashCode() @ReadOnly;
     }

     boolean equals(@ReadOnly Object o) @ReadOnly;
     int hashCode() @ReadOnly;
}

... and the get method has the parameter annotated properly.

-Telmo


On Mon, 11 Aug 2008, Mahmood Ali wrote:

> Hi Telmo,
>
> I spent some time debugging this problem a bit.
>
> In the case of:
> static <T> void (Map<T, T> map, T key) {
>   map.get(key); // currently issue a false positive
> }
>
> The problem is that the parameter is Object.  key's type T defaults  (T 
> extends @ReadOnly Object), while maps.get parameter is defaults to '@Mutable 
> Object'.  Hence the false positive.
>
> Personally, I think that the best solution for you is annotate any *use* of 
> Object as ReadOnly by default.  No reference of type 'Object' can be used to 
> mutate that object (unless cast is used, or a subclass violates subclass 
> rules).
>
> Needless to say, this false positive is eliminated by using the Javari 
> annotated JDK.  However, Javari's promise of validity of any un-annotated 
> code would be not deliverable.
>
> Regards,
> Mahmood
>
> On Aug 10, 2008, at 5:19 AM, Telmo wrote:
>
>> Hello.
>> 
>> I spent the night tracking the bug from the most recent test you committed. 
>> A @Mutable annotation is being added to the type of the parameter for the 
>> method get, in map. The problem seems to happen because the method is 
>> obtained via element, and the mutable annotation is added on the following 
>> method in JavariAnnotatedTypeFactory:
>>
>>   @Override
>>   protected void annotateImplicit(Element element, /*\@Mutable*/ 
>> AnnotatedTypeMirror type) {
>>       if (element.getKind().isClass() || element.getKind().isInterface()) {
>>           if (!hasImmutabilityAnnotation(type))
>>               type.addAnnotation(MUTABLE);
>>       }
>>       typePost.visit(type);
>>   }
>> 
>> If this method did not override the super method, where would the @ReadOnly 
>> annotation from the JDK be received? Just removing the method causes an 
>> assertion error, and I will probably be more productive if I have a better 
>> idea of where to look.
>> 
>> (That said, I am not sure I will be able to fix this for the next release.)
>> 
>> -Telmo
>