Package org.checkerframework.checker.nullness

Class NullnessTransfer

java.lang.Object

org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

org.checkerframework.framework.flow.CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

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	Description
protected final @Nullable KeyForAnnotatedTypeFactory	keyForTypeFactory	The type factory for the map key analysis, or null if the Map Key Checker should not be run.
protected final AnnotatedTypeMirror.AnnotatedDeclaredType	MAP_TYPE	Java's Map interface.
protected final AnnotationMirror	NONNULL	The @NonNull annotation.
protected final AnnotationMirror	NULLABLE	The @Nullable annotation.
protected final NullnessAnnotatedTypeFactory	nullnessTypeFactory	The type factory for the nullness analysis that was passed to the constructor.
protected final 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	Description
NullnessTransfer(NullnessAnalysis analysis)	Create a new NullnessTransfer for the given analysis.

Method Summary

Modifier and Type	Method	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, then 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, createTransferResult, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, insertIntoStoresPermitNonDeterministic, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, recreateTransferResult, setFixedInitialStore, shouldPerformWholeProgramInference, shouldPerformWholeProgramInference, splitAssignments, usesSequentialSemantics, visitAnyPattern, visitCase, visitClassName, visitConditionalNot, visitDeconstructorPattern, visitEqualTo, visitExpressionStatement, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitStringConversion, visitSwitchExpressionNode, 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 Details

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 NullnessAnnotatedTypeFactory nullnessTypeFactory

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

keyForTypeFactory

protected final @Nullable KeyForAnnotatedTypeFactory keyForTypeFactory

The type factory for the map key analysis, or null if the Map Key Checker should not be run.

Constructor Details

NullnessTransfer

public NullnessTransfer(NullnessAnalysis analysis)

Create a new NullnessTransfer for the given analysis.

Parameters:

analysis - nullness analysis

Method Details

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.

Parameters:

store - the store to update

node - the node that should be non-null

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

firstNode - the node that might be more precise

secondNode - the node whose type to possibly refine

firstValue - the abstract value that might be more precise

secondValue - the abstract value that might be less precise

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 res

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, then 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)

When the invocationPreservesArgumentNullness flag is turned on, the receiver and arguments that are passed to non-null parameters in a method call or constructor invocation are unsoundly assumed to be non-null after the invocation.

When the flag is turned off, the analysis is sound: it checks that the method is SideEffectFree or the receiver is unassignable. Only if either one of the two is true, is the receiver made non-null. Similar logic is applied to the arguments of the invocation.

Provided that m is of a type that implements interface java.util.Map:

• Given a call m.get(k), if k is @KeyFor("m") and m's value type is @NonNull, then the result is @NonNull in the thenStore and elseStore of the transfer result.

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>