org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceScenes

java.lang.Object

org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenes

All Implemented Interfaces:

WholeProgramInference

public class WholeProgramInferenceScenes
extends Object
implements WholeProgramInference

WholeProgramInferenceScenes is an implementation of WholeProgramInference.

Its file format is .jaif files.

It stores annotations using the storage class (WholeProgramInferenceScenesStorage).

Calling an update* method replaces the currently-stored type for an element in a AScene, if any, by the LUB of it and the update method's argument.

This class does not perform inference for an element if the element has explicit annotations: calling an update* method on an explicitly annotated field, method return, or method parameter has no effect.

In addition, whole program inference ignores inferred types in a few scenarios. When discovering a use, if:

1. The inferred type of an element that should be written into a .jaif file is a subtype of the upper bounds of this element's currently-written type on the source code.
2. The annotation annotates a null literal, except when doing inference for the NullnessChecker. (The rationale for this is that null is a frequently-used default value, and it would be undesirable to compute any inferred type if null were the only value passed as an argument.)

When outputting a .jaif file, if:

1. The @Target annotation does not permit the annotation to be written at this location.
2. The inferred annotation has the @InvisibleQualifier meta-annotation.
3. The inferred annotation would be the same annotation applied via defaulting — that is, if omitting it has the same effect as writing it.

Nested Class Summary

Nested classes/interfaces inherited from interface org.checkerframework.common.wholeprograminference.WholeProgramInference

WholeProgramInference.OutputFormat

Field Summary

Fields

Modifier and Type	Field and Description
protected AnnotatedTypeFactory	atypeFactory The type factory associated with this.
protected WholeProgramInferenceScenesStorage	storage This stores the inferred annotations.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
void	addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno) Updates a method to add a declaration annotation.
AnnotatedTypeMirror	atmFromATypeElement(TypeMirror typeMirror, scenelib.annotations.el.ATypeElement type) Obtain the type from an ATypeElement (which is part of a Scene).
protected boolean	ignoreFieldInWPI(Element element, String fieldName) Returns true if an assignment to the given field should be ignored by WPI.
void	prepareClassForWriting(scenelib.annotations.el.AClass classAnnos) Side-effects the class annotations to make any desired changes before writing to a file.
void	prepareMethodForWriting(scenelib.annotations.el.AMethod methodAnnos) Side-effects the method or constructor annotations to make any desired changes before writing to a file.
void	prepareSceneForWriting(scenelib.annotations.el.AScene compilationUnitAnnos) Side-effects the compilation unit annotations to make any desired changes before writing to a file.
protected void	updateAnnotationSet(scenelib.annotations.el.ATypeElement typeToUpdate, TypeUseLocation defLoc, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, String file) Updates the set of annotations in a location in a program.
protected void	updateAnnotationSet(scenelib.annotations.el.ATypeElement typeToUpdate, TypeUseLocation defLoc, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, String file, boolean ignoreIfAnnotated) Updates the set of annotations in a location in a program.
void	updateContracts(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElt, CFAbstractStore<?,?> store) Updates the preconditions or postconditions of the current method, from a store.
void	updateFieldFromType(Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM) Updates the type of field based on an assignment whose right-hand side has type rhsATM.
void	updateFromFieldAssignment(Node lhs, Node rhs, ClassTree classTree) Updates the type of field based on an assignment of rhs to field.
void	updateFromFormalParameterAssignment(LocalVariableNode lhs, Node rhs, VariableElement paramElt) Updates the type of lhs based on an assignment of rhs to lhs.
void	updateFromMethodInvocation(MethodInvocationNode methodInvNode, Tree receiverTree, ExecutableElement methodElt, CFAbstractStore<?,?> store) Updates the parameter types of the method methodElt based on the arguments in the method invocation methodInvNode.
void	updateFromObjectCreation(ObjectCreationNode objectCreationNode, ExecutableElement constructorElt, CFAbstractStore<?,?> store) Updates the parameter types of the constructor constructorElt based on the arguments in objectCreationNode.
void	updateFromOverride(MethodTree methodTree, ExecutableElement methodElt, AnnotatedTypeMirror.AnnotatedExecutableType overriddenMethod) Updates the parameter types (including the receiver) of the method methodTree based on the parameter types of the overridden method overriddenMethod.
void	updateFromReturn(ReturnNode retNode, com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol, MethodTree methodDeclTree, Map<AnnotatedTypeMirror.AnnotatedDeclaredType,ExecutableElement> overriddenMethods) Updates the return type of the method methodDeclTree in the Scene of the class with symbol classSymbol.
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

atypeFactory

protected final AnnotatedTypeFactory atypeFactory

