Package org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceScenesStorage

java.lang.Object

org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesStorage

All Implemented Interfaces:

WholeProgramInferenceStorage<ATypeElement>

public class WholeProgramInferenceScenesStorage
extends Object
implements WholeProgramInferenceStorage<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.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	WholeProgramInferenceScenesStorage.AnnotationsInContexts	Maps the aTypeElementToString(org.checkerframework.afu.scenelib.el.ATypeElement) representation of an ATypeElement and its TypeUseLocation to a set of names of annotations.

Field Summary

Fields

Modifier and Type	Field	Description
protected final AnnotatedTypeFactory	atypeFactory	The type factory associated with this WholeProgramInferenceScenesStorage.
static final String	JAIF_FILES_PATH	Directory where .jaif files will be written to and read from.
final Set<String>	modifiedScenes	Scenes that were modified since the last time all Scenes were written into .jaif files.
final Map<String,ASceneWrapper>	scenes	Maps .jaif file paths (Strings) to Scenes.

Constructor Summary

Constructors

Constructor	Description
WholeProgramInferenceScenesStorage(AnnotatedTypeFactory atypeFactory)	Default constructor.

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, ATypeElement storageLocation)	Obtain the type from a storage location.
static String	aTypeElementToString(ATypeElement aType)	Returns a string representation of an ATypeElement, for use as part of a key in WholeProgramInferenceScenesStorage.AnnotationsInContexts.
protected AClass	getAClass(@BinaryName String className, String jaifPath)	Returns the scene-lib representation of the given className in the scene identified by the given jaifPath.
protected 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.
ATypeElement	getFieldAnnotations(Element element, String fieldName, AnnotatedTypeMirror lhsATM, AnnotatedTypeFactory atypeFactory)	Returns the annotations for a field type.
String	getFileForElement(Element elt)	Returns the file corresponding to the given element.
protected String	getJaifPath(String className)	Returns the String representing the .jaif path of a class given its name.
AnnotationMirrorSet	getMethodDeclarationAnnotations(ExecutableElement elt)	Returns the list of declaration annotations inferred on the given method so far in this round of WPI.
ATypeElement	getParameterAnnotations(ExecutableElement methodElt, @org.checkerframework.checker.index.qual.Positive int index_1based, AnnotatedTypeMirror paramATM, VariableElement ve, AnnotatedTypeFactory atypeFactory)	Returns the annotations for a formal parameter type.
AnnotatedTypeMirror	getPostconditionDeclaredType(AMethod m, String expression)	Fetches the declared type of an expression for which a postcondition was inferred, for the given AMethod.
AnnotatedTypeMirror	getPreconditionDeclaredType(AMethod m, String expression)	Fetches the declared type of an expression for which a precondition was inferred, for the given AMethod.
ATypeElement	getPreOrPostconditions(String className, Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElement, String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atypeFactory)	Returns the pre- or postcondition annotations for an expression.
ATypeElement	getReceiverAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror paramATM, AnnotatedTypeFactory atypeFactory)	Returns the annotations for the receiver type.
ATypeElement	getReturnAnnotations(ExecutableElement methodElt, AnnotatedTypeMirror atm, AnnotatedTypeFactory atypeFactory)	Returns 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	prepareSceneForWriting(AScene compilationUnitAnnos)	Side-effects the compilation unit 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.
boolean	removeMethodDeclarationAnnotation(ExecutableElement methodElt, 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.
protected void	updateAnnotationSetInScene(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.
void	updateStorageLocationFromAtm(AnnotatedTypeMirror newATM, AnnotatedTypeMirror curATM, ATypeElement typeToUpdate, TypeUseLocation defLoc, boolean ignoreIfAnnotated)	Updates a storage location to have the annotations of the given AnnotatedTypeMirror.
void	wpiPrepareClassForWriting(AClass classAnnos)	Side-effects the class annotations to make any desired changes before writing to a file.
void	wpiPrepareMethodForWriting(String className, AMethod methodAnnos)	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.
void	writeScenes(WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker)	Write all modified scenes into files.

Methods inherited from class java.lang.Object

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

Field Details

JAIF_FILES_PATH

public static final String JAIF_FILES_PATH

Directory where .jaif files will be written to and read from. This directory is relative to where the CF's javac command is executed.

atypeFactory

protected final AnnotatedTypeFactory atypeFactory

The type factory associated with this WholeProgramInferenceScenesStorage.

scenes

public final Map<String,ASceneWrapper> scenes

Maps .jaif file paths (Strings) to Scenes. Relative to JAIF_FILES_PATH.

modifiedScenes

public final Set<String> modifiedScenes

Scenes that were modified since the last time all Scenes were written into .jaif files. Each String element of this set is a path (relative to JAIF_FILES_PATH) to the .jaif file of the corresponding Scene in the set. It is obtained by passing a class name as argument to the getJaifPath(java.lang.String) method.

Modifying a Scene means adding (or changing) a type annotation for a field, method return type, or method parameter type in the Scene. (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).)

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

Parameters:

methodElt - a method or constructor Element

Returns:

true if the storage has a method corresponding to elt

getParameterAnnotations

public ATypeElement getParameterAnnotations(ExecutableElement methodElt,
 @org.checkerframework.checker.index.qual.Positive int index_1based,
 AnnotatedTypeMirror paramATM,
 VariableElement ve,
 AnnotatedTypeFactory atypeFactory)

Description copied from interface: WholeProgramInferenceStorage

Returns the annotations for a formal parameter type.

Specified by:

getParameterAnnotations in interface WholeProgramInferenceStorage<ATypeElement>

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 ATypeElement getReceiverAnnotations(ExecutableElement methodElt,
 AnnotatedTypeMirror paramATM,
 AnnotatedTypeFactory atypeFactory)

Description copied from interface: WholeProgramInferenceStorage

Returns the annotations for the receiver type.

Specified by:

getReceiverAnnotations in interface WholeProgramInferenceStorage<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

Returns the list of declaration annotations inferred on the given method so far in this round of WPI.

Specified by:

getMethodDeclarationAnnotations in interface WholeProgramInferenceStorage<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<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 ATypeElement getReturnAnnotations(ExecutableElement methodElt,
 AnnotatedTypeMirror atm,
 AnnotatedTypeFactory atypeFactory)

Description copied from interface: WholeProgramInferenceStorage

Returns the annotations for the return type.

Specified by:

getReturnAnnotations in interface WholeProgramInferenceStorage<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 ATypeElement getFieldAnnotations(Element element,
 String fieldName,
 AnnotatedTypeMirror lhsATM,
 AnnotatedTypeFactory atypeFactory)

Description copied from interface: WholeProgramInferenceStorage

Returns the annotations for a field type.

Specified by:

getFieldAnnotations in interface WholeProgramInferenceStorage<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 ATypeElement getPreOrPostconditions(String className,
 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<ATypeElement>

Parameters:

className - the class that contains the method, for diagnostics only

preOrPost - true if 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(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(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<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<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,
 @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<ATypeElement>

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<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 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 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(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 - the ATypeElement of the Scene which will be modified

defLoc - the location where the annotation will be added

rhsATM - the RHS of the annotated type on the source code

lhsATM - the LHS of the annotated type on the source code

jaifPath - path to a .jaif file for a Scene; used for marking the scene as modified (needing to be written to disk)

ignoreIfAnnotated - if true, don't update any type that is explicitly annotated in the source code

atmFromStorageLocation

public AnnotatedTypeMirror atmFromStorageLocation(TypeMirror typeMirror,
 ATypeElement storageLocation)

Description copied from interface: WholeProgramInferenceStorage

Obtain the type from a storage location.

Specified by:

atmFromStorageLocation in interface WholeProgramInferenceStorage<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,
 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<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(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(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(String className,
 AMethod methodAnnos)

Side-effects the method or constructor annotations to make any desired changes before writing to a file.

Parameters:

className - the class that contains the method, for diagnostics only

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

Parameters:

classTree - the class to preprocess

aTypeElementToString

public static String aTypeElementToString(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