org.checkerframework.checker.nullness

Class NullnessTransfer

java.lang.Object

org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<TransferResult<V,S>,TransferInput<V,S>>

org.checkerframework.framework.flow.CFAbstractTransfer<V,S,T>

org.checkerframework.checker.initialization.InitializationTransfer<NullnessValue,NullnessTransfer,NullnessStore>

org.checkerframework.checker.nullness.NullnessTransfer

All Implemented Interfaces:

ForwardTransferFunction<NullnessValue,NullnessStore>, TransferFunction<NullnessValue,NullnessStore>, NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

public class NullnessTransfer
extends InitializationTransfer<NullnessValue,NullnessTransfer,NullnessStore>

Transfer function for the non-null type system. Performs the following refinements:

1. After an expression is compared with the null literal, then that expression can safely be considered NonNull if the result of the comparison is false or Nullable if the result is true.
2. If an expression is dereferenced, then it can safely be assumed to non-null in the future. If it would not be, then the dereference would have raised a NullPointerException.
3. Tracks whether PolyNull is known to be NonNull or Nullable (or not known to be either).

Field Summary

Fields

Modifier and Type	Field and Description
protected KeyForAnnotatedTypeFactory	keyForTypeFactory The type factory for the map key analysis.
protected AnnotatedTypeMirror.AnnotatedDeclaredType	MAP_TYPE Java's Map interface.
protected AnnotationMirror	NONNULL The @NonNull annotation.
protected AnnotationMirror	NULLABLE The @Nullable annotation.
protected GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,? extends CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>>	nullnessTypeFactory The type factory for the nullness analysis that was passed to the constructor.
protected AnnotationMirror	POLYNULL The @PolyNull annotation.

Fields inherited from class org.checkerframework.checker.initialization.InitializationTransfer

atypeFactory

Fields inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
NullnessTransfer(NullnessAnalysis analysis) Create a new NullnessTransfer for the given analysis.

Method Summary

Modifier and Type	Method and Description
protected @Nullable NullnessValue	finishValue(@Nullable NullnessValue value, NullnessStore store) A hook for subclasses to modify the result of the transfer function.
protected @Nullable NullnessValue	finishValue(@Nullable NullnessValue value, NullnessStore thenStore, NullnessStore elseStore) A hook for subclasses to modify the result of the transfer function.
protected void	makeNonNull(NullnessStore store, Node node) Sets a given Node to non-null in the given store.
protected void	makeNonNull(TransferResult<NullnessValue,NullnessStore> result, Node node) Sets a given Node node to non-null in the given TransferResult.
protected void	refineToNonNull(TransferResult<NullnessValue,NullnessStore> result) Refine the given result to @NonNull.
protected TransferResult<NullnessValue,NullnessStore>	strengthenAnnotationOfEqualTo(TransferResult<NullnessValue,NullnessStore> res, Node firstNode, Node secondNode, NullnessValue firstValue, NullnessValue secondValue, boolean notEqualTo) Refine the annotation of secondNode if the annotation secondValue is less precise than firstValue.
TransferResult<NullnessValue,NullnessStore>	visitArrayAccess(ArrayAccessNode n, TransferInput<NullnessValue,NullnessStore> p)
TransferResult<NullnessValue,NullnessStore>	visitFieldAccess(FieldAccessNode n, TransferInput<NullnessValue,NullnessStore> p) If an invariant field is initialized and has the invariant annotation, than it has at least the invariant annotation.
TransferResult<NullnessValue,NullnessStore>	visitInstanceOf(InstanceOfNode n, TransferInput<NullnessValue,NullnessStore> p)
TransferResult<NullnessValue,NullnessStore>	visitMethodAccess(MethodAccessNode n, TransferInput<NullnessValue,NullnessStore> p)
TransferResult<NullnessValue,NullnessStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<NullnessValue,NullnessStore> in)
TransferResult<NullnessValue,NullnessStore>	visitReturn(ReturnNode n, TransferInput<NullnessValue,NullnessStore> in)
TransferResult<NullnessValue,NullnessStore>	visitThrow(ThrowNode n, TransferInput<NullnessValue,NullnessStore> p)

Methods inherited from class org.checkerframework.checker.initialization.InitializationTransfer

initializedFieldsAfterCall, isNotFullyInitializedReceiver, markInvariantFieldsAsInitialized, visitAssignment

Methods inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

addInformationFromPreconditions, createTransferResult, getNarrowedValue, getValueFromFactory, getValueWithSameAnnotations, getWidenedValue, initialStore, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThis, visitVariableDeclaration, visitWideningConversion

Methods inherited from class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitTypeCast, visitUnsignedRightShift, visitValueLiteral

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.cfg.node.NodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitTypeCast, visitUnsignedRightShift

Field Detail

NONNULL

protected final AnnotationMirror NONNULL

The @NonNull annotation.

NULLABLE

protected final AnnotationMirror NULLABLE

The @Nullable annotation.

POLYNULL

protected final AnnotationMirror POLYNULL

The @PolyNull annotation.

MAP_TYPE

protected final AnnotatedTypeMirror.AnnotatedDeclaredType MAP_TYPE

Java's Map interface.

The qualifiers in this type don't matter -- it is not used as a fully-annotated AnnotatedDeclaredType, but just passed to asSuper().

