Package org.checkerframework.framework.type

Class GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends CFAbstractStore<Value,Store>,TransferFunction extends CFAbstractTransfer<Value,Store,TransferFunction>,FlowAnalysis extends CFAbstractAnalysis<Value,Store,TransferFunction>>

java.lang.Object
org.checkerframework.framework.type.AnnotatedTypeFactory
org.checkerframework.framework.type.GenericAnnotatedTypeFactory<Value,Store,TransferFunction,FlowAnalysis>
All Implemented Interfaces:
AnnotationProvider
Direct Known Subclasses:
AccumulationAnnotatedTypeFactory, BaseAnnotatedTypeFactory, InitializationAnnotatedTypeFactory, KeyForAnnotatedTypeFactory, LockAnnotatedTypeFactory
public abstract class GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends CFAbstractStore<Value,Store>,TransferFunction extends CFAbstractTransfer<Value,Store,TransferFunction>,FlowAnalysis extends CFAbstractAnalysis<Value,Store,TransferFunction>> extends AnnotatedTypeFactory
A factory that extends AnnotatedTypeFactory to optionally use flow-sensitive qualifier inference.

It also adds other features: qualifier polymorphism, default annotations via DefaultFor, user-specified defaults via DefaultQualifier, standardization via DependentTypesHelper, etc. Those features, and addComputedTypeAnnotations(com.sun.source.tree.Tree, org.checkerframework.framework.type.AnnotatedTypeMirror) (other than the part related to flow-sensitivity), could and should be in the superclass AnnotatedTypeFactory; it is not clear why they are defined in this class.

  • Field Details

  • Constructor Details

    • GenericAnnotatedTypeFactory

      protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow)
      Creates a type factory. Its compilation unit is not yet set.
      Parameters:
      checker - the checker to which this type factory belongs
      useFlow - whether flow analysis should be performed

    • GenericAnnotatedTypeFactory

      protected GenericAnnotatedTypeFactory(BaseTypeChecker checker)
      Creates a type factory. Its compilation unit is not yet set.
      Parameters:
      checker - the checker to which this type factory belongs

  • Method Details

    • postInit

      protected void postInit(@UnderInitialization(GenericAnnotatedTypeFactory.class) GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends CFAbstractStore<Value,Store>,TransferFunction extends CFAbstractTransfer<Value,Store,TransferFunction>,FlowAnalysis extends CFAbstractAnalysis<Value,Store,TransferFunction>> this)
      Description copied from class: AnnotatedTypeFactory
      Actions that logically belong in the constructor, but need to run after the subclass constructor has completed. In particular, AnnotationFileElementTypes.parseStubFiles() may try to do type resolution with this AnnotatedTypeFactory.
      Overrides:
      postInit in class AnnotatedTypeFactory

    • preProcessClassTree

      public void preProcessClassTree(ClassTree classTree)
      Performs flow-sensitive type refinement on classTree if this type factory is configured to do so.
      Overrides:
      preProcessClassTree in class AnnotatedTypeFactory
      Parameters:
      classTree - tree on which to perform flow-sensitive type refinement

    • setRoot

      public void setRoot(@Nullable CompilationUnitTree root)
      Description copied from class: AnnotatedTypeFactory
      Set the CompilationUnitTree that should be used.
      Overrides:
      setRoot in class AnnotatedTypeFactory
      Parameters:
      root - the new compilation unit to use

    • getSupportedMonotonicTypeQualifiers

      public final Set<Class<? extends Annotation>> getSupportedMonotonicTypeQualifiers()
      Returns an immutable set of the monotonic type qualifiers supported by this checker.
      Returns:
      the monotonic type qualifiers supported this processor, or an empty set if none
      See Also:

    • createTreeAnnotator

      protected TreeAnnotator createTreeAnnotator()
      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));
      Returns:
      a tree annotator

    • createTypeAnnotator

      protected TypeAnnotator createTypeAnnotator()
      Returns a DefaultForTypeAnnotator that adds annotations to a type based on the content of the type itself.

      Subclass may override this method. The default type annotator is a ListTypeAnnotator of the following:

      1. IrrelevantTypeAnnotator: Adds top to types not listed in the @RelevantJavaTypes annotation on the checker.
      2. PropagationTypeAnnotator: Propagates annotation onto wildcards.
      Returns:
      a type annotator

    • annotationsForIrrelevantJavaType

      public AnnotationMirrorSet annotationsForIrrelevantJavaType(TypeMirror tm)
      Returns the annotations that should appear on the given irrelevant Java type. If the type is relevant, this method's behavior is undefined.
      Parameters:
      tm - an irrelevant Java type
      Returns:
      the annotations that should appear on the given irrelevant Java type

    • createDefaultForUseTypeAnnotator

      protected DefaultQualifierForUseTypeAnnotator createDefaultForUseTypeAnnotator()
      Creates an DefaultQualifierForUseTypeAnnotator.
      Returns:
      a new DefaultQualifierForUseTypeAnnotator

    • createDefaultForTypeAnnotator

      protected DefaultForTypeAnnotator createDefaultForTypeAnnotator()
      Creates an DefaultForTypeAnnotator.
      Returns:
      a new DefaultForTypeAnnotator

    • getDefaultForTypeAnnotator

      public DefaultForTypeAnnotator getDefaultForTypeAnnotator()
      Returns the DefaultForTypeAnnotator.
      Returns:
      the DefaultForTypeAnnotator

    • createFlowAnalysis

      protected FlowAnalysis createFlowAnalysis()
      Returns the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis.

      This implementation uses the checker naming convention to create the appropriate analysis. If no transfer function is found, it returns an instance of CFAnalysis.

      Subclasses have to override this method to create the appropriate analysis if they do not follow the checker naming convention.

      Returns:
      the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis

    • createFlowTransferFunction

      public TransferFunction createFlowTransferFunction(CFAbstractAnalysis<Value,Store,TransferFunction> analysis)
      Returns the appropriate transfer function that is used for the given org.checkerframework.dataflow analysis.

      This implementation uses the checker naming convention to create the appropriate transfer function. If no transfer function is found, it returns an instance of CFTransfer.

      Subclasses have to override this method to create the appropriate transfer function if they do not follow the checker naming convention.

      Parameters:
      analysis - a dataflow analysis
      Returns:
      a new transfer function

    • createDependentTypesHelper

      protected DependentTypesHelper createDependentTypesHelper()
      Creates a DependentTypesHelper and returns it. Use getDependentTypesHelper() to access the value.
      Returns:
      a new DependentTypesHelper

    • getDependentTypesHelper

      public DependentTypesHelper getDependentTypesHelper()
      Returns the DependentTypesHelper.
      Returns:
      the DependentTypesHelper

    • createContractsFromMethod

      protected ContractsFromMethod createContractsFromMethod()
      Creates an ContractsFromMethod and returns it.
      Returns:
      a new ContractsFromMethod

    • getContractsFromMethod

      public ContractsFromMethod getContractsFromMethod()
      Returns the helper for method pre- and postconditions.
      Returns:
      the helper for method pre- and postconditions

    • getExplicitNewClassClassTypeArgs

      protected List<AnnotatedTypeMirror> getExplicitNewClassClassTypeArgs(NewClassTree newClassTree)
      Description copied from class: AnnotatedTypeFactory
      Returns the partially-annotated explicit class type arguments of the new class tree. The AnnotatedTypeMirror only include the annotations explicitly written on the explict type arguments. (If newClass use a diamond operator, this method returns the empty list.) For example, when called with new MyClass<@HERE String>() this method would return a list containing @HERE String.
      Overrides:
      getExplicitNewClassClassTypeArgs in class AnnotatedTypeFactory
      Parameters:
      newClassTree - a new class tree
      Returns:
      the partially annotated AnnotatedTypeMirrors for the (explicit) class type arguments of the new class tree

    • getExplicitNewClassAnnos

      public AnnotationMirrorSet getExplicitNewClassAnnos(NewClassTree newClassTree)
      Description copied from class: AnnotatedTypeFactory
      Returns the annotations explicitly written on a NewClassTree.

      new @HERE Class()

      Overrides:
      getExplicitNewClassAnnos in class AnnotatedTypeFactory
      Parameters:
      newClassTree - a constructor invocation
      Returns:
      the annotations explicitly written on a NewClassTree

    • createAndInitQualifierDefaults

      protected final QualifierDefaults createAndInitQualifierDefaults()
      Create QualifierDefaults which handles checker specified defaults, and initialize the created QualifierDefaults. Subclasses should override addCheckedCodeDefaults(QualifierDefaults defs) to add more defaults or use different defaults.
      Returns:
      the QualifierDefaults object

    • createQualifierDefaults

      protected QualifierDefaults createQualifierDefaults()
      Create QualifierDefaults which handles checker specified defaults. Sub-classes override this method to provide a different QualifierDefault implementation.

    • getSortedQualifierNames

      protected final String getSortedQualifierNames()
      Creates and returns a string containing the number of qualifiers and the canonical class names of each qualifier that has been added to this checker's supported qualifier set. The names are alphabetically sorted.
      Returns:
      a string containing the number of qualifiers and canonical names of each qualifier

    • addCheckedCodeDefaults

      protected void addCheckedCodeDefaults(QualifierDefaults defs)
      Adds default qualifiers for type-checked code by reading DefaultFor and DefaultQualifierInHierarchy meta-annotations. Subclasses may override this method to add defaults that cannot be specified with a DefaultFor or DefaultQualifierInHierarchy meta-annotations.
      Parameters:
      defs - the QualifierDefault object to which defaults are added

    • addCheckedStandardDefaults

      protected void addCheckedStandardDefaults(QualifierDefaults defs)
      Adds the standard CLIMB defaults that do not conflict with previously added defaults.
      Parameters:
      defs - QualifierDefaults object to which defaults are added

    • addUncheckedStandardDefaults

      protected void addUncheckedStandardDefaults(QualifierDefaults defs)
      Adds standard unchecked defaults that do not conflict with previously added defaults.
      Parameters:
      defs - QualifierDefaults object to which defaults are added

    • checkForDefaultQualifierInHierarchy

      protected void checkForDefaultQualifierInHierarchy(QualifierDefaults defs)
      Check that a default qualifier (in at least one hierarchy) has been set and issue an error if not.
      Parameters:
      defs - QualifierDefaults object to which defaults are added

    • createQualifierPolymorphism

      protected QualifierPolymorphism createQualifierPolymorphism()
      Creates the QualifierPolymorphism instance which supports the QualifierPolymorphism mechanism.
      Returns:
      the QualifierPolymorphism instance to use

    • getQualifierPolymorphism

      public QualifierPolymorphism getQualifierPolymorphism()
      Gives the current QualifierPolymorphism instance which supports the QualifierPolymorphism mechanism.
      Returns:
      the QualifierPolymorphism instance to use

    • postDirectSuperTypes

      protected void postDirectSuperTypes(AnnotatedTypeMirror type, List<? extends AnnotatedTypeMirror> supertypes)
      Description copied from class: AnnotatedTypeFactory
      A callback method for the AnnotatedTypeFactory subtypes to customize directSupertypes(). Overriding methods should merely change the annotations on the supertypes, without adding or removing new types.

      The default provided implementation adds type annotations to supertypes. This allows the type and its supertypes to have the qualifiers.

      Overrides:
      postDirectSuperTypes in class AnnotatedTypeFactory
      Parameters:
      type - the type whose supertypes are desired
      supertypes - the supertypes as specified by the base AnnotatedTypeFactory

    • getAnnotationFromJavaExpressionString

      public @Nullable AnnotationMirror getAnnotationFromJavaExpressionString(String expression, Tree tree, TreePath path, Class<? extends Annotation> clazz) throws JavaExpressionParseUtil.JavaExpressionParseException
      Returns the primary annotation on expression if it were evaluated at path.
      Parameters:
      expression - a Java expression
      tree - current tree
      path - location at which expression is evaluated
      clazz - class of the annotation
      Returns:
      the annotation on expression or null if one does not exist
      Throws:
      JavaExpressionParseUtil.JavaExpressionParseException - thrown if the expression cannot be parsed

    • getAnnotationFromJavaExpression

      public @Nullable AnnotationMirror getAnnotationFromJavaExpression(JavaExpression expr, Tree tree, Class<? extends Annotation> clazz)
      Returns the primary annotation on an expression, at a particular location.
      Parameters:
      expr - the expression for which the annotation is returned
      tree - current tree
      clazz - the Class of the annotation
      Returns:
      the annotation on expression or null if one does not exist

    • getAnnotationsFromJavaExpression

      public @Nullable AnnotationMirrorSet getAnnotationsFromJavaExpression(JavaExpression expr, Tree tree)
      Returns the primary annotations on an expression, at a particular location.
      Parameters:
      expr - the expression for which the annotation is returned
      tree - current tree
      Returns:
      the annotation on expression or null if one does not exist

    • parseJavaExpressionString

      public JavaExpression parseJavaExpressionString(String expression, TreePath currentPath) throws JavaExpressionParseUtil.JavaExpressionParseException
      Produces the JavaExpression as if expression were written at currentPath.
      Parameters:
      expression - a Java expression
      currentPath - the current path
      Returns:
      the JavaExpression associated with expression on currentPath
      Throws:
      JavaExpressionParseUtil.JavaExpressionParseException - thrown if the expression cannot be parsed

    • getExpressionAndOffsetFromJavaExpressionString

      public org.plumelib.util.IPair<JavaExpression,String> getExpressionAndOffsetFromJavaExpressionString(String expression, TreePath currentPath) throws JavaExpressionParseUtil.JavaExpressionParseException
      Produces the JavaExpression and offset associated with an expression. For instance, "n+1" has no associated JavaExpression, but this method produces a pair of a JavaExpression (for "n") and an offset ("1").
      Parameters:
      expression - a Java expression, possibly with a constant offset
      currentPath - location at which expression is evaluated
      Returns:
      the JavaExpression and offset for the given expression
      Throws:
      JavaExpressionParseUtil.JavaExpressionParseException - thrown if the expression cannot be parsed

    • getAnnotationMirrorFromJavaExpressionString

      public @Nullable AnnotationMirror getAnnotationMirrorFromJavaExpressionString(String expression, Tree tree, TreePath currentPath) throws JavaExpressionParseUtil.JavaExpressionParseException
      Returns the annotation mirror from dataflow for expression.

      This will output a different annotation than getAnnotationFromJavaExpressionString(String, Tree, TreePath, Class), because if the specified annotation isn't found in the store, the type from the factory is used.

      Parameters:
      expression - a Java expression
      tree - the tree at the location to parse the expression
      currentPath - location at which expression is evaluated
      Returns:
      an AnnotationMirror representing the type in the store at the given location from this type factory's type system, or null if one is not available
      Throws:
      JavaExpressionParseUtil.JavaExpressionParseException - thrown if the expression cannot be parsed

    • isUnreachable

      public boolean isUnreachable(ExpressionTree exprTree)
      Returns true if the exprTree is unreachable. This is a conservative estimate and may return false even though the exprTree is unreachable.
      Parameters:
      exprTree - an expression tree
      Returns:
      true if the exprTree is unreachable

    • getRegularExitStore

      public @Nullable Store getRegularExitStore(Tree tree)
      Returns the regular exit store for a method or another code block (such as static initializers). Returns null if there is no such store. This can happen because the method cannot exit through the regular exit block, or it is abstract or in an interface.
      Parameters:
      tree - a MethodTree or other code block, such as a static initializer
      Returns:
      the regular exit store, or null

    • getExceptionalExitStore

      public @Nullable Store getExceptionalExitStore(Tree tree)
      Returns the exceptional exit store for a method or another code block (such as static initializers).
      Parameters:
      tree - a MethodTree or other code block, such as a static initializer
      Returns:
      the exceptional exit store, or null, if there is no such store

    • getReturnStatementStores

      public List<org.plumelib.util.IPair<ReturnNode,TransferResult<Value,Store>>> getReturnStatementStores(MethodTree methodTree)
      Returns a list of all return statements of method paired with their corresponding TransferResult. If method has no return statement, then the empty list is returned.
      Parameters:
      methodTree - method whose return statements should be returned
      Returns:
      a list of all return statements of method paired with their corresponding TransferResult or an empty list if method has no return statements

    • getStoreBefore

      public Store getStoreBefore(Tree tree)
      Returns the store immediately before a given Tree.
      Returns:
      the store immediately before a given Tree

    • getStoreBefore

      public Store getStoreBefore(Set<Node> nodes)
      Returns the store immediately before a given Set of Nodes.
      Returns:
      the store immediately before a given Set of Nodes

    • getStoreBefore

      public @Nullable Store getStoreBefore(Node node)
      Returns the store immediately before a given node.
      Parameters:
      node - a node whose pre-store to return
      Returns:
      the store immediately before node

    • getStoreAfter

      public @Nullable Store getStoreAfter(Tree tree)
      Returns the store immediately after a given tree.

      May return null; for example, after a return statement.

      Parameters:
      tree - the tree whose post-store to return
      Returns:
      the store immediately after a given tree

    • getStoreAfter

      public Store getStoreAfter(Set<Node> nodes)
      Returns the store immediately after a given set of nodes.
      Parameters:
      nodes - the nodes whose post-stores to LUB
      Returns:
      the LUB of the stores store immediately after nodes

    • getStoreAfter

      public Store getStoreAfter(Node node)
      Returns the store immediately after a given Node.
      Parameters:
      node - node after which the store is returned
      Returns:
      the store immediately after a given Node

    • getNodesForTree

      public @Nullable Set<Node> getNodesForTree(Tree tree)
      See AnalysisResult.getNodesForTree(Tree).
      Parameters:
      tree - a tree
      Returns:
      the Nodes for a given Tree
      See Also:

    • getFirstNodeOfKindForTree

      public <T extends Node> @Nullable T getFirstNodeOfKindForTree(Tree tree, Class<T> kind)
      Return the first Node for a given Tree that has class kind.

      You probably don't want to use this function: iterate over the result of getNodesForTree(Tree) yourself or ask for a conservative approximation of the store using getStoreBefore(Tree) or getStoreAfter(Tree). This method is for code that uses a Node in a rather unusual way. Callers should probably be rewritten to not use a Node at all.

      Type Parameters:
      T - the class of the node to return
      Parameters:
      tree - a tree in which to search for a node of class kind
      kind - the class of the node to return
      Returns:
      the first Node for a given Tree that has class kind
      See Also:

    • getFinalLocalValues

      public Map<VariableElement,Value> getFinalLocalValues()
      Returns the value of effectively final local variables.
      Returns:
      the value of effectively final local variables

    • performFlowAnalysis

      protected void performFlowAnalysis(ClassTree classTree)
      Perform a org.checkerframework.dataflow analysis over a single class tree and its nested classes.
      Parameters:
      classTree - the class to analyze

    • analyze

      protected void analyze(Queue<org.plumelib.util.IPair<ClassTree,Store>> classQueue, Queue<org.plumelib.util.IPair<LambdaExpressionTree,Store>> lambdaQueue, UnderlyingAST ast, List<CFAbstractAnalysis.FieldInitialValue<Value>> fieldValues, ClassTree currentClass, boolean isInitializationCode, boolean updateInitializationStore, boolean isStatic, @Nullable Store capturedStore)
      Analyze the AST ast and store the result. Additional operations that should be performed after analysis should be implemented in postAnalyze(ControlFlowGraph).
      Parameters:
      classQueue - the queue for encountered class trees and their initial stores
      lambdaQueue - the queue for encountered lambda expression trees and their initial stores
      ast - the AST to analyze
      fieldValues - the abstract values for all fields of the same class
      currentClass - the class we are currently looking at
      isInitializationCode - are we analyzing a (static/non-static) initializer block of a class
      updateInitializationStore - should the initialization store be updated
      isStatic - are we analyzing a static construct
      capturedStore - the input Store to use for captured variables, e.g. in a lambda
      See Also:

    • isIgnoredExceptionType

      public boolean isIgnoredExceptionType(TypeMirror typeMirror)
      Returns true if typeMirror is an exception type that should be ignored.
      Parameters:
      typeMirror - an exception type
      Returns:
      true if typeMirror is an exception type that should be ignored

    • postAnalyze

      protected void postAnalyze(ControlFlowGraph cfg)
      Perform any additional operations on a CFG. Called once per CFG, after the CFG has been analyzed by analyze(Queue, Queue, UnderlyingAST, List, ClassTree, boolean, boolean, boolean, CFAbstractStore). This method can be used to initialize additional state or to perform any analyses that are easier to perform on the CFG instead of the AST.
      Parameters:
      cfg - the CFG
      See Also:

    • handleCFGViz

      protected void handleCFGViz(ControlFlowGraph cfg)
      Handle the visualization of the CFG, if necessary.
      Parameters:
      cfg - the CFG

    • getAnnotatedTypeLhsNoTypeVarDefault

      public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree)
      Returns the type of the left-hand side of an assignment without applying local variable defaults to type variables.

      The type variables that are types of local variables are defaulted to top so that they can be refined by dataflow. When these types are used as context during type argument inference, this default is too conservative. So this method is used instead of getAnnotatedTypeLhs(Tree).

      InferenceFactory.assignedToVariable(AnnotatedTypeFactory, Tree) explains why a different type is used.

      Parameters:
      lhsTree - left-hand side of an assignment
      Returns:
      AnnotatedTypeMirror of lhsTree

    • getAnnotatedTypeLhs

      public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree)
      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.

      Parameters:
      lhsTree - left-hand side of an assignment
      Returns:
      AnnotatedTypeMirror of lhsTree

    • getAnnotatedTypeVarargsArray

      public @Nullable AnnotatedTypeMirror getAnnotatedTypeVarargsArray(Tree tree)
      Returns the type of a varargs array of a method invocation or a constructor invocation. Returns null only if private field useFlow is false.
      Parameters:
      tree - a method invocation or a constructor invocation
      Returns:
      AnnotatedTypeMirror of varargs array for a method or constructor invocation tree; returns null if private field useFlow is false

    • getAnnotatedTypeRhsUnaryAssign

      public AnnotatedTypeMirror getAnnotatedTypeRhsUnaryAssign(UnaryTree tree)
      Returns the type of v + 1 or v - 1 where v is the expression in the postfixed increment or decrement expression.
      Parameters:
      tree - a postfixed increment or decrement tree
      Returns:
      AnnotatedTypeMirror of a right-hand side of an assignment for unary operation

    • constructorFromUse

      protected AnnotatedTypeFactory.ParameterizedExecutableType constructorFromUse(NewClassTree tree, boolean inferTypeArgs)
      Description copied from class: AnnotatedTypeFactory
      The implementation of AnnotatedTypeFactory.constructorFromUse(NewClassTree) and AnnotatedTypeFactory.constructorFromUseWithoutTypeArgInference(NewClassTree).
      Overrides:
      constructorFromUse in class AnnotatedTypeFactory
      Parameters:
      tree - the constructor invocation tree
      inferTypeArgs - whether the type arguments should be inferred
      Returns:
      the annotated type of the invoked constructor (as an executable type) and the type arguments

    • constructorFromUsePreSubstitution

      protected void constructorFromUsePreSubstitution(NewClassTree tree, AnnotatedTypeMirror.AnnotatedExecutableType type, boolean resolvePolyQuals)
      Description copied from class: AnnotatedTypeFactory
      A callback method for the AnnotatedTypeFactory subtypes to customize the handling of the declared constructor type before type variable substitution.
      Overrides:
      constructorFromUsePreSubstitution in class AnnotatedTypeFactory
      Parameters:
      tree - a NewClassTree from constructorFromUse()
      type - declared method type before type variable substitution
      resolvePolyQuals - whether to resolve polymorphic qualifiers

    • getMethodReturnType

      public AnnotatedTypeMirror getMethodReturnType(MethodTree m)
      Description copied from class: AnnotatedTypeFactory
      Returns the return type of the method m.
      Overrides:
      getMethodReturnType in class AnnotatedTypeFactory
      Parameters:
      m - tree of a method declaration
      Returns:
      the return type of the method

    • addDefaultAnnotations

      public void addDefaultAnnotations(AnnotatedTypeMirror type)
      Description copied from class: AnnotatedTypeFactory
      Adds default annotations to type. This method should only be used in places where the correct annotations cannot be computed because of type argument of raw types. (See AnnotatedTypeMirror.AnnotatedWildcardType.isTypeArgOfRawType().)
      Overrides:
      addDefaultAnnotations in class AnnotatedTypeFactory
      Parameters:
      type - annotated type to which default annotations are added

    • addComputedTypeAnnotations

      protected final void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type)
      This method is final; override addComputedTypeAnnotations(Tree, AnnotatedTypeMirror, boolean) instead.

      Changes annotations on a type obtained from a Tree. By default, this method does nothing. GenericAnnotatedTypeFactory uses this method to implement defaulting and inference (flow-sensitive type refinement). Its subclasses usually override it only to customize default annotations.

      Subclasses that override this method should also override AnnotatedTypeFactory.addComputedTypeAnnotations(Element, AnnotatedTypeMirror).

      In classes that extend GenericAnnotatedTypeFactory, override addComputedTypeAnnotations(Tree, AnnotatedTypeMirror, boolean) instead of this method.

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

    • getDefaultAnnotations

      public AnnotatedTypeMirror getDefaultAnnotations(Tree tree, AnnotatedTypeMirror type)
      Removes all primary annotations on a copy of the type and calculates the default annotations that apply to the copied type, without type refinements.
      Parameters:
      tree - tree where the type is used
      type - type to determine the defaulted version for
      Returns:
      the annotated type mirror with default annotations

    • getDefaultAnnotationsForWarnRedundant

      public AnnotatedTypeMirror getDefaultAnnotationsForWarnRedundant(Tree tree, AnnotatedTypeMirror type)
      Like getDefaultAnnotations(Tree, AnnotatedTypeMirror).

      For use ONLY by the -AwarnRedundantAnnotations command-line option. May add fewer annotations than getDefaultAnnotations(Tree, AnnotatedTypeMirror).

      Parameters:
      tree - tree where the type is used
      type - type to determine the defaulted version for
      Returns:
      the annotated type mirror with default annotations

    • addComputedTypeAnnotations

      protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow)
      Like addComputedTypeAnnotations(Tree, AnnotatedTypeMirror). Overriding implementations typically simply pass the boolean to calls to super.
      Parameters:
      tree - an AST node
      type - the type obtained from tree
      iUseFlow - whether to use information from dataflow analysis

    • addComputedTypeAnnotationsForWarnRedundant

      protected void addComputedTypeAnnotationsForWarnRedundant(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow)
      Like addComputedTypeAnnotations(Tree, AnnotatedTypeMirror, boolean).

      For use ONLY by the -AwarnRedundantAnnotations command-line option. May add fewer annotations than addComputedTypeAnnotations(Tree, AnnotatedTypeMirror, boolean).

      Parameters:
      tree - an AST node
      type - the type obtained from tree
      iUseFlow - whether to use information from dataflow analysis

    • checkAndPerformFlowAnalysis

      protected void checkAndPerformFlowAnalysis(Tree tree)
      Flow analysis will be performed if all of the following are true.
      • tree is a ClassTree
      • Flow analysis has not already been performed on tree
      Parameters:
      tree - the tree to check and possibly perform flow analysis on

    • getInferredValueFor

      public @Nullable Value getInferredValueFor(Tree tree)
      Returns the inferred value (by the org.checkerframework.dataflow analysis) for a given tree.
      Parameters:
      tree - the tree
      Returns:
      the value for the tree, if one has been computed by dataflow. If no value has been computed, null is returned (this does not mean that no value will ever be computed for the given tree).

    • applyInferredAnnotations

      protected void applyInferredAnnotations(AnnotatedTypeMirror type, Value inferred)
      Applies the annotations inferred by the org.checkerframework.dataflow analysis to the type type.
      Parameters:
      type - the type to modify
      inferred - the inferred annotations to apply

    • applyQualifierParameterDefaults

      protected void applyQualifierParameterDefaults(Tree tree, AnnotatedTypeMirror type)
      Applies defaults for types in a class with an qualifier parameter.

      Within a class with @HasQualifierParameter, types with that class default to the polymorphic qualifier rather than the typical default. Local variables with a type that has a qualifier parameter are initialized to the type of their initializer, rather than the default for local variables.

      Parameters:
      tree - a Tree whose type is type
      type - where the defaults are applied

    • applyQualifierParameterDefaults

      protected void applyQualifierParameterDefaults(@Nullable Element elt, AnnotatedTypeMirror type)
      Applies defaults for types in a class with an qualifier parameter.

      Within a class with @HasQualifierParameter, types with that class default to the polymorphic qualifier rather than the typical default. Local variables with a type that has a qualifier parameter are initialized to the type of their initializer, rather than the default for local variables.

      Parameters:
      elt - an Element whose type is type
      type - where the defaults are applied

    • addComputedTypeAnnotations

      public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type)
      To add annotations to the type of method or constructor parameters, add a TypeAnnotator using createTypeAnnotator() and see the comment in TypeAnnotator.visitExecutable(org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType, Void).
      Overrides:
      addComputedTypeAnnotations in class AnnotatedTypeFactory
      Parameters:
      elt - an element
      type - the type obtained from elt

    • methodFromUse

      protected AnnotatedTypeFactory.ParameterizedExecutableType methodFromUse(MethodInvocationTree tree, boolean inferTypeArg)
      Description copied from class: AnnotatedTypeFactory
      The implementation of AnnotatedTypeFactory.methodFromUse(MethodInvocationTree) and AnnotatedTypeFactory.methodFromUseWithoutTypeArgInference(MethodInvocationTree).
      Overrides:
      methodFromUse in class AnnotatedTypeFactory
      Parameters:
      tree - a method invocation tree
      inferTypeArg - whether type arguments should be inferred
      Returns:
      the type of the invoked method, any explicit type arguments, and if inferTypeArgs is true, any inferred type arguments

    • methodFromUsePreSubstitution

      public void methodFromUsePreSubstitution(ExpressionTree tree, AnnotatedTypeMirror.AnnotatedExecutableType type, boolean resolvePolyQuals)
      Description copied from class: AnnotatedTypeFactory
      A callback method for the AnnotatedTypeFactory subtypes to customize the handling of the declared method type before type variable substitution.
      Overrides:
      methodFromUsePreSubstitution in class AnnotatedTypeFactory
      Parameters:
      tree - either a method invocation or a member reference tree
      type - declared method type before type variable substitution
      resolvePolyQuals - whether to resolve polymorphic qualifiers

    • typeVariablesFromUse

      public List<AnnotatedTypeParameterBounds> typeVariablesFromUse(AnnotatedTypeMirror.AnnotatedDeclaredType type, TypeElement element)
      Description copied from class: AnnotatedTypeFactory
      Adapt the upper bounds of the type variables of a class relative to the type instantiation. In some type systems, the upper bounds depend on the instantiation of the class. For example, in the Generic Universe Type system, consider a class declaration 
        class C<X extends @Peer Object>
      then the instantiation 
        @Rep C<@Rep Object>
      is legal. The upper bounds of class C have to be adapted by the main modifier.

      An example of an adaptation follows. Suppose, I have a declaration: 

       class MyClass<E extends List<E>>
      And an instantiation: 
       new MyClass<@NonNull String>()

      The upper bound of E adapted to the argument String, would be List<@NonNull String> and the lower bound would be an AnnotatedNullType.

      TODO: ensure that this method is consistently used instead of directly querying the type variables.

      Overrides:
      typeVariablesFromUse in class AnnotatedTypeFactory
      Parameters:
      type - the use of the type
      element - the corresponding element
      Returns:
      the adapted bounds of the type parameters

    • getEmptyStore

      public Store getEmptyStore()
      Returns the empty store.
      Returns:
      the empty store

    • getTypeFactoryOfSubchecker

      public final <T extends GenericAnnotatedTypeFactory<?, ?, ?, ?>> T getTypeFactoryOfSubchecker(Class<? extends BaseTypeChecker> subCheckerClass)
      Returns the type factory used by a subchecker. Throws an exception if no matching subchecker was found or if the type factory is null. The caller must know the exact checker class to request.

      Because the visitor path is copied, call this method each time a subfactory is needed rather than store the returned subfactory in a field.

      Type Parameters:
      T - the type of subCheckerClass's AnnotatedTypeFactory
      Parameters:
      subCheckerClass - the exact class of the subchecker
      Returns:
      the AnnotatedTypeFactory of the subchecker; never null
      See Also:

    • getTypeFactoryOfSubcheckerOrNull

      public <T extends GenericAnnotatedTypeFactory<?, ?, ?, ?>> @Nullable T getTypeFactoryOfSubcheckerOrNull(Class<? extends BaseTypeChecker> subCheckerClass)
      Returns the type factory used by a subchecker. Returns null if no matching subchecker was found or if the type factory is null. The caller must know the exact checker class to request.

      Because the visitor path is copied, call this method each time a subfactory is needed rather than store the returned subfactory in a field.

      Type Parameters:
      T - the type of subCheckerClass's AnnotatedTypeFactory
      Parameters:
      subCheckerClass - the exact class of the subchecker
      Returns:
      the AnnotatedTypeFactory of the subchecker or null if no subchecker exists
      See Also:

    • getShouldDefaultTypeVarLocals

      public boolean getShouldDefaultTypeVarLocals()
      Should the local variable default annotation be applied to type variables?

      It is initialized to true if data flow is used by the checker. It is set to false when getting the assignment context for type argument inference.

      Returns:
      shouldDefaultTypeVarLocals
      See Also:

    • createCFGVisualizer

      protected @Nullable CFGVisualizer<Value,Store,TransferFunction> createCFGVisualizer()
      Create a new CFGVisualizer.
      Returns:
      a new CFGVisualizer, or null if none will be used on this run

    • getCFGVisualizer

      public CFGVisualizer<Value,Store,TransferFunction> getCFGVisualizer()
      The CFGVisualizer to be used by all CFAbstractAnalysis instances.

    • postAsMemberOf

      public void postAsMemberOf(AnnotatedTypeMirror type, AnnotatedTypeMirror owner, Element element)
      Description copied from class: AnnotatedTypeFactory
      A callback method for the AnnotatedTypeFactory subtypes to customize AnnotatedTypes.asMemberOf(). Overriding methods should merely change the annotations on the subtypes, without changing the types.
      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

    • addAnnotationsFromDefaultForType

      protected void addAnnotationsFromDefaultForType(@Nullable Element element, AnnotatedTypeMirror type)
      Adds default qualifiers based on the underlying type of type to type. If element is a local variable, or if the type already has an annotation from the relevant type hierarchy, then the defaults are not added.

      (This uses both the DefaultQualifierForUseTypeAnnotator and DefaultForTypeAnnotator.)

      Parameters:
      element - possibly null element whose type is type
      type - the type to which defaults are added

    • isRelevant

      public final boolean isRelevant(TypeMirror tm)
      Returns true if users can write type annotations from this type system directly on the given Java type.

      For a compound type, returns true only if a programmer may write a type qualifier on the top level of the compound type. That is, this method may return false, when it is possible to write type qualifiers on elements of the type.

      Subclasses should override #isRelevantImpl instead of this method.

      Parameters:
      tm - a type
      Returns:
      true if users can write type annotations from this type system directly on the given Java type

    • isRelevant

      public final boolean isRelevant(AnnotatedTypeMirror tm)
      Returns true if users can write type annotations from this type system directly on the given Java type.

      For a compound type, returns true only if it a programmer may write a type qualifier on the top level of the compound type. That is, this method may return false, when it is possible to write type qualifiers on elements of the type.

      Subclasses should override #isRelevantImpl instead of this method.

      Parameters:
      tm - a type
      Returns:
      true if users can write type annotations from this type system directly on the given Java type

    • isRelevantImpl

      protected boolean isRelevantImpl(TypeMirror tm)
      Returns true if users can write type annotations from this type system on the given Java type. Does not use a cache.

      Clients should never call this. Call isRelevant(javax.lang.model.type.TypeMirror) instead. This is a helper method for isRelevant(javax.lang.model.type.TypeMirror).

      Parameters:
      tm - a type
      Returns:
      true if users can write type annotations from this type system on the given Java type

    • irrelevantExtraMessage

      public String irrelevantExtraMessage()
      Returns a string that can be passed to the "anno.on.irrelevant" error, giving information about which types are relevant.
      Returns:
      a string that can be passed to the "anno.on.irrelevant" error, possibly the empty string

    • getDefaultValueAnnotatedType

      public AnnotatedTypeMirror getDefaultValueAnnotatedType(TypeMirror typeMirror)
      Return the type of the default value of the given type. The default value is 0, false, or null.
      Parameters:
      typeMirror - a type
      Returns:
      the annotated type of type's default value

    • getContractAnnotations

      public List<AnnotationMirror> getContractAnnotations(org.checkerframework.afu.scenelib.el.AMethod m)
      Return the contract annotations (that is, pre- and post-conditions) for the given AMethod. Does not modify the AMethod.

      This overload must only be called when using WholeProgramInferenceScenes.

      Parameters:
      m - the AFU representation of a method
      Returns:
      the contract annotations for the method

    • getPreconditionAnnotations

      public List<AnnotationMirror> getPreconditionAnnotations(org.checkerframework.afu.scenelib.el.AMethod m)
      Return the precondition annotations for the given AMethod. Does not modify the AMethod.

      This overload must only be called when using WholeProgramInferenceScenes.

      Parameters:
      m - the AFU representation of a method
      Returns:
      the precondition annotations for the method

    • getPostconditionAnnotations

      public List<AnnotationMirror> getPostconditionAnnotations(org.checkerframework.afu.scenelib.el.AMethod m, List<AnnotationMirror> preconds)
      Return the postcondition annotations for the given AMethod. Does not modify the AMethod.

      This overload must only be called when using WholeProgramInferenceScenes.

      Parameters:
      m - the AFU representation of a method
      preconds - the precondition annotations for the method; used to suppress redundant postconditions
      Returns:
      the postcondition annotations for the method

    • getContractAnnotations

      public List<AnnotationMirror> getContractAnnotations(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos methodAnnos)
      Return the contract annotations (that is, pre- and post-conditions) for the given CallableDeclarationAnnos. Does not modify the CallableDeclarationAnnos.

      This overload must only be called when using WholeProgramInferenceJavaParserStorage.

      Parameters:
      methodAnnos - annotation data for a method
      Returns:
      contract annotations for the method

    • getPreconditionAnnotations

      public List<AnnotationMirror> getPreconditionAnnotations(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos methodAnnos)
      Return the precondition annotations for the given CallableDeclarationAnnos. Does not modify the CallableDeclarationAnnos.

      This overload must only be called when using WholeProgramInferenceJavaParserStorage.

      Parameters:
      methodAnnos - annotation data for a method
      Returns:
      precondition annotations for the method

    • getPostconditionAnnotations

      public List<AnnotationMirror> getPostconditionAnnotations(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos methodAnnos, List<AnnotationMirror> preconds)
      Return the postcondition annotations for the given CallableDeclarationAnnos. Does not modify the CallableDeclarationAnnos.

      This overload must only be called when using WholeProgramInferenceJavaParserStorage.

      Parameters:
      methodAnnos - annotation data for a method
      preconds - the precondition annotations for the method; used to suppress redundant postconditions
      Returns:
      postcondition annotations for the method

    • getPreconditionAnnotations

      public final List<AnnotationMirror> getPreconditionAnnotations(String expression, AnnotatedTypeMirror inferredType, AnnotatedTypeMirror declaredType)
      Returns a list of inferred @RequiresQualifier annotations for the given expression. By default this list does not include any qualifier that has elements/arguments, which @RequiresQualifier does not support. Subclasses may remove this restriction by overriding createRequiresOrEnsuresQualifier(java.lang.String, javax.lang.model.element.AnnotationMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.dataflow.analysis.Analysis.BeforeOrAfter, java.util.List<javax.lang.model.element.AnnotationMirror>).

      Each annotation in the list is of the form @RequiresQualifier(expression="expression", qualifier=MyQual.class). expression must be a valid Java Expression string, in the same format used by RequiresQualifier.

      Parameters:
      expression - an expression
      inferredType - the type of the expression, on method entry
      declaredType - the declared type of the expression
      Returns:
      precondition annotations for the element (possibly an empty list)

    • getPostconditionAnnotations

      public final List<AnnotationMirror> getPostconditionAnnotations(String expression, AnnotatedTypeMirror inferredType, AnnotatedTypeMirror declaredType, List<AnnotationMirror> preconds)
      Returns a list of inferred @EnsuresQualifier annotations for the given expression. By default this list does not include any qualifier that has elements/arguments, which @EnsuresQualifier does not support; and, preconditions are not used to suppress redundant postconditions. Subclasses may remove these restrictions by overriding createRequiresOrEnsuresQualifier(java.lang.String, javax.lang.model.element.AnnotationMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.dataflow.analysis.Analysis.BeforeOrAfter, java.util.List<javax.lang.model.element.AnnotationMirror>).

      Each annotation in the list is of the form @EnsuresQualifier(expression="expression", qualifier=MyQual.class). expression must be a valid Java Expression string, in the same format used by EnsuresQualifier.

      Parameters:
      expression - an expression
      inferredType - the type of the expression, on method exit
      declaredType - the declared type of the expression
      preconds - the precondition annotations for the method; used to suppress redundant postconditions
      Returns:
      postcondition annotations for the element (possibly an empty list)

    • getPreOrPostconditionAnnotations

      protected List<AnnotationMirror> getPreOrPostconditionAnnotations(String expression, AnnotatedTypeMirror inferredType, AnnotatedTypeMirror declaredType, Analysis.BeforeOrAfter preOrPost, @Nullable List<AnnotationMirror> preconds)
      Creates pre- and postcondition annotations. Helper method for getPreconditionAnnotations(org.checkerframework.afu.scenelib.el.AMethod) and getPostconditionAnnotations(org.checkerframework.afu.scenelib.el.AMethod, java.util.List<javax.lang.model.element.AnnotationMirror>).

      Returns a @RequiresQualifier or @EnsuresQualifier annotation for the given expression. Returns an empty list if none can be created, because the qualifier has elements/arguments, which @RequiresQualifier and @EnsuresQualifier do not support.

      This implementation makes no assumptions about preconditions suppressing postconditions, but subclasses may do so.

      Parameters:
      expression - an expression whose type annotations to return
      inferredType - the type of the expression, on method entry or exit (depending on the value of preOrPost)
      declaredType - the declared type of the expression, which is used to determine if the inferred type supplies no additional information beyond the declared type
      preOrPost - whether to return preconditions or postconditions
      preconds - the precondition annotations for the method; used to suppress redundant postconditions; non-null exactly when preOrPost is AFTER
      Returns:
      precondition or postcondition annotations for the element (possibly an empty list)

    • createRequiresOrEnsuresQualifier

      protected @Nullable AnnotationMirror createRequiresOrEnsuresQualifier(String expression, AnnotationMirror qualifier, AnnotatedTypeMirror declaredType, Analysis.BeforeOrAfter preOrPost, @Nullable List<AnnotationMirror> preconds)
      Creates a RequiresQualifier("...") or EnsuresQualifier("...") annotation for the given expression.

      This is of the form @RequiresQualifier(expression="expression", qualifier=MyQual.class) or @EnsuresQualifier(expression="expression", qualifier=MyQual.class), where "expression" is exactly the string expression and MyQual is the annotation represented by qualifier.

      Returns null if the expression is invalid when combined with the kind of annotation: for example, precondition annotations on "this" and parameters ("#1", etc.) are not supported, because receiver/parameter annotations should be inferred instead.

      This implementation returns null if no annotation can be created, because the qualifier has elements/arguments, which @RequiresQualifier and @EnsuresQualifier do not support. Subclasses may override this method to return qualifiers that do have arguments instead of returning null.

      Parameters:
      expression - the expression to which the qualifier applies
      qualifier - the qualifier that must be present
      declaredType - the declared type of the expression, which is used to avoid inferring redundant pre- or postcondition annotations
      preOrPost - whether to return a precondition or postcondition annotation
      preconds - the list of precondition annotations; used to suppress redundant postconditions; non-null exactly when preOrPost is BeforeOrAfter.BEFORE
      Returns:
      a RequiresQualifier("...") or EnsuresQualifier("...") annotation for the given expression, or null

    • addSharedCFGForTree

      public boolean addSharedCFGForTree(Tree tree, ControlFlowGraph cfg)
      Add a new entry to the shared CFG. If this is a subchecker, this method delegates to the superchecker's GenericAnnotatedTypeFactory, if it exists. Duplicate keys must map to the same CFG.

      Calls to this method should be guarded by checking hasOrIsSubchecker; it is nonsensical to have a shared CFG when a checker is running alone.

      Parameters:
      tree - the source code corresponding to cfg
      cfg - the control flow graph to use for tree
      Returns:
      whether a shared CFG was found to actually add to (duplicate keys also return true)

    • getSharedCFGForTree

      public @Nullable ControlFlowGraph getSharedCFGForTree(Tree tree)
      Get the shared control flow graph used for tree by this checker's topmost superchecker. Returns null if no information is available about the given tree, or if this checker has a parent checker that does not have a GenericAnnotatedTypeFactory.

      Calls to this method should be guarded by checking hasOrIsSubchecker; it is nonsensical to have a shared CFG when a checker is running alone.

      Parameters:
      tree - the tree whose CFG should be looked up
      Returns:
      the CFG stored by this checker's uppermost superchecker for tree, or null if it is not available

    • getEnsuresQualifierIfResult

      public @Nullable Boolean getEnsuresQualifierIfResult(Contract.Kind kind, AnnotationMirror contractAnnotation)
      If kind = CONDITIONALPOSTCONDITION, return the result element, e.g. EnsuresQualifierIf.result(). Otherwise, return null.
      Parameters:
      kind - the kind of contractAnnotation
      contractAnnotation - a RequiresQualifier, EnsuresQualifier, or EnsuresQualifierIf
      Returns:
      the result element of contractAnnotation, or null if it doesn't have a result element

    • getContractExpressions

      public @Nullable List<String> getContractExpressions(Contract.Kind kind, AnnotationMirror contractAnnotation)
      If contractAnnotation is a framework annotation, return its expression element. Otherwise, contractAnnotation is defined in a checker. If kind = CONDITIONALPOSTCONDITION, return its expression element, else return its value element.
      Parameters:
      kind - the kind of contractAnnotation
      contractAnnotation - a RequiresQualifier, EnsuresQualifier, or EnsuresQualifierIf
      Returns:
      the result element of contractAnnotation, or null if it doesn't have a result element