The type factory associated with this.

storage

protected final WholeProgramInferenceScenesStorage storage

This stores the inferred annotations.

Constructor Detail

WholeProgramInferenceScenes

public WholeProgramInferenceScenes(AnnotatedTypeFactory atypeFactory)

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

Parameters:

atypeFactory - the associated type factory

Method Detail

updateFromObjectCreation

public void updateFromObjectCreation(ObjectCreationNode objectCreationNode,
                                     ExecutableElement constructorElt,
                                     CFAbstractStore<?,?> store)

Description copied from interface: WholeProgramInference

Updates the parameter types of the constructor constructorElt based on the arguments in objectCreationNode.

For each parameter in constructorElt:

• If there is no stored annotated type for that parameter, then use the type of the corresponding argument in the object creation call objectCreationNode.
• If there was a stored annotated type for that parameter, then its new type will be the LUB between the previous type and the type of the corresponding argument in the object creation call.

Specified by:

updateFromObjectCreation in interface WholeProgramInference

Parameters:

objectCreationNode - the Node that invokes the constructor

constructorElt - the Element of the constructor

store - the store just before the call

updateFromMethodInvocation

public void updateFromMethodInvocation(MethodInvocationNode methodInvNode,
                                       Tree receiverTree,
                                       ExecutableElement methodElt,
                                       CFAbstractStore<?,?> store)

Description copied from interface: WholeProgramInference

Updates the parameter types of the method methodElt based on the arguments in the method invocation methodInvNode.

For each formal parameter in methodElt (including the receiver):

• If there is no stored annotated type for that parameter, then use the type of the corresponding argument in the method call methodInvNode.
• If there was a stored annotated type for that parameter, then its new type will be the LUB between the previous type and the type of the corresponding argument in the method call.

Specified by:

updateFromMethodInvocation in interface WholeProgramInference

Parameters:

methodInvNode - the node representing a method invocation

receiverTree - the Tree of the class that contains the method being invoked

methodElt - the element of the method being invoked

store - the store before the method call, used for inferring method preconditions

updateContracts

public void updateContracts(Analysis.BeforeOrAfter preOrPost,
                            ExecutableElement methodElt,
                            CFAbstractStore<?,?> store)

Description copied from interface: WholeProgramInference

Updates the preconditions or postconditions of the current method, from a store.

Specified by:

updateContracts in interface WholeProgramInference

Parameters:

preOrPost - whether to update preconditions or postconditions

methodElt - the method or constructor whose preconditions or postconditions to update

store - the store at the method's entry or normal exit, for reading types of expressions

updateFromOverride

public void updateFromOverride(MethodTree methodTree,
                               ExecutableElement methodElt,
                               AnnotatedTypeMirror.AnnotatedExecutableType overriddenMethod)

Description copied from interface: WholeProgramInference

Updates the parameter types (including the receiver) of the method methodTree based on the parameter types of the overridden method overriddenMethod.

For each formal parameter in methodElt:

• If there is no stored annotated type for that parameter, then use the type of the corresponding parameter on the overridden method.
• If there is a stored annotated type for that parameter, then its new type will be the LUB between the previous type and the type of the corresponding parameter on the overridden method.

Specified by:

updateFromOverride in interface WholeProgramInference

Parameters:

methodTree - the tree of the method that contains the parameter(s)

methodElt - the element of the method

overriddenMethod - the AnnotatedExecutableType of the overridden method

updateFromFormalParameterAssignment

public void updateFromFormalParameterAssignment(LocalVariableNode lhs,
                                                Node rhs,
                                                VariableElement paramElt)

Description copied from interface: WholeProgramInference

Updates the type of lhs based on an assignment of rhs to lhs.

• If there is no stored annotated type for lhs, then use the type of the corresponding argument in the method call methodInvNode.
• If there is a stored annotated type for lhs, then its new type will be the LUB between the previous type and the type of the corresponding argument in the method call.

Specified by:

updateFromFormalParameterAssignment in interface WholeProgramInference

Parameters:

lhs - the node representing the formal parameter

rhs - the node being assigned to the parameter in the method body

paramElt - the formal parameter

updateFromFieldAssignment

public void updateFromFieldAssignment(Node lhs,
                                      Node rhs,
                                      ClassTree classTree)

Description copied from interface: WholeProgramInference

Updates the type of field based on an assignment of rhs to field. If the field has a declaration annotation with the IgnoreInWholeProgramInference meta-annotation, no type annotation will be inferred for that field.

If there is no stored entry for the field lhs, the entry will be created and its type will be the type of rhs. If there is a stored entry/type for lhs, its new type will be the LUB between the previous type and the type of rhs.

