Package org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceJavaParserStorage

java.lang.Object

org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage

All Implemented Interfaces:

WholeProgramInferenceStorage<AnnotatedTypeMirror>

public class WholeProgramInferenceJavaParserStorage
extends Object
implements WholeProgramInferenceStorage<AnnotatedTypeMirror>

This is an implementation of WholeProgramInferenceStorage that stores annotations directly with the JavaParser node corresponding to the annotation's location. It outputs ajava files.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
class	WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos	Stores the JavaParser node for a method or constructor and the annotations that have been inferred about its parameters and return type.

Field Summary

Fields

Modifier and Type	Field	Description
static final File	AJAVA_FILES_PATH	Directory where .ajava files will be written to and read from.
protected final AnnotatedTypeFactory	atypeFactory	The type factory associated with this.
protected final Elements	elements	The element utilities for atypeFactory.

Constructor Summary

Constructors

Constructor	Description
WholeProgramInferenceJavaParserStorage(AnnotatedTypeFactory atypeFactory, boolean inferOutputOriginal)	Constructs a new WholeProgramInferenceJavaParser that has not yet inferred any annotations.

Method Summary

Modifier and Type	Method	Description
boolean	addClassDeclarationAnnotation(TypeElement classElt, AnnotationMirror anno)	Adds an annotation to a class declaration.
boolean	addDeclarationAnnotationToFormalParameter(ExecutableElement methodElt, @org.checkerframework.checker.index.qual.Positive int index_1based, AnnotationMirror anno)	Adds a declaration annotation to a formal parameter.
boolean	addFieldDeclarationAnnotation(VariableElement field, 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, AnnotatedTypeMirror storageLocation)	Obtain the type from a storage location.
@Nullable AnnotatedTypeMirror	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.
static Set<String>	getInvisibleQualifierNames(AnnotatedTypeFactory atypeFactory)	Returns the names of all qualifiers that are marked with InvisibleQualifier, and that are supported by the given type factory.
AnnotationMirrorSet	getMethodDeclarationAnnotations(ExecutableElement methodElt)	Return the list of declaration annotations inferred on the given method so far in this round of WPI.
AnnotatedTypeMirror	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.
AnnotatedTypeMirror	getPreOrPostconditions(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElement, String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atypeFactory)	Returns the pre- or postcondition annotations for an expression.
AnnotatedTypeMirror	getReceiverAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror paramATM, AnnotatedTypeFactory atypeFactory)	Get the annotations for the receiver type.
AnnotatedTypeMirror	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.
static boolean	isInvisible(Class<? extends Annotation> qual)	Is the definition of the given annotation class annotated with InvisibleQualifier?
void	preprocessClassTree(ClassTree classTree)	Performs any preparation required for inference on the elements of a class.
boolean	removeMethodDeclarationAnnotation(ExecutableElement elt, AnnotationMirror anno)	Removes the given annotation from the given method element's inferred declaration annotation.
void	setFileModified(String path)	Indicates that inferred annotations for the file at path have changed since last written.
void	setSupertypesAndSubtypesModified()	For every modified file, consider its subclasses and superclasses modified, too.
void	updateStorageLocationFromAtm(AnnotatedTypeMirror newATM, AnnotatedTypeMirror curATM, AnnotatedTypeMirror typeToUpdate, TypeUseLocation defLoc, boolean ignoreIfAnnotated)	Updates a storage location to have the annotations of the given AnnotatedTypeMirror.
void	wpiPrepareClassForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.ClassOrInterfaceAnnos classAnnos, Collection<@BinaryName String> supertypes, Collection<@BinaryName String> subtypes)	Side-effects the class annotations to make any desired changes before writing to a file.
void	wpiPrepareCompilationUnitForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.CompilationUnitAnnos compilationUnitAnnos)	Side-effects the compilation unit annotations to make any desired changes before writing to a file.
void	wpiPrepareMethodForWriting(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos methodAnnos, Collection<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos> inSupertypes, Collection<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos> inSubtypes)	Side-effects the method or constructor annotations to make any desired changes before writing to a file.
void	writeResultsToFile(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker)	Writes the inferred results to a file.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

AJAVA_FILES_PATH

public static final File AJAVA_FILES_PATH

Directory where .ajava files will be written to and read from. This directory is relative to where the javac command is executed.

atypeFactory

protected final AnnotatedTypeFactory atypeFactory

The type factory associated with this.

elements

protected final Elements elements

The element utilities for atypeFactory.

Constructor Details

WholeProgramInferenceJavaParserStorage

public WholeProgramInferenceJavaParserStorage(AnnotatedTypeFactory atypeFactory,
 boolean inferOutputOriginal)

Constructs a new WholeProgramInferenceJavaParser that has not yet inferred any annotations.

Parameters:

atypeFactory - the associated type factory

inferOutputOriginal - whether the -AinferOutputOriginal option was supplied to the checker

Method Details

getInvisibleQualifierNames

