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 Summary

Modifier and Type	Method and Description
boolean	addClassDeclarationAnnotation(TypeElement classElt, AnnotationMirror anno) Adds an annotation to a class declaration.
boolean	addDeclarationAnnotationToFormalParameter(ExecutableElement methodElt, int index, AnnotationMirror anno) Adds a declaration annotation to a formal parameter.
boolean	addFieldDeclarationAnnotation(VariableElement fieldElt, AnnotationMirror anno) Updates a field to add a declaration annotation.
boolean	addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno) Updates a method to add a declaration annotation.
AnnotatedTypeMirror	atmFromStorageLocation(TypeMirror typeMirror, T storageLocation) Obtain the type from a storage location.
T	getFieldAnnotations(Element element, String fieldName, AnnotatedTypeMirror lhsATM, AnnotatedTypeFactory atypeFactory) Get the annotations for a field type.
String	getFileForElement(Element elt) Returns the file corresponding to the given element.
T	getParameterAnnotations(ExecutableElement methodElt, int i, AnnotatedTypeMirror paramATM, VariableElement ve, AnnotatedTypeFactory atypeFactory) Get the annotations for a formal parameter type.
T	getPreOrPostconditions(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElement, String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atypeFactory) Returns the pre- or postcondition annotations for an expression.
T	getReceiverAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror paramATM, AnnotatedTypeFactory atypeFactory) Get the annotations for the receiver type.
T	getReturnAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror atm, AnnotatedTypeFactory atypeFactory) Get the annotations for the return type.
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.
void	preprocessClassTree(ClassTree classTree) Performs any preparation required for inference on the elements of a class.
void	setFileModified(String path) Indicates that inferred annotations for the file at path have changed since last written.
void	updateStorageLocationFromAtm(AnnotatedTypeMirror newATM, AnnotatedTypeMirror curATM, T storageLocationToUpdate, TypeUseLocation defLoc, boolean ignoreIfAnnotated) Updates a storage location to have the annotations of the given AnnotatedTypeMirror.
void	writeResultsToFile(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker) Writes the inferred results to a file.

Method Detail

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,
                          int i,
                          AnnotatedTypeMirror paramATM,
                          VariableElement ve,
                          AnnotatedTypeFactory atypeFactory)

Get the annotations for a formal parameter type.

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

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

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,
                                                  int index,
                                                  AnnotationMirror anno)

Adds a declaration annotation to a formal parameter.

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

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

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