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:

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.

Nested Class Summary

Nested Classes

Modifier and Type	Class and 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 and 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 ProcessingEnvironment	env The associated processing environment.
protected List<CFAbstractAnalysis.FieldInitialValue<V>>	fieldValues Initial abstract types for fields.
protected QualifierHierarchy	qualifierHierarchy The qualifier hierarchy for which to track annotations.
protected TypeHierarchy	typeHierarchy The type hierarchy.
protected 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 and 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 and Description
V	createAbstractValue(AnnotatedTypeMirror type) Creates an abstract value from the annotated type mirror.
abstract V	createAbstractValue(Set<AnnotationMirror> annotations, 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(AnnotationMirror anno, 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.
CFValue	defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis, Set<AnnotationMirror> annotations, TypeMirror underlyingType) Default implementation for createAbstractValue(Set, TypeMirror).
ProcessingEnvironment	getEnv() Get the processing environment.
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()
Types	getTypes() Get the types utility.
void	performAnalysis(ControlFlowGraph cfg, 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, 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

qualifierHierarchy

protected final QualifierHierarchy qualifierHierarchy

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 List<CFAbstractAnalysis.FieldInitialValue<V extends CFAbstractValue<V>>> fieldValues

Initial abstract types for fields.

env

protected final ProcessingEnvironment env

The associated processing environment.

types

protected final 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,
                            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 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 V createAbstractValue(Set<AnnotationMirror> annotations,
                                      TypeMirror underlyingType)

Returns an abstract value containing the given annotations and underlyingType. Returns null if the annotation set has missing annotations.

Returns:

an abstract value containing the given annotations and underlyingType

defaultCreateAbstractValue

public CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis,
                                          Set<AnnotationMirror> annotations,
                                          TypeMirror underlyingType)

Default implementation for createAbstractValue(Set, 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.

getTypes

public Types getTypes()

Get the types utility.

Returns:

types

getEnv

public ProcessingEnvironment getEnv()

Get the processing environment.

Returns:

env