Package org.checkerframework.common.value.util

Class Range

java.lang.Object

org.checkerframework.common.value.util.Range

public class Range
extends Object

The Range class models a 64-bit two's-complement integral interval, such as all integers between 1 and 10, inclusive.

Range is immutable.

Field Summary

Fields

Modifier and Type	Field	Description
static final Range	BYTE_EVERYTHING	A range containing all possible 8-bit values.
static final Range	CHAR_EVERYTHING	A range containing all possible char values.
static final Range	EVERYTHING	An alias to the range containing all possible 64-bit values.
final long	from	The lower bound of the interval, inclusive.
static boolean	ignoreOverflow	Should ranges take overflow into account or ignore it? If ignoreOverflow is true, then operations that would result in more than the max value are clipped to the max value (and similarly for the min).
static final Range	INT_EVERYTHING	A range containing all possible 32-bit values.
static final Range	LONG_EVERYTHING	A range containing all possible 64-bit values.
static final @InternedDistinct Range	NOTHING	The empty range.
static final Range	SHORT_EVERYTHING	A range containing all possible 16-bit values.
final long	to	The upper bound of the interval, inclusive.

Method Summary

Modifier and Type	Method	Description
Range	bitwiseAnd(Range right)	Returns a range that includes all possible values resulting from performing the bitwise and operation on a value in this range by a mask in the specified range.
Range	bitwiseComplement()	Returns the range of a variable that falls within this range after applying the bitwise complement operation.
Range	bitwiseOr(Range right)	We give up the analysis for bitwise OR operation.
Range	bitwiseXor(Range right)	We give up the analysis for bitwise XOR operation.
Range	byteRange()	Converts this range to an 8-bit byte range.
Range	charRange()	Converts this range to a char range.
boolean	contains(long element)	Returns true if the element is contained in this range.
boolean	contains(Range other)	Returns true if the other range is contained in this range.
static Range	create(long from, long to)	Constructs a range with its bounds specified by two parameters, from and to.
static Range	create(Collection<? extends Number> values)	Create a Range from a collection of Numbers.
static Range	create(TypeKind typeKind)	Returns a Range representing all possible values for the given primitive type.
Range	divide(Range right)	Returns the smallest range that includes all possible values resulting from dividing (integer division) an arbitrary value in this range by an arbitrary value in the specified range.
boolean	equals(@Nullable Object obj)
int	hashCode()
Range	intersect(Range right)	Returns the smallest range that includes all values contained in both of the two ranges.
Range	intRange()	Converts this range to a 32-bit integral range.
boolean	isByteEverything()	Return true if this range contains every byte value.
boolean	isCharEverything()	Return true if this range contains every char value.
boolean	isConstant()	Returns true if this range represents a constant value.
boolean	isIntEverything()	Return true if this range contains every int value.
boolean	isLongEverything()	Return true if this range contains every long value.
boolean	isNothing()	Return true if this range contains no values.
boolean	isShortEverything()	Return true if this range contains every short value.
boolean	isWiderThan(long value)	Returns true if the range is wider than a given value, i.e., if the number of possible values enclosed by this range is more than the given value.
boolean	isWithin(long lb, long ub)	Returns true if this range is completely contained in the range specified by the given lower bound inclusive and upper bound inclusive.
boolean	isWithinInteger()	Returns true if this range is completely contained in the scope of the Integer type.
Range	max(Range other)	Returns the range with the highest to and from values of this range and the passed range.
Range	min(Range other)	Returns the range with the lowest to and from values of this range and the passed range.
Range	minus(Range right)	Returns the smallest range that includes all possible values resulting from subtracting an arbitrary value in the specified range from an arbitrary value in this range.
Range	plus(Range right)	Returns the smallest range that includes all possible values resulting from adding an arbitrary value in the specified range to an arbitrary value in this range.
Range	refineEqualTo(Range right)	Refines this range to reflect that some value in it can be equal to a value in the given range.
Range	refineGreaterThan(Range right)	Refines this range to reflect that some value in it can be greater than a value in the given range.
Range	refineGreaterThanEq(Range right)	Refines this range to reflect that some value in it can be greater than or equal to a value in the given range.
Range	refineLessThan(Range right)	Refines this range to reflect that some value in it can be less than a value in the given range.
Range	refineLessThanEq(Range right)	Refines this range to reflect that some value in it can be less than or equal to a value in the given range.
Range	refineNotEqualTo(Range right)	Refines this range to reflect that some value in it must not be equal to a value in the given range.
Range	remainder(Range right)	Returns a range that includes all possible values of the remainder of dividing an arbitrary value in this range by an arbitrary value in the specified range.
Range	shiftLeft(Range right)	Returns a range that includes all possible values resulting from left shifting an arbitrary value in this range by an arbitrary number of bits in the specified range.
Range	shortRange()	Converts a this range to a 16-bit short range.
Range	signedShiftRight(Range right)	Returns a range that includes all possible values resulting from signed right shifting an arbitrary value in this range by an arbitrary number of bits in the specified range.
Range	times(Range right)	Returns the smallest range that includes all possible values resulting from multiplying an arbitrary value in the specified range by an arbitrary value in this range.
String	toString()
Range	unaryMinus()	Returns the range of a variable that falls within this range after applying the unary minus operation.
Range	unaryPlus()	Returns the range of a variable that falls within this range after applying the unary plus operation (which is a no-op).
Range	union(Range right)	Returns the smallest range that includes all values contained in either of the two ranges.
Range	unsignedShiftRight(Range right)	When this range only contains non-negative values, the refined result should be the same as signedShiftRight(Range).

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Details

