kelloggm / checker-framework Goto Github PK

From the pilot study:

UBC fails to correctly type this:

for (int i = 0; i < arr.length && i < arr2.length; i++){
arr[i] = arr2[i];
}

Consider these output messages:

src/plume/BCELUtil.java:313: warning: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound
      StackTraceElement caller = ste[1];
                                     ^
  found   : @UpperBoundUnknown int
  required: @LTLengthOf(ste)
src/plume/BCELUtil.java:511: warning: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound
      mg.addLocalVariable(arg_names[ii], arg_types[ii], null, null);
                                                   ^
  found   : @LTLengthOf("arg_names") int
  required: @LTLengthOf(arg_types)

There are two problems with the "required" types.

• The variable name should appear in quotes, as it would in the program.
• The base type (int) is missing.

Knowing that a GTENegativeOne is not -1 should refine it to being NonNegative.

void test(@GTENegativeOne int y) {
    int[] arr = new int[10];
    if (-1 != y){
        int k = arr[y];
    }
}

I think this might be a value checker issue.

Math.random() always returns a number between 0 and 1, and a common pattern for generating a random integer is to call Math.random() and multiply by the upperbound of the integers you would like. Then, the resulting double is casted to an int. This should result in a NonNegative int, but currently it's lower bound unknown.

More to the point, though, I would expect the value checker to be able to handle this case. I suspect a special case would need to be added for these. I should write an email to Suzanne.

Here is a test case, which also appears in file checker/tests/upperbound/ZeroMinLen.java:

public class ZeroMinLen {

    int /*@MinLen(1)*/ [] nums;
    /*@IndexFor("nums")*/ int current_index;

    void test() {
        current_index = 0;
    }

}

The result of List.toArray is, conservatively, @MinLen(0). However, it should be the same as the @MinLen annotation on its receiver. This should be able to be handled by adding a @PolyMinLen annotation in the JDK.

Test case:

  public String /*@MinLen(1)*/ [] m(/*@MinLen(1)*/ ArrayList<String> compiler) {
    return compiler.toArray(new String[0]);
  }

I don't know how to do this. This is to remind me to ask Suzanne about it when she gets back on Monday.

This comes up in a common idiom for comparing adjacent list elements, such as checking sortedness.

For instance:

    for (int i = 0; i < a.length - 1; i++) {
      if (a[i + 1] < a[i]) {
        return false;
      }
    }
    return true;

The JDK should be annotated so that if endsWith returns true, then the receiver has @MinLen at least that of the argument.

See a test case in checker-framework/checker/tests/minlen/EndsWith.java.

There's a test for this here: 540696d

From a pilot study. Test case:

class Pilot4Subtraction {

    private static int[] getSecondHalf(int[] array) {
	int len = array.length/2;
	int b=len-1;
	int[] arr = new int[len];
	for(int a=0; a<len; a++){
	    arr[a]= array[b];
	    b--;
	}
	return arr;
    }

I'll check that code in as Pilot4Subtraction.java, set up to skip for now.

if it is unknown or bottom it wont have a value

Joe knows why

Consider the following code:

int[] newArray = new int[firstArray.length + secondArray.length];
for (int i = 0; i < firstArray.length; i++){	
    newArray[i] = firstArray[i]; //or newArray[i] = secondArray[i];
}

This access should definitely be legal. This came from a pilot study too.

Here is a test case:

  public static String lpad(String s, int length) {
    if (s.length() < length) {
      // unimportant code
    } else {
      return s.substring(0, length);
    }
  }

The checker issues this warning:

warning: [argument.type.incompatible] incompatible types in argument.
      return s.substring(0, length);
                            ^
  found   : @LowerBoundUnknown int
  required: @NonNegative int

There should be a warning issued if a user tries to instantiate an array with a possibly negative number.

import org.checkerframework.checker.lowerbound.qual.*;

// @skip-test until the bug is fixed

public class NegativeArray {

    public static void negativeArray (@GTENegativeOne int len) {
        //:: error: (array.length.negative)
       int [] arr = new int[len];
    }

}

Test Case: checker-framework/checker/tests/lowerbound/NegativeArray.java

We currently don't have a way to deal with offsets. This is a pretty common pattern for accessing arrays, and it almost always results in warnings from the UBC, and sometimes even from the LBC, as well.

I should think a bit about how we might be able to handle offsets in a way that's clean and doesn't require the user to be suppressing warnings all the time.

The UBC is crashing with a null pointer exception on ArraysMDE when run as part of the full Index Checker. Investigate. This is a reminder to myself.

enum.values() should return a array with a minlen of the number of enum values

ie:

    public static enum Direction {
        NORTH, SOUTH, EAST, WEST
    };

