Package org.checkerframework.checker.index.samelen

Class SameLenAnnotatedTypeFactory

java.lang.Object
org.checkerframework.framework.type.AnnotatedTypeFactory
org.checkerframework.framework.type.GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
org.checkerframework.checker.index.samelen.SameLenAnnotatedTypeFactory
All Implemented Interfaces:
AnnotationProvider
public class SameLenAnnotatedTypeFactory extends BaseAnnotatedTypeFactory
The SameLen Checker is used to determine whether there are multiple fixed-length sequences (such as arrays or strings) in a program that share the same length. It is part of the Index Checker, and is used as a subchecker by the Index Checker's components.

This type factory adds extra expressions to @SameLen annotations when necessary. For example, if the full version of the type @SameLen({"a","b"}) should include "a", "b", and whatever is in the @SameLen types for "a" and for "b".

Also, every sequence s should have type @SameLen("s"). However, sometimes the sequence has no @SameLen annotation, and users may write the annotation without the variable itself, as in 

@SameLen("b") String a;
rather than the more pedantic 
@SameLen({"a", "b"}) String a;

Here are two specific examples where this annotated type factory refines types:

  • User-written SameLen: If a variable is declared with a user-written @SameLen annotation, then the type of the new variable is the union of the user-written arrays in the annotation and the arrays listed in the SameLen types of each of those arrays.
  • New array: The type of an expression of the form new T[a.length] is the union of the SameLen type of a and the arrays listed in a's SameLen type.

  • Field Details

  • Constructor Details

    • SameLenAnnotatedTypeFactory

      public SameLenAnnotatedTypeFactory(BaseTypeChecker checker)
      Create a new SameLenAnnotatedTypeFactory.

  • Method Details

    • createSupportedTypeQualifiers

      protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers()
      Description copied from class: AnnotatedTypeFactory
      Returns a mutable set of annotation classes that are supported by a checker.

      Subclasses may override this method to return a mutable set of their supported type qualifiers through one of the 5 approaches shown below.

      Subclasses should not call this method; they should call AnnotatedTypeFactory.getSupportedTypeQualifiers() instead.

      By default, a checker supports all annotations located in a subdirectory called qual that's located in the same directory as the checker. Note that only annotations defined with the @Target({ElementType.TYPE_USE}) meta-annotation (and optionally with the additional value of ElementType.TYPE_PARAMETER, but no other ElementType values) are automatically considered as supported annotations.

      To support a different set of annotations than those in the qual subdirectory, or that have other ElementType values, see examples below.

      In total, there are 5 ways to indicate annotations that are supported by a checker:

      1. Only support annotations located in a checker's qual directory:

        This is the default behavior. Simply place those annotations within the qual directory.

      2. Support annotations located in a checker's qual directory and a list of other annotations:

        Place those annotations within the qual directory, and override AnnotatedTypeFactory.createSupportedTypeQualifiers() by calling AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) with a varargs parameter list of the other annotations. Code example: 

         @Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
      return getBundledTypeQualifiers(Regex.class, PartialRegex.class, RegexBottom.class, UnknownRegex.class);
  }
      3. Supporting only annotations that are explicitly listed: Override AnnotatedTypeFactory.createSupportedTypeQualifiers() and return a mutable set of the supported annotations. Code example: 
         @Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
      return new HashSet<Class<? extends Annotation>>(
              Arrays.asList(A.class, B.class));
  }
        The set of qualifiers returned by AnnotatedTypeFactory.createSupportedTypeQualifiers() must be a fresh, mutable set. The methods AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) must return a fresh, mutable set
      Overrides:
      createSupportedTypeQualifiers in class AnnotatedTypeFactory
      Returns:
      the type qualifiers supported this processor, or an empty set if none

    • createQualifierHierarchy

      protected QualifierHierarchy createQualifierHierarchy()
      Description copied from class: AnnotatedTypeFactory
      Returns the QualifierHierarchy to be used by this checker.

      The implementation builds the type qualifier hierarchy for the AnnotatedTypeFactory.getSupportedTypeQualifiers() using the meta-annotations found in them. The current implementation returns an instance of NoElementQualifierHierarchy.

      Subclasses must override this method if their qualifiers have elements; the method must return an implementation of QualifierHierarchy, such as ElementQualifierHierarchy.

      Overrides:
      createQualifierHierarchy in class AnnotatedTypeFactory
      Returns:
      a QualifierHierarchy for this type system

    • getAnnotatedTypeLhs

      public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree tree)
      Description copied from class: GenericAnnotatedTypeFactory
      Returns the type of a left-hand side of an assignment.

      The default implementation returns the type without considering dataflow type refinement. Subclass can override this method and add additional logic for computing the type of a LHS.

      Overrides:
      getAnnotatedTypeLhs in class GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
      Parameters:
      tree - left-hand side of an assignment
      Returns:
      AnnotatedTypeMirror of lhsTree

    • mayAppearInSameLen

      public static boolean mayAppearInSameLen(JavaExpression expr)
      Returns true if the given expression may appear in a @SameLen annotation.

    • createTreeAnnotator

      public TreeAnnotator createTreeAnnotator()
      Description copied from class: GenericAnnotatedTypeFactory
      Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.

      The default tree annotator is a ListTreeAnnotator of the following:

      1. PropagationTreeAnnotator: Propagates annotations from subtrees
      2. LiteralTreeAnnotator: Adds annotations based on QualifierForLiterals meta-annotations
      3. DependentTypesTreeAnnotator: Adapts dependent annotations based on context

      Subclasses may override this method to specify additional tree annotators, for example: 

       new ListTreeAnnotator(super.createTreeAnnotator(), new KeyLookupTreeAnnotator(this));
      Overrides:
      createTreeAnnotator in class GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis>
      Returns:
      a tree annotator

    • getSameLensFromString

      public List<String> getSameLensFromString(String sequenceExpression, Tree tree, TreePath currentPath)
      Find all the sequences that are members of the SameLen annotation associated with the sequence named in sequenceExpression along the current path.

    • createSameLen

      public AnnotationMirror createSameLen(Collection<String> exprs)
      Creates a @SameLen annotation whose values are the given strings.
      Parameters:
      exprs - the values for the @SameLen annotation. This must be an ordered collection such as a list or TreeSet in which the strings are in alphabetical order.
      Returns:
      a @SameLen annotation whose values are the given strings

    • createCombinedSameLen

      public AnnotationMirror createCombinedSameLen(List<JavaExpression> exprs, List<AnnotationMirror> annos)
      Generates a SameLen that includes each expression, as well as everything in the annotations2, if they are SameLen annotations.
      Parameters:
      exprs - a list of expressions representing arrays to be included in the combined annotation
      annos - a list of annotations
      Returns:
      a combined SameLen annotation