[Checkers] Daikon Output

Telmo telmo at MIT.EDU
Mon Aug 18 12:03:35 EDT 2008


This idea improves usability, so it is good.

It also goes against the idea of an expanded type hierarchy, with 
@ReadOnly Object at the top, for the convenience of using the checker 
with types not properly specified.

I probably should look at how often the intended upper bound is @Mutable 
Object and how often it is @ReadOnly Object, but I'd guess that  @Mutable 
Object is more common.

I am ok with making this change if modifying the type hierarchy 
conventions is not an issue.

-Telmo


On Mon, 18 Aug 2008, Mahmood Ali wrote:

> 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



More information about the checkers mailing list