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.
AbstractAnalysis.Worklist
Analysis.BeforeOrAfter, Analysis.Direction
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<Pair<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.
|
protected Types |
types
Instance of the types utility.
|
blockCount, elseStores, maxCountBeforeWidening, storesAtReturnStatements, thenStores
cfg, currentInput, currentNode, currentTree, direction, finalLocalValues, inputs, isRunning, nodeValues, transferFunction, worklist
Modifier | Constructor and Description |
---|---|
protected |
CFAbstractAnalysis(BaseTypeChecker checker,
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory,
List<Pair<VariableElement,V>> fieldValues) |
protected |
CFAbstractAnalysis(BaseTypeChecker checker,
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory,
List<Pair<VariableElement,V>> fieldValues,
int maxCountBeforeWidening)
Create a CFAbstractAnalysis.
|
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<Pair<VariableElement,V>> |
getFieldValues() |
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> |
getTypeFactory() |
TypeHierarchy |
getTypeHierarchy() |
Types |
getTypes()
Get the types utility.
|
void |
performAnalysis(ControlFlowGraph cfg,
List<Pair<VariableElement,V>> fieldValues) |
addStoreBefore, callTransferFunction, getInput, getInputBefore, getReturnStatementStores, getStoreBefore, initFields, initInitialInputs, performAnalysis, performAnalysisBlock, propagateStoresTo, runAnalysisFor
addToWorklist, getContainingClass, getContainingMethod, getCurrentTree, getDirection, getExceptionalExitStore, getNodesForTree, getNodeValues, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, init, isRunning, readFromStore, setCurrentNode, setCurrentTree, updateNodeValues
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getDirection, getExceptionalExitStore, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, isRunning
protected final QualifierHierarchy qualifierHierarchy
protected final TypeHierarchy typeHierarchy
protected final DependentTypesHelper dependentTypesHelper
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
protected final SourceChecker checker
protected final List<Pair<VariableElement,V extends CFAbstractValue<V>>> fieldValues
protected final ProcessingEnvironment env
protected final Types types
protected CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, List<Pair<VariableElement,V>> fieldValues, int maxCountBeforeWidening)
checker
- a checker that contains command-line arguments and other informationfactory
- an annotated type factory to introduce type and dataflow rulesfieldValues
- initial abstract types for fieldsmaxCountBeforeWidening
- number of times a block can be analyzed before wideningprotected CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, List<Pair<VariableElement,V>> fieldValues)
public void performAnalysis(ControlFlowGraph cfg, List<Pair<VariableElement,V>> fieldValues)
public List<Pair<VariableElement,V>> getFieldValues()
public T createTransferFunction()
public abstract S createEmptyStore(boolean sequentialSemantics)
public abstract S createCopiedStore(S s)
s
.s
public V createAbstractValue(AnnotatedTypeMirror type)
CFAbstractValue
for an explanation.type
- the type to convert into an abstract valuetype
public abstract V createAbstractValue(Set<AnnotationMirror> annotations, TypeMirror underlyingType)
annotations
and underlyingType
.
Returns null if the annotation set has missing annotations.annotations
and underlyingType
public CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis, Set<AnnotationMirror> annotations, TypeMirror underlyingType)
createAbstractValue(Set, TypeMirror)
.public TypeHierarchy getTypeHierarchy()
public GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> getTypeFactory()
public V createSingleAnnotationValue(AnnotationMirror anno, TypeMirror underlyingType)
anno
, and
'top' for all other hierarchies. The underlying type is underlyingType
.public ProcessingEnvironment getEnv()
env