from

public final long from

The lower bound of the interval, inclusive.

to

public final long to

The upper bound of the interval, inclusive.

ignoreOverflow

public static boolean ignoreOverflow

Should ranges take overflow into account or ignore it?

• If ignoreOverflow is true, then operations that would result in more than the max value are clipped to the max value (and similarly for the min).
• If ignoreOverflow is false, then operations that would result in more than the max wrap around according to the rules of twos-complement arithmetic and produce a smaller value (and similarly for the min).

Any checker that uses this library should set this field. By default, this field is set to false (meaning overflow is taken into account), but a previous checker might have set it to true.

A static field is used because passing an instance field throughout the class bloats the code.

LONG_EVERYTHING

public static final Range LONG_EVERYTHING

A range containing all possible 64-bit values.

INT_EVERYTHING

public static final Range INT_EVERYTHING

A range containing all possible 32-bit values.

SHORT_EVERYTHING

public static final Range SHORT_EVERYTHING

A range containing all possible 16-bit values.

CHAR_EVERYTHING

public static final Range CHAR_EVERYTHING

A range containing all possible char values.

BYTE_EVERYTHING

public static final Range BYTE_EVERYTHING

A range containing all possible 8-bit values.

NOTHING

public static final @InternedDistinct Range NOTHING

The empty range. This is the only Range object that contains nothing

EVERYTHING

public static final Range EVERYTHING

An alias to the range containing all possible 64-bit values.

Method Details

create

public static Range create(long from,
 long to)

Constructs a range with its bounds specified by two parameters, from and to. Requires from <= to.

Parameters:

from - the lower bound (inclusive)

to - the upper bound (inclusive)

Returns:

the Range [from..to]

create

public static Range create(Collection<? extends Number> values)

Create a Range from a collection of Numbers.

Parameters:

values - collection whose min and max values will be used as the range's from and to values

Returns:

a range that encompasses all the argument's values (NOTHING if the argument is an empty collection)

create

public static Range create(TypeKind typeKind)

Returns a Range representing all possible values for the given primitive type.

Parameters:

typeKind - one of INT, SHORT, BYTE, CHAR, or LONG

Returns:

the range for the given primitive type

toString

public String toString()

Overrides:

toString in class Object

equals

public boolean equals(@Nullable Object obj)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

isLongEverything

public boolean isLongEverything()

Return true if this range contains every long value.

isIntEverything

public boolean isIntEverything()

Return true if this range contains every int value.

isShortEverything