nullnessTypeFactory

protected final GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,? extends CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>> nullnessTypeFactory

The type factory for the nullness analysis that was passed to the constructor.

keyForTypeFactory

protected final KeyForAnnotatedTypeFactory keyForTypeFactory

The type factory for the map key analysis.

Constructor Detail

NullnessTransfer

public NullnessTransfer(NullnessAnalysis analysis)

Create a new NullnessTransfer for the given analysis.

Method Detail

makeNonNull

protected void makeNonNull(NullnessStore store,
                           Node node)

Sets a given Node to non-null in the given store. Calls to this method implement case 2.

makeNonNull

protected void makeNonNull(TransferResult<NullnessValue,NullnessStore> result,
                           Node node)

Sets a given Node node to non-null in the given TransferResult.

refineToNonNull

protected void refineToNonNull(TransferResult<NullnessValue,NullnessStore> result)

Refine the given result to @NonNull.

finishValue

protected @Nullable NullnessValue finishValue(@Nullable NullnessValue value,
                                              NullnessStore store)

Description copied from class: CFAbstractTransfer

A hook for subclasses to modify the result of the transfer function. This method is called before returning the abstract value value as the result of the transfer function.

If a subclass overrides this method, the subclass should also override CFAbstractTransfer.finishValue(CFAbstractValue,CFAbstractStore,CFAbstractStore).

Overrides:

finishValue in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

Parameters:

value - a value to possibly modify

store - the store

Returns:

the possibly-modified value

finishValue

protected @Nullable NullnessValue finishValue(@Nullable NullnessValue value,
                                              NullnessStore thenStore,
                                              NullnessStore elseStore)

Description copied from class: CFAbstractTransfer

A hook for subclasses to modify the result of the transfer function. This method is called before returning the abstract value value as the result of the transfer function.

If a subclass overrides this method, the subclass should also override CFAbstractTransfer.finishValue(CFAbstractValue,CFAbstractStore).

Overrides:

finishValue in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

Parameters:

value - the value to finish

thenStore - the "then" store

elseStore - the "else" store

Returns:

the possibly-modified value

strengthenAnnotationOfEqualTo

protected TransferResult<NullnessValue,NullnessStore> strengthenAnnotationOfEqualTo(TransferResult<NullnessValue,NullnessStore> res,
                                                                                    Node firstNode,
                                                                                    Node secondNode,
                                                                                    NullnessValue firstValue,
                                                                                    NullnessValue secondValue,
                                                                                    boolean notEqualTo)

Refine the annotation of secondNode if the annotation secondValue is less precise than firstValue. This is possible, if secondNode is an expression that is tracked by the store (e.g., a local variable or a field). Clients usually call this twice with firstNode and secondNode reversed, to refine each of them.

Note that when overriding this method, when a new type is inserted into the store, CFAbstractTransfer.splitAssignments(org.checkerframework.dataflow.cfg.node.Node) should be called, and the new type should be inserted into the store for each of the resulting nodes.

Furthermore, this method refines the type to NonNull for the appropriate branch if an expression is compared to the null literal (listed as case 1 in the class description).

Overrides:

strengthenAnnotationOfEqualTo in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

Parameters:

res - the previous result

notEqualTo - if true, indicates that the logic is flipped (i.e., the information is added to the elseStore instead of the thenStore) for a not-equal comparison.

Returns:

the conditional transfer result (if information has been added), or null.

visitArrayAccess

public TransferResult<NullnessValue,NullnessStore> visitArrayAccess(ArrayAccessNode n,
                                                                    TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitArrayAccess in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitArrayAccess in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

visitInstanceOf

public TransferResult<NullnessValue,NullnessStore> visitInstanceOf(InstanceOfNode n,
                                                                   TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitInstanceOf in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitInstanceOf in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

visitMethodAccess

public TransferResult<NullnessValue,NullnessStore> visitMethodAccess(MethodAccessNode n,
                                                                     TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitMethodAccess in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitMethodAccess in class AbstractNodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

visitFieldAccess

public TransferResult<NullnessValue,NullnessStore> visitFieldAccess(FieldAccessNode n,
                                                                    TransferInput<NullnessValue,NullnessStore> p)

Description copied from class: InitializationTransfer

If an invariant field is initialized and has the invariant annotation, than it has at least the invariant annotation. Note that only fields of the 'this' receiver are tracked for initialization.

Specified by:

visitFieldAccess in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitFieldAccess in class InitializationTransfer<NullnessValue,NullnessTransfer,NullnessStore>

visitThrow

public TransferResult<NullnessValue,NullnessStore> visitThrow(ThrowNode n,
                                                              TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitThrow in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitThrow in class AbstractNodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

visitMethodInvocation

public TransferResult<NullnessValue,NullnessStore> visitMethodInvocation(MethodInvocationNode n,
                                                                         TransferInput<NullnessValue,NullnessStore> in)

Specified by:

visitMethodInvocation in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitMethodInvocation in class InitializationTransfer<NullnessValue,NullnessTransfer,NullnessStore>

visitReturn

public TransferResult<NullnessValue,NullnessStore> visitReturn(ReturnNode n,
                                                               TransferInput<NullnessValue,NullnessStore> in)

Specified by:

visitReturn in interface NodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitReturn in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>