org.checkerframework.checker.index.lowerbound

Class LowerBoundTransfer

java.lang.Object

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

org.checkerframework.framework.flow.CFAbstractTransfer<CFValue,CFStore,CFTransfer>

org.checkerframework.framework.flow.CFTransfer

org.checkerframework.checker.index.IndexAbstractTransfer

org.checkerframework.checker.index.lowerbound.LowerBoundTransfer

All Implemented Interfaces:

TransferFunction<CFValue,CFStore>, NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

public class LowerBoundTransfer
extends IndexAbstractTransfer

Implements dataflow refinement rules based on tests: <, >, ==, and their derivatives.

Also implements the logic for binary operations: +, -, *, /, and %.

>, <, ≥, ≤, ==, and != nodes are represented as combinations of > and ≥ (e.g. == is ≥ in both directions in the then branch), and implement refinements based on these decompositions.

 Refinement/transfer rules for conditionals:

 There are two "primitives":

 x > y, which implies things about x based on y's type:

 y has type:    implies x has type:
  gte-1                nn
  nn                   pos
  pos                  pos

 and x ≥ y:

 y has type:    implies x has type:
  gte-1                gte-1
  nn                   nn
  pos                  pos

 These two "building blocks" can be combined to make all
 other conditional expressions:

 EXPR             THEN          ELSE
 x > y            x > y         y ≥ x
 x ≥ y           x ≥ y        y > x
 x < y            y > x         x ≥ y
 x ≤ y           y ≥ x        x > y

 Or, more formally:

 EXPR        THEN                                        ELSE
 x > y       x_refined = GLB(x_orig, promote(y))         y_refined = GLB(y_orig, x)
 x ≥ y      x_refined = GLB(x_orig, y)                  y_refined = GLB(y_orig, promote(x))
 x < y       y_refined = GLB(y_orig, promote(x))         x_refined = GLB(x_orig, y)
 x ≤ y      y_refined = GLB(y_orig, x)                  x_refined = GLB(x_orig, promote(y))

 where GLB is the greatest lower bound and promote is the increment
 function on types (or, equivalently, the function specified by the "x
 > y" information above).

 There's also ==, which is a special case. Only the THEN
 branch is refined:

 EXPR             THEN                   ELSE
 x == y           x ≥ y && y ≥ x       nothing known

 or, more formally:

 EXPR            THEN                                    ELSE
 x == y          x_refined = GLB(x_orig, y_orig)         nothing known
                y_refined = GLB(x_orig, y_orig)

 finally, not equal:

 EXPR             THEN                   ELSE
 x != y           nothing known          x ≥ y && y ≥ x

 more formally:

 EXPR            THEN               ELSE
 x != y          nothing known      x_refined = GLB(x_orig, y_orig)
                                   y_refined = GLB(x_orig, y_orig)

 

Field Summary

Fields

Modifier and Type	Field and Description
javax.lang.model.element.AnnotationMirror	GTEN1 The canonical GTENegativeOne annotation.
javax.lang.model.element.AnnotationMirror	NN The canonical NonNegative annotation.
javax.lang.model.element.AnnotationMirror	POS The canonical Positive annotation.
javax.lang.model.element.AnnotationMirror	UNKNOWN The canonical LowerBoundUnknown annotation.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
LowerBoundTransfer(CFAnalysis analysis)

Method Summary

Modifier and Type	Method and Description
javax.lang.model.element.AnnotationMirror	getAnnotationForRemainder(IntegerRemainderNode node, TransferInput<CFValue,CFStore> p) getAnnotationForRemainder handles these cases: * % 1/-1 → nn pos/nn % * → nn gten1 % * → gten1 * % * → lbu
protected void	refineGT(Node left, javax.lang.model.element.AnnotationMirror leftAnno, Node right, javax.lang.model.element.AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in) The implementation of the algorithm for refining a > test.
protected void	refineGTE(Node left, javax.lang.model.element.AnnotationMirror leftAnno, Node right, javax.lang.model.element.AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in) Refines left to exactly the level of right, since in the worst case they're equal.
protected TransferResult<CFValue,CFStore>	strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> result, Node firstNode, Node secondNode, CFValue firstValue, CFValue secondValue, boolean notEqualTo) Implements the transfer rules for both equal nodes and not-equals nodes.
TransferResult<CFValue,CFStore>	visitBitwiseAnd(BitwiseAndNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitIntegerDivision(IntegerDivisionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitIntegerRemainder(IntegerRemainderNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalAddition(NumericalAdditionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalMultiplication(NumericalMultiplicationNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitNumericalSubtraction(NumericalSubtractionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitSignedRightShift(SignedRightShiftNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitUnsignedRightShift(UnsignedRightShiftNode n, TransferInput<CFValue,CFStore> p)

Methods inherited from class org.checkerframework.checker.index.IndexAbstractTransfer

visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqual

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

addInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversion

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

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, 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, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast

Field Detail

GTEN1

public final javax.lang.model.element.AnnotationMirror GTEN1

The canonical GTENegativeOne annotation.

NN

public final javax.lang.model.element.AnnotationMirror NN

The canonical NonNegative annotation.

POS

public final javax.lang.model.element.AnnotationMirror POS

The canonical Positive annotation.

UNKNOWN

public final javax.lang.model.element.AnnotationMirror UNKNOWN

The canonical LowerBoundUnknown annotation.

Constructor Detail

LowerBoundTransfer

public LowerBoundTransfer(CFAnalysis analysis)

Method Detail

strengthenAnnotationOfEqualTo

protected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> result,
                                                                        Node firstNode,
                                                                        Node secondNode,
                                                                        CFValue firstValue,
                                                                        CFValue secondValue,
                                                                        boolean notEqualTo)

Implements the transfer rules for both equal nodes and not-equals nodes.

Overrides:

strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

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

refineGT

protected void refineGT(Node left,
                        javax.lang.model.element.AnnotationMirror leftAnno,
                        Node right,
                        javax.lang.model.element.AnnotationMirror rightAnno,
                        CFStore store,
                        TransferInput<CFValue,CFStore> in)

The implementation of the algorithm for refining a > test. Changes the type of left (the greater one) to one closer to bottom than the type of right. Can't call the promote function from the ATF directly because a new expression isn't introduced here - the modifications have to be made to an existing one.

Specified by:

refineGT in class IndexAbstractTransfer

refineGTE

protected void refineGTE(Node left,
                         javax.lang.model.element.AnnotationMirror leftAnno,
                         Node right,
                         javax.lang.model.element.AnnotationMirror rightAnno,
                         CFStore store,
                         TransferInput<CFValue,CFStore> in)

Refines left to exactly the level of right, since in the worst case they're equal. Modifies an existing type in the store, but has to be careful not to overwrite a more precise existing type.

Specified by:

refineGTE in class IndexAbstractTransfer

getAnnotationForRemainder

public javax.lang.model.element.AnnotationMirror getAnnotationForRemainder(IntegerRemainderNode node,
                                                                           TransferInput<CFValue,CFStore> p)

getAnnotationForRemainder handles these cases: * % 1/-1 → nn pos/nn % * → nn gten1 % * → gten1 * % * → lbu

visitNumericalAddition

public TransferResult<CFValue,CFStore> visitNumericalAddition(NumericalAdditionNode n,
                                                              TransferInput<CFValue,CFStore> p)

Specified by:

visitNumericalAddition in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitNumericalAddition in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitNumericalSubtraction

public TransferResult<CFValue,CFStore> visitNumericalSubtraction(NumericalSubtractionNode n,
                                                                 TransferInput<CFValue,CFStore> p)

Specified by:

visitNumericalSubtraction in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitNumericalSubtraction in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitNumericalMultiplication

public TransferResult<CFValue,CFStore> visitNumericalMultiplication(NumericalMultiplicationNode n,
                                                                    TransferInput<CFValue,CFStore> p)

Specified by:

visitNumericalMultiplication in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitNumericalMultiplication in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitIntegerDivision

public TransferResult<CFValue,CFStore> visitIntegerDivision(IntegerDivisionNode n,
                                                            TransferInput<CFValue,CFStore> p)

Specified by:

visitIntegerDivision in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitIntegerDivision in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitIntegerRemainder

public TransferResult<CFValue,CFStore> visitIntegerRemainder(IntegerRemainderNode n,
                                                             TransferInput<CFValue,CFStore> p)

Specified by:

visitIntegerRemainder in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitIntegerRemainder in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitSignedRightShift

public TransferResult<CFValue,CFStore> visitSignedRightShift(SignedRightShiftNode n,
                                                             TransferInput<CFValue,CFStore> p)

Specified by:

visitSignedRightShift in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitSignedRightShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitUnsignedRightShift

public TransferResult<CFValue,CFStore> visitUnsignedRightShift(UnsignedRightShiftNode n,
                                                               TransferInput<CFValue,CFStore> p)

Specified by:

visitUnsignedRightShift in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitUnsignedRightShift in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitBitwiseAnd

public TransferResult<CFValue,CFStore> visitBitwiseAnd(BitwiseAndNode n,
                                                       TransferInput<CFValue,CFStore> p)

Specified by:

visitBitwiseAnd in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitBitwiseAnd in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>