[Checkers] Daikon Output

[Mahmood Ali]

Greetings,

I have just typed-check daikon with the javari type-checker and got  
118 false positives.

It seems to me that all of them are due to the bounds of type  
variables in a way or another.  The problem is that currently Javari  
sets the upperbound for a wildcard or a type parameter to @ReadOnly  
Object (or whatever the specified upper bound is).  This creates a  
problem, since the values of the container would be treated as  
readonly and thus cannot pass the value to something else.

Consider the following case:
   List<?> lst = null;   // Javari treats it like Constructor<?  
extends @ReadOnly Object>
   Object o = lst.get(0); // .get() would return '? extends @ReadOnly  
Object' not necessary @Mutable Object.
Thus, the checker would emit an error for the second line, as it is an  
assignment from @ReadOnly Object to @Mutable Object.

There was some cases where an array of a type parameter was marked as  
readonly instead of mutable.  I haven't investigated the problem  
further.

I think that the proper fix is to treat the upperbound of a type  
parameter (within a declaration) differently from a type argument  
(within a use).  The upper-bound of a type parameter within a generic  
class or method declaration should be @ReadOnly, however when  
initiating that class or invoking the generic method the type argument  
is assumed to be a subtype of @Mutable unless the user specified  
otherwise.  Consider the following cases:

class List<E> { ... }  // Javari assumes it to be 'class List<E  
extends @ReadOnly Object> { ... }'

1. List<Object> o1;   // List<@Mutable Object>
2. List<?> o2;    // List<? extends @Mutable Object>
3. List o3;         // raw type which is treated like List<? extends  
@Mutable Object>
4. List<@ReadOnly Object> o4; // List<@ReadOnly Object>

Currently, we treat these similarly.  So it's either that type 4 would  
be an invalid type (if E in List<E> is E extends @Mutable Object) or  
that any usage of o2 and o3 would cause a false positive (when we  
assign o2.get(0) to Object).

I think that the separation makes sense, and it is a better way than  
the way I solved in IGJ.  Thoughts?

Regards,
Mahmood
-------------- next part --------------
A non-text attachment was scrubbed...
Name: daikon-javari-output
Type: application/octet-stream
Size: 25778 bytes
Desc: not available
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20080818/5597193d/attachment-0001.obj 
-------------- next part --------------