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 and 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 and Description
static String	AJAVA_FILES_PATH Directory where .ajava files will be written to and read from.
protected AnnotatedTypeFactory	atypeFactory The type factory associated with this.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
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.
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.
AnnotatedTypeMirror	getParameterAnnotations(ExecutableElement methodElt, int i, 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.
void	prepareClassForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.ClassOrInterfaceAnnos classAnnos) Side-effects the class annotations to make any desired changes before writing to a file.
void	prepareCompilationUnitForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.CompilationUnitAnnos compilationUnitAnnos) Side-effects the compilation unit annotations to make any desired changes before writing to a file.
void	prepareMethodForWriting(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos methodAnnos) Side-effects the method or constructor annotations to make any desired changes before writing to a file.
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, AnnotatedTypeMirror typeToUpdate, 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.

Methods inherited from class java.lang.Object

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

Field Detail

AJAVA_FILES_PATH

public static final String 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.

Constructor Detail

WholeProgramInferenceJavaParserStorage

public WholeProgramInferenceJavaParserStorage(AnnotatedTypeFactory atypeFactory)

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

Parameters:

atypeFactory - the associated type factory

Method Detail

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

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

getParameterAnnotations

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

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

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

prepareCompilationUnitForWriting

public void prepareCompilationUnitForWriting(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

prepareClassForWriting

public void prepareClassForWriting(org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.ClassOrInterfaceAnnos classAnnos)

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

Parameters:

classAnnos - the class annotations to modify

prepareMethodForWriting

public void prepareMethodForWriting(WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos 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<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