public boolean isShortEverything()

Return true if this range contains every short value.

isCharEverything

public boolean isCharEverything()

Return true if this range contains every char value.

isByteEverything

public boolean isByteEverything()

Return true if this range contains every byte value.

isNothing

public boolean isNothing()

Return true if this range contains no values.

intRange

public Range intRange()

Converts this range to a 32-bit integral range.

If ignoreOverflow is true and one of the bounds is outside the Integer range, then that bound is set to the bound of the Integer range.

If ignoreOverflow is false and this range is too wide, i.e., wider than the full range of the Integer class, return INT_EVERYTHING.

If ignoreOverflow is false and the bounds of this range are not representable as 32-bit integers, convert the bounds to Integer type in accordance with Java twos-complement overflow rules, e.g., Integer.MAX_VALUE + 1 is converted to Integer.MIN_VALUE.

Returns:

this range, converted to a 32-bit integral range

shortRange

public Range shortRange()

Converts a this range to a 16-bit short range.

If ignoreOverflow is true and one of the bounds is outside the Short range, then that bound is set to the bound of the Short range.

If ignoreOverflow is false and this range is too wide, i.e., wider than the full range of the Short class, return SHORT_EVERYTHING.

If ignoreOverflow is false and the bounds of this range are not representable as 16-bit integers, convert the bounds to Short type in accordance with Java twos-complement overflow rules, e.g., Short.MAX_VALUE + 1 is converted to Short.MIN_VALUE.

Returns:

this range, converted to a 16-bit short range

charRange

public Range charRange()

Converts this range to a char range.

If ignoreOverflow is true and one of the bounds is outside the Character range, then that bound is set to the bound of the Character range.

If ignoreOverflow is false and this range is too wide, i.e., wider than the full range of the Character class, return CHAR_EVERYTHING.

If ignoreOverflow is false and the bounds of this range are not representable as 8-bit integers, convert the bounds to Character type in accordance with Java overflow rules (twos-complement), e.g., Character.MAX_VALUE + 1 is converted to Character.MIN_VALUE.

byteRange

public Range byteRange()

Converts this range to an 8-bit byte range.

If ignoreOverflow is true and one of the bounds is outside the Byte range, then that bound is set to the bound of the Byte range.

If ignoreOverflow is false and this range is too wide, i.e., wider than the full range of the Byte class, return BYTE_EVERYTHING.

If ignoreOverflow is false and the bounds of this range are not representable as 8-bit integers, convert the bounds to Byte type in accordance with Java twos-complement overflow rules, e.g., Byte.MAX_VALUE + 1 is converted to Byte.MIN_VALUE.

Returns:

this range, converted to an 8-bit byte range

contains

public boolean contains(long element)

Returns true if the element is contained in this range.

Parameters:

element - the value to seek

Returns:

true if element is in this range

contains

public boolean contains(Range other)

Returns true if the other range is contained in this range.

Parameters:

other - the range that might be within this one

Returns:

true if other is within this range

union

public Range union(Range right)

Returns the smallest range that includes all values contained in either of the two ranges. We call this the union of two ranges.

Parameters:

right - a range to union with this range

Returns:

a range resulting from the union of the specified range and this range

intersect

public Range intersect(Range right)

Returns the smallest range that includes all values contained in both of the two ranges. We call this the intersection of two ranges. If there is no overlap between the two ranges, returns an empty range.

Parameters:

right - the range to intersect with this range

Returns:

a range resulting from the intersection of the specified range and this range

min

public Range min(Range other)

Returns the range with the lowest to and from values of this range and the passed range.

Parameters:

other - the range to compare

Returns:

the range with the lowest to and from values of this range and the passed range

max

public Range max(Range other)

Returns the range with the highest to and from values of this range and the passed range.

Parameters:

other - the range to compare

Returns:

the range with the highest to and from values of this range and the passed range

plus

public Range plus(Range right)

Returns the smallest range that includes all possible values resulting from adding an arbitrary value in the specified range to an arbitrary value in this range. We call this the addition of two ranges.

Parameters:

right - a range to be added to this range

Returns:

the range resulting from the addition of the specified range and this range

minus

public Range minus(Range right)

Returns the smallest range that includes all possible values resulting from subtracting an arbitrary value in the specified range from an arbitrary value in this range. We call this the subtraction of two ranges.

Parameters:

right - the range to be subtracted from this range

Returns:

the range resulting from subtracting the specified range from this range

times

public Range times(Range right)

Returns the smallest range that includes all possible values resulting from multiplying an arbitrary value in the specified range by an arbitrary value in this range. We call this the multiplication of two ranges.

Parameters:

right - the specified range to be multiplied by this range

Returns:

the range resulting from multiplying the specified range by this range

divide

public Range divide(Range right)

Returns the smallest range that includes all possible values resulting from dividing (integer division) an arbitrary value in this range by an arbitrary value in the specified range. We call this the division of two ranges.

Parameters:

right - the specified range by which this range is divided

Returns:

the range resulting from dividing this range by the specified range

remainder

public Range remainder(Range right)

Returns a range that includes all possible values of the remainder of dividing an arbitrary value in this range by an arbitrary value in the specified range.

In the current implementation, the result might not be the smallest range that includes all the possible values.

Parameters:

right - the specified range by which this range is divided

Returns:

the range of the remainder of dividing this range by the specified range

shiftLeft

public Range shiftLeft(Range right)

Returns a range that includes all possible values resulting from left shifting an arbitrary value in this range by an arbitrary number of bits in the specified range. We call this the left shift of a range.

Parameters:

right - the range of bits by which this range is left shifted

Returns:

the range resulting from left shifting this range by the specified range

signedShiftRight

public Range signedShiftRight(Range right)

Returns a range that includes all possible values resulting from signed right shifting an arbitrary value in this range by an arbitrary number of bits in the specified range. We call this the signed right shift operation of a range.

Parameters:

right - the range of bits by which this range is signed right shifted

Returns:

the range resulting from signed right shifting this range by the specified range

unsignedShiftRight

public Range unsignedShiftRight(Range right)

When this range only contains non-negative values, the refined result should be the same as signedShiftRight(Range). We give up the analysis when this range contains negative value(s).

bitwiseAnd

public Range bitwiseAnd(Range right)

Returns a range that includes all possible values resulting from performing the bitwise and operation on a value in this range by a mask in the specified range. We call this the bitwise and operation of a range.

The current implementation is conservative: it only refines the cases where the range of mask represents a constant. In other cases, it gives up on the refinement and returns EVERYTHING instead.

Parameters:

right - the range of mask of the bitwise and operation

Returns:

the range resulting from the bitwise and operation of this range and the specified range of mask

bitwiseOr

public Range bitwiseOr(Range right)

We give up the analysis for bitwise OR operation.

bitwiseXor

public Range bitwiseXor(Range right)

We give up the analysis for bitwise XOR operation.

unaryPlus

public Range unaryPlus()

Returns the range of a variable that falls within this range after applying the unary plus operation (which is a no-op).

Returns:

this range

unaryMinus

public Range unaryMinus()

Returns the range of a variable that falls within this range after applying the unary minus operation.

Returns:

the resulted range of applying unary minus on an arbitrary value in this range

bitwiseComplement

public Range bitwiseComplement()

Returns the range of a variable that falls within this range after applying the bitwise complement operation.

Returns:

the resulting range of applying bitwise complement on an arbitrary value in this range

refineLessThan

public Range refineLessThan(Range right)

Refines this range to reflect that some value in it can be less than a value in the given range. This is used for calculating the control-flow-refined result of the < operator. For example:

 
    @IntRange(from = 0, to = 10) int a;
    @IntRange(from = 3, to = 7) int b;
     ...
     if (a < b) {
         // range of a is now refined to [0, 6] because a value in range [7, 10]
         // cannot be smaller than variable b with range [3, 7].
         ...
     }
 
 

Use the refineGreaterThanEq(Range) method if you are also interested in refining the range of b in the code above.

Parameters:

