org.checkerframework.checker.nullness

Class NullnessTransfer

java.lang.Object

org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<V,S>,org.checkerframework.dataflow.analysis.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:

org.checkerframework.dataflow.analysis.TransferFunction<NullnessValue,NullnessStore>, org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.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.
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 Nullable.

Field Summary

Fields

Modifier and Type	Field and Description
protected KeyForAnnotatedTypeFactory	keyForTypeFactory
protected javax.lang.model.element.AnnotationMirror	NONNULL Annotations of the non-null type system.
protected javax.lang.model.element.AnnotationMirror	NULLABLE Annotations of the non-null type system.

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)

Method Summary

Modifier and Type	Method and Description
protected NullnessValue	finishValue(NullnessValue value, NullnessStore store)
protected void	makeNonNull(NullnessStore store, org.checkerframework.dataflow.cfg.node.Node node) Sets a given Node to non-null in the given store.
protected void	makeNonNull(org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> result, org.checkerframework.dataflow.cfg.node.Node node) Sets a given Node node to non-null in the given TransferResult.
protected org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	strengthenAnnotationOfEqualTo(org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> res, org.checkerframework.dataflow.cfg.node.Node firstNode, org.checkerframework.dataflow.cfg.node.Node secondNode, NullnessValue firstValue, NullnessValue secondValue, boolean notEqualTo)
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitArrayAccess(org.checkerframework.dataflow.cfg.node.ArrayAccessNode n, org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitFieldAccess(org.checkerframework.dataflow.cfg.node.FieldAccessNode n, org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p) If an invariant field is initialized and has the invariant annotation, than it has at least the invariant annotation.
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitInstanceOf(org.checkerframework.dataflow.cfg.node.InstanceOfNode n, org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitMethodAccess(org.checkerframework.dataflow.cfg.node.MethodAccessNode n, org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitMethodInvocation(org.checkerframework.dataflow.cfg.node.MethodInvocationNode n, org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> in)
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitReturn(org.checkerframework.dataflow.cfg.node.ReturnNode n, org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> in)
org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>	visitThrow(org.checkerframework.dataflow.cfg.node.ThrowNode n, org.checkerframework.dataflow.analysis.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, finishValue, getValueFromFactory, getValueWithSameAnnotations, initialStore, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversion

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

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, 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, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, 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

Annotations of the non-null type system.

NULLABLE

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

Annotations of the non-null type system.

keyForTypeFactory

protected final KeyForAnnotatedTypeFactory keyForTypeFactory

Constructor Detail

NullnessTransfer

public NullnessTransfer(NullnessAnalysis analysis)

Method Detail

makeNonNull

protected void makeNonNull(NullnessStore store,
                           org.checkerframework.dataflow.cfg.node.Node node)

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

makeNonNull

protected void makeNonNull(org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> result,
                           org.checkerframework.dataflow.cfg.node.Node node)

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

finishValue

protected NullnessValue finishValue(NullnessValue value,
                                    NullnessStore store)

Overrides:

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

strengthenAnnotationOfEqualTo

protected org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> strengthenAnnotationOfEqualTo(org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> res,
                                                                                                                           org.checkerframework.dataflow.cfg.node.Node firstNode,
                                                                                                                           org.checkerframework.dataflow.cfg.node.Node secondNode,
                                                                                                                           NullnessValue firstValue,
                                                                                                                           NullnessValue secondValue,
                                                                                                                           boolean notEqualTo)

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 org.checkerframework.framework.flow.CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

visitArrayAccess

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitArrayAccess(org.checkerframework.dataflow.cfg.node.ArrayAccessNode n,
                                                                                                           org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitArrayAccess in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

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

visitInstanceOf

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitInstanceOf(org.checkerframework.dataflow.cfg.node.InstanceOfNode n,
                                                                                                          org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitInstanceOf in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitInstanceOf in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

visitMethodAccess

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitMethodAccess(org.checkerframework.dataflow.cfg.node.MethodAccessNode n,
                                                                                                            org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitMethodAccess in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitMethodAccess in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

visitFieldAccess

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitFieldAccess(org.checkerframework.dataflow.cfg.node.FieldAccessNode n,
                                                                                                           org.checkerframework.dataflow.analysis.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 field of the 'this' receiver are tracked for initialization.

Specified by:

visitFieldAccess in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitFieldAccess in class InitializationTransfer<NullnessValue,NullnessTransfer,NullnessStore>

visitThrow

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitThrow(org.checkerframework.dataflow.cfg.node.ThrowNode n,
                                                                                                     org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> p)

Specified by:

visitThrow in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitThrow in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

visitMethodInvocation

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitMethodInvocation(org.checkerframework.dataflow.cfg.node.MethodInvocationNode n,
                                                                                                                org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> in)

Specified by:

visitMethodInvocation in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

visitMethodInvocation in class InitializationTransfer<NullnessValue,NullnessTransfer,NullnessStore>

visitReturn

public org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore> visitReturn(org.checkerframework.dataflow.cfg.node.ReturnNode n,
                                                                                                      org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore> in)

Specified by:

visitReturn in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<NullnessValue,NullnessStore>,org.checkerframework.dataflow.analysis.TransferInput<NullnessValue,NullnessStore>>

Overrides:

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