Package org.checkerframework.framework.flow

Class CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>

java.lang.Object
org.checkerframework.dataflow.analysis.AbstractAnalysis<V,S,T>
org.checkerframework.dataflow.analysis.ForwardAnalysisImpl<V,S,T>
org.checkerframework.framework.flow.CFAbstractAnalysis<V,S,T>
All Implemented Interfaces:
Analysis<V,S,T>, ForwardAnalysis<V,S,T>
Direct Known Subclasses:
AccumulationAnalysis, CFAnalysis, KeyForAnalysis, LockAnalysis, NullnessAnalysis
public abstract class CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>> extends ForwardAnalysisImpl<V,S,T>
CFAbstractAnalysis is an extensible org.checkerframework.dataflow analysis for the Checker Framework that tracks the annotations using a flow-sensitive analysis. It uses an AnnotatedTypeFactory to provide checker-specific logic how to combine types (e.g., what is the type of a string concatenation, given the types of the two operands) and as an abstraction function (e.g., determine the annotations on literals).

The purpose of this class is twofold: Firstly, it serves as factory for abstract values, stores and the transfer function. Furthermore, it makes it easy for the transfer function and the stores to access the AnnotatedTypeFactory, the qualifier hierarchy, etc.

  • Field Details

  • Constructor Details

    • CFAbstractAnalysis

      protected CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, int maxCountBeforeWidening)
      Create a CFAbstractAnalysis.
      Parameters:
      checker - a checker that contains command-line arguments and other information
      factory - an annotated type factory to introduce type and dataflow rules
      maxCountBeforeWidening - number of times a block can be analyzed before widening

    • CFAbstractAnalysis

      protected CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory)
      Create a CFAbstractAnalysis.
      Parameters:
      checker - a checker that contains command-line arguments and other information
      factory - an annotated type factory to introduce type and dataflow rules

  • Method Details

    • performAnalysis

      public void performAnalysis(ControlFlowGraph cfg, List<CFAbstractAnalysis.FieldInitialValue<V>> fieldValues)
      Analyze the given control flow graph.
      Parameters:
      cfg - control flow graph to analyze
      fieldValues - initial values of the fields

    • getSideEffectsOnlyExpressions

      public @Nullable List<JavaExpression> getSideEffectsOnlyExpressions(MethodInvocationNode methodInvocationNode)
      Returns the expressions that the invoked method side-effects (specified as arguments/elements of @SideEffectsOnly), viewpoint-adapted to the given method invocation. Returns null if the invoked method has no @SideEffectsOnly annotation.

      Also returns null if any of the annotation's expressions cannot be parsed at the call site. Null means "the method might side-effect anything", which is the conservative result; returning a list that omits the unparseable expression would treat the method as side-effecting less than it was declared to. The parse error itself is reported at the call site in addition to at the declaration, since the callee's declaration may not be under compilation.

      The result is cached, because dataflow calls this once per iteration per call site and parsing an expression is not cheap. Clients should not side-effect the returned value, which is aliased to internal state.

      Parameters:
      methodInvocationNode - the call site at which the side-effecting expressions will be used
      Returns:
      the expressions that the method side-effects, viewpoint-adapted to the given invocation; or null if the method has no valid @SideEffectsOnly annotation

    • getFieldInitialValues

      public List<CFAbstractAnalysis.FieldInitialValue<V>> getFieldInitialValues()
      A list of initial abstract values for the fields.
      Returns:
      a list of initial abstract values for the fields

    • createTransferFunction

      public T createTransferFunction()
      Returns the transfer function to be used by the analysis.
      Returns:
      the transfer function to be used by the analysis

    • createEmptyStore

      public abstract S createEmptyStore(boolean sequentialSemantics)
      Returns an empty store of the appropriate type.
      Returns:
      an empty store of the appropriate type

    • createCopiedStore

      public abstract S createCopiedStore(S s)
      Returns an identical copy of the store s.
      Returns:
      an identical copy of the store s

    • createAbstractValue

      public @Nullable V createAbstractValue(AnnotatedTypeMirror type)
      Creates an abstract value from the annotated type mirror. The value contains the set of primary annotations on the type, unless the type is an AnnotatedWildcardType. For an AnnotatedWildcardType, the annotations in the created value are the primary annotations on the extends bound. See CFAbstractValue for an explanation.
      Parameters:
      type - the type to convert into an abstract value
      Returns:
      an abstract value containing the given annotated type or null if type is missing annotations

    • createAbstractValue

      public abstract @Nullable V createAbstractValue(AnnotationMirrorSet annotations, TypeMirror underlyingType)
      Returns an abstract value containing the given annotations and underlyingType. Returns null if the annotation set has missing annotations.
      Parameters:
      annotations - the annotations for the result annotated type
      underlyingType - the unannotated type for the result annotated type
      Returns:
      an abstract value containing the given annotations and underlyingType or null if annotations is missing annotations

    • getCfValue

      public final @Nullable CFValue getCfValue(CFAbstractAnalysis<CFValue,?,?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType)
      Default implementation for createAbstractValue(AnnotationMirrorSet, TypeMirror).
      Parameters:
      analysis - the analysis
      annotations - the annotations for the result annotated type
      underlyingType - the unannotated type for the result annotated type
      Returns:
      an abstract value containing the given annotations and underlyingType

    • getTypeHierarchy

      public TypeHierarchy getTypeHierarchy()
      Returns the type hierarchy.
      Returns:
      the type hierarchy

    • getTypeFactory

      public GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> getTypeFactory()

    • callTransferFunction

      protected TransferResult<V,S> callTransferFunction(Node node, TransferInput<V,S> input)
      Description copied from class: AbstractAnalysis
      Call the transfer function for node node, and set that node as current node first. This method requires a transferInput that the method can modify.
      Overrides:
      callTransferFunction in class ForwardAnalysisImpl<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>
      Parameters:
      node - the given node
      input - the transfer input
      Returns:
      the output of the transfer function

    • createSingleAnnotationValue

      public V createSingleAnnotationValue(AnnotationMirror anno, TypeMirror underlyingType)
      Returns an abstract value containing an annotated type with the annotation anno, and 'top' for all other hierarchies. The underlying type is underlyingType.
      Parameters:
      anno - the annotation for the result annotated type
      underlyingType - the unannotated type for the result annotated type
      Returns:
      an abstract value with anno and underlyingType

    • getTypes

      public Types getTypes()
      Returns the types utility.
      Returns:
      types

    • getEnv

      public ProcessingEnvironment getEnv()
      Returns the processing environment.
      Returns:
      env