    public static void enumValues() {
        Direction @MinLen(4)[] arr = Direction.values();
    }

There is a test case in checker-framework/checker/tests/minlen/EnumValues.java

This may also just be a bug in the CF itself; I'm not sure.

Consider the following code:

    assert max_values > 0;
    values = new int[max_values];

The LBC issues a warning here. If that was an if statement, it wouldn't have done. Is this the right behavior? It seems wrong to me.

Please see test case in file checker/tests/upperbound/IndexForTwoArrays2.java

e.g.

void copy (int @MinLen(1) [] nums) {
	int[] nums_copy = new int[nums.length];
	nums = nums_copy; // nums_copy doesn't have @MinLen(1)
    }

In the Lower Bound Checker, these should be @NonNegative:

• the result of a mask, if the first mask bit not 1
• the result of a mask, if the masked value is @NonNegative
• the result of a signed shift, if the shifted value is @NonNegative

In addition to more focused tests, please ensure that the following type-checks:

  public static String hexEncode(byte[] bytes) {
    StringBuffer s = new StringBuffer(bytes.length * 2);
    for (int i = 0; i < bytes.length; i++) {
      byte b = bytes[i];
      s.append(digits[(b & 0xf0) >> 4]);
      s.append(digits[b & 0x0f]);
    }
    return s.toString();
  }

This problem shows up in the all systems tests.

Consider the following code (from AssignmentContext.java in all-systems):

 void t1(boolean b) {
        String[] s = b ? new String[] {""} : null;
    }

I think MinLen can't unify MLBottom and ML(1) for some reason. The answer should be MLBottom.

For example

    public static void main (@NonNegative int i) {
        if (i != 0) {
            @Positive int m = i;
        }
    }

Should type check

Test case added in checker/tests/lowerbound/nonNegNotZero.java

I've checked in a test case for this: Reassignment.java. 77304ff

Essentially, if you have a LTL int for an array and then resize the array to be some other, new array (or just assign another array into it...), then the LTL needs to be no longer true.

THIS IS A SOUNDNESS BUG

Also thanks to Suzanne for mentioning this (in an unrelated discussion) earlier; I realized while walking home that I didn't remember implementing it...

There are two different ways that a routine may indicate a subarray:

• take as arguments two indexes into the array (start index and end index)
• take as arguments a start index (sometimes called an offset) into the array, and a length of the subarray

It would be nice to have a way to indicate the latter pattern, such as indicating that startIndex + len is an index for an array. The len variable could be annotated as something like @IndexFor("a", offset="startIndex").

Here is a real bug in plume-lib that indicates that programmers mix this up:

  /**
   * Write a portion of a string.
   *
   * @param s string to be printed
   * @param off offset from which to start writing characters
   * @param len number of characters to write
   */
  public void write(String s, int off, int len) {
    writtenBytes += countBytes(s.substring(off, len)); // "len" should be "off+len"
    writtenChars += len;
    super.write(s, off, len);
  }

LUB of LTL(a) and LTEL(a,b) is LTEL(a)

An example of code that causes this:

Object[] o = { {null}, null };

The null inside the inner array is @minlen(0) instead of @MinLenBottom. That is wrong.

using the equal to operator should expand knowledge about a type

ie

    public static void equalToUpper(@LTLengthOf("a") int m, @LTEqLengthOf("a") int r) {
        if ( r == m ) {
		@LTLengthOf("a") int j = r;
	}
    }

    public static void equalToMinLen(@MinLen(2) String m, @MinLen(0) String r) {
        if ( r == m ) {
		@MinLen(2) String j = r;
	}
    }

Test Cases:
checker-framework/checker/tests/upperbound/equalTo.java
checker-framework/checker/tests/minlen/equalTo.java

Consider this code:

public class ArrayLength2 {
    public static void main(String[] args) {
        int N = 8;
        int @MinLen(8) [] Grid = new int[N];
        @LessThanLength("Grid") int i = 0;
    }
}

This should type-check, but the final assignment fails.

This test case is checked into the repository as file checker/tests/upperbound/ArrayLength2.java.

Consider the following code:

