Package org.checkerframework.checker.index.upperbound

Class OffsetEquation

java.lang.Object
org.checkerframework.checker.index.upperbound.OffsetEquation
public class OffsetEquation extends Object
An offset equation is 2 sets of Java expression strings, one set of added terms and one set of subtracted terms, and a single integer constant. The Java expression strings have been standardized and viewpoint-adapted.

For example, the offset equation for "end - start - 1" has "end" as its only added term, "start" as its only subtracted term, and -1 as its integer constant. Integer literals are folded into the integer constant rather than being kept as terms, so an offset equation with no added terms and no subtracted terms is just an integer constant, as ZERO is.

An offset equation represents the offset element of an Index Checker annotation such as @LTLengthOf. For example, @LTLengthOf(value = "a", offset = "end - start - 1") means that the annotated expression plus end - start - 1 is less than a.length. The Upper Bound Checker adds, subtracts, and compares offset equations in order to compute types; for instance, if i has that type, then i + 1 has type @LTLengthOf(value = "a", offset = "end - start - 2").

An OffsetEquation is mutable.

  • Field Details

    • ZERO

      public static final OffsetEquation ZERO
      The equation for 0 (zero).

    • NEG_1

      public static final OffsetEquation NEG_1
      The equation for -1.

    • ONE

      public static final OffsetEquation ONE
      The equation for 1.

  • Constructor Details

    • OffsetEquation

      protected OffsetEquation(OffsetEquation other)
      Create a new OffsetEquation that is a copy of the given one.
      Parameters:
      other - the OffsetEquation to copy

  • Method Details

    • hasError

      public boolean hasError()

    • getError

      public @Nullable String getError()

    • equals

      public boolean equals(@Nullable Object o)
      Overrides:
      equals in class Object

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • removeSequenceLengths

      public @Nullable OffsetEquation removeSequenceLengths(List<String> sequences)
      Makes a copy of this offset and removes any added terms that are accesses to the length of the listed sequences. If any terms were removed, then the copy is returned. Otherwise, null is returned.
      Parameters:
      sequences - list of sequences (arrays or strings)
      Returns:
      a copy of this equation with array.length and string.length() removed or null if no array.lengths or string.length() could be removed

    • copyAdd

      public OffsetEquation copyAdd(char op, OffsetEquation other)
      Adds or subtracts the other equation to a copy of this one.

      If subtraction is specified, then every term in other is subtracted.

      Parameters:
      op - '-' for subtraction or '+' for addition
      other - equation to add or subtract
      Returns:
      a copy of this equation +/- other

    • lessThanOrEqual

      public boolean lessThanOrEqual(OffsetEquation other)
      Returns true if this equation is known to be less than or equal to the other equation.
      Parameters:
      other - equation
      Returns:
      true if this equation is known to be less than or equal to the other equation

    • isOnlyInt

      public boolean isOnlyInt()
      Returns true if this equation is a single int value.
      Returns:
      true if this equation is a single int value

    • getIntPart

      public int getIntPart()
      Returns the int part of this equation.

      The equation may or may not have other terms. Use isOnlyInt() to determine if the equation is only this int value.

      Returns:
      the int part of this equation

    • isNegOne

      public boolean isNegOne()
      Returns true if this equation is exactly -1.
      Returns:
      true if this equation is exactly -1

    • isNonNegativeInt

      public boolean isNonNegativeInt()
      Returns true if this equation is only an int value that is non-negative.
      Returns:
      true if this equation is only an int value that is non-negative

    • isNonPositiveInt

      public boolean isNonPositiveInt()
      Returns true if this equation is only an int value that is non-positive.
      Returns:
      true if this equation is only an int value that is non-positive

    • getOnlyIntOffsetEquation

      public static @Nullable OffsetEquation getOnlyIntOffsetEquation(Set<OffsetEquation> equationSet)
      Returns an offset equation in the given set that is only an int value, or null if there isn't one.
      Parameters:
      equationSet - a set of offset equations
      Returns:
      an offset equation that is only an int value, or null if there isn't one

    • createOffsetForInt

      public static OffsetEquation createOffsetForInt(int value)
      Creates an offset equation that is only the int value specified.
      Parameters:
      value - int value of the equation
      Returns:
      an offset equation that is only the int value specified

    • createOffsetFromJavaExpression

      public static OffsetEquation createOffsetFromJavaExpression(String expressionEquation)
      Creates an offset equation from the expressionEquation. The expressionEquation may be several Java expressions added or subtracted from each other. The expressionEquation may also start with + or -. If the expressionEquation is the empty string, then the offset equation returned is zero.
      Parameters:
      expressionEquation - a Java expression made up of sums and differences
      Returns:
      an offset equation created from expressionEquation

    • createOffsetFromNodesValue

      public static @Nullable OffsetEquation createOffsetFromNodesValue(Node node, ValueAnnotatedTypeFactory factory, char op)
      If node is an int value known at compile time, then the returned equation is just the int value or if op is '-', the return equation is the negation of the int value.

      Otherwise, null is returned.

      Parameters:
      node - the Node from which to create an offset equation
      factory - an AnnotationTypeFactory
      op - '+' or '-'
      Returns:
      an offset equation from value of known or null if the value isn't known

    • createOffsetFromNode

      public static OffsetEquation createOffsetFromNode(Node node, AnnotationProvider factory, char op)
      Creates an offset equation from the Node.

      If node is an addition or subtracted node, then this method is called recursively on the left and right-hand nodes and the two equations are added/subtracted to each other depending on the value of op.

      Otherwise the return equation is created by converting the node to a JavaExpression and then added as a term to the returned equation. If op is '-' then it is a subtracted term.

      Parameters:
      node - the Node from which to create an offset equation
      factory - an AnnotationTypeFactory
      op - '+' or '-'
      Returns:
      an offset equation from the Node