Package org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceScenesStorage

java.lang.Object
org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesStorage
All Implemented Interfaces:
WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
public class WholeProgramInferenceScenesStorage extends Object implements WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
This class stores annotations using scenelib objects.

The set of annotations inferred for a certain class is stored in an AScene, which writeScenes() can write into a file. For example, a class my.pakkage.MyClass will have its members' inferred types stored in a Scene, and later written into a file named my.pakkage.MyClass.jaif if using WholeProgramInference.OutputFormat.JAIF, or my.pakkage.MyClass.astub if using WholeProgramInference.OutputFormat.STUB.

This class populates the initial Scenes by reading existing .jaif files on the JAIF_FILES_PATH directory (regardless of output format). Having more information in those initial .jaif files means that the precision achieved by the whole-program inference analysis will be better. writeScenes(org.checkerframework.common.wholeprograminference.WholeProgramInference.OutputFormat, org.checkerframework.common.basetype.BaseTypeChecker) rewrites the initial .jaif files and may create new ones.

  • Field Details

  • Constructor Details

    • WholeProgramInferenceScenesStorage

      public WholeProgramInferenceScenesStorage(AnnotatedTypeFactory atypeFactory)
      Default constructor.
      Parameters:
      atypeFactory - the type factory associated with this WholeProgramInferenceScenesStorage

  • Method Details

    • getFileForElement

      public String getFileForElement(Element elt)
      Description copied from interface: WholeProgramInferenceStorage
      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.
      Specified by:
      getFileForElement in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      elt - an element
      Returns:
      the path to the file where inference results for the element will be written

    • hasStorageLocationForMethod

      public boolean hasStorageLocationForMethod(ExecutableElement methodElt)
      Description copied from interface: WholeProgramInferenceStorage
      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.

      Specified by:
      hasStorageLocationForMethod in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      methodElt - a method or constructor Element
      Returns:
      true if the storage has a method corresponding to elt

    • getParameterAnnotations

      public org.checkerframework.afu.scenelib.el.ATypeElement getParameterAnnotations(ExecutableElement methodElt, int i, AnnotatedTypeMirror paramATM, VariableElement ve, AnnotatedTypeFactory atypeFactory)
      Description copied from interface: WholeProgramInferenceStorage
      Get the annotations for a formal parameter type.
      Specified by:
      getParameterAnnotations in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      methodElt - the method or constructor Element
      i - the parameter index (0-based)
      paramATM - the parameter type
      ve - the parameter variable
      atypeFactory - the type factory
      Returns:
      the annotations for a formal parameter type

    • getReceiverAnnotations

      public org.checkerframework.afu.scenelib.el.ATypeElement getReceiverAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror paramATM, AnnotatedTypeFactory atypeFactory)
      Description copied from interface: WholeProgramInferenceStorage
      Get the annotations for the receiver type.
      Specified by:
      getReceiverAnnotations in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      methodElt - the method or constructor Element
      paramATM - the receiver type
      atypeFactory - the type factory
      Returns:
      the annotations for the receiver type

    • getMethodDeclarationAnnotations

      public AnnotationMirrorSet getMethodDeclarationAnnotations(ExecutableElement elt)
      Description copied from interface: WholeProgramInferenceStorage
      Return the list of declaration annotations inferred on the given method so far in this round of WPI.
      Specified by:
      getMethodDeclarationAnnotations in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      elt - a method
      Returns:
      the declaration annotations inferred on elt so far (may be empty)

    • removeMethodDeclarationAnnotation

      public boolean removeMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno)
      Description copied from interface: WholeProgramInferenceStorage
      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.
      Specified by:
      removeMethodDeclarationAnnotation in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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)

    • getReturnAnnotations

      public org.checkerframework.afu.scenelib.el.ATypeElement getReturnAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror atm, AnnotatedTypeFactory atypeFactory)
      Description copied from interface: WholeProgramInferenceStorage
      Get the annotations for the return type.
      Specified by:
      getReturnAnnotations in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      methodElt - the method or constructor Element
      atm - the return type
      atypeFactory - the type factory
      Returns:
      the annotations for the return type

    • getFieldAnnotations

      public org.checkerframework.afu.scenelib.el.ATypeElement getFieldAnnotations(Element element, String fieldName, AnnotatedTypeMirror lhsATM, AnnotatedTypeFactory atypeFactory)
      Description copied from interface: WholeProgramInferenceStorage
      Get the annotations for a field type.
      Specified by:
      getFieldAnnotations in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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

      public org.checkerframework.afu.scenelib.el.ATypeElement getPreOrPostconditions(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElement, String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atypeFactory)
      Description copied from interface: WholeProgramInferenceStorage
      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).

      Specified by:
      getPreOrPostconditions in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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

    • getPreconditionDeclaredType

      public AnnotatedTypeMirror getPreconditionDeclaredType(org.checkerframework.afu.scenelib.el.AMethod m, String expression)
      Fetches the declared type of an expression for which a precondition was inferred, for the given AMethod.
      Parameters:
      m - a method
      expression - the expression
      Returns:
      the declared type

    • getPostconditionDeclaredType

      public AnnotatedTypeMirror getPostconditionDeclaredType(org.checkerframework.afu.scenelib.el.AMethod m, String expression)
      Fetches the declared type of an expression for which a postcondition was inferred, for the given AMethod.
      Parameters:
      m - a method
      expression - the expression
      Returns:
      the declared type

    • addMethodDeclarationAnnotation

      public boolean addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno)
      Description copied from interface: WholeProgramInferenceStorage
      Updates a method to add a declaration annotation.
      Specified by:
      addMethodDeclarationAnnotation in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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

      public boolean addFieldDeclarationAnnotation(VariableElement field, AnnotationMirror anno)
      Description copied from interface: WholeProgramInferenceStorage
      Updates a field to add a declaration annotation.
      Specified by:
      addFieldDeclarationAnnotation in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      field - 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

      public boolean addDeclarationAnnotationToFormalParameter(ExecutableElement methodElt, int index, AnnotationMirror anno)
      Description copied from interface: WholeProgramInferenceStorage
      Adds a declaration annotation to a formal parameter.
      Specified by:
      addDeclarationAnnotationToFormalParameter in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      methodElt - the method whose formal parameter will be annotated
      index - the index of the parameter (0-indexed)
      anno - the annotation to add
      Returns:
      true if anno is a new declaration annotation for methodElt, false otherwise

    • addClassDeclarationAnnotation

      public boolean addClassDeclarationAnnotation(TypeElement classElt, AnnotationMirror anno)
      Description copied from interface: WholeProgramInferenceStorage
      Adds an annotation to a class declaration.
      Specified by:
      addClassDeclarationAnnotation in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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

    • writeScenes

      public void writeScenes(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker)
      Write all modified scenes into files. (Scenes are modified by the method updateAnnotationSetInScene(org.checkerframework.afu.scenelib.el.ATypeElement, org.checkerframework.framework.qual.TypeUseLocation, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, java.lang.String, boolean).)
      Parameters:
      outputFormat - the output format to use when writing files
      checker - the checker from which this method is called, for naming stub files

    • getJaifPath

      protected String getJaifPath(String className)
      Returns the String representing the .jaif path of a class given its name.
      Parameters:
      className - the simple name of a class
      Returns:
      the path to the .jaif file

    • getAClass

      protected org.checkerframework.afu.scenelib.el.AClass getAClass(@BinaryName String className, String jaifPath, @Nullable com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol)
      Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.
      Parameters:
      className - the name of the class to get, in binary form
      jaifPath - the path to the jaif file that would represent that class (must end in ".jaif")
      classSymbol - optionally, the ClassSymbol representing the class. Used to set the symbol information stored on an AClass.
      Returns:
      a version of the scene-lib representation of the class, augmented with symbol information if classSymbol was non-null

    • getAClass

      protected org.checkerframework.afu.scenelib.el.AClass getAClass(@BinaryName String className, String jaifPath)
      Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.
      Parameters:
      className - the name of the class to get, in binary form
      jaifPath - the path to the jaif file that would represent that class (must end in ".jaif")
      Returns:
      the scene-lib representation of the class, possibly augmented with symbol information if getAClass(String, String, com.sun.tools.javac.code.Symbol.ClassSymbol) has already been called with a non-null third argument

    • updateAnnotationSetInScene

      protected void updateAnnotationSetInScene(org.checkerframework.afu.scenelib.el.ATypeElement type, TypeUseLocation defLoc, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, String jaifPath, boolean ignoreIfAnnotated)
      Updates the set of annotations in a location of a Scene, as the result of a pseudo-assignment.
      • 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.
      Parameters:
      type - ATypeElement of the Scene which will be modified
      jaifPath - path to a .jaif file for a Scene; used for marking the scene as modified (needing to be written to disk)
      rhsATM - the RHS of the annotated type on the source code
      lhsATM - the LHS of the annotated type on the source code
      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

    • atmFromStorageLocation

      public AnnotatedTypeMirror atmFromStorageLocation(TypeMirror typeMirror, org.checkerframework.afu.scenelib.el.ATypeElement storageLocation)
      Description copied from interface: WholeProgramInferenceStorage
      Obtain the type from a storage location.
      Specified by:
      atmFromStorageLocation in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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

      public void updateStorageLocationFromAtm(AnnotatedTypeMirror newATM, AnnotatedTypeMirror curATM, org.checkerframework.afu.scenelib.el.ATypeElement typeToUpdate, TypeUseLocation defLoc, boolean ignoreIfAnnotated)
      Description copied from interface: WholeProgramInferenceStorage
      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.)

      Specified by:
      updateStorageLocationFromAtm in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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
      typeToUpdate - 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

    • prepareSceneForWriting

      public void prepareSceneForWriting(org.checkerframework.afu.scenelib.el.AScene compilationUnitAnnos)
      Side-effects the compilation unit annotations to make any desired changes before writing to a file.
      Parameters:
      compilationUnitAnnos - the compilation unit annotations to modify

    • wpiPrepareClassForWriting

      public void wpiPrepareClassForWriting(org.checkerframework.afu.scenelib.el.AClass classAnnos)
      Side-effects the class annotations to make any desired changes before writing to a file.
      Parameters:
      classAnnos - the class annotations to modify

    • wpiPrepareMethodForWriting

      public void wpiPrepareMethodForWriting(org.checkerframework.afu.scenelib.el.AMethod methodAnnos)
      Side-effects the method or constructor annotations to make any desired changes before writing to a file.
      Parameters:
      methodAnnos - the method or constructor annotations to modify

    • writeResultsToFile

      public void writeResultsToFile(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker)
      Description copied from interface: WholeProgramInferenceStorage
      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 WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      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

      public void setFileModified(String path)
      Description copied from interface: WholeProgramInferenceStorage
      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 WholeProgramInferenceStorage.writeResultsToFile(org.checkerframework.common.wholeprograminference.WholeProgramInference.OutputFormat, org.checkerframework.common.basetype.BaseTypeChecker) is called.
      Specified by:
      setFileModified in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      path - path to the file with annotations that have been modified

    • preprocessClassTree

      public void preprocessClassTree(ClassTree classTree)
      Description copied from interface: WholeProgramInferenceStorage
      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.
      Specified by:
      preprocessClassTree in interface WholeProgramInferenceStorage<org.checkerframework.afu.scenelib.el.ATypeElement>
      Parameters:
      classTree - the class to preprocess

    • aTypeElementToString

      public static String aTypeElementToString(org.checkerframework.afu.scenelib.el.ATypeElement aType)
      Returns a string representation of an ATypeElement, for use as part of a key in WholeProgramInferenceScenesStorage.AnnotationsInContexts.
      Parameters:
      aType - an ATypeElement to convert to a string representation
      Returns:
      a string representation of the argument