checkers.javari
Class JavariAnnotatedTypeFactory

java.lang.Object
  extended by checkers.types.AnnotatedTypeFactory
      extended by checkers.javari.JavariAnnotatedTypeFactory

public class JavariAnnotatedTypeFactory
extends AnnotatedTypeFactory

Generates a AnnotatedTypeMirror with Javari annotations from a Tree or a Element parameter. Implicit annotations are added as follows: 1. Qualified class types without annotations receive the \@Mutable annotation. 2. Qualified executable types receivers without annotations are annotated with the qualified executable type owner's annotation. 3. Qualified declared types are annotated with their underlying type's element annotations. 4. Qualified types whose elements correspond to fields, and all its subtypes, are annotated with \@ReadOnly, \@Mutable or \@PolyRead), according to the qualified type of {@code this}.


Field Summary
 
Fields inherited from class checkers.types.AnnotatedTypeFactory
annoRelations, annotations, atypes, checker, elements, env, root, trees, types, visitorState
 
Constructor Summary
JavariAnnotatedTypeFactory(JavariChecker checker, CompilationUnitTree root)
          Creates a new JavariAnnotatedTypeFactory that operates on a particular AST.
 
Method Summary
protected  void annotateImplicit(Element element, AnnotatedTypeMirror type)
          Adds annotations to qualified types according to their provided element, as follows: Qualified class types without annotations corresponding to class or interface elements receive the \@Mutable annotation.
protected  void annotateImplicit(Tree tree, AnnotatedTypeMirror type)
          Adds implicit annotations to a qualified type, based on its tree, as follows: 1.
protected  void annotateInheritedFromClass(AnnotatedTypeMirror type)
          Does nothing.
 AnnotatedTypeMirror.AnnotatedDeclaredType getSelfType(Tree tree)
          Returns a type of the class and the field this.
 boolean hasImmutabilityAnnotation(AnnotatedTypeMirror type)
           
 AnnotatedTypeMirror.AnnotatedExecutableType methodFromUse(MethodInvocationTree tree)
          Determines the type of the invoked method based on the passed method invocation tree.
 void postAsMemberOf(AnnotatedTypeMirror type, AnnotatedTypeMirror owner, Element element)
          We modify this callback method to replace @ThisMutable implicit annotations with the qualified supertype annotation, if the owner doesn't have a @ReadOnly annotation; otherwise one could violate the typesystem as follows: \@PolyRead Object breakJavari(\@PolyRead Object s) \@ReadOnly { tmObject = s; return null; } If ThisMutable tmObject were resolved as \@ReadOnly tmObject, the code above would be legal.
 Collection<AnnotationMirror> unify(Collection<AnnotationMirror> c1, Collection<AnnotationMirror> c2)
          Returns a singleton collection with the most restrictive immutability annotation that is a supertype of the annotations on both collections.
 
Methods inherited from class checkers.types.AnnotatedTypeFactory
constructorFromUse, createLRUCache, declarationFromElement, fromClass, fromElement, fromElement, fromElement, fromExpression, fromMember, fromTypeTree, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFromTypeTree, getBoxedType, getCurrentClassType, getCurrentMethodReceiver, getCurrentRoot, getPath, getReceiver, getUnboxedType, getVisitorState, postDirectSuperTypes, type
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

JavariAnnotatedTypeFactory

public JavariAnnotatedTypeFactory(JavariChecker checker,
                                  CompilationUnitTree root)
Creates a new JavariAnnotatedTypeFactory that operates on a particular AST.

Parameters:
checker - the checker to which this factory belongs
root - the AST on which this type factory operates
Method Detail

hasImmutabilityAnnotation

public boolean hasImmutabilityAnnotation(AnnotatedTypeMirror type)
Parameters:
type - an annotated type mirror
Returns:
true iff the type is specified an immutability type other than this-mutable, false otherwise

annotateImplicit

protected void annotateImplicit(Tree tree,
                                AnnotatedTypeMirror type)
Adds implicit annotations to a qualified type, based on its tree, as follows: 1. Resolves qualified types from MemberSelectTree, inheritting from the expression to the identifier if the identifier is @ThisMutable. 2. Qualified class types without annotations receive the \@Mutable annotation. 3. Qualified executable types receivers without annotations are annotated with the qualified executable type owner's annotation. 4. Qualified declared types are annotated with their underlying type's element annotations. 5. Qualified types whose elements correspond to fields, and all its subtypes, are annotated with \@ReadOnly, \@Mutable or \@PolyRead), according to the qualified type of {@code this}.

Overrides:
annotateImplicit in class AnnotatedTypeFactory
Parameters:
tree - an AST node
type - the type obtained from tree

annotateImplicit

protected void annotateImplicit(Element element,
                                AnnotatedTypeMirror type)
Adds annotations to qualified types according to their provided element, as follows:

Overrides:
annotateImplicit in class AnnotatedTypeFactory
Parameters:
element - an element
type - the type obtained from elt

annotateInheritedFromClass

protected void annotateInheritedFromClass(AnnotatedTypeMirror type)
Does nothing. Don't use the framework to inherit annotations from classes; Javari behavior about inherittng annotations is ad hoc enough, so we instead implement it all on this class, and override this method with an empty method to remove the framework behavior.

Overrides:
annotateInheritedFromClass in class AnnotatedTypeFactory
Parameters:
type - the type for which class annotations will be inherited if there are no annotations already present

getSelfType

public AnnotatedTypeMirror.AnnotatedDeclaredType getSelfType(Tree tree)
Returns a type of the class and the field this. On Javari, this means to retrieve the annotations present at the method receiver, if any, applied to the qualified type of the enclosing class.

Overrides:
getSelfType in class AnnotatedTypeFactory

unify

public Collection<AnnotationMirror> unify(Collection<AnnotationMirror> c1,
                                          Collection<AnnotationMirror> c2)
Returns a singleton collection with the most restrictive immutability annotation that is a supertype of the annotations on both collections.

Overrides:
unify in class AnnotatedTypeFactory
Parameters:
c1 - type qualifiers for the first type
c2 - tyep qualifiers for the second type
Returns:
the least restrictive qualifiers for both types

methodFromUse

public AnnotatedTypeMirror.AnnotatedExecutableType methodFromUse(MethodInvocationTree tree)
Determines the type of the invoked method based on the passed method invocation tree. Invokes the super method, then resolves annotations \@PolyRead at the raw level on return values by looking at the mutability of any parameters marked as \@PolyRead. For this purpose, a \@PolyRead annotation on the receiver counts as if this were being passed as an argument to a parameter marked as \@PolyRead.

Overrides:
methodFromUse in class AnnotatedTypeFactory
Parameters:
tree - the method invocation tree
Returns:
AnnotatedExecutableType with return value resolved as described.

postAsMemberOf

public void postAsMemberOf(AnnotatedTypeMirror type,
                           AnnotatedTypeMirror owner,
                           Element element)
We modify this callback method to replace @ThisMutable implicit annotations with the qualified supertype annotation, if the owner doesn't have a @ReadOnly annotation; otherwise one could violate the typesystem as follows: \@PolyRead Object breakJavari(\@PolyRead Object s) \@ReadOnly { tmObject = s; return null; } If ThisMutable tmObject were resolved as \@ReadOnly tmObject, the code above would be legal. One could then create such a class, invoke this method, and obtain \@Mutable access to tmObject from a \@ReadOnly reference to it, without errors.

Overrides:
postAsMemberOf in class AnnotatedTypeFactory
Parameters:
type - the annotated type of the element
owner - the annotated type of the receiver of the accessing tree
element - the element of the field or method