[Checkers] Dealing with @I/@OI etc

Mahmood Ali mahmood at MIT.EDU
Sat Feb 21 00:59:51 EST 2009

Greetings Alex,

I am sorry that I didn't reply to your email early.  I am not quite  
sure what the story is with regards to @PrivateI or @OI, I will try to  
look into this maybe later this week.

IGJ story (within IGJAnnotatedTypeFactory):
The guiding principle for the framework is that the  
AnnotatedTypeFactory (or its subtypes) is responsible for determining  
the annotated type of any tree.  The visitor (e.g. BaseTypeVisitor)  
can simply lookup the type of a tree by supplying the tree itself.   
Thus, the visitor doesn't need to deal with polymorphism complexities.

There two classes that are involved with the resolution of annotated  
1. ImmutabilityTemplateCollector
    Given a list of some types (e.g. List<@Mutable String>) [first  
parameter] and the actual declared type with the polymorphic qualifier  
(e.g. List<@I String>) [second parameter],  
ImmutabilityTemplateCollector finds what each @I in the expected type  
corresponds to in the actual type and returns the least upper bound  
for the multiple possible corresponding types if exited.  This is the  
jest of it, but it is slightly more complicated.
P.S. the parameter names should be renamed!

2. ImmutabilityResolver
    Given a type and a mapping of @I value string to corresponding  
annotations, the class substitutes each instance of @I in a type with  
the corresponding resolved annotation.

As you probably see in the code, there are three cases where @I is  
1. Method Invocation (in methodFromUse): The method collects the  
mappings of @I's to their resolved types based on the arguments passed  
and the receiver/call-site of the method invocation.
2. type supertype finding (in postDirectSupertypes): Given the  
mutability of a class, the method resolves the @I in the supertype.
3. Member select/dereference (in AnnotatedTypes.asMemberOf): In an  
explicit dereference (e.g. foo.b) or an implicit dereference of this,  
the @I in the accessed field type is resolved based on the  
dereferenced expression type.

The example you provided below falls under the third case and is  
handled properly by IGJ.  I don't know what's going on in IOGJ.  I am  


On Feb 16, 2009, at 10:58 PM, Alex Potanin wrote:

> Hi Mahmood,
> I wonder if you can please explain to me how exactly is @I/@OI is  
> replaced? There is ImmutabilityTemplateCollector that I expect to  
> pick up in its visitDeclared method all the occurences of types that  
> are *declared* with @I/@OI declaration, right? This doesn't seem to  
> pick up all the ones with @PrivateI - I only get 2 if I print it out  
> using the example I sent before. Every time it picks it up, it then  
> uses the "type" to see what @I/@OI should be instantiated as - why?  
> For example, in the code like:
> import checkers.oigj.quals.*;
> @OI class Bar {}
> @OI class Foo {
>    @OI Bar b;
>    public static void doIt() {
> 	(new @Mutable Foo()).b = new @Mutable Bar();
>    }
> }
> I would expect any use of (new @Mutable Foo()).b to infer that b has  
> @Mutable Bar type and not @I Bar type. But is the above enough to  
> detect this? How does type and actualType relate to the kind of  
> check performed above? Or is that picked up in a different place in  
> the AnnotatedTypeFactory? :-)
> I know this is rather confusing, but I am trying my best to put it  
> in writing. :-)
> Thanks for your help!
> Cheers,
> Alex.

More information about the checkers mailing list