org.checkerframework.common.wholeprograminference

Interface WholeProgramInference

All Known Implementing Classes:

WholeProgramInferenceScenes

public interface WholeProgramInference

Interface for recording facts at (pseudo-)assignments. It is used by the -Ainfer command-line argument. The -Ainfer command-line argument is used by the whole-program-inference loop, but this class does not implement that loop and its name WholeProgramInference is misleading.

This interface has update* methods that should be called at certain (pseudo-)assignments, and they may update the type of the LHS of the (pseudo-)assignment based on the type of the RHS. In case the element on the LHS already had an inferred type, its new type will be the LUB between the previous and new types.

See the Checker Framework Manual:

Whole-program inference

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	WholeProgramInference.OutputFormat The kinds of output that whole-program inference can produce.

Method Summary

Modifier and Type	Method and Description
void	addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno) Updates a method to add a declaration annotation.
void	updateFromFieldAssignment(Node field, Node rhs, ClassTree classTree, AnnotatedTypeFactory atf) Updates the type of field based on an assignment of rhs to field.
void	updateFromLocalAssignment(LocalVariableNode lhs, Node rhs, ClassTree classTree, MethodTree methodTree, AnnotatedTypeFactory atf) Updates the type of lhs based on an assignment of rhs to lhs.
void	updateFromMethodInvocation(MethodInvocationNode methodInvNode, Tree receiverTree, ExecutableElement methodElt, AnnotatedTypeFactory atf) Updates the parameter types of the method methodElt based on the arguments in the method invocation methodInvNode.
void	updateFromObjectCreation(ObjectCreationNode objectCreationNode, ExecutableElement constructorElt, AnnotatedTypeFactory atf) Updates the parameter types of the constructor constructorElt based on the arguments in objectCreationNode.
void	updateFromOverride(MethodTree methodTree, ExecutableElement methodElt, AnnotatedTypeMirror.AnnotatedExecutableType overriddenMethod, AnnotatedTypeFactory atf) 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 methodTree, Map<AnnotatedTypeMirror.AnnotatedDeclaredType,ExecutableElement> overriddenMethods, AnnotatedTypeFactory atf) Updates the return type of the method methodTree based on returnedExpression.
void	writeResultsToFile(WholeProgramInference.OutputFormat format, BaseTypeChecker checker) Writes the inferred results to a file.

Method Detail

updateFromObjectCreation

void updateFromObjectCreation(ObjectCreationNode objectCreationNode,
                              ExecutableElement constructorElt,
                              AnnotatedTypeFactory atf)

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.

Parameters:

objectCreationNode - the Node that invokes the constructor

constructorElt - the Element of the constructor

atf - the annotated type factory of a given type system, whose type hierarchy will be used to update the constructor's parameters' types

updateFromMethodInvocation

void updateFromMethodInvocation(MethodInvocationNode methodInvNode,
                                Tree receiverTree,
                                ExecutableElement methodElt,
                                AnnotatedTypeFactory atf)

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.

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

atf - the annotated type factory of a given type system, whose type hierarchy will be used to update the method parameters' types

updateFromOverride

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

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.

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

atf - the annotated type factory of a given type system, whose type hierarchy will be used to update the parameter type

updateFromLocalAssignment

void updateFromLocalAssignment(LocalVariableNode lhs,
                               Node rhs,
                               ClassTree classTree,
                               MethodTree methodTree,
                               AnnotatedTypeFactory atf)

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.

Parameters:

lhs - the node representing the local variable, such as a formal parameter

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

classTree - the tree of the class that contains the parameter

methodTree - the tree of the method that contains the parameter

atf - the annotated type factory of a given type system, whose type hierarchy will be used to update the parameter type

updateFromFieldAssignment

void updateFromFieldAssignment(Node field,
                               Node rhs,
                               ClassTree classTree,
                               AnnotatedTypeFactory atf)

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.

Parameters:

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

atf - the annotated type factory of a given type system, whose type hierarchy will be used to update the field's type

updateFromReturn

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

Updates the return type of the method methodTree based on returnedExpression. Also updates the return types of any methods that this method overrides that are available as source code.

If there is no stored annotated return type for the method methodTree, then the type of the return expression will be added to the return type of that method. If there is a stored annotated return type for the method methodTree, its new type will be the LUB between the previous type and the type of the return expression.

Parameters:

retNode - the node that contains the expression returned

classSymbol - the symbol of the class that contains the method

methodTree - the tree of the method whose return type may be updated

overriddenMethods - the methods that the given method return overrides, indexed by the annotated type of the superclass in which each method is defined

atf - the annotated type factory of a given type system, whose type hierarchy will be used to update the method's return type

addMethodDeclarationAnnotation

void 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

writeResultsToFile

void writeResultsToFile(WholeProgramInference.OutputFormat format,
                        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:

format - the file format in which to write the results

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