public static Set<String> getInvisibleQualifierNames(AnnotatedTypeFactory atypeFactory)

Returns the names of all qualifiers that are marked with InvisibleQualifier, and that are supported by the given type factory.

Parameters:

atypeFactory - a type factory

Returns:

the names of every invisible qualifier supported by atypeFactory

isInvisible

@Pure
public static boolean isInvisible(Class<? extends Annotation> qual)

Is the definition of the given annotation class annotated with InvisibleQualifier?

Parameters:

qual - an annotation class

Returns:

true iff qual is meta-annotated with InvisibleQualifier

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<AnnotatedTypeMirror>

Parameters:

elt - an element

Returns:

the path to the file where inference results for the element will be written

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<AnnotatedTypeMirror>

Parameters:

path - path to the file with annotations that have been modified

setSupertypesAndSubtypesModified

public void setSupertypesAndSubtypesModified()

For every modified file, consider its subclasses and superclasses modified, too. The reason is that an annotation change in a class might require annotations in its superclasses and supclasses to be modified, in order to preserve behavioral subtyping. Setting it modified will cause it to be written out, and while writing out, the annotations will be made consistent across the class hierarchy by wpiPrepareCompilationUnitForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.CompilationUnitAnnos).

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<AnnotatedTypeMirror>

Parameters:

methodElt - a method or constructor Element

Returns:

true if the storage has a method corresponding to elt

getMethodDeclarationAnnotations

public AnnotationMirrorSet getMethodDeclarationAnnotations(ExecutableElement methodElt)

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<AnnotatedTypeMirror>

Parameters:

methodElt - a method

Returns:

the declaration annotations inferred on elt so far (may be empty)

getParameterAnnotations

public AnnotatedTypeMirror getParameterAnnotations(ExecutableElement methodElt,
 @org.checkerframework.checker.index.qual.Positive int index_1based,
 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<AnnotatedTypeMirror>

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

public AnnotatedTypeMirror 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<AnnotatedTypeMirror>

Parameters:

methodElt - the method or constructor Element

paramATM - the receiver type

atypeFactory - the type factory

Returns:

the annotations for the receiver type

getReturnAnnotations

public AnnotatedTypeMirror 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<AnnotatedTypeMirror>

Parameters:

methodElt - the method or constructor Element

atm - the return type

atypeFactory - the type factory

Returns:

the annotations for the return type

getFieldAnnotations

public @Nullable AnnotatedTypeMirror 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<AnnotatedTypeMirror>

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 AnnotatedTypeMirror 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<AnnotatedTypeMirror>

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

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<AnnotatedTypeMirror>

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

removeMethodDeclarationAnnotation

public boolean removeMethodDeclarationAnnotation(ExecutableElement elt,
 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<AnnotatedTypeMirror>

Parameters:

elt - 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)

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<AnnotatedTypeMirror>

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,
 @org.checkerframework.checker.index.qual.Positive int index_1based,
 AnnotationMirror anno)

Description copied from interface: WholeProgramInferenceStorage

Adds a declaration annotation to a formal parameter.

Specified by:

addDeclarationAnnotationToFormalParameter in interface WholeProgramInferenceStorage<AnnotatedTypeMirror>

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

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<AnnotatedTypeMirror>

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

public AnnotatedTypeMirror atmFromStorageLocation(TypeMirror typeMirror,
 AnnotatedTypeMirror storageLocation)

Description copied from interface: WholeProgramInferenceStorage

Obtain the type from a storage location.

Specified by:

atmFromStorageLocation in interface WholeProgramInferenceStorage<AnnotatedTypeMirror>

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,
 AnnotatedTypeMirror 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<AnnotatedTypeMirror>

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

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<AnnotatedTypeMirror>

Parameters:

classTree - the class to preprocess

wpiPrepareCompilationUnitForWriting

public void wpiPrepareCompilationUnitForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.CompilationUnitAnnos 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.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.ClassOrInterfaceAnnos classAnnos,
 Collection<@BinaryName String> supertypes,
 Collection<@BinaryName String> subtypes)

Side-effects the class annotations to make any desired changes before writing to a file.

Because of the side effect, clients may want to pass a copy into this method.

Parameters:

classAnnos - the class annotations to modify

supertypes - the binary names of all supertypes; not side-effected

subtypes - the binary names of all subtypes; not side-effected

wpiPrepareMethodForWriting

public void wpiPrepareMethodForWriting(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos methodAnnos,
 Collection<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos> inSupertypes,
 Collection<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos> inSubtypes)

Side-effects the method or constructor annotations to make any desired changes before writing to a file. For example, this method may make inferred annotations consistent with one another between superclasses and subclasses.

Parameters:

methodAnnos - the method or constructor annotations to modify

inSupertypes - the method or constructor annotations for all overridden methods; not side-effected

inSubtypes - the method or constructor annotations for all overriding methods; not side-effected

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<AnnotatedTypeMirror>

Parameters:

outputFormat - the file format in which to write the results

checker - the checker from which this method is called, for naming annotation files