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

    • 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

    • 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

    • defaultCreateAbstractValue

      public @Nullable CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType)
      Default implementation for createAbstractValue(AnnotationMirrorSet, TypeMirror).

    • getTypeHierarchy

      public TypeHierarchy getTypeHierarchy()

    • getTypeFactory

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

    • 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()
      Get the types utility.
      Returns:
      types

    • getEnv

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