    	int[] firstHalf = new int[array.length/2];
    	for(int i = 0; i < firstHalf.length; i++){
    		firstHalf[i] = array[i];
    	}

The UBC warns about the access to array. This is clearly a false positive, since i is @LTLengthOf("firstHalf"), and we can reason that firstHalf's MinLen has to be smaller than array's. But the UBC warns anyway. This showed up in a pilot of the IC study.

Currently, the LBC just runs the UBC as a subchecker, so the LBC is the Index Checker. We need to build a proper index checker which just extends the LBC and does nothing else.

In it, we should document what we'd actually like: an aggregate checker that has the ability (currently unique to compound checkers) to run each of its subcheckers only once in a reasonable order that respects dependencies.

void test() {
	Random rand = new Random();
	int[] a = new int[8];
	@NonNegative @LessThanLength("a") int deref = (int)(Math.random()*a.length);
	@NonNegative @LessThanLength("a") int deref2 = (int)(rand.nextDouble()*a.length);
	@NonNegative @LessThanLength("a") int deref3 = rand.nextInt(a.length);
}

These test cases result in the lowerbound and upperbound checker reporting the type of deref, deref2, and deref3 as LowerBoundUnknown and UpperBoundUnknown.

Given this code:

  public static int[] fn_compose(/*@IndexFor("#2")*/ int[] a, int[] b) {
    int[] result = new int[a.length];
    for (int i = 0; i < a.length; i++) {
      int inner = a[i];
      if (inner == -1) {
        result[i] = -1;
      } else {
        result[i] = b[inner];
      }
    }
    return result;
  }

the checker issues this warning:

warning: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound
        result[i] = b[inner];
                      ^
  found   : @LTLengthOf("#2") int
  required: @LTLengthOf("b") int

Here, "#2" and "b" should be treated the same.

Consider:

public void test(int[] b){
	int [] a = new int[b.length + 1];
	a[b.length] = 5;
    }

You and I know that b.length is less than a.length, but the checker doesn't learn that fact right now.

The Math.max of two values should be the GLB? of the two types

void mathmax() {
   @Positive int i = Math.max(-15, 2); // this gives an error but should not
}

With Math.min is should be the LUB? of the two

void mathmin() {
   @GTENegativeOne int i = Math.min(-1, 2); // this gives an error but should not
}

Needs to be investigated. This is why the travis builds are failing.

A literal string should be assigned a @MinLen annotation equal to its length.

See the test case in
checker-framework/checker/tests/minlen/LiteralString.java

Instead, it should be GLB. See LTLDivide.java for an example of this.

predecrement in an array access does not give a warning but should

  void pre1(int [] args) {
    int ii = 0;
    while ((ii < args.length)) {
      //:: warning: (array.access.unsafe.high)
      int m = args[++ii];
    }
  }

Test Case: checker-framework/checker/tests/upperbound/PreAndPostDec.java

What the title says. This came up in the pilot study. I've checked in a test case in 5623400

The Index Checker manual chapter should document the Min Length Checker.
It should also document why MinLen even exists, which is a commonly-asked question. Do this by showing that there are two different situations when a[i] is legal: when i is known to be an index for a independent of the length of a, and when i is actually a compile-time constant but facts are known about the length of a, in particular a compile-time bound on its minimum length.

The manual still mentions @EqualToLength, which has been removed.

Including from the LBC, UBC, and MinLen.

File checker-framework/checker/manual/upperbound.svg still uses the old name @LessThanLength.

It should be set intersection when the two types are the same ignoring values. It's currently set union.

Consider this code (thanks Mike):

if (cond) then x = a.length else x = b.length fi

after the fi, the UBC currently gives x type LTEL(a,b). It should be unknown.

if you have a minlen(4) arr; arr.length -2 could still be positive etc.

public class NonNegArrayLength {

    public static void NonNegArrayLength (int @MinLen(4)[] arr) {
        @Positive int i = arr.length - 2;
    }

}

Consider the following code, which compares two arrays first by length and then lexigraphically:

    public int compare(int[] a1, int[] a2) {
      if (a1.length != a2.length) {
        return a1.length - a2.length;
      }
      for (int i = 0; i < a1.length; i++) {
        if (a1[i] != a2[i]) {
          return ((a1[i] > a2[i]) ? 1 : -1);
        }
      }
      return 0;
    }

Here is a test case:

  public static String replaceString(String target, String oldStr, String newStr) {
    if (oldStr.equals("")) {
      throw new IllegalArgumentException();
    }

    StringBuffer result = new StringBuffer();
    int lastend = 0;
    int pos;
    while ((pos = target.indexOf(oldStr, lastend)) != -1) {
      result.append(target.substring(lastend, pos));
      result.append(newStr);
      lastend = pos + oldStr.length();
    }
    result.append(target.substring(lastend));
    return result.toString();
  }

The checker can't tell that pos is @NonNegative. The checker issues this warning:

warning: [argument.type.incompatible] incompatible types in argument.
      result.append(target.substring(lastend, pos));
                                              ^
  found   : @GTENegativeOne int
  required: @NonNegative int

VarArgsIncompatible.java in the minlen test suite is currently failing. @MinLenBottom is being applied in the wrong place. Fix.