Package org.checkerframework.checker.nullness

Class NullnessNoInitTransfer

java.lang.Object

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

org.checkerframework.framework.flow.CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

org.checkerframework.checker.nullness.NullnessNoInitTransfer

All Implemented Interfaces:

ForwardTransferFunction<NullnessNoInitValue,NullnessNoInitStore>, TransferFunction<NullnessNoInitValue,NullnessNoInitStore>, NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

public class NullnessNoInitTransfer
extends CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

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 @Nullable KeyForAnnotatedTypeFactory	keyForTypeFactory	The type factory for the map key analysis, or null if the Map Key Checker should not be run.
protected AnnotatedTypeMirror.AnnotatedDeclaredType	MAP_TYPE	Java's Map interface.
protected javax.lang.model.element.AnnotationMirror	NONNULL	The @NonNull annotation.
protected javax.lang.model.element.AnnotationMirror	NULLABLE	The @Nullable annotation.
protected NullnessNoInitAnnotatedTypeFactory	nullnessTypeFactory	The type factory for the nullness analysis that was passed to the constructor.
protected javax.lang.model.element.AnnotationMirror	POLYNULL	The @PolyNull annotation.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
NullnessNoInitTransfer(NullnessNoInitAnalysis analysis)	Create a new NullnessTransfer for the given analysis.

Method Summary

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

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

addInformationFromPreconditions, createTransferResult, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitAssignment, 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 Detail

NONNULL

protected final javax.lang.model.element.AnnotationMirror NONNULL

The @NonNull annotation.

NULLABLE

protected final javax.lang.model.element.AnnotationMirror NULLABLE

The @Nullable annotation.

POLYNULL

protected final javax.lang.model.element.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 NullnessNoInitAnnotatedTypeFactory 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 Detail

NullnessNoInitTransfer

public NullnessNoInitTransfer(NullnessNoInitAnalysis analysis)

Create a new NullnessTransfer for the given analysis.

Parameters:

analysis - nullness analysis

Method Detail

makeNonNull

protected void makeNonNull(NullnessNoInitStore 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<NullnessNoInitValue,NullnessNoInitStore> result,
                           Node node)

Sets a given node to non-null in the given transfer result.

Parameters:

result - the transfer result

node - the node to make non-null

refineToNonNull

protected void refineToNonNull(TransferResult<NullnessNoInitValue,NullnessNoInitStore> result)

Refine the given result to @NonNull.

Parameters:

result - the result to refine

finishValue

protected @Nullable NullnessNoInitValue finishValue(@Nullable NullnessNoInitValue value,
                                                    NullnessNoInitStore 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<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

Parameters:

value - a value to possibly modify

store - the store

Returns:

the possibly-modified value

finishValue

protected @Nullable NullnessNoInitValue finishValue(@Nullable NullnessNoInitValue value,
                                                    NullnessNoInitStore thenStore,
                                                    NullnessNoInitStore 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<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

Parameters:

value - the value to finish

thenStore - the "then" store

elseStore - the "else" store

Returns:

the possibly-modified value

strengthenAnnotationOfEqualTo

protected TransferResult<NullnessNoInitValue,NullnessNoInitStore> strengthenAnnotationOfEqualTo(TransferResult<NullnessNoInitValue,NullnessNoInitStore> res,
                                                                                                      Node firstNode,
                                                                                                      Node secondNode,
                                                                                                      NullnessNoInitValue firstValue,
                                                                                                      NullnessNoInitValue 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<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

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<NullnessNoInitValue,NullnessNoInitStore> visitArrayAccess(ArrayAccessNode n,
                                                                                      TransferInput<NullnessNoInitValue,NullnessNoInitStore> p)

Specified by:

visitArrayAccess in interface NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitArrayAccess in class CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

visitInstanceOf

public TransferResult<NullnessNoInitValue,NullnessNoInitStore> visitInstanceOf(InstanceOfNode n,
                                                                                     TransferInput<NullnessNoInitValue,NullnessNoInitStore> p)

Specified by:

visitInstanceOf in interface NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitInstanceOf in class CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

visitMethodAccess

public TransferResult<NullnessNoInitValue,NullnessNoInitStore> visitMethodAccess(MethodAccessNode n,
                                                                                       TransferInput<NullnessNoInitValue,NullnessNoInitStore> p)

Specified by:

visitMethodAccess in interface NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitMethodAccess in class AbstractNodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

visitFieldAccess

public TransferResult<NullnessNoInitValue,NullnessNoInitStore> visitFieldAccess(FieldAccessNode n,
                                                                                      TransferInput<NullnessNoInitValue,NullnessNoInitStore> p)

Specified by:

visitFieldAccess in interface NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitFieldAccess in class CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

visitThrow

public TransferResult<NullnessNoInitValue,NullnessNoInitStore> visitThrow(ThrowNode n,
                                                                                TransferInput<NullnessNoInitValue,NullnessNoInitStore> p)

Specified by:

visitThrow in interface NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitThrow in class AbstractNodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

visitMethodInvocation

public TransferResult<NullnessNoInitValue,NullnessNoInitStore> visitMethodInvocation(MethodInvocationNode n,
                                                                                           TransferInput<NullnessNoInitValue,NullnessNoInitStore> in)

When the conservativeArgumentNullnessAfterInvocation flag is turned off, 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 on, the analysis is more conservative by checking 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<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitMethodInvocation in class CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>

visitReturn

public TransferResult<NullnessNoInitValue,NullnessNoInitStore> visitReturn(ReturnNode n,
                                                                                 TransferInput<NullnessNoInitValue,NullnessNoInitStore> in)

Specified by:

visitReturn in interface NodeVisitor<TransferResult<NullnessNoInitValue,NullnessNoInitStore>,TransferInput<NullnessNoInitValue,NullnessNoInitStore>>

Overrides:

visitReturn in class CFAbstractTransfer<NullnessNoInitValue,NullnessNoInitStore,NullnessNoInitTransfer>