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.
-
Nested Class Summary
Modifier and TypeClassDescriptionstatic class
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
Modifier and TypeFieldDescriptionprotected final GenericAnnotatedTypeFactory<V,
S, T, ? extends CFAbstractAnalysis<V, S, T>> A type factory that can provide static type annotations for AST Trees.protected final SourceChecker
A checker that contains command-line arguments and other information.protected final DependentTypesHelper
The dependent type helper used to standardize both annotations belonging to the type hierarchy, and contract expressions.protected final ProcessingEnvironment
The associated processing environment.protected final List<CFAbstractAnalysis.FieldInitialValue<V>>
Initial abstract types for fields.protected final QualifierHierarchy
The qualifier hierarchy for which to track annotations.protected final TypeHierarchy
The type hierarchy.protected final 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
ModifierConstructorDescriptionprotected
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 TypeMethodDescriptionprotected TransferResult<V,
S> callTransferFunction
(Node node, TransferInput<V, S> input) Call the transfer function for nodenode
, and set that node as current node first.Creates an abstract value from the annotated type mirror.createAbstractValue
(AnnotationMirrorSet annotations, TypeMirror underlyingType) Returns an abstract value containing the givenannotations
andunderlyingType
.abstract S
Returns an identical copy of the stores
.abstract S
createEmptyStore
(boolean sequentialSemantics) Returns an empty store of the appropriate type.createSingleAnnotationValue
(AnnotationMirror anno, TypeMirror underlyingType) Returns an abstract value containing an annotated type with the annotationanno
, and 'top' for all other hierarchies.Returns the transfer function to be used by the analysis.defaultCreateAbstractValue
(CFAbstractAnalysis<CFValue, ?, ?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType) Default implementation forcreateAbstractValue(AnnotationMirrorSet, TypeMirror)
.getEnv()
Get the processing environment.A list of initial abstract values for the fields.GenericAnnotatedTypeFactory<V,
S, T, ? extends CFAbstractAnalysis<V, S, T>> 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, getInput, getInputBefore, getReturnStatementStores, getStoreBefore, initFields, initInitialInputs, performAnalysis, performAnalysisBlock, propagateStoresTo, runAnalysisFor
Methods inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis
addToWorklist, getContainingClass, getContainingMethod, getCurrentTree, getDirection, getEnclosingClass, getEnclosingMethod, getExceptionalExitStore, getNodesForTree, getNodeValues, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, init, isIgnoredExceptionType, isRunning, 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 Details
-
qualHierarchy
The qualifier hierarchy for which to track annotations. -
typeHierarchy
The type hierarchy. -
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, atypeFactoryS>, T extends CFAbstractTransfer<V, S, T>, ? extends CFAbstractAnalysis<V extends CFAbstractValue<V>, S extends CFAbstractStore<V, S>, T extends CFAbstractTransfer<V, S, T>>> A type factory that can provide static type annotations for AST Trees. -
checker
A checker that contains command-line arguments and other information. -
fieldValues
protected final List<CFAbstractAnalysis.FieldInitialValue<V extends CFAbstractValue<V>>> fieldValuesInitial abstract types for fields. -
env
The associated processing environment. -
types
Instance of the types utility.
-
-
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 informationfactory
- an annotated type factory to introduce type and dataflow rulesmaxCountBeforeWidening
- 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 informationfactory
- 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 analyzefieldValues
- initial values of the fields
-
getFieldInitialValues
A list of initial abstract values for the fields.- Returns:
- a list of initial abstract values for the fields
-
createTransferFunction
Returns the transfer function to be used by the analysis.- Returns:
- the transfer function to be used by the analysis
-
createEmptyStore
Returns an empty store of the appropriate type.- Returns:
- an empty store of the appropriate type
-
createCopiedStore
Returns an identical copy of the stores
.- Returns:
- an identical copy of the store
s
-
createAbstractValue
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. SeeCFAbstractValue
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 givenannotations
andunderlyingType
. Returns null if the annotation set has missing annotations.- Parameters:
annotations
- the annotations for the result annotated typeunderlyingType
- the unannotated type for the result annotated type- Returns:
- an abstract value containing the given
annotations
andunderlyingType
-
defaultCreateAbstractValue
public @Nullable CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue, ?, ?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType) Default implementation forcreateAbstractValue(AnnotationMirrorSet, TypeMirror)
. -
getTypeHierarchy
-
getTypeFactory
-
callTransferFunction
Description copied from class:AbstractAnalysis
Call the transfer function for nodenode
, and set that node as current node first. This method requires atransferInput
that the method can modify.- Overrides:
callTransferFunction
in classForwardAnalysisImpl<V extends CFAbstractValue<V>,
S extends CFAbstractStore<V, S>, T extends CFAbstractTransfer<V, S, T>> - Parameters:
node
- the given nodeinput
- the transfer input- Returns:
- the output of the transfer function
-
createSingleAnnotationValue
Returns an abstract value containing an annotated type with the annotationanno
, and 'top' for all other hierarchies. The underlying type isunderlyingType
.- Parameters:
anno
- the annotation for the result annotated typeunderlyingType
- the unannotated type for the result annotated type- Returns:
- an abstract value with
anno
andunderlyingType
-
getTypes
Get the types utility.- Returns:
types
-
getEnv
Get the processing environment.- Returns:
env
-