Package org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceImplementation<T>

java.lang.Object
org.checkerframework.common.wholeprograminference.WholeProgramInferenceImplementation<T>
Type Parameters:
T - the type used by the storage to store annotations
All Implemented Interfaces:
WholeProgramInference
public class WholeProgramInferenceImplementation<T> extends Object implements WholeProgramInference
This is the primary implementation of WholeProgramInference. It uses an instance of WholeProgramInferenceStorage to store annotations and to create output files.

This class does not perform inference for an element if the element has explicit annotations. That is, calling an update* method on an explicitly annotated field, method return, or method parameter has no effect.

In addition, whole program inference ignores inferred types in a few scenarios. When discovering a use, WPI ignores an inferred type if:

  1. The inferred type of an element that should be written into a file is a subtype of the upper bounds of this element's written type in the source code.
  2. The annotation annotates a null literal, except when doing inference for the NullnessChecker. (The rationale for this is that null is a frequently-used default value, and it would be undesirable to infer the bottom type if null were the only value passed as an argument.)
When outputting a file, WPI ignores an inferred type if:
  1. The @Target annotation does not permit the annotation to be written at this location.
  2. The @RelevantJavaTypes annotation does not permit the annotation to be written at this location.
  3. The inferred annotation has the @InvisibleQualifier meta-annotation.
  4. The inferred annotation would be the same annotation applied via defaulting — that is, if omitting it has the same effect as writing it.
See Also:

  • Field Details

    • atypeFactory

      protected final AnnotatedTypeFactory atypeFactory
      The type factory associated with this.

  • Constructor Details

    • WholeProgramInferenceImplementation

      public WholeProgramInferenceImplementation(AnnotatedTypeFactory atypeFactory, WholeProgramInferenceStorage<T> storage, boolean showWpiFailedInferences)
      Constructs a new WholeProgramInferenceImplementation that has not yet inferred any annotations.
      Parameters:
      atypeFactory - the associated type factory
      storage - the storage used for inferred annotations and for writing output files
      showWpiFailedInferences - whether the -AshowWpiFailedInferences argument was passed to the checker, and therefore whether to print debugging messages when inference fails

  • Method Details

    • getStorage

      public WholeProgramInferenceStorage<T> getStorage()
      Returns the storage for inferred annotations.
      Returns:
      the storage for the inferred annotations

    • updateFromObjectCreation

      public void updateFromObjectCreation(ObjectCreationNode objectCreationNode, ExecutableElement constructorElt, CFAbstractStore<?,?> store)
      Description copied from interface: WholeProgramInference
      Updates the parameter types of the constructor constructorElt based on the arguments in objectCreationNode.

      For each parameter in constructorElt:

      • If there is no stored annotated type for that parameter, then use the type of the corresponding argument in the object creation call objectCreationNode.
      • If there was a stored annotated type for that parameter, then its new type will be the LUB between the previous type and the type of the corresponding argument in the object creation call.
      Specified by:
      updateFromObjectCreation in interface WholeProgramInference
      Parameters:
      objectCreationNode - the Node that invokes the constructor
      constructorElt - the Element of the constructor
      store - the store just before the call

    • updateFromMethodInvocation

      public void updateFromMethodInvocation(MethodInvocationNode methodInvNode, ExecutableElement methodElt, CFAbstractStore<?,?> store)
      Description copied from interface: WholeProgramInference
      Updates the parameter types of the method methodElt based on the arguments in the method invocation methodInvNode.

      For each formal parameter in methodElt (including the receiver):

      • If there is no stored annotated type for that parameter, then use the type of the corresponding argument in the method call methodInvNode.
      • If there was a stored annotated type for that parameter, then its new type will be the LUB between the previous type and the type of the corresponding argument in the method call.
      Specified by:
      updateFromMethodInvocation in interface WholeProgramInference
      Parameters:
      methodInvNode - the node representing a method invocation
      methodElt - the element of the method being invoked
      store - the store before the method call, used for inferring method preconditions

    • updateContracts

      public void updateContracts(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElt, CFAbstractStore<?,?> store)
      Description copied from interface: WholeProgramInference
      Updates the preconditions or postconditions of the current method, from a store.
      Specified by:
      updateContracts in interface WholeProgramInference
      Parameters:
      preOrPost - whether to update preconditions or postconditions
      methodElt - the method or constructor whose preconditions or postconditions to update
      store - the store at the method's entry or normal exit, for reading types of expressions

    • updateFromOverride

      public void updateFromOverride(MethodTree methodTree, ExecutableElement methodElt, AnnotatedTypeMirror.AnnotatedExecutableType overriddenMethod)
      Description copied from interface: WholeProgramInference
      Updates the parameter types (including the receiver) of the method methodTree based on the parameter types of the overridden method overriddenMethod.

      For each formal parameter in methodElt:

      • If there is no stored annotated type for that parameter, then use the type of the corresponding parameter on the overridden method.
      • If there is a stored annotated type for that parameter, then its new type will be the LUB between the previous type and the type of the corresponding parameter on the overridden method.
      Specified by:
      updateFromOverride in interface WholeProgramInference
      Parameters:
      methodTree - the tree of the method that contains the parameter(s)
      methodElt - the element of the method
      overriddenMethod - the AnnotatedExecutableType of the overridden method

    • updateFromFormalParameterAssignment

      public void updateFromFormalParameterAssignment(LocalVariableNode lhs, Node rhs, VariableElement paramElt)
      Description copied from interface: WholeProgramInference
      Updates the type of lhs based on an assignment of rhs to lhs.
      • If there is no stored annotated type for lhs, then use the type of the corresponding argument in the method call methodInvNode.
      • If there is a stored annotated type for lhs, then its new type will be the LUB between the previous type and the type of the corresponding argument in the method call.
      Specified by:
      updateFromFormalParameterAssignment in interface WholeProgramInference
      Parameters:
      lhs - the node representing the formal parameter
      rhs - the node being assigned to the parameter in the method body
      paramElt - the formal parameter

    • updateFromFieldAssignment

      public void updateFromFieldAssignment(Node lhs, Node rhs)
      Description copied from interface: WholeProgramInference
      Updates the type of field based on an assignment of rhs to field. If the field has a declaration annotation with the IgnoreInWholeProgramInference meta-annotation, no type annotation will be inferred for that field.

      If there is no stored entry for the field lhs, the entry will be created and its type will be the type of rhs. If there is a stored entry/type for lhs, its new type will be the LUB between the previous type and the type of rhs.

      Specified by:
      updateFromFieldAssignment in interface WholeProgramInference
      Parameters:
      lhs - the field whose type will be refined. Must be either a FieldAccessNode or a LocalVariableNode whose element kind is FIELD.
      rhs - the expression being assigned to the field

    • updateFieldFromType

      public void updateFieldFromType(Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM)
      Description copied from interface: WholeProgramInference
      Updates the type of field based on an assignment whose right-hand side has type rhsATM. See more details at WholeProgramInference.updateFromFieldAssignment(org.checkerframework.dataflow.cfg.node.Node, org.checkerframework.dataflow.cfg.node.Node).
      Specified by:
      updateFieldFromType in interface WholeProgramInference
      Parameters:
      lhsTree - the tree for the field whose type will be refined
      element - the element for the field whose type will be refined
      fieldName - the name of the field whose type will be refined
      rhsATM - the type of the expression being assigned to the field

    • ignoreFieldInWPI

      protected boolean ignoreFieldInWPI(Element element, String fieldName)
      Returns true if an assignment to the given field should be ignored by WPI.
      Parameters:
      element - the field's element
      fieldName - the field's name
      Returns:
      true if an assignment to the given field should be ignored by WPI

    • updateFromReturn

      public void updateFromReturn(ReturnNode retNode, com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol, MethodTree methodDeclTree, Map<AnnotatedTypeMirror.AnnotatedDeclaredType,ExecutableElement> overriddenMethods)
      Description copied from interface: WholeProgramInference
      Updates the return type of the method methodTree based on returnedExpression. Also updates the return types of any methods that this method overrides that are available as source code.

      If there is no stored annotated return type for the method methodTree, then the type of the return expression will be added to the return type of that method. If there is a stored annotated return type for the method methodTree, its new type will be the LUB between the previous type and the type of the return expression.

      Specified by:
      updateFromReturn in interface WholeProgramInference
      Parameters:
      retNode - the node that contains the expression returned
      classSymbol - the symbol of the class that contains the method
      methodDeclTree - the tree of the method whose return type may be updated
      overriddenMethods - the methods that the given method return overrides, indexed by the annotated type of the superclass in which each method is defined

    • addMethodDeclarationAnnotation

      public void addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno)
      Description copied from interface: WholeProgramInference
      Updates a method to add a declaration annotation.
      Specified by:
      addMethodDeclarationAnnotation in interface WholeProgramInference
      Parameters:
      methodElt - the method to annotate
      anno - the declaration annotation to add to the method

    • addMethodDeclarationAnnotation

      public void addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno, boolean lubPurity)
      Description copied from interface: WholeProgramInference
      Updates a method to add a declaration annotation. Optionally, may replace the current purity annotation on elt with the logical least upper bound between that purity annotation and anno, if anno is also a purity annotation.
      Specified by:
      addMethodDeclarationAnnotation in interface WholeProgramInference
      Parameters:
      methodElt - the method to annotate
      anno - the declaration annotation to add to the method
      lubPurity - if true and anno is a purity annotation, replaces the current purity annotation with a least upper bound rather than just adding anno

    • addFieldDeclarationAnnotation

      public void addFieldDeclarationAnnotation(VariableElement field, AnnotationMirror anno)
      Description copied from interface: WholeProgramInference
      Updates a field to add a declaration annotation.
      Specified by:
      addFieldDeclarationAnnotation in interface WholeProgramInference
      Parameters:
      field - the field to annotate
      anno - the declaration annotation to add to the field

    • addDeclarationAnnotationToFormalParameter

      public void addDeclarationAnnotationToFormalParameter(ExecutableElement methodElt, int index, AnnotationMirror anno)
      Description copied from interface: WholeProgramInference
      Adds a declaration annotation to a formal parameter.
      Specified by:
      addDeclarationAnnotationToFormalParameter in interface WholeProgramInference
      Parameters:
      methodElt - the method whose formal parameter will be annotated
      index - the index of the parameter (0-indexed)
      anno - the annotation to add

    • addClassDeclarationAnnotation

      public void addClassDeclarationAnnotation(TypeElement classElt, AnnotationMirror anno)
      Description copied from interface: WholeProgramInference
      Adds an annotation to a class declaration.
      Specified by:
      addClassDeclarationAnnotation in interface WholeProgramInference
      Parameters:
      classElt - the class declaration to annotate
      anno - the annotation to add

    • updateAnnotationSet

      protected void updateAnnotationSet(T annotationsToUpdate, TypeUseLocation defLoc, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, String file)
      Updates the set of annotations in a location in a program.
      • If there was no previous annotation for that location, then the updated set will be the annotations in rhsATM.
      • If there was a previous annotation, the updated set will be the LUB between the previous annotation and rhsATM.

      Subclasses can customize this behavior.

      Parameters:
      annotationsToUpdate - the type whose annotations are modified by this method
      defLoc - the location where the annotation will be added
      rhsATM - the RHS of the annotated type on the source code
      lhsATM - the LHS of the annotated type on the source code
      file - the annotation file containing the executable; used for marking the scene as modified (needing to be written to disk)

    • updateAnnotationSet

      protected void updateAnnotationSet(T annotationsToUpdate, TypeUseLocation defLoc, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, String file, boolean ignoreIfAnnotated)
      Updates the set of annotations in a location in a program.
      • If there was no previous annotation for that location, then the updated set will be the annotations in rhsATM.
      • If there was a previous annotation, the updated set will be the LUB between the previous annotation and rhsATM.

      Subclasses can customize this behavior.

      Parameters:
      annotationsToUpdate - the type whose annotations are modified by this method
      defLoc - the location where the annotation will be added
      rhsATM - the RHS of the annotated type on the source code
      lhsATM - the LHS of the annotated type on the source code
      file - annotation file containing the executable; used for marking the scene as modified (needing to be written to disk)
      ignoreIfAnnotated - if true, don't update any type that is explicitly annotated in the source code

    • updateAtmWithLub

      public void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMirror ajavaATM)
      Description copied from interface: WholeProgramInference
      Updates sourceCodeATM to contain the LUB between sourceCodeATM and ajavaATM, ignoring missing AnnotationMirrors from ajavaATM -- it considers the LUB between an AnnotationMirror am and a missing AnnotationMirror to be am. The results are stored in sourceCodeATM.
      Specified by:
      updateAtmWithLub in interface WholeProgramInference
      Parameters:
      sourceCodeATM - the annotated type on the source code; side effected by this method
      ajavaATM - the annotated type on the annotation file

    • writeResultsToFile

      public void writeResultsToFile(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker)
      Description copied from interface: WholeProgramInference
      Writes the inferred results to a file. Ideally, it should be called at the end of the type-checking process. In practice, it is called after each class, because we don't know which class will be the last one in the type-checking process.
      Specified by:
      writeResultsToFile in interface WholeProgramInference
      Parameters:
      outputFormat - the file format in which to write the results
      checker - the checker from which this method is called, for naming annotation files

    • preprocessClassTree

      public void preprocessClassTree(ClassTree classTree)
      Description copied from interface: WholeProgramInference
      Performs any preparation required for inference on Elements of a class. Should be called on each toplevel class declaration in a compilation unit before processing it.
      Specified by:
      preprocessClassTree in interface WholeProgramInference
      Parameters:
      classTree - the class to preprocess