right - the specified Range to compare with

Returns:

the refined Range

refineLessThanEq

public Range refineLessThanEq(Range right)

Refines this range to reflect that some value in it can be less than or equal to a value in the given range. This is used for calculating the control-flow-refined result of the <= operator. For example:

 
    @IntRange(from = 0, to = 10) int a;
    @IntRange(from = 3, to = 7) int b;
     ...
     if (a <= b) {
         // range of a is now refined to [0, 7] because a value in range [8, 10]
         // cannot be less than or equal to variable b with range [3, 7].
         ...
     }
 
 

Use the refineGreaterThan(Range) method if you are also interested in refining the range of b in the code above.

Parameters:

right - the specified Range to compare with

Returns:

the refined Range

refineGreaterThan

public Range refineGreaterThan(Range right)

Refines this range to reflect that some value in it can be greater than a value in the given range. This is used for calculating the control-flow-refined result of the > operator. For example:

 
    @IntRange(from = 0, to = 10) int a;
    @IntRange(from = 3, to = 7) int b;
     ...
     if (a > b) {
         // range of a is now refined to [4, 10] because a value in range [0, 3]
         // cannot be greater than variable b with range [3, 7].
         ...
     }
 
 

Use the refineLessThanEq(Range) method if you are also interested in refining the range of b in the code above.

Parameters:

right - the specified Range to compare with

Returns:

the refined Range

refineGreaterThanEq

public Range refineGreaterThanEq(Range right)

Refines this range to reflect that some value in it can be greater than or equal to a value in the given range. This is used for calculating the control-flow-refined result of the >= operator. For example:

 
    @IntRange(from = 0, to = 10) int a;
    @IntRange(from = 3, to = 7) int b;
     ...
     if (a >= b) {
         // range of a is now refined to [3, 10] because a value in range [0, 2]
         // cannot be greater than or equal to variable b with range [3, 7].
         ...
     }
 
 

Use the refineLessThan(Range) method if you are also interested in refining the range of b in the code above.

Parameters:

right - the specified Range to compare with

Returns:

the refined Range

refineEqualTo

public Range refineEqualTo(Range right)

Refines this range to reflect that some value in it can be equal to a value in the given range. This is used for calculating the control-flow-refined result of the == operator. For example:

 
    @IntRange(from = 0, to = 10) int a;
    @IntRange(from = 3, to = 15) int b;
     ...
     if (a == b) {
         // range of a is now refined to [3, 10] because a value in range [0, 2]
         // cannot be equal to variable b with range [3, 15].
         ...
     }
 
 

Parameters:

right - the specified Range to compare with

Returns:

the refined Range

refineNotEqualTo

public Range refineNotEqualTo(Range right)

Refines this range to reflect that some value in it must not be equal to a value in the given range. This only changes the range if the given range (right) contains exactly one integer, and that integer is one of the bounds of this range. This is used for calculating the control-flow-refined result of the != operator. For example:

 
    @IntRange(from = 0, to = 10) int a;
    @IntRange(from = 0, to = 0) int b;
     ...
     if (a != b) {
         // range of a is now refined to [1, 10] because it cannot
         // be zero.
         ...
     }
 
 

Parameters:

right - the specified Range to compare with

Returns:

the refined Range

isWiderThan

public boolean isWiderThan(long value)

Returns true if the range is wider than a given value, i.e., if the number of possible values enclosed by this range is more than the given value.

Parameters:

value - the value to compare with

Returns:

true if wider than the given value

isConstant

public boolean isConstant()

Returns true if this range represents a constant value.

Returns:

true if this range represents a constant value

isWithin

public boolean isWithin(long lb,
 long ub)

Returns true if this range is completely contained in the range specified by the given lower bound inclusive and upper bound inclusive.

Parameters:

lb - lower bound for the range that might contain this one

ub - upper bound for the range that might contain this one

Returns:

true if this range is within the given bounds

isWithinInteger

public boolean isWithinInteger()

Returns true if this range is completely contained in the scope of the Integer type.

Returns:

true if the range is contained within the Integer range inclusive