Package org.checkerframework.common.wholeprograminference

Interface WholeProgramInference

All Known Implementing Classes:
WholeProgramInferenceImplementation
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

  • Method Details

    • updateFromObjectCreation

      void updateFromObjectCreation(ObjectCreationNode objectCreationNode, ExecutableElement constructorElt, CFAbstractStore<?,?> store)
      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
      store - the store just before the call

    • updateFromMethodInvocation

      void updateFromMethodInvocation(MethodInvocationNode methodInvNode, ExecutableElement methodElt, CFAbstractStore<?,?> store)
      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
      methodElt - the element of the method being invoked
      store - the store before the method call, used for inferring method preconditions

    • updateFromOverride

      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.

      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

    • updateFromFormalParameterAssignment

      void updateFromFormalParameterAssignment(LocalVariableNode lhs, Node rhs, VariableElement paramElt)
      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 formal parameter
      rhs - the node being assigned to the parameter in the method body
      paramElt - the formal parameter

    • updateFromFieldAssignment

      void updateFromFieldAssignment(Node field, Node rhs)
      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

    • updateFieldFromType

      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. See more details at updateFromFieldAssignment(org.checkerframework.dataflow.cfg.node.Node, org.checkerframework.dataflow.cfg.node.Node).
      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

    • updateFromReturn

      void updateFromReturn(ReturnNode retNode, com.sun.tools.javac.code.Symbol.ClassSymbol classSymbol, MethodTree methodTree, Map<AnnotatedTypeMirror.AnnotatedDeclaredType,ExecutableElement> overriddenMethods)
      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

    • updateContracts

      void updateContracts(Analysis.BeforeOrAfter preOrPost, ExecutableElement methodElement, CFAbstractStore<?,?> store)
      Updates the preconditions or postconditions of the current method, from a store.
      Parameters:
      methodElement - the method or constructor whose preconditions or postconditions to update
      preOrPost - whether to update preconditions or postconditions
      store - the store at the method's entry or normal exit, for reading types of expressions

    • updateAtmWithLub

      void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMirror ajavaATM)
      Updates sourceCodeATM to contain the LUB between sourceCodeATM and ajavaATM, ignoring missing AnnotationMirrors from ajavaATM -- it considers the LUB between an AnnotationMirror am and a missing AnnotationMirror to be am. The results are stored in sourceCodeATM.
      Parameters:
      sourceCodeATM - the annotated type on the source code; side effected by this method
      ajavaATM - the annotated type on the annotation file

    • 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

    • addMethodDeclarationAnnotation

      void addMethodDeclarationAnnotation(ExecutableElement elt, AnnotationMirror anno, boolean lubPurity)
      Updates a method to add a declaration annotation. Optionally, may replace the current purity annotation on elt with the logical least upper bound between that purity annotation and anno, if anno is also a purity annotation.
      Parameters:
      elt - the method to annotate
      anno - the declaration annotation to add to the method
      lubPurity - if true and anno is a purity annotation, replaces the current purity annotation with a least upper bound rather than just adding anno

    • addFieldDeclarationAnnotation

      void addFieldDeclarationAnnotation(VariableElement fieldElt, AnnotationMirror anno)
      Updates a field to add a declaration annotation.
      Parameters:
      fieldElt - the field to annotate
      anno - the declaration annotation to add to the field

    • addDeclarationAnnotationToFormalParameter

      void addDeclarationAnnotationToFormalParameter(ExecutableElement methodElt, int index, AnnotationMirror anno)
      Adds a declaration annotation to a formal parameter.
      Parameters:
      methodElt - the method whose formal parameter will be annotated
      index - the index of the parameter (0-indexed)
      anno - the annotation to add

    • addClassDeclarationAnnotation

      void addClassDeclarationAnnotation(TypeElement classElt, AnnotationMirror anno)
      Adds an annotation to a class declaration.
      Parameters:
      classElt - the class declaration to annotate
      anno - the annotation to add

    • 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 annotation files

    • preprocessClassTree

      void preprocessClassTree(ClassTree classTree)
      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.
      Parameters:
      classTree - the class to preprocess