kelloggm / checker-framework Goto Github PK
View Code? Open in Web Editor NEWThis project forked from typetools/checker-framework
Pluggable type-checking for Java
Home Page: http://checkerframework.org/
License: Other
This project forked from typetools/checker-framework
Pluggable type-checking for Java
Home Page: http://checkerframework.org/
License: Other
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.
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
:
@NonNegative
@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:
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.