[Checkers] State-Type Prototype

[Mahmood Ali]

Greetings Daniel,

Please note that the provided implementation is by no means a  
reference implementation.  I realize that I should have documented it  
more.

__ Overall Usage __
Each Resource annotated type either is Opened or Closed.  Each  
resource is initialized to be closed, until a ChangeStatusTo-annotated  
method is invoked on such resource reference.  One approach is to  
utilize Flow to switch the resource qualified type throughout its scope.

__ Flow utilization __
Flow class provides a flow-sensitive analysis for qualifier  
inference.  The implementation uses Gen-Kill algorithm to infer  
qualifiers.  The default implementation in Flow handles qualifiers on  
local variables, parameters, and fields only; and by default only take  
analyzation and assignment into account.  One can extend Flow to  
customize special cases and only need to specify the generation part:  
specifying where a type gets a new qualifier.  Flow uses the new  
qualifier for the element in the scope till it gets re-assigned, out- 
of-scope, or some other special cases.

We can extend Flow to change the stateful qualifier based on method  
invocation.  The provided implementation is as follows, but with  
documentations and some re-ordering:

         @Override
         public Void visitMethodInvocation(MethodInvocationTree node,  
Void p) {
             // apply default method invocation before applying this one
             super.visitMethodInvocation(node, p);

             // Check if the invoked method is annotated with  
ChangeStatusTo or not
             ExecutableElement method = TreeUtils.elementFromUse(node);
             if (method.getAnnotation(ChangeStatusTo.class) == null)
                 return null;

             // Get the new status: the value of ChangeStatusTo
             // Look below to understand try/catch
             AnnotationUtils annoUtils = new AnnotationUtils(env);
             Name newStatusName = null;
             try { method.getAnnotation(ChangeStatusTo.class).value(); }
             catch (MirroredTypeException e) {
                 newStatusName =  
TypesUtils.getQualifiedName((DeclaredType)e.getTypeMirro
r());
             }
             AnnotationMirror newStatusAnno =  
annoUtils.fromName(newStatusName);

             // Get the element representing the call site
             // some java trees don't represent elements: new class  
expressions, ?: expressions
             // we cannot do much about 'new File().open()'
             Element site = getCallSite(node);
             if (site == null)
                 return null;

             // Check flow maintains support for the site element
             if (vars.contains(site)) {
                 int idx = vars.indexOf(site);
                 // clear the qualifiers on the site element and add  
the new status
                 for (AnnotationMirror possible: annotations)
                     annos.clear(possible, idx);
                 annos.set(newStatusAnno, idx);
             }
             return null;
         }


__ getSite implementation:
As I stated earlier, Flow would only support local variables,  
parameters, and local variable.  In this case, it simply calls  
AnnotatedTypeFactory.getReceiver() and see if the call site element is  
supported and return it if so.

This mainly excludes method elements analysis, so Flow does not do  
anything about:
   getFile().open();
   getFile().write(2);  // provided implementation would report a  
false positive here
   getFile().close();

I am not quite sure if Flow supports self elements or not, and the  
provided implementation has an incomplete empty if statement for it.

__ try/catch block related to Element.getAnnotation().value()
If an Annotation object is retrieved through Element.getAnnotation(),  
and annotation element is of type java.lang.Class, then any access to  
such element would cause a MirroredTypeException: http://java.sun.com/javase/6/docs/api/javax/lang/model/element/Element.html#getAnnotation(java.lang.Class) 
  .  The proper way for getting the value in this case is through  
MirroredTypeException.getTypeMirror() as was provided in the example.

__ limitation
This proposal needs substantial improvements: it does not provide  
aliasing analysis; and it does not allow changing the stateful type  
without direct method invocation on the resource.  For
instance, it cannot express that the following method changes the  
status of the parameter to Open
   static void open(File f) { f.open(); }
   {
       File f = new File();
       open(f);
       f.write(2); // false positive here
       ...
    }

Hope this helps,
Mahmood