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:

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.
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.

Author:

Stefan Heule

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) This method is called before returning the abstract value value as 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 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, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitCase, visitClassName, visitConditionalNot, visitEqualTo, 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,
                           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.

finishValue

protected NullnessValue finishValue(NullnessValue value,
                                    NullnessStore store)

Description copied from class: CFAbstractTransfer

This method is called before returning the abstract value value as the result of the transfer function. By default, the value is not changed but subclasses might decide to implement some functionality. The store at this position is also passed.

Overrides:

finishValue in class CFAbstractTransfer<NullnessValue,NullnessStore,NullnessTransfer>

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).

Note that when overriding this method, when a new type is inserted into the store, splitAssignments 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 AbstractNodeVisitor<TransferResult<NullnessValue,NullnessStore>,TransferInput<NullnessValue,NullnessStore>>

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 field 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>