Package org.checkerframework.common.accumulation

Class AccumulationAnnotatedTypeFactory

java.lang.Object
org.checkerframework.framework.type.AnnotatedTypeFactory
org.checkerframework.framework.type.GenericAnnotatedTypeFactory<AccumulationValue,AccumulationStore,AccumulationTransfer,AccumulationAnalysis>
org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory
All Implemented Interfaces:
AnnotationProvider
Direct Known Subclasses:
CalledMethodsAnnotatedTypeFactory, InitializedFieldsAnnotatedTypeFactory
public abstract class AccumulationAnnotatedTypeFactory extends GenericAnnotatedTypeFactory<AccumulationValue,AccumulationStore,AccumulationTransfer,AccumulationAnalysis>
An annotated type factory for an accumulation checker.

New accumulation checkers should extend this class and implement a constructor, which should take a BaseTypeChecker and call both the constructor defined in this class and GenericAnnotatedTypeFactory.postInit().

  • Field Details

    • accumulationChecker

      public final AccumulationChecker accumulationChecker
      The typechecker associated with this factory.

    • top

      public final AnnotationMirror top
      The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments.

    • bottom

      public final AnnotationMirror bottom
      The canonical bottom annotation for this accumulation checker.

  • Constructor Details

    • AccumulationAnnotatedTypeFactory

      protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom, @Nullable Class<? extends Annotation> predicate)
      Create an annotated type factory for an accumulation checker.
      Parameters:
      checker - the checker
      accumulator - the accumulator type in the hierarchy. Must be an annotation with a single argument named "value" whose type is a String array.
      bottom - the bottom type in the hierarchy, which must be a subtype of accumulator. The bottom type should be an annotation with no arguments.
      predicate - the predicate annotation. Either null (if predicates are not supported), or an annotation with a single element named "value" whose type is a String.

    • AccumulationAnnotatedTypeFactory

      protected AccumulationAnnotatedTypeFactory(BaseTypeChecker checker, Class<? extends Annotation> accumulator, Class<? extends Annotation> bottom)
      Create an annotated type factory for an accumulation checker.
      Parameters:
      checker - the checker
      accumulator - the accumulator type in the hierarchy. Must be an annotation with a single argument named "value" whose type is a String array.
      bottom - the bottom type in the hierarchy, which must be a subtype of accumulator. The bottom type should be an annotation with no arguments.

  • Method Details

    • createAccumulatorAnnotation

      public AnnotationMirror createAccumulatorAnnotation(List<String> values)
      Creates a new instance of the accumulator annotation that contains the elements of values.
      Parameters:
      values - the arguments to the annotation. The values can contain duplicates and can be in any order.
      Returns:
      an annotation mirror representing the accumulator annotation with values's arguments; this is top if values is empty

    • createAccumulatorAnnotation

      public AnnotationMirror createAccumulatorAnnotation(String value)
      Creates a new instance of the accumulator annotation that contains exactly one value.
      Parameters:
      value - the argument to the annotation
      Returns:
      an annotation mirror representing the accumulator annotation with value as its argument

    • returnsThis

      public boolean returnsThis(MethodInvocationTree tree)
      Returns true if the return type of the given method invocation tree has an @This annotation from the Returns Receiver Checker.
      Parameters:
      tree - a method invocation tree
      Returns:
      true if the method being invoked returns its receiver

    • isAccumulatorAnnotation

      public boolean isAccumulatorAnnotation(AnnotationMirror anm)
      Is the given annotation an accumulator annotation? Returns false if the argument is bottom.
      Parameters:
      anm - an annotation mirror
      Returns:
      true if the annotation mirror is an instance of this factory's accumulator annotation

    • createTreeAnnotator

      protected 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<AccumulationValue,AccumulationStore,AccumulationTransfer,AccumulationAnalysis>
      Returns:
      a tree annotator

    • 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

    • getAccumulatedValues

      public List<String> getAccumulatedValues(AnnotationMirror anno)
      Returns all the values that anno has accumulated.
      Parameters:
      anno - an accumulator annotation; must not be bottom
      Returns:
      the list of values the annotation has accumulated; it is a new list, so it is safe for clients to side-effect

    • getAccumulatedValues

      public Collection<String> getAccumulatedValues(Tree tree)
      Returns the accumulated values on the given (expression, usually) tree. This differs from calling AnnotatedTypeFactory.getAnnotatedType(Tree), because this version takes into account accumulated methods that are stored on the value. This is useful when dealing with accumulated facts on variables whose types are type variables (because type variable types cannot be refined directly, due to the quirks of subtyping between type variables and its interactions with the qualified type system).

      The returned collection may be either a list or a set.

      Parameters:
      tree - a tree
      Returns:
      the accumulated values for the given tree, including those stored on the value

    • isPredicateSubtype

      protected boolean isPredicateSubtype(String p, String q)
      Extension point for subtyping behavior between predicates. This implementation conservatively returns true only if the predicates are equal, or if the prospective supertype (q) is equivalent to top (that is, the empty string).
      Parameters:
      p - a predicate
      q - another predicate
      Returns:
      true if p is a subtype of q

    • evaluatePredicate

      protected boolean evaluatePredicate(AnnotationMirror subAnno, String pred)
      Evaluates whether the accumulator annotation subAnno makes the predicate pred true.
      Parameters:
      subAnno - an accumulator annotation
      pred - a predicate
      Returns:
      whether the accumulator annotation satisfies the predicate

    • evaluatePredicate

      protected boolean evaluatePredicate(List<String> trueVariables, String pred)
      Evaluates whether treating the variables in trueVariables as true literals (and all other names as false literals) makes the predicate pred evaluate to true.
      Parameters:
      trueVariables - a list of names that should be replaced with true
      pred - a predicate
      Returns:
      whether the true variables satisfy the predicate

    • createPredicateAnnotation

      protected AnnotationMirror createPredicateAnnotation(String p)
      Creates a new predicate annotation from the given string.
      Parameters:
      p - a valid predicate
      Returns:
      an annotation representing that predicate

    • convertToPredicate

      protected String convertToPredicate(AnnotationMirror anno)
      Converts the given annotation mirror to a predicate.
      Parameters:
      anno - an annotation
      Returns:
      the predicate, as a String, that is equivalent to that annotation. May return the empty string.

    • isPredicate

      protected boolean isPredicate(AnnotationMirror anno)
      Returns true if anno is a predicate annotation.
      Parameters:
      anno - an annotation
      Returns:
      true if anno is a predicate annotation