Specified by:

updateFromFieldAssignment in interface WholeProgramInference

Parameters:

lhs - the field whose type will be refined. Must be either a FieldAccessNode or a LocalVariableNode whose element kind is FIELD.

rhs - the expression being assigned to the field

classTree - the ClassTree for the enclosing class of the assignment

updateFieldFromType

public void updateFieldFromType(Tree lhsTree,
                                Element element,
                                String fieldName,
                                AnnotatedTypeMirror rhsATM)

Description copied from interface: WholeProgramInference

Updates the type of field based on an assignment whose right-hand side has type rhsATM. See more details at WholeProgramInference.updateFromFieldAssignment(org.checkerframework.dataflow.cfg.node.Node, org.checkerframework.dataflow.cfg.node.Node, com.sun.source.tree.ClassTree).

Specified by:

updateFieldFromType in interface WholeProgramInference

Parameters:

lhsTree - the tree for the field whose type will be refined

element - the element for the field whose type will be refined

fieldName - the name of the field whose type will be refined

rhsATM - the type of the expression being assigned to the field

ignoreFieldInWPI

protected boolean ignoreFieldInWPI(Element element,
                                   String fieldName)

Returns true if an assignment to the given field should be ignored by WPI.

Parameters:

element - the field's element

fieldName - the field's name

Returns:

true if an assignment to the given field should be ignored by WPI

updateFromReturn

public void updateFromReturn(ReturnNode retNode,
                             com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol,
                             MethodTree methodDeclTree,
                             Map<AnnotatedTypeMirror.AnnotatedDeclaredType,ExecutableElement> overriddenMethods)

Updates the return type of the method methodDeclTree in the Scene of the class with symbol classSymbol. Also updates the return types of methods that this method overrides, if they are available as source.

If the Scene does not contain an annotated return type for the method methodDeclTree, then the type of the value passed to the return expression will be added to the return type of that method in the Scene. If the Scene previously contained an annotated return type for the method methodDeclTree, its new type will be the LUB between the previous type and the type of the value passed to the return expression.

Specified by:

updateFromReturn in interface WholeProgramInference

Parameters:

retNode - the node that contains the expression returned

classSymbol - the symbol of the class that contains the method

methodDeclTree - the declaration of the method whose return type may be updated

overriddenMethods - the methods that the given method return overrides, each indexed by the annotated type of the class that defines it

addMethodDeclarationAnnotation

public void addMethodDeclarationAnnotation(ExecutableElement methodElt,
                                           AnnotationMirror anno)

Description copied from interface: WholeProgramInference

Updates a method to add a declaration annotation.

Specified by:

addMethodDeclarationAnnotation in interface WholeProgramInference

Parameters:

methodElt - the method to annotate

anno - the declaration annotation to add to the method

updateAnnotationSet

protected final void updateAnnotationSet(scenelib.annotations.el.ATypeElement typeToUpdate,
                                         TypeUseLocation defLoc,
                                         AnnotatedTypeMirror rhsATM,
                                         AnnotatedTypeMirror lhsATM,
                                         String file)

Updates the set of annotations in a location in a program.

Parameters:

typeToUpdate - the type whose annotations are modified by this method

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

file - path to the annotation file containing the executable; used for marking the scene as modified (needing to be written to disk)

updateAnnotationSet

protected void updateAnnotationSet(scenelib.annotations.el.ATypeElement typeToUpdate,
                                   TypeUseLocation defLoc,
                                   AnnotatedTypeMirror rhsATM,
                                   AnnotatedTypeMirror lhsATM,
                                   String file,
                                   boolean ignoreIfAnnotated)

Updates the set of annotations in a location in a program.

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

Subclasses can customize its behavior.

Parameters:

typeToUpdate - the type whose annotations are modified by this method

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

file - path to the annotation file containing the executable; 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

atmFromATypeElement

public AnnotatedTypeMirror atmFromATypeElement(TypeMirror typeMirror,
                                               scenelib.annotations.el.ATypeElement type)

Obtain the type from an ATypeElement (which is part of a Scene).

Parameters:

typeMirror - the underlying type for the result

type - the ATypeElement from which to obtain annotations

Returns:

an annotated type mirror with underlying type typeMirror and annotations from type

prepareSceneForWriting

public void prepareSceneForWriting(scenelib.annotations.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

prepareClassForWriting

public void prepareClassForWriting(scenelib.annotations.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

prepareMethodForWriting

public void prepareMethodForWriting(scenelib.annotations.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: WholeProgramInference

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 WholeProgramInference

Parameters:

outputFormat - the file format in which to write the results

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