Class AccumulationAnnotatedTypeFactory

    • Field Detail

      • accumulationChecker

        public final AccumulationChecker accumulationChecker
        The typechecker associated with this factory.
      • top

        public final javax.lang.model.element.AnnotationMirror top
        The canonical top annotation for this accumulation checker: an instance of the accumulator annotation with no arguments.
      • bottom

        public final javax.lang.model.element.AnnotationMirror bottom
        The canonical bottom annotation for this accumulation checker.
    • Constructor Detail

      • AccumulationAnnotatedTypeFactory

        protected AccumulationAnnotatedTypeFactory​(BaseTypeChecker checker,
                                                   java.lang.Class<? extends java.lang.annotation.Annotation> accumulator,
                                                   java.lang.Class<? extends java.lang.annotation.Annotation> bottom,
                                                   @Nullable java.lang.Class<? extends java.lang.annotation.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,
                                                   java.lang.Class<? extends java.lang.annotation.Annotation> accumulator,
                                                   java.lang.Class<? extends java.lang.annotation.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 Detail

      • createAccumulatorAnnotation

        public javax.lang.model.element.AnnotationMirror createAccumulatorAnnotation​(java.util.List<java.lang.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 javax.lang.model.element.AnnotationMirror createAccumulatorAnnotation​(java.lang.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​(com.sun.source.tree.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​(javax.lang.model.element.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
      • getAccumulatedValues

        public java.util.List<java.lang.String> getAccumulatedValues​(javax.lang.model.element.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 java.util.Collection<java.lang.String> getAccumulatedValues​(com.sun.source.tree.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​(java.lang.String p,
                                             java.lang.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​(javax.lang.model.element.AnnotationMirror subAnno,
                                            java.lang.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​(java.util.List<java.lang.String> trueVariables,
                                            java.lang.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 javax.lang.model.element.AnnotationMirror createPredicateAnnotation​(java.lang.String p)
        Creates a new predicate annotation from the given string.
        Parameters:
        p - a valid predicate
        Returns:
        an annotation representing that predicate
      • convertToPredicate

        protected java.lang.String convertToPredicate​(javax.lang.model.element.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​(javax.lang.model.element.AnnotationMirror anno)
        Returns true if anno is a predicate annotation.
        Parameters:
        anno - an annotation
        Returns:
        true if anno is a predicate annotation