Add @IndexOrLow annotation (#1013)

typetools · Jan 21, 2017 · 5596a01 · 5596a01
1 parent d71777c
commit 5596a01
Show file tree

Hide file tree

Showing 6 changed files with 92 additions and 0 deletions.
diff --git a/...ker/src/org/checkerframework/checker/index/lowerbound/LowerBoundAnnotatedTypeFactory.java b/...ker/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
@@ -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.
+ *
+ * <p>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/...ker/src/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java b/...ker/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<String> stringList =
+                    AnnotationUtils.getElementValueArray(a, "value", String.class, true);
+            return createLTLengthOfAnnotation(stringList.toArray(new String[0]));
+        }
         if (AnnotationUtils.areSameByClass(a, IndexOrHigh.class)) {
             List<String> stringList =
                     AnnotationUtils.getElementValueArray(a, "value", String.class, true);

diff --git a/checker/tests/lowerbound/IndexOrLowTests.java 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
@@ -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
@@ -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}}