diff --git a/checker/src/org/checkerframework/checker/index/lowerbound/LowerBoundAnnotatedTypeFactory.java b/checker/src/org/checkerframework/checker/index/lowerbound/LowerBoundAnnotatedTypeFactory.java index d8947a5ee00..0d84399eb7a 100644 --- a/checker/src/org/checkerframework/checker/index/lowerbound/LowerBoundAnnotatedTypeFactory.java +++ b/checker/src/org/checkerframework/checker/index/lowerbound/LowerBoundAnnotatedTypeFactory.java @@ -21,6 +21,7 @@ import org.checkerframework.checker.index.qual.GTENegativeOne; import org.checkerframework.checker.index.qual.IndexFor; import org.checkerframework.checker.index.qual.IndexOrHigh; +import org.checkerframework.checker.index.qual.IndexOrLow; import org.checkerframework.checker.index.qual.LowerBoundUnknown; import org.checkerframework.checker.index.qual.MinLen; import org.checkerframework.checker.index.qual.NonNegative; @@ -75,6 +76,7 @@ public class LowerBoundAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { public LowerBoundAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker); addAliasedAnnotation(IndexFor.class, NN); + addAliasedAnnotation(IndexOrLow.class, GTEN1); addAliasedAnnotation(IndexOrHigh.class, NN); imf = new IndexMethodIdentifier(processingEnv); diff --git a/checker/src/org/checkerframework/checker/index/qual/IndexOrLow.java b/checker/src/org/checkerframework/checker/index/qual/IndexOrLow.java new file mode 100644 index 00000000000..0c779e5046c --- /dev/null +++ b/checker/src/org/checkerframework/checker/index/qual/IndexOrLow.java @@ -0,0 +1,18 @@ +package org.checkerframework.checker.index.qual; + +/** + * An integer that is either -1 or is a valid index for each of the given sequences. + * + *

Writing {@code @IndexOrLow("arr")} is equivalent to writing {@link + * GTENegativeOne @GTENegativeOne} {@link LTLengthOf @LTLengthOf("arr")}, and that is how it is + * treated internally by the checker. Thus, if you write an {@code @IndexOrLow("arr")} annotation, + * you might see warnings about {@code @GTENegativeOne} or {@code @LTLengthOf}. + * + * @see GTENegativeOne + * @see LTLengthOf + * @checker_framework.manual #index-checker Index Checker + */ +public @interface IndexOrLow { + /** Sequences that the annotated expression is a valid index for (or it's -1). */ + String[] value() default {}; +} diff --git a/checker/src/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java b/checker/src/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java index ff9f1342268..c638fd2f21f 100644 --- a/checker/src/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java +++ b/checker/src/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java @@ -22,6 +22,7 @@ import org.checkerframework.checker.index.minlen.MinLenChecker; import org.checkerframework.checker.index.qual.IndexFor; import org.checkerframework.checker.index.qual.IndexOrHigh; +import org.checkerframework.checker.index.qual.IndexOrLow; import org.checkerframework.checker.index.qual.LTEqLengthOf; import org.checkerframework.checker.index.qual.LTLengthOf; import org.checkerframework.checker.index.qual.LTOMLengthOf; @@ -66,6 +67,7 @@ public UpperBoundAnnotatedTypeFactory(BaseTypeChecker checker) { UNKNOWN = AnnotationUtils.fromClass(elements, UpperBoundUnknown.class); addAliasedAnnotation(IndexFor.class, createLTLengthOfAnnotation(new String[0])); + addAliasedAnnotation(IndexOrLow.class, createLTLengthOfAnnotation(new String[0])); addAliasedAnnotation(IndexOrHigh.class, createLTEqLengthOfAnnotation(new String[0])); imf = new IndexMethodIdentifier(processingEnv); @@ -126,6 +128,7 @@ protected ExpressionAnnotationHelper createExpressionAnnotationHelper() { annos.add(LTLengthOf.class); annos.add(LTEqLengthOf.class); annos.add(IndexFor.class); + annos.add(IndexOrLow.class); annos.add(IndexOrHigh.class); annos.add(LTOMLengthOf.class); return new ExpressionAnnotationHelper(this, annos) { @@ -155,6 +158,11 @@ public AnnotationMirror aliasedAnnotation(AnnotationMirror a) { AnnotationUtils.getElementValueArray(a, "value", String.class, true); return createLTLengthOfAnnotation(stringList.toArray(new String[0])); } + if (AnnotationUtils.areSameByClass(a, IndexOrLow.class)) { + List stringList = + AnnotationUtils.getElementValueArray(a, "value", String.class, true); + return createLTLengthOfAnnotation(stringList.toArray(new String[0])); + } if (AnnotationUtils.areSameByClass(a, IndexOrHigh.class)) { List stringList = AnnotationUtils.getElementValueArray(a, "value", String.class, true); diff --git a/checker/tests/lowerbound/IndexOrLowTests.java b/checker/tests/lowerbound/IndexOrLowTests.java new file mode 100644 index 00000000000..f30566c7276 --- /dev/null +++ b/checker/tests/lowerbound/IndexOrLowTests.java @@ -0,0 +1,29 @@ +import org.checkerframework.checker.index.qual.GTENegativeOne; +import org.checkerframework.checker.index.qual.IndexOrLow; +import org.checkerframework.checker.index.qual.LTLengthOf; + +public class IndexOrLowTests { + int[] array = {1, 2}; + + @IndexOrLow("array") + int index = -1; + + void test() { + //:: error: (array.access.unsafe.low) + array[index] = 1; + + int y = index + 1; + array[y] = 1; + if (y < array.length) { + array[y] = 1; + } + //:: error: (assignment.type.incompatible) + index = -4; + } + + void test2(@LTLengthOf("array") @GTENegativeOne int param) { + index = array.length - 1; + @LTLengthOf("array") @GTENegativeOne int x = index; + index = param; + } +} diff --git a/checker/tests/upperbound/IndexOrLowTests.java b/checker/tests/upperbound/IndexOrLowTests.java new file mode 100644 index 00000000000..82acd73a92a --- /dev/null +++ b/checker/tests/upperbound/IndexOrLowTests.java @@ -0,0 +1,29 @@ +import org.checkerframework.checker.index.qual.GTENegativeOne; +import org.checkerframework.checker.index.qual.IndexOrLow; +import org.checkerframework.checker.index.qual.LTLengthOf; + +public class IndexOrLowTests { + int[] array = {1, 2}; + + @IndexOrLow("array") + int index = -1; + + void test() { + array[index] = 1; + + int y = index + 1; + //:: error: (array.access.unsafe.high) + array[y] = 1; + if (y < array.length) { + array[y] = 1; + } + //:: error: (assignment.type.incompatible) + index = array.length; + } + + void test2(@LTLengthOf("array") @GTENegativeOne int param) { + index = array.length - 1; + @LTLengthOf("array") @GTENegativeOne int x = index; + index = param; + } +} diff --git a/docs/manual/index-checker.tex b/docs/manual/index-checker.tex index 82a27bc6046..a314185f1c4 100644 --- a/docs/manual/index-checker.tex +++ b/docs/manual/index-checker.tex @@ -75,6 +75,12 @@ \section{Index Checker structure and annotations\label{index-annotations}} each named array. This type combines \refqualclass{checker/index/qual}{NonNegative} and \refqualclass{checker/index/qual}{LTEqLengthOf}. + + \item[\refqualclasswithparams{checker/index/qual}{IndexOrLow}{String[] names}] + The value is -1 or is a valid index for + each named array. This type combines + \refqualclass{checker/index/qual}{GTENegativeOne} and + \refqualclass{checker/index/qual}{LTEqLengthOf}. \end{description} \section{Lower bounds\label{index-lowerbound}}