| package org.checkerframework.common.wholeprograminference; |
| |
| import com.sun.source.tree.ClassTree; |
| import com.sun.source.tree.MethodTree; |
| import com.sun.source.tree.Tree; |
| import com.sun.tools.javac.code.Symbol.ClassSymbol; |
| import java.util.Map; |
| import javax.lang.model.element.AnnotationMirror; |
| import javax.lang.model.element.Element; |
| import javax.lang.model.element.ExecutableElement; |
| import javax.lang.model.element.VariableElement; |
| import org.checkerframework.common.basetype.BaseTypeChecker; |
| import org.checkerframework.dataflow.analysis.Analysis; |
| import org.checkerframework.dataflow.cfg.node.LocalVariableNode; |
| import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; |
| import org.checkerframework.dataflow.cfg.node.Node; |
| import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; |
| import org.checkerframework.dataflow.cfg.node.ReturnNode; |
| import org.checkerframework.framework.flow.CFAbstractStore; |
| import org.checkerframework.framework.qual.IgnoreInWholeProgramInference; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; |
| |
| /** |
| * 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 {@code WholeProgramInference} is misleading. |
| * |
| * <p>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. |
| * |
| * @checker_framework.manual #whole-program-inference Whole-program inference |
| */ |
| public interface WholeProgramInference { |
| |
| /** |
| * Updates the parameter types of the constructor {@code constructorElt} based on the arguments in |
| * {@code objectCreationNode}. |
| * |
| * <p>For each parameter in constructorElt: |
| * |
| * <ul> |
| * <li>If there is no stored annotated type for that parameter, then use the type of the |
| * corresponding argument in the object creation call objectCreationNode. |
| * <li>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. |
| * </ul> |
| * |
| * @param objectCreationNode the Node that invokes the constructor |
| * @param constructorElt the Element of the constructor |
| * @param store the store just before the call |
| */ |
| void updateFromObjectCreation( |
| ObjectCreationNode objectCreationNode, |
| ExecutableElement constructorElt, |
| CFAbstractStore<?, ?> store); |
| |
| /** |
| * Updates the parameter types of the method {@code methodElt} based on the arguments in the |
| * method invocation {@code methodInvNode}. |
| * |
| * <p>For each formal parameter in methodElt (including the receiver): |
| * |
| * <ul> |
| * <li>If there is no stored annotated type for that parameter, then use the type of the |
| * corresponding argument in the method call methodInvNode. |
| * <li>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. |
| * </ul> |
| * |
| * @param methodInvNode the node representing a method invocation |
| * @param methodElt the element of the method being invoked |
| * @param store the store before the method call, used for inferring method preconditions |
| */ |
| void updateFromMethodInvocation( |
| MethodInvocationNode methodInvNode, ExecutableElement methodElt, CFAbstractStore<?, ?> store); |
| |
| /** |
| * Updates the parameter types (including the receiver) of the method {@code methodTree} based on |
| * the parameter types of the overridden method {@code overriddenMethod}. |
| * |
| * <p>For each formal parameter in methodElt: |
| * |
| * <ul> |
| * <li>If there is no stored annotated type for that parameter, then use the type of the |
| * corresponding parameter on the overridden method. |
| * <li>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. |
| * </ul> |
| * |
| * @param methodTree the tree of the method that contains the parameter(s) |
| * @param methodElt the element of the method |
| * @param overriddenMethod the AnnotatedExecutableType of the overridden method |
| */ |
| void updateFromOverride( |
| MethodTree methodTree, ExecutableElement methodElt, AnnotatedExecutableType overriddenMethod); |
| |
| /** |
| * Updates the type of {@code lhs} based on an assignment of {@code rhs} to {@code lhs}. |
| * |
| * <ul> |
| * <li>If there is no stored annotated type for lhs, then use the type of the corresponding |
| * argument in the method call methodInvNode. |
| * <li>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. |
| * </ul> |
| * |
| * @param lhs the node representing the formal parameter |
| * @param rhs the node being assigned to the parameter in the method body |
| * @param paramElt the formal parameter |
| */ |
| void updateFromFormalParameterAssignment( |
| LocalVariableNode lhs, Node rhs, VariableElement paramElt); |
| |
| /** |
| * Updates the type of {@code field} based on an assignment of {@code rhs} to {@code field}. If |
| * the field has a declaration annotation with the {@link IgnoreInWholeProgramInference} |
| * meta-annotation, no type annotation will be inferred for that field. |
| * |
| * <p>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. |
| * |
| * @param field the field whose type will be refined. Must be either a FieldAccessNode or a |
| * LocalVariableNode whose element kind is FIELD. |
| * @param rhs the expression being assigned to the field |
| * @param classTree the ClassTree for the enclosing class of the assignment |
| */ |
| void updateFromFieldAssignment(Node field, Node rhs, ClassTree classTree); |
| |
| /** |
| * Updates the type of {@code field} based on an assignment whose right-hand side has type {@code |
| * rhsATM}. See more details at {@link #updateFromFieldAssignment}. |
| * |
| * @param lhsTree the tree for the field whose type will be refined |
| * @param element the element for the field whose type will be refined |
| * @param fieldName the name of the field whose type will be refined |
| * @param rhsATM the type of the expression being assigned to the field |
| */ |
| void updateFieldFromType( |
| Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM); |
| |
| /** |
| * Updates the return type of the method {@code methodTree} based on {@code returnedExpression}. |
| * Also updates the return types of any methods that this method overrides that are available as |
| * source code. |
| * |
| * <p>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. |
| * |
| * @param retNode the node that contains the expression returned |
| * @param classSymbol the symbol of the class that contains the method |
| * @param methodTree the tree of the method whose return type may be updated |
| * @param overriddenMethods the methods that the given method return overrides, indexed by the |
| * annotated type of the superclass in which each method is defined |
| */ |
| void updateFromReturn( |
| ReturnNode retNode, |
| ClassSymbol classSymbol, |
| MethodTree methodTree, |
| Map<AnnotatedDeclaredType, ExecutableElement> overriddenMethods); |
| |
| /** |
| * Updates the preconditions or postconditions of the current method, from a store. |
| * |
| * @param methodElement the method or constructor whose preconditions or postconditions to update |
| * @param preOrPost whether to update preconditions or postconditions |
| * @param store the store at the method's entry or normal exit, for reading types of expressions |
| */ |
| void updateContracts( |
| Analysis.BeforeOrAfter preOrPost, |
| ExecutableElement methodElement, |
| CFAbstractStore<?, ?> store); |
| |
| /** |
| * Updates a method to add a declaration annotation. |
| * |
| * @param methodElt the method to annotate |
| * @param anno the declaration annotation to add to the method |
| */ |
| void addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno); |
| |
| /** |
| * 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. |
| * |
| * @param format the file format in which to write the results |
| * @param checker the checker from which this method is called, for naming stub files |
| */ |
| void writeResultsToFile(OutputFormat format, BaseTypeChecker checker); |
| |
| /** |
| * Performs any preparation required for inference on Elements of a class. Should be called on |
| * each toplevel class declaration in a compilation unit before processing it. |
| * |
| * @param classTree the class to preprocess |
| */ |
| void preprocessClassTree(ClassTree classTree); |
| |
| /** The kinds of output that whole-program inference can produce. */ |
| enum OutputFormat { |
| /** |
| * Output the results of whole-program inference as a stub file that can be parsed back into the |
| * Checker Framework by the Stub Parser. |
| */ |
| STUB(), |
| |
| /** |
| * Output the results of whole-program inference as a Java annotation index file. The Annotation |
| * File Utilities project contains code for reading and writing .jaif files. |
| */ |
| JAIF(), |
| |
| /** |
| * Output the results of whole-program inference as an ajava file that can be read in using the |
| * -Aajava option. |
| */ |
| AJAVA(), |
| } |
| } |