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, InitializationAnalysis, KeyForAnalysis, LockAnalysis, NullnessNoInitAnalysis

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.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	CFAbstractAnalysis.FieldInitialValue<V extends CFAbstractValue<V>>	A triple of field, value corresponding to the annotations on its declared type, value of its initializer.

Nested classes/interfaces inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

AbstractAnalysis.Worklist

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Analysis

Analysis.BeforeOrAfter, Analysis.Direction

Field Summary

Fields

Modifier and Type	Field	Description
protected GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>>	atypeFactory	A type factory that can provide static type annotations for AST Trees.
protected SourceChecker	checker	A checker that contains command-line arguments and other information.
protected DependentTypesHelper	dependentTypesHelper	The dependent type helper used to standardize both annotations belonging to the type hierarchy, and contract expressions.
protected javax.annotation.processing.ProcessingEnvironment	env	The associated processing environment.
protected java.util.List<CFAbstractAnalysis.FieldInitialValue<V>>	fieldValues	Initial abstract types for fields.
protected QualifierHierarchy	qualHierarchy	The qualifier hierarchy for which to track annotations.
protected TypeHierarchy	typeHierarchy	The type hierarchy.
protected javax.lang.model.util.Types	types	Instance of the types utility.

Fields inherited from class org.checkerframework.dataflow.analysis.ForwardAnalysisImpl

blockCount, elseStores, maxCountBeforeWidening, storesAtReturnStatements, thenStores

Fields inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

cfg, currentInput, currentNode, currentTree, direction, finalLocalValues, inputs, isRunning, nodeValues, transferFunction, worklist

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory)	Create a CFAbstractAnalysis.
protected	CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, int maxCountBeforeWidening)	Create a CFAbstractAnalysis.

Method Summary

Modifier and Type	Method	Description
@Nullable V	createAbstractValue(AnnotatedTypeMirror type)	Creates an abstract value from the annotated type mirror.
abstract @Nullable V	createAbstractValue(AnnotationMirrorSet annotations, javax.lang.model.type.TypeMirror underlyingType)	Returns an abstract value containing the given annotations and underlyingType.
abstract S	createCopiedStore(S s)	Returns an identical copy of the store s.
abstract S	createEmptyStore(boolean sequentialSemantics)	Returns an empty store of the appropriate type.
V	createSingleAnnotationValue(javax.lang.model.element.AnnotationMirror anno, javax.lang.model.type.TypeMirror underlyingType)	Returns an abstract value containing an annotated type with the annotation anno, and 'top' for all other hierarchies.
T	createTransferFunction()	Returns the transfer function to be used by the analysis.
@Nullable CFValue	defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis, AnnotationMirrorSet annotations, javax.lang.model.type.TypeMirror underlyingType)	Default implementation for createAbstractValue(AnnotationMirrorSet, TypeMirror).
javax.annotation.processing.ProcessingEnvironment	getEnv()	Get the processing environment.
java.util.List<CFAbstractAnalysis.FieldInitialValue<V>>	getFieldInitialValues()	A list of initial abstract values for the fields.
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>>	getTypeFactory()
TypeHierarchy	getTypeHierarchy()
javax.lang.model.util.Types	getTypes()	Get the types utility.
void	performAnalysis(ControlFlowGraph cfg, java.util.List<CFAbstractAnalysis.FieldInitialValue<V>> fieldValues)	Analyze the given control flow graph.

Methods inherited from class org.checkerframework.dataflow.analysis.ForwardAnalysisImpl

addStoreBefore, callTransferFunction, getInput, getInputBefore, getReturnStatementStores, getStoreBefore, initFields, initInitialInputs, performAnalysis, performAnalysisBlock, propagateStoresTo, runAnalysisFor

Methods inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

addToWorklist, getContainingClass, getContainingMethod, getCurrentTree, getDirection, getExceptionalExitStore, getNodesForTree, getNodeValues, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, init, isIgnoredExceptionType, isRunning, readFromStore, setCurrentNode, setCurrentTree, updateNodeValues

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.checkerframework.dataflow.analysis.Analysis

getDirection, getExceptionalExitStore, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, isRunning

Field Detail

qualHierarchy

protected final QualifierHierarchy qualHierarchy

The qualifier hierarchy for which to track annotations.

typeHierarchy

protected final TypeHierarchy typeHierarchy

The type hierarchy.

dependentTypesHelper

protected final DependentTypesHelper dependentTypesHelper

The dependent type helper used to standardize both annotations belonging to the type hierarchy, and contract expressions.

atypeFactory

protected final GenericAnnotatedTypeFactory<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>,? extends CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>> atypeFactory

A type factory that can provide static type annotations for AST Trees.

checker

protected final SourceChecker checker

A checker that contains command-line arguments and other information.

fieldValues

protected final java.util.List<CFAbstractAnalysis.FieldInitialValue<V extends CFAbstractValue<V>>> fieldValues

Initial abstract types for fields.

env

protected final javax.annotation.processing.ProcessingEnvironment env

The associated processing environment.

types

protected final javax.lang.model.util.Types types

Instance of the types utility.

Constructor Detail

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 Detail

performAnalysis

public void performAnalysis(ControlFlowGraph cfg,
                            java.util.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 java.util.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,
                                                javax.lang.model.type.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,
                                                    javax.lang.model.type.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(javax.lang.model.element.AnnotationMirror anno,
                                     javax.lang.model.type.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 javax.lang.model.util.Types getTypes()

Get the types utility.

Returns:

types

getEnv

public javax.annotation.processing.ProcessingEnvironment getEnv()

Get the processing environment.

Returns:

env