Package org.checkerframework.common.wholeprograminference

Interface WholeProgramInferenceStorage<T>

Type Parameters:
T - the type used by the storage to store annotations. The methods atmFromStorageLocation(javax.lang.model.type.TypeMirror, T) and updateStorageLocationFromAtm(org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, T, org.checkerframework.framework.qual.TypeUseLocation, boolean) can be used to manipulate a storage location.
All Known Implementing Classes:
WholeProgramInferenceJavaParserStorage, WholeProgramInferenceScenesStorage
public interface WholeProgramInferenceStorage<T>
Stores annotations from whole-program inference. For a given location such as a field or method, an object can be obtained containing the inferred annotations for that object.

Also writes stored annotations to storage files. The specific format depends on the implementation.

  • Method Details

    • getFileForElement

      String getFileForElement(Element elt)
      Returns the file corresponding to the given element. This may side-effect the storage to load the file if it hasn't been read yet.
      Parameters:
      elt - an element
      Returns:
      the path to the file where inference results for the element will be written

    • hasStorageLocationForMethod

      boolean hasStorageLocationForMethod(ExecutableElement methodElt)
      Given an ExecutableElement in a compilation unit that has already been read into storage, returns whether there exists a stored method matching elt.

      An implementation is permitted to return false if elt represents a method that was synthetically added by javac, such as zero-argument constructors or valueOf(String) methods for enum types.

      Parameters:
      methodElt - a method or constructor Element
      Returns:
      true if the storage has a method corresponding to elt

    • getParameterAnnotations

      T getParameterAnnotations(ExecutableElement methodElt, @org.checkerframework.checker.index.qual.Positive int index_1based, AnnotatedTypeMirror paramATM, VariableElement ve, AnnotatedTypeFactory atypeFactory)
      Get the annotations for a formal parameter type.
      Parameters:
      methodElt - the method or constructor Element
      index_1based - the parameter index (1-based)
      paramATM - the parameter type
      ve - the parameter variable
      atypeFactory - the type factory
      Returns:
      the annotations for a formal parameter type

    • getReceiverAnnotations

      T getReceiverAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror paramATM, AnnotatedTypeFactory atypeFactory)
      Get the annotations for the receiver type.
      Parameters:
      methodElt - the method or constructor Element
      paramATM - the receiver type
      atypeFactory - the type factory
      Returns:
      the annotations for the receiver type

    • getReturnAnnotations

      T getReturnAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror atm, AnnotatedTypeFactory atypeFactory)
      Get the annotations for the return type.
      Parameters:
      methodElt - the method or constructor Element
      atm - the return type
      atypeFactory - the type factory
      Returns:
      the annotations for the return type

    • getFieldAnnotations

      T getFieldAnnotations(Element element, String fieldName, AnnotatedTypeMirror lhsATM, AnnotatedTypeFactory atypeFactory)
      Get the annotations for a field type.
      Parameters:
      element - the element for the field
      fieldName - the simple field name
      lhsATM - the field type
      atypeFactory - the annotated type factory
      Returns:
      the annotations for a field type

    • getPreOrPostconditions

      @Nullable T getPreOrPostconditions(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElement, String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atypeFactory)
      Returns the pre- or postcondition annotations for an expression. The format of the expression is the same as a programmer would write in a RequiresQualifier or EnsuresQualifier annotation.

      This method may return null if the given expression is not a supported expression type. Currently, the supported expression types are: fields of "this" (e.g. "this.f", pre- and postconditions), "this" (postconditions only), and method parameters (e.g. "#1", "#2", postconditions only).

      Parameters:
      preOrPost - whether to get the precondition or postcondition
      methodElement - the method
      expression - the expression
      declaredType - the declared type of the expression
      atypeFactory - the type factory
      Returns:
      the pre- or postcondition annotations for an expression, or null if the given expression is not a supported expression type

    • addMethodDeclarationAnnotation

      boolean addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno)
      Updates a method to add a declaration annotation.
      Parameters:
      methodElt - the method to annotate
      anno - the declaration annotation to add to the method
      Returns:
      true if anno is a new declaration annotation for methodElt, false otherwise

    • addFieldDeclarationAnnotation

      boolean addFieldDeclarationAnnotation(VariableElement fieldElt, AnnotationMirror anno)
      Updates a field to add a declaration annotation.
      Parameters:
      fieldElt - the field
      anno - the declaration annotation to add to the field
      Returns:
      true if anno is a new declaration annotation for fieldElt, false otherwise

    • addDeclarationAnnotationToFormalParameter

      boolean addDeclarationAnnotationToFormalParameter(ExecutableElement methodElt, @org.checkerframework.checker.index.qual.Positive int index_1based, AnnotationMirror anno)
      Adds a declaration annotation to a formal parameter.
      Parameters:
      methodElt - the method whose formal parameter will be annotated
      index_1based - the index of the parameter (1-indexed)
      anno - the annotation to add
      Returns:
      true if anno is a new declaration annotation for methodElt, false otherwise

    • addClassDeclarationAnnotation

      boolean addClassDeclarationAnnotation(TypeElement classElt, AnnotationMirror anno)
      Adds an annotation to a class declaration.
      Parameters:
      classElt - the class declaration to annotate
      anno - the annotation to add
      Returns:
      true if anno is a new declaration annotation for classElt, false otherwise

    • getMethodDeclarationAnnotations

      AnnotationMirrorSet getMethodDeclarationAnnotations(ExecutableElement elt)
      Return the list of declaration annotations inferred on the given method so far in this round of WPI.
      Parameters:
      elt - a method
      Returns:
      the declaration annotations inferred on elt so far (may be empty)

    • removeMethodDeclarationAnnotation

      boolean removeMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno)
      Removes the given annotation from the given method element's inferred declaration annotation. If the given annotation was not in the list of inferred declaration annotations on the given method, calling this method is a no-op.
      Parameters:
      methodElt - a method element
      anno - a declaration annotation to remove
      Returns:
      true if the annotation was successfully removed, false if not (e.g., if it wasn't present)

    • atmFromStorageLocation

      AnnotatedTypeMirror atmFromStorageLocation(TypeMirror typeMirror, T storageLocation)
      Obtain the type from a storage location.
      Parameters:
      typeMirror - the underlying type for the result
      storageLocation - the storage location from which to obtain annotations
      Returns:
      an annotated type mirror with underlying type typeMirror and annotations from storageLocation

    • updateStorageLocationFromAtm

      void updateStorageLocationFromAtm(AnnotatedTypeMirror newATM, AnnotatedTypeMirror curATM, T storageLocationToUpdate, TypeUseLocation defLoc, boolean ignoreIfAnnotated)
      Updates a storage location to have the annotations of the given AnnotatedTypeMirror. Annotations in the original set that should be ignored are not added to the resulting set. If ignoreIfAnnotated is true, doesn't add annotations for locations with explicit annotations in source code.

      This method removes from the storage location all annotations supported by the AnnotatedTypeFactory before inserting new ones. It is assumed that every time this method is called, the new AnnotatedTypeMirror has a better type estimate for the given location. Therefore, it is not a problem to remove all annotations before inserting the new annotations.

      The update* methods in WholeProgramInference perform LUB. This one just does replacement. (Thus, the naming may be a bit confusing.)

      Parameters:
      newATM - the type whose annotations will be added to the AnnotatedTypeMirror
      curATM - the annotations currently stored at the location, used to check if the element that will be updated has explicit annotations in source code
      storageLocationToUpdate - the storage location that will be updated
      defLoc - the location where the annotation will be added
      ignoreIfAnnotated - if true, don't update any type that is explicitly annotated in the source code

    • writeResultsToFile

      void writeResultsToFile(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker)
      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.
      Parameters:
      outputFormat - the file format in which to write the results
      checker - the checker from which this method is called, for naming annotation files

    • setFileModified

      void setFileModified(String path)
      Indicates that inferred annotations for the file at path have changed since last written. This causes output files for path to be written out next time writeResultsToFile(org.checkerframework.common.wholeprograminference.WholeProgramInference.OutputFormat, org.checkerframework.common.basetype.BaseTypeChecker) is called.
      Parameters:
      path - path to the file with annotations that have been modified

    • preprocessClassTree

      void preprocessClassTree(ClassTree classTree)
      Performs any preparation required for inference on the elements of a class. Should be called on each top-level class declaration in a compilation unit before processing it.
      Parameters:
      classTree - the class to preprocess