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.Analysis<V,S,T>

org.checkerframework.framework.flow.CFAbstractAnalysis<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 Analysis<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.

Author:

Charlie Garrett, Stefan Heule

Nested Class Summary

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

Analysis.Worklist

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 used to do error reporting.
protected java.util.List<Pair<javax.lang.model.element.VariableElement,V>>	fieldValues Initial abstract types for fields.
protected QualifierHierarchy	qualifierHierarchy The qualifier hierarchy for which to track annotations.
protected TypeHierarchy	typeHierarchy The type hierarchy.

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

blockCount, cfg, currentInput, currentNode, currentTree, elseStores, env, finalLocalValues, inputs, isRunning, maxCountBeforeWidening, nodeValues, storesAtReturnStatements, thenStores, transferFunction, types, worklist

Constructor Summary

Constructors

Constructor and Description
CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, java.util.List<Pair<javax.lang.model.element.VariableElement,V>> fieldValues)
CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, java.util.List<Pair<javax.lang.model.element.VariableElement,V>> fieldValues, int maxCountBeforeWidening)

Method Summary

Modifier and Type	Method and Description
V	createAbstractValue(AnnotatedTypeMirror type) Creates an abstract value from the annotated type mirror.
abstract V	createAbstractValue(java.util.Set<javax.lang.model.element.AnnotationMirror> annotations, javax.lang.model.type.TypeMirror underlyingType)
abstract S	createCopiedStore(S s)
abstract S	createEmptyStore(boolean sequentialSemantics)
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()
CFValue	defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis, java.util.Set<javax.lang.model.element.AnnotationMirror> annotations, javax.lang.model.type.TypeMirror underlyingType) Default implementation for createAbstractValue(Set, TypeMirror)
java.util.List<Pair<javax.lang.model.element.VariableElement,V>>	getFieldValues()
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>>	getTypeFactory()
<W extends GenericAnnotatedTypeFactory<?,?,?,?>,U extends BaseTypeChecker> W	getTypeFactoryOfSubchecker(java.lang.Class<U> checkerClass)
TypeHierarchy	getTypeHierarchy()
void	visualizeCFG() Perform a visualization of the CFG and analysis info for inspection.

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

addStoreBefore, addToWorklist, callTransferFunction, getContainingClass, getContainingMethod, getCurrentTree, getEnv, getExceptionalExitStore, getInput, getInputBefore, getNodeForTree, getRegularExitStore, getResult, getReturnStatementStores, getStoreBefore, getTransferFunction, getTypes, getValue, getValue, init, isRunning, performAnalysis, propagateStoresTo, readFromStore, setCurrentTree, setTransferFunction, updateNodeValues

Methods inherited from class java.lang.Object

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

Field Detail

qualifierHierarchy

protected final QualifierHierarchy qualifierHierarchy

The qualifier hierarchy for which to track annotations.

typeHierarchy

protected final TypeHierarchy typeHierarchy

The type hierarchy.

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 used to do error reporting. TODO: if it's only for error reporting, should it be an (extended) ErrorHandler?

fieldValues

protected final java.util.List<Pair<javax.lang.model.element.VariableElement,V extends CFAbstractValue<V>>> fieldValues

Initial abstract types for fields.

Constructor Detail

CFAbstractAnalysis

public CFAbstractAnalysis(BaseTypeChecker checker,
                          GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory,
                          java.util.List<Pair<javax.lang.model.element.VariableElement,V>> fieldValues,
                          int maxCountBeforeWidening)

CFAbstractAnalysis

public CFAbstractAnalysis(BaseTypeChecker checker,
                          GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory,
                          java.util.List<Pair<javax.lang.model.element.VariableElement,V>> fieldValues)

Method Detail

getFieldValues

public java.util.List<Pair<javax.lang.model.element.VariableElement,V>> getFieldValues()

createTransferFunction

public T createTransferFunction()

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

createCopiedStore

public abstract S createCopiedStore(S 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. In that case, the annotations in the created value are the primary annotations on the extends bound. See CFAbstractValue for an explanation.

Returns:

an abstract value containing the given annotated type.

createAbstractValue

public abstract V createAbstractValue(java.util.Set<javax.lang.model.element.AnnotationMirror> annotations,
                                      javax.lang.model.type.TypeMirror underlyingType)

Returns:

an abstract value containing the given annotations and underlyingType.

defaultCreateAbstractValue

public CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis,
                                          java.util.Set<javax.lang.model.element.AnnotationMirror> annotations,
                                          javax.lang.model.type.TypeMirror underlyingType)

Default implementation for createAbstractValue(Set, TypeMirror)

getTypeHierarchy

public TypeHierarchy getTypeHierarchy()

getTypeFactory

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

visualizeCFG

public void visualizeCFG()

Perform a visualization of the CFG and analysis info for inspection.

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 Object.

getTypeFactoryOfSubchecker

public <W extends GenericAnnotatedTypeFactory<?,?,?,?>,U extends BaseTypeChecker> W getTypeFactoryOfSubchecker(java.lang.Class<U> checkerClass)

See Also:

GenericAnnotatedTypeFactory.getTypeFactoryOfSubchecker(Class)