diff --git a/gson/pom.xml b/gson/pom.xml index cf32962ad0..e2436ac1db 100644 --- a/gson/pom.xml +++ b/gson/pom.xml @@ -11,15 +11,44 @@ Gson + + org.checkerframework + checker + 3.4.0 + junit junit test - + + + maven-compiler-plugin + 3.8.1 + + 11 + + 10000 + 10000 + + + + org.checkerframework + checker + 3.4.0 + + + + org.checkerframework.checker.index.IndexChecker + + + -AprintErrorStack + + + org.apache.maven.plugins maven-javadoc-plugin diff --git a/gson/src/main/java/com/google/gson/FieldNamingPolicy.java b/gson/src/main/java/com/google/gson/FieldNamingPolicy.java index ddb9a93d62..4e13a461a7 100644 --- a/gson/src/main/java/com/google/gson/FieldNamingPolicy.java +++ b/gson/src/main/java/com/google/gson/FieldNamingPolicy.java @@ -18,6 +18,7 @@ import java.lang.reflect.Field; import java.util.Locale; +import org.checkerframework.checker.index.qual.LTLengthOf; /** * An enumeration that defines a few standard naming conventions for JSON field names. @@ -158,8 +159,12 @@ static String separateCamelCase(String name, String separator) { /** * Ensures the JSON field names begins with an upper case letter. */ + /*firstLetterIndex is assigned with 0 #1, length of a field name would be atleast 1, + substring(1) may be out or range if length of field is 1 + though no exception is thrown by function substring*/ + @SuppressWarnings({"index:assignment.type.incompatible","index:argument.type.incompatible"}) static String upperCaseFirstLetter(String name) { - int firstLetterIndex = 0; + @LTLengthOf(value="name") int firstLetterIndex = 0; //#1 int limit = name.length() - 1; for(; !Character.isLetter(name.charAt(firstLetterIndex)) && firstLetterIndex < limit; ++firstLetterIndex); @@ -170,7 +175,7 @@ static String upperCaseFirstLetter(String name) { char uppercased = Character.toUpperCase(firstLetter); if(firstLetterIndex == 0) { //First character in the string is the first letter, saves 1 substring - return uppercased + name.substring(1); + return uppercased + name.substring(1); //#2 } return name.substring(0, firstLetterIndex) + uppercased + name.substring(firstLetterIndex + 1); diff --git a/gson/src/main/java/com/google/gson/JsonArray.java b/gson/src/main/java/com/google/gson/JsonArray.java index 4b61a90969..23c3b65cad 100644 --- a/gson/src/main/java/com/google/gson/JsonArray.java +++ b/gson/src/main/java/com/google/gson/JsonArray.java @@ -21,6 +21,7 @@ import java.util.ArrayList; import java.util.Iterator; import java.util.List; +import org.checkerframework.checker.index.qual.NonNegative; /** * A class representing an array type in Json. An array is a list of {@link JsonElement}s each of @@ -40,7 +41,7 @@ public JsonArray() { elements = new ArrayList(); } - public JsonArray(int capacity) { + public JsonArray(@NonNegative int capacity) { elements = new ArrayList(capacity); } @@ -391,3 +392,4 @@ public int hashCode() { return elements.hashCode(); } } + diff --git a/gson/src/main/java/com/google/gson/JsonPrimitive.java b/gson/src/main/java/com/google/gson/JsonPrimitive.java index 5e95d5a82b..a87484f538 100644 --- a/gson/src/main/java/com/google/gson/JsonPrimitive.java +++ b/gson/src/main/java/com/google/gson/JsonPrimitive.java @@ -233,9 +233,11 @@ public byte getAsByte() { return isNumber() ? getAsNumber().byteValue() : Byte.parseByte(getAsString()); } + //getAsString returns a String of minimum length 1, charAt(0) is safe + @SuppressWarnings("index:argument.type.incompatible") @Override public char getAsCharacter() { - return getAsString().charAt(0); + return getAsString().charAt(0); //#1 } @Override diff --git a/gson/src/main/java/com/google/gson/internal/$Gson$Types.java b/gson/src/main/java/com/google/gson/internal/$Gson$Types.java index adea605f59..2d9fbd4af2 100644 --- a/gson/src/main/java/com/google/gson/internal/$Gson$Types.java +++ b/gson/src/main/java/com/google/gson/internal/$Gson$Types.java @@ -30,6 +30,10 @@ import static com.google.gson.internal.$Gson$Preconditions.checkArgument; import static com.google.gson.internal.$Gson$Preconditions.checkNotNull; +import org.checkerframework.common.value.qual.ArrayLen; +import org.checkerframework.common.value.qual.MinLen; +import org.checkerframework.checker.index.qual.NonNegative; + /** * Static methods for working with types. * @@ -70,10 +74,12 @@ public static GenericArrayType arrayOf(Type componentType) { * {@code ? extends CharSequence}. If {@code bound} is {@code Object.class}, * this returns {@code ?}, which is shorthand for {@code ? extends Object}. */ + /*Missing annotation in JDK in @MinLen(1) getUpperBounds() of WildcardType #2*/ + @SuppressWarnings("assignment.type.incompatible") public static WildcardType subtypeOf(Type bound) { - Type[] upperBounds; + Type @MinLen(1)[] upperBounds; if (bound instanceof WildcardType) { - upperBounds = ((WildcardType) bound).getUpperBounds(); + upperBounds = ((WildcardType) bound).getUpperBounds(); //#2 } else { upperBounds = new Type[] { bound }; } @@ -100,6 +106,8 @@ public static WildcardType supertypeOf(Type bound) { * according to {@link Object#equals(Object) Object.equals()}. The returned * type is {@link java.io.Serializable}. */ + /*Missing annotation in JDK in @MinLen(1) getUpperBounds() of WildcardType #3*/ + @SuppressWarnings("argument.type.incompatible") public static Type canonicalize(Type type) { if (type instanceof Class) { Class c = (Class) type; @@ -116,14 +124,15 @@ public static Type canonicalize(Type type) { } else if (type instanceof WildcardType) { WildcardType w = (WildcardType) type; - return new WildcardTypeImpl(w.getUpperBounds(), w.getLowerBounds()); + return new WildcardTypeImpl(w.getUpperBounds(), w.getLowerBounds()); //#3 } else { // type is either serializable as-is or unsupported return type; } } - + /*Missing annotation in JDK in @MinLen(1) getUpperBounds() of WildcardType #4*/ + @SuppressWarnings("array.access.unsafe.high.constant") public static Class getRawType(Type type) { if (type instanceof Class) { // type is a normal class. @@ -149,7 +158,7 @@ public static Class getRawType(Type type) { return Object.class; } else if (type instanceof WildcardType) { - return getRawType(((WildcardType) type).getUpperBounds()[0]); + return getRawType(((WildcardType) type).getUpperBounds()[0]); //#4 } else { String className = type == null ? "null" : type.getClass().getName(); @@ -233,6 +242,9 @@ public static String typeToString(Type type) { * IntegerSet}, the result for when supertype is {@code Set.class} is {@code Set} and the * result when the supertype is {@code Collection.class} is {@code Collection}. */ + /*getGenericInterfaces and getInterfaces #7 return the same length array therefore #8 #9 + i which is an index of `interfaces` can be used for the returned array of getGenericInterfaces*/ + @SuppressWarnings("array.access.unsafe.high") static Type getGenericSupertype(Type context, Class rawType, Class toResolve) { if (toResolve == rawType) { return context; @@ -240,12 +252,12 @@ static Type getGenericSupertype(Type context, Class rawType, Class toResol // we skip searching through interfaces if unknown is an interface if (toResolve.isInterface()) { - Class[] interfaces = rawType.getInterfaces(); + Class[] interfaces = rawType.getInterfaces(); //#7 for (int i = 0, length = interfaces.length; i < length; i++) { if (interfaces[i] == toResolve) { - return rawType.getGenericInterfaces()[i]; + return rawType.getGenericInterfaces()[i]; //#8 } else if (toResolve.isAssignableFrom(interfaces[i])) { - return getGenericSupertype(rawType.getGenericInterfaces()[i], interfaces[i], toResolve); + return getGenericSupertype(rawType.getGenericInterfaces()[i], interfaces[i], toResolve); //#9 } } } @@ -274,10 +286,12 @@ static Type getGenericSupertype(Type context, Class rawType, Class toResol * * @param supertype a superclass of, or interface implemented by, this. */ + /*Missing annotation in JDK in @MinLen(1) getUpperBounds() of WildcardType #5*/ + @SuppressWarnings("array.access.unsafe.high.constant") static Type getSupertype(Type context, Class contextRawType, Class supertype) { if (context instanceof WildcardType) { // wildcards are useless for resolving supertypes. As the upper bound has the same raw type, use it instead - context = ((WildcardType)context).getUpperBounds()[0]; + context = ((WildcardType)context).getUpperBounds()[0]; //#5 } checkArgument(supertype.isAssignableFrom(contextRawType)); return resolve(context, contextRawType, @@ -298,11 +312,13 @@ public static Type getArrayComponentType(Type array) { * Returns the element type of this collection type. * @throws IllegalArgumentException if this type is not a collection. */ + /*Missing annotation in JDK in @MinLen(1) getUpperBounds() of WildcardType #6*/ + @SuppressWarnings("array.access.unsafe.high.constant") public static Type getCollectionElementType(Type context, Class contextRawType) { Type collectionType = getSupertype(context, contextRawType, Collection.class); if (collectionType instanceof WildcardType) { - collectionType = ((WildcardType)collectionType).getUpperBounds()[0]; + collectionType = ((WildcardType)collectionType).getUpperBounds()[0]; //#6 } if (collectionType instanceof ParameterizedType) { return ((ParameterizedType) collectionType).getActualTypeArguments()[0]; @@ -314,7 +330,9 @@ public static Type getCollectionElementType(Type context, Class contextRawTyp * Returns a two element array containing this map's key and value types in * positions 0 and 1 respectively. */ - public static Type[] getMapKeyAndValueTypes(Type context, Class contextRawType) { + //Map takes two parameters therefore returned array is of length 2 in #1 + @SuppressWarnings("return.type.incompatible") + public static Type @ArrayLen(2)[] getMapKeyAndValueTypes(Type context, Class contextRawType) { /* * Work around a problem with the declaration of java.util.Properties. That * class should extend Hashtable, but it's declared to @@ -328,7 +346,7 @@ public static Type[] getMapKeyAndValueTypes(Type context, Class contextRawTyp // TODO: strip wildcards? if (mapType instanceof ParameterizedType) { ParameterizedType mapParameterizedType = (ParameterizedType) mapType; - return mapParameterizedType.getActualTypeArguments(); + return mapParameterizedType.getActualTypeArguments(); //#1 } return new Type[] { Object.class, Object.class }; } @@ -416,6 +434,10 @@ private static Type resolve(Type context, Class contextRawType, Type toResolv } } + /*as getTypeParameters and getTypeArguments return an array of same length + * `index` being an index of getTypeParameters's array is also a valid valid index + * for getActualTypeArguments's array #10*/ + @SuppressWarnings({"array.access.unsafe.high"}) static Type resolveTypeVariable(Type context, Class contextRawType, TypeVariable unknown) { Class declaredByRaw = declaringClassOf(unknown); @@ -426,14 +448,14 @@ static Type resolveTypeVariable(Type context, Class contextRawType, TypeVaria Type declaredBy = getGenericSupertype(context, contextRawType, declaredByRaw); if (declaredBy instanceof ParameterizedType) { - int index = indexOf(declaredByRaw.getTypeParameters(), unknown); - return ((ParameterizedType) declaredBy).getActualTypeArguments()[index]; + @NonNegative int index = indexOf(declaredByRaw.getTypeParameters(), unknown); + return ((ParameterizedType) declaredBy).getActualTypeArguments()[index]; //#10 } return unknown; } - private static int indexOf(Object[] array, Object toFind) { + private static @NonNegative int indexOf(Object[] array, Object toFind) { for (int i = 0, length = array.length; i < length; i++) { if (toFind.equals(array[i])) { return i; @@ -504,14 +526,16 @@ public Type getOwnerType() { ^ hashCodeOrZero(ownerType); } + //#11 already ensures typeArguments.length is not 0 when it reaches #12 + @SuppressWarnings("array.access.unsafe.high.constant") @Override public String toString() { int length = typeArguments.length; - if (length == 0) { + if (length == 0) { //#11 return typeToString(rawType); } StringBuilder stringBuilder = new StringBuilder(30 * (length + 1)); - stringBuilder.append(typeToString(rawType)).append("<").append(typeToString(typeArguments[0])); + stringBuilder.append(typeToString(rawType)).append("<").append(typeToString(typeArguments[0])); //#12 for (int i = 1; i < length; i++) { stringBuilder.append(", ").append(typeToString(typeArguments[i])); } @@ -557,7 +581,7 @@ private static final class WildcardTypeImpl implements WildcardType, Serializabl private final Type upperBound; private final Type lowerBound; - public WildcardTypeImpl(Type[] upperBounds, Type[] lowerBounds) { + public WildcardTypeImpl(Type @MinLen(1)[] upperBounds, Type[] lowerBounds) { checkArgument(lowerBounds.length <= 1); checkArgument(upperBounds.length == 1); @@ -576,7 +600,7 @@ public WildcardTypeImpl(Type[] upperBounds, Type[] lowerBounds) { } } - public Type[] getUpperBounds() { + public Type @MinLen(1)[] getUpperBounds() { return new Type[] { upperBound }; } diff --git a/gson/src/main/java/com/google/gson/internal/ConstructorConstructor.java b/gson/src/main/java/com/google/gson/internal/ConstructorConstructor.java index 5fab460105..e4caa449c4 100644 --- a/gson/src/main/java/com/google/gson/internal/ConstructorConstructor.java +++ b/gson/src/main/java/com/google/gson/internal/ConstructorConstructor.java @@ -130,7 +130,8 @@ private ObjectConstructor newDefaultConstructor(Class rawType) * Constructors for common interface types like Map and List and their * subtypes. */ - @SuppressWarnings("unchecked") // use runtime checks to guarantee that 'T' is what it is + //getActualTypeArguments may return an empty array #1 #2 + @SuppressWarnings({"unchecked","array.access.unsafe.high.constant"}) // use runtime checks to guarantee that 'T' is what it is private ObjectConstructor newDefaultImplementationConstructor( final Type type, Class rawType) { if (Collection.class.isAssignableFrom(rawType)) { @@ -145,7 +146,7 @@ private ObjectConstructor newDefaultImplementationConstructor( @SuppressWarnings("rawtypes") @Override public T construct() { if (type instanceof ParameterizedType) { - Type elementType = ((ParameterizedType) type).getActualTypeArguments()[0]; + Type elementType = ((ParameterizedType) type).getActualTypeArguments()[0]; //#1 if (elementType instanceof Class) { return (T) EnumSet.noneOf((Class)elementType); } else { @@ -197,7 +198,7 @@ private ObjectConstructor newDefaultImplementationConstructor( } }; } else if (type instanceof ParameterizedType && !(String.class.isAssignableFrom( - TypeToken.get(((ParameterizedType) type).getActualTypeArguments()[0]).getRawType()))) { + TypeToken.get(((ParameterizedType) type).getActualTypeArguments()[0]).getRawType()))) { //#2 return new ObjectConstructor() { @Override public T construct() { return (T) new LinkedHashMap(); diff --git a/gson/src/main/java/com/google/gson/internal/LinkedHashTreeMap.java b/gson/src/main/java/com/google/gson/internal/LinkedHashTreeMap.java index b2707c50da..14ce8c15fd 100644 --- a/gson/src/main/java/com/google/gson/internal/LinkedHashTreeMap.java +++ b/gson/src/main/java/com/google/gson/internal/LinkedHashTreeMap.java @@ -28,7 +28,8 @@ import java.util.LinkedHashMap; import java.util.NoSuchElementException; import java.util.Set; - +import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.checker.index.qual.IndexFor; /** * A map of comparable keys to values. Unlike {@code TreeMap}, this class uses * insertion order for iteration order. Comparison order is only used as an @@ -48,7 +49,7 @@ public int compare(Comparable a, Comparable b) { Comparator comparator; Node[] table; final Node header; - int size = 0; + @NonNegative int size = 0; int modCount = 0; int threshold; @@ -78,7 +79,7 @@ public LinkedHashTreeMap(Comparator comparator) { this.threshold = (table.length / 2) + (table.length / 4); // 3/4 capacity } - @Override public int size() { + @Override public @NonNegative int size() { return size; } @@ -128,11 +129,14 @@ public LinkedHashTreeMap(Comparator comparator) { * @throws ClassCastException if {@code key} and the tree's keys aren't * mutually comparable. */ + /*hash & table.length-1 ensures index to be less than table.length-1 + therefore it is safe as an index #4*/ + @SuppressWarnings("assignment.type.incompatible") Node find(K key, boolean create) { Comparator comparator = this.comparator; Node[] table = this.table; int hash = secondaryHash(key.hashCode()); - int index = hash & (table.length - 1); + @IndexFor("table") int index = hash & (table.length - 1); //#4 Node nearest = table[index]; int comparison = 0; @@ -230,7 +234,10 @@ private boolean equal(Object a, Object b) { * uses power-of-two length hash tables, that otherwise encounter collisions * for hashCodes that do not differ in lower or upper bits. */ - private static int secondaryHash(int h) { + /*using unsigned right shift fills zeroes at the left end therefore making it + NonNegative*/ + @SuppressWarnings("return.type.incompatible") + private static @NonNegative int secondaryHash(int h) { // Doug Lea's supplemental hash function h ^= (h >>> 20) ^ (h >>> 12); return h ^ (h >>> 7) ^ (h >>> 4); @@ -242,6 +249,8 @@ private static int secondaryHash(int h) { * * @param unlink true to also unlink this node from the iteration linked list. */ + //Size during remove is > 0 #3 + @SuppressWarnings("unary.decrement.type.incompatible") void removeInternal(Node node, boolean unlink) { if (unlink) { node.prev.next = node.next; @@ -296,7 +305,7 @@ void removeInternal(Node node, boolean unlink) { } rebalance(originalParent, false); - size--; + size--; //#3 modCount++; } @@ -307,7 +316,9 @@ Node removeInternalByKey(Object key) { } return node; } - + /*hash & table.length-1 #1 ensures index to be less than table.length-1 + therefore it is safe as an index*/ + @SuppressWarnings("assignment.type.incompatible") private void replaceInParent(Node node, Node replacement) { Node parent = node.parent; node.parent = null; @@ -323,7 +334,7 @@ private void replaceInParent(Node node, Node replacement) { parent.right = replacement; } } else { - int index = node.hash & (table.length - 1); + @IndexFor("table") int index = node.hash & (table.length - 1); //#1 table[index] = replacement; } } @@ -563,6 +574,9 @@ private void doubleCapacity() { * Returns a new array containing the same nodes as {@code oldTable}, but with * twice as many trees, each of (approximately) half the previous size. */ + /*i is an index of oldTable and length of newTable is twice the length of + oldTable therefore index of oldTable is safe as an index for newTable #2*/ + @SuppressWarnings("array.access.unsafe.high") static Node[] doubleCapacity(Node[] oldTable) { // TODO: don't do anything if we're already at MAX_CAPACITY int oldCapacity = oldTable.length; @@ -604,7 +618,7 @@ static Node[] doubleCapacity(Node[] oldTable) { } // Populate the enlarged array with these new roots. - newTable[i] = leftSize > 0 ? leftBuilder.root() : null; + newTable[i] = leftSize > 0 ? leftBuilder.root() : null; //#2 newTable[i + oldCapacity] = rightSize > 0 ? rightBuilder.root() : null; } return newTable; @@ -792,7 +806,7 @@ public final void remove() { } final class EntrySet extends AbstractSet> { - @Override public int size() { + @Override public @NonNegative int size() { return size; } @@ -827,7 +841,7 @@ public Entry next() { } final class KeySet extends AbstractSet { - @Override public int size() { + @Override public @NonNegative int size() { return size; } diff --git a/gson/src/main/java/com/google/gson/internal/LinkedTreeMap.java b/gson/src/main/java/com/google/gson/internal/LinkedTreeMap.java index 80462742e3..6b8cfa5c33 100644 --- a/gson/src/main/java/com/google/gson/internal/LinkedTreeMap.java +++ b/gson/src/main/java/com/google/gson/internal/LinkedTreeMap.java @@ -27,6 +27,7 @@ import java.util.LinkedHashMap; import java.util.NoSuchElementException; import java.util.Set; +import org.checkerframework.checker.index.qual.NonNegative; /** * A map of comparable keys to values. Unlike {@code TreeMap}, this class uses @@ -45,7 +46,7 @@ public int compare(Comparable a, Comparable b) { Comparator comparator; Node root; - int size = 0; + @NonNegative int size = 0; int modCount = 0; // Used to preserve iteration order @@ -74,7 +75,7 @@ public LinkedTreeMap(Comparator comparator) { : (Comparator) NATURAL_ORDER; } - @Override public int size() { + @Override public @NonNegative int size() { return size; } @@ -214,6 +215,8 @@ private boolean equal(Object a, Object b) { * * @param unlink true to also unlink this node from the iteration linked list. */ + //Size while removing is > 0 #1 + @SuppressWarnings("unary.decrement.type.incompatible") void removeInternal(Node node, boolean unlink) { if (unlink) { node.prev.next = node.next; @@ -269,7 +272,7 @@ void removeInternal(Node node, boolean unlink) { } rebalance(originalParent, false); - size--; + size--; //#1 modCount++; } @@ -558,7 +561,7 @@ public final void remove() { } class EntrySet extends AbstractSet> { - @Override public int size() { + @Override public @NonNegative int size() { return size; } @@ -593,7 +596,7 @@ public Entry next() { } final class KeySet extends AbstractSet { - @Override public int size() { + @Override public @NonNegative int size() { return size; } diff --git a/gson/src/main/java/com/google/gson/internal/Streams.java b/gson/src/main/java/com/google/gson/internal/Streams.java index ac99910a97..2bfe765922 100644 --- a/gson/src/main/java/com/google/gson/internal/Streams.java +++ b/gson/src/main/java/com/google/gson/internal/Streams.java @@ -28,6 +28,10 @@ import java.io.EOFException; import java.io.IOException; import java.io.Writer; +import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.checker.index.qual.IndexFor; +import org.checkerframework.checker.index.qual.LTLengthOf; +import org.checkerframework.checker.index.qual.LTEqLengthOf; /** * Reads and writes GSON parse trees over streams. @@ -88,7 +92,9 @@ private static final class AppendableWriter extends Writer { this.appendable = appendable; } - @Override public void write(char[] chars, int offset, int length) throws IOException { + //here currentWrite is used with chars + @SuppressWarnings("argument.type.incompatible") + @Override public void write(char[] chars, @NonNegative @LTEqLengthOf(value="#1") int offset, @NonNegative @LTLengthOf(value="#1",offset="#2 - 1")int length) throws IOException { currentWrite.chars = chars; appendable.append(currentWrite, offset, offset + length); } @@ -103,16 +109,26 @@ private static final class AppendableWriter extends Writer { /** * A mutable char sequence pointing at a single char[]. */ + /*Code is dangerous as functions can be called without initializing chars*/ + @SuppressWarnings("initialization.fields.uninitialized") static class CurrentWrite implements CharSequence { char[] chars; - public int length() { + /*chars stores the char sequence not `this`*/ + @SuppressWarnings("override.return.invalid") + public @NonNegative @LTEqLengthOf("chars") int length() { return chars.length; } - public char charAt(int i) { + /*chars stores the char sequence not `this`*/ + @SuppressWarnings("override.param.invalid") + public char charAt(@IndexFor("chars") int i) { return chars[i]; } - public CharSequence subSequence(int start, int end) { - return new String(chars, start, end - start); + + /*chars stores the char seq not `this`*/ + /*end - start may be negative.#2*/ + @SuppressWarnings({"override.param.invalid","argument.type.incompatible"}) + public CharSequence subSequence(@NonNegative @LTLengthOf(value="chars") int start, @NonNegative @LTLengthOf(value="this.chars") int end) { + return new String(chars, start, end - start); //#2 } } } diff --git a/gson/src/main/java/com/google/gson/internal/bind/ArrayTypeAdapter.java b/gson/src/main/java/com/google/gson/internal/bind/ArrayTypeAdapter.java index 56101706b3..4f2916d3b1 100644 --- a/gson/src/main/java/com/google/gson/internal/bind/ArrayTypeAdapter.java +++ b/gson/src/main/java/com/google/gson/internal/bind/ArrayTypeAdapter.java @@ -60,6 +60,9 @@ public ArrayTypeAdapter(Gson context, TypeAdapter componentTypeAdapter, Class this.componentType = componentType; } + /*array has the same size as list due to statements #1 and #2, + therefore i is an index for both list and array hence #3 is safe*/ + @SuppressWarnings("argument.type.incompatible") @Override public Object read(JsonReader in) throws IOException { if (in.peek() == JsonToken.NULL) { in.nextNull(); @@ -74,10 +77,10 @@ public ArrayTypeAdapter(Gson context, TypeAdapter componentTypeAdapter, Class } in.endArray(); - int size = list.size(); - Object array = Array.newInstance(componentType, size); + int size = list.size(); //#1 + Object array = Array.newInstance(componentType, size); //#2 for (int i = 0; i < size; i++) { - Array.set(array, i, list.get(i)); + Array.set(array, i, list.get(i)); //#3 } return array; } diff --git a/gson/src/main/java/com/google/gson/internal/bind/JsonTreeReader.java b/gson/src/main/java/com/google/gson/internal/bind/JsonTreeReader.java index a223754aed..2227876dbe 100644 --- a/gson/src/main/java/com/google/gson/internal/bind/JsonTreeReader.java +++ b/gson/src/main/java/com/google/gson/internal/bind/JsonTreeReader.java @@ -28,6 +28,10 @@ import java.util.Iterator; import java.util.Map; import java.util.Arrays; +import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.checker.index.qual.GTENegativeOne; +import org.checkerframework.checker.index.qual.LTEqLengthOf; +import org.checkerframework.checker.index.qual.LTLengthOf; /** * This reader walks the elements of a JsonElement as if it was coming from a @@ -37,7 +41,7 @@ */ public final class JsonTreeReader extends JsonReader { private static final Reader UNREADABLE_READER = new Reader() { - @Override public int read(char[] buffer, int offset, int count) throws IOException { + @Override public @GTENegativeOne @LTEqLengthOf("#1") int read(char[] buffer, @NonNegative @LTEqLengthOf("#1") int offset, @NonNegative @LTLengthOf(value="#1", offset="#2-1") int count) throws IOException { throw new AssertionError(); } @Override public void close() throws IOException { @@ -50,7 +54,7 @@ public final class JsonTreeReader extends JsonReader { * The nesting stack. Using a manual array rather than an ArrayList saves 20%. */ private Object[] stack = new Object[32]; - private int stackSize = 0; + private @NonNegative @LTEqLengthOf(value={"stack","pathIndices","pathNames"}) int stackSize = 0; /* * The path members. It corresponds directly to stack: At indices where the @@ -68,11 +72,13 @@ public JsonTreeReader(JsonElement element) { push(element); } + //push #1 ensures statckSize > 0, therefore stackSize-1 is a safe index #2 + @SuppressWarnings("array.access.unsafe.low") @Override public void beginArray() throws IOException { expect(JsonToken.BEGIN_ARRAY); JsonArray array = (JsonArray) peekStack(); - push(array.iterator()); - pathIndices[stackSize - 1] = 0; + push(array.iterator()); //#1 + pathIndices[stackSize - 1] = 0; //#2 } @Override public void endArray() throws IOException { @@ -104,13 +110,18 @@ public JsonTreeReader(JsonElement element) { return token != JsonToken.END_OBJECT && token != JsonToken.END_ARRAY; } + /*if #3 is true, the stack has atleast two elements + one inserted by the constructor and another by beginArray() + which pushes array.iterator() similar to what is been checked in #3, + therefore stackSize-2 is safe*/ + @SuppressWarnings("array.access.unsafe.low") @Override public JsonToken peek() throws IOException { if (stackSize == 0) { return JsonToken.END_DOCUMENT; } Object o = peekStack(); - if (o instanceof Iterator) { + if (o instanceof Iterator) {//#3 boolean isObject = stack[stackSize - 2] instanceof JsonObject; Iterator iterator = (Iterator) o; if (iterator.hasNext()) { @@ -147,12 +158,17 @@ public JsonTreeReader(JsonElement element) { } } + /*peekStack() is a private function and is called when stackSize>0 #4*/ + @SuppressWarnings("array.access.unsafe.low") private Object peekStack() { - return stack[stackSize - 1]; + return stack[stackSize - 1]; //#4 } + /*popStack() is a private function and is called when stackSize>0 #5, + therefore --stackSize is a valid index*/ + @SuppressWarnings({"array.access.unsafe.low","unary.decrement.type.incompatible"}) private Object popStack() { - Object result = stack[--stackSize]; + Object result = stack[--stackSize]; //#5 stack[stackSize] = null; return result; } @@ -164,12 +180,15 @@ private void expect(JsonToken expected) throws IOException { } } + /*#6 expect() checks if peek() is equal to expect's arg, if this turns + false it throws an exception, therefore stackSize>0 and index stackSize-1 is safe #7*/ + @SuppressWarnings("array.access.unsafe.low") @Override public String nextName() throws IOException { - expect(JsonToken.NAME); + expect(JsonToken.NAME); //#6 Iterator i = (Iterator) peekStack(); Map.Entry entry = (Map.Entry) i.next(); String result = (String) entry.getKey(); - pathNames[stackSize - 1] = result; + pathNames[stackSize - 1] = result; //#7 push(entry.getValue()); return result; } @@ -249,15 +268,20 @@ private void expect(JsonToken expected) throws IOException { return result; } + //#8 initializes a new stack with 1 element, therefore #9 is accurate and valid + @SuppressWarnings("assignment.type.incompatible") @Override public void close() throws IOException { - stack = new Object[] { SENTINEL_CLOSED }; - stackSize = 1; + stack = new Object[] { SENTINEL_CLOSED }; //#8 + stackSize = 1; //#9 } + /*if #10 is true there are atleast two elements, Json.BEGIN_ARRAY and array.iterator() + therefore stackSize>1 and stackSize-2 is safe #11*/ + @SuppressWarnings("array.access.unsafe.low") @Override public void skipValue() throws IOException { - if (peek() == JsonToken.NAME) { + if (peek() == JsonToken.NAME) { //#10 nextName(); - pathNames[stackSize - 2] = "null"; + pathNames[stackSize - 2] = "null"; //#11 } else { popStack(); if (stackSize > 0) { @@ -281,21 +305,28 @@ public void promoteNameToValue() throws IOException { push(new JsonPrimitive((String) entry.getKey())); } + /*If #12 ensures to double the array size if stack is full, + therefore stackSize++ is a safe index #13*/ + @SuppressWarnings({"array.access.unsafe.high","unary.increment.type.incompatible"}) private void push(Object newTop) { - if (stackSize == stack.length) { + if (stackSize == stack.length) { //#12 int newLength = stackSize * 2; stack = Arrays.copyOf(stack, newLength); pathIndices = Arrays.copyOf(pathIndices, newLength); pathNames = Arrays.copyOf(pathNames, newLength); } - stack[stackSize++] = newTop; + stack[stackSize++] = newTop; //#13 } + /*the loop #14 should have been from 0 to stackSize-1, + though according to the developers logic #15 would ensure #16 is never + out of range*/ + @SuppressWarnings("array.access.unsafe.high") @Override public String getPath() { StringBuilder result = new StringBuilder().append('$'); - for (int i = 0; i < stackSize; i++) { - if (stack[i] instanceof JsonArray) { - if (stack[++i] instanceof Iterator) { + for (int i = 0; i < stackSize; i++) { //#14 + if (stack[i] instanceof JsonArray) { //#15 + if (stack[++i] instanceof Iterator) { //#16 result.append('[').append(pathIndices[i]).append(']'); } } else if (stack[i] instanceof JsonObject) { diff --git a/gson/src/main/java/com/google/gson/internal/bind/util/ISO8601Utils.java b/gson/src/main/java/com/google/gson/internal/bind/util/ISO8601Utils.java index 99ec679a71..7bcfbfa34d 100644 --- a/gson/src/main/java/com/google/gson/internal/bind/util/ISO8601Utils.java +++ b/gson/src/main/java/com/google/gson/internal/bind/util/ISO8601Utils.java @@ -3,6 +3,7 @@ import java.text.ParseException; import java.text.ParsePosition; import java.util.*; +import org.checkerframework.checker.index.qual.NonNegative; /** * Utilities methods for manipulating dates in iso8601 format. This is much much faster and GC friendly than using SimpleDateFormat so @@ -123,7 +124,7 @@ public static String format(Date date, boolean millis, TimeZone tz) { public static Date parse(String date, ParsePosition pos) throws ParseException { Exception fail = null; try { - int offset = pos.getIndex(); + @NonNegative int offset = pos.getIndex(); // extract year int year = parseInt(date, offset, offset += 4); @@ -284,7 +285,7 @@ public static Date parse(String date, ParsePosition pos) throws ParseException { * @param expected the expected character * @return true if the expected character exist at the given offset */ - private static boolean checkOffset(String value, int offset, char expected) { + private static boolean checkOffset(String value, @NonNegative int offset, char expected) { return (offset < value.length()) && (value.charAt(offset) == expected); } @@ -341,7 +342,7 @@ private static void padInt(StringBuilder buffer, int value, int length) { /** * Returns the index of the first character in the string that is not a digit, starting at offset. */ - private static int indexOfNonDigit(String string, int offset) { + private static @NonNegative int indexOfNonDigit(String string, @NonNegative int offset) { for (int i = offset; i < string.length(); i++) { char c = string.charAt(i); if (c < '0' || c > '9') return i; diff --git a/gson/src/main/java/com/google/gson/reflect/TypeToken.java b/gson/src/main/java/com/google/gson/reflect/TypeToken.java index 3fb8af2bcf..5883c9d47a 100644 --- a/gson/src/main/java/com/google/gson/reflect/TypeToken.java +++ b/gson/src/main/java/com/google/gson/reflect/TypeToken.java @@ -25,6 +25,8 @@ import java.util.HashMap; import java.util.Map; +import org.checkerframework.checker.index.qual.LTEqLengthOf; + /** * Represents a generic type {@code T}. Java doesn't yet provide a way to * represent generic types, so this class does. Forces clients to create a @@ -78,13 +80,15 @@ protected TypeToken() { * Returns the type from super class's type parameter in {@link $Gson$Types#canonicalize * canonical form}. */ + //getActualTypeArguments() may return an empty array as per documentation + @SuppressWarnings("array.access.unsafe.high") static Type getSuperclassTypeParameter(Class subclass) { Type superclass = subclass.getGenericSuperclass(); if (superclass instanceof Class) { throw new RuntimeException("Missing type parameter."); } ParameterizedType parameterized = (ParameterizedType) superclass; - return $Gson$Types.canonicalize(parameterized.getActualTypeArguments()[0]); + return $Gson$Types.canonicalize(parameterized.getActualTypeArguments()[0]); //#1 } /** @@ -182,6 +186,9 @@ private static boolean isAssignableFrom(Type from, GenericArrayType to) { * Private recursive helper function to actually do the type-safe checking * of assignability. */ + /*Statements #1 #3 #4 #5 lead to the same length of tArgs and tParams + therefore i in #6 could be used as an index for both*/ + @SuppressWarnings({"index:array.access.unsafe.high"}) private static boolean isAssignableFrom(Type from, ParameterizedType to, Map typeVarMap) { @@ -194,17 +201,17 @@ private static boolean isAssignableFrom(Type from, ParameterizedType to, } // First figure out the class and any type information. - Class clazz = $Gson$Types.getRawType(from); + Class clazz = $Gson$Types.getRawType(from); //#1 ParameterizedType ptype = null; if (from instanceof ParameterizedType) { - ptype = (ParameterizedType) from; + ptype = (ParameterizedType) from; //#3 } // Load up parameterized variable info if it was parameterized. if (ptype != null) { - Type[] tArgs = ptype.getActualTypeArguments(); - TypeVariable[] tParams = clazz.getTypeParameters(); - for (int i = 0; i < tArgs.length; i++) { + Type[] tArgs = ptype.getActualTypeArguments(); //#4 + TypeVariable[] tParams = clazz.getTypeParameters(); //#5 + for (int i = 0; i < tArgs.length; i++) { //#6 Type arg = tArgs[i]; TypeVariable var = tParams[i]; while (arg instanceof TypeVariable) { @@ -235,12 +242,15 @@ private static boolean isAssignableFrom(Type from, ParameterizedType to, * Checks if two parameterized types are exactly equal, under the variable * replacement described in the typeVarMap. */ + /*toArgs and fromArgs have the same length in this case due to #2, + therefore i could be used as an index for both*/ + @SuppressWarnings({"index:array.access.unsafe.high"}) private static boolean typeEquals(ParameterizedType from, ParameterizedType to, Map typeVarMap) { - if (from.getRawType().equals(to.getRawType())) { + if (from.getRawType().equals(to.getRawType())) { //#2 Type[] fromArgs = from.getActualTypeArguments(); Type[] toArgs = to.getActualTypeArguments(); - for (int i = 0; i < fromArgs.length; i++) { + for (@LTEqLengthOf({"fromArgs"}) int i = 0; i < fromArgs.length; i++) { if (!matches(fromArgs[i], toArgs[i], typeVarMap)) { return false; } diff --git a/gson/src/main/java/com/google/gson/stream/JsonReader.java b/gson/src/main/java/com/google/gson/stream/JsonReader.java index e71fbabf71..061b980480 100644 --- a/gson/src/main/java/com/google/gson/stream/JsonReader.java +++ b/gson/src/main/java/com/google/gson/stream/JsonReader.java @@ -23,6 +23,11 @@ import java.io.IOException; import java.io.Reader; import java.util.Arrays; +import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.checker.index.qual.LTLengthOf; +import org.checkerframework.checker.index.qual.LTEqLengthOf; +import org.checkerframework.checker.index.qual.IndexFor; +import org.checkerframework.checker.index.qual.GTENegativeOne; /** * Reads a JSON (RFC 7159) @@ -188,6 +193,9 @@ * @author Jesse Wilson * @since 1.6 */ +/*#1 is inserting the first element into the stack, stackSize is 1 which is less than length of stackSize +and is equal to the number of elements in stack, therefore is valid and safe (Could not add SuppressWarnings to instance initializer block)*/ +@SuppressWarnings("unary.increment.type.incompatible") public class JsonReader implements Closeable { private static final long MIN_INCOMPLETE_INTEGER = Long.MIN_VALUE / 10; @@ -235,8 +243,8 @@ public class JsonReader implements Closeable { * long as the longest token that can be reported as a number. */ private final char[] buffer = new char[1024]; - private int pos = 0; - private int limit = 0; + private @NonNegative @LTLengthOf(value="buffer") int pos = 0; + private @NonNegative @LTLengthOf("buffer") int limit = 0; private int lineNumber = 0; private int lineStart = 0; @@ -253,7 +261,7 @@ public class JsonReader implements Closeable { * The number of characters in a peeked number literal. Increment 'pos' by * this after reading a number. */ - private int peekedNumberLength; + private @NonNegative @LTLengthOf(value="this.buffer", offset="this.pos-1") int peekedNumberLength; /** * A peeked string that should be parsed on the next double, long or string. @@ -266,9 +274,9 @@ public class JsonReader implements Closeable { * The nesting stack. Using a manual array rather than an ArrayList saves 20%. */ private int[] stack = new int[32]; - private int stackSize = 0; + private @NonNegative @LTEqLengthOf({"stack", "pathNames", "pathIndices"}) int stackSize = 0; { - stack[stackSize++] = JsonScope.EMPTY_DOCUMENT; + stack[stackSize++] = JsonScope.EMPTY_DOCUMENT; //#1 } /* @@ -336,14 +344,16 @@ public final boolean isLenient() { * Consumes the next token from the JSON stream and asserts that it is the * beginning of a new array. */ + /*push #2 ensures the stackSize>1 therefore stackSize - 1 #3 is a safe index*/ + @SuppressWarnings("array.access.unsafe.low") public void beginArray() throws IOException { int p = peeked; if (p == PEEKED_NONE) { p = doPeek(); } if (p == PEEKED_BEGIN_ARRAY) { - push(JsonScope.EMPTY_ARRAY); - pathIndices[stackSize - 1] = 0; + push(JsonScope.EMPTY_ARRAY); //#2 + pathIndices[stackSize - 1] = 0; //#3 peeked = PEEKED_NONE; } else { throw new IllegalStateException("Expected BEGIN_ARRAY but was " + peek() + locationString()); @@ -354,14 +364,18 @@ public void beginArray() throws IOException { * Consumes the next token from the JSON stream and asserts that it is the * end of the current array. */ + /*if #4 condition is true, there are more than two elements in the stack + pushed by the instance initializer block and by beginArray(), + therefore #5 and #6 are safe*/ + @SuppressWarnings({"array.access.unsafe.low","unary.decrement.type.incompatible"}) public void endArray() throws IOException { int p = peeked; if (p == PEEKED_NONE) { p = doPeek(); } - if (p == PEEKED_END_ARRAY) { - stackSize--; - pathIndices[stackSize - 1]++; + if (p == PEEKED_END_ARRAY) { //#4 + stackSize--; //#5 + pathIndices[stackSize - 1]++; //#6 peeked = PEEKED_NONE; } else { throw new IllegalStateException("Expected END_ARRAY but was " + peek() + locationString()); @@ -389,15 +403,19 @@ public void beginObject() throws IOException { * Consumes the next token from the JSON stream and asserts that it is the * end of the current object. */ + /*if #7 condition is true, there are more than two elements in the stack, + pushed by the instance initializer block and by beginObject(), + therefore #8 and #9 are safe*/ + @SuppressWarnings({"array.access.unsafe.low","unary.decrement.type.incompatible"}) public void endObject() throws IOException { int p = peeked; if (p == PEEKED_NONE) { p = doPeek(); } - if (p == PEEKED_END_OBJECT) { - stackSize--; + if (p == PEEKED_END_OBJECT) { //#7 + stackSize--; //#8 pathNames[stackSize] = null; // Free the last path name so that it can be garbage collected! - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#9 peeked = PEEKED_NONE; } else { throw new IllegalStateException("Expected END_OBJECT but was " + peek() + locationString()); @@ -457,8 +475,13 @@ public JsonToken peek() throws IOException { } } + /*the stack contains atleast one elemnent pushed by the instance initializer block + therefore #10 is safe*/ + /*pos > 0 as atleast one character is read, therefore #11 #14 #15 are safe*/ + /*pos is ensured to be less than limit #12 therefore pos++ #13 is safe*/ + @SuppressWarnings({"array.access.unsafe.low","unary.decrement.type.incompatible","unary.increment.type.incompatible"}) int doPeek() throws IOException { - int peekStack = stack[stackSize - 1]; + int peekStack = stack[stackSize - 1]; //#10 if (peekStack == JsonScope.EMPTY_ARRAY) { stack[stackSize - 1] = JsonScope.NONEMPTY_ARRAY; } else if (peekStack == JsonScope.NONEMPTY_ARRAY) { @@ -505,7 +528,7 @@ int doPeek() throws IOException { } default: checkLenient(); - pos--; // Don't consume the first character in an unquoted string. + pos--; // Don't consume the first character in an unquoted string //#11 if (isLiteral((char) c)) { return peeked = PEEKED_UNQUOTED_NAME; } else { @@ -521,8 +544,8 @@ int doPeek() throws IOException { break; case '=': checkLenient(); - if ((pos < limit || fillBuffer(1)) && buffer[pos] == '>') { - pos++; + if ((pos < limit || fillBuffer(1)) && buffer[pos] == '>') { //#12 + pos++; //#13 } break; default: @@ -539,7 +562,7 @@ int doPeek() throws IOException { return peeked = PEEKED_EOF; } else { checkLenient(); - pos--; + pos--; //#14 } } else if (peekStack == JsonScope.CLOSED) { throw new IllegalStateException("JsonReader is closed"); @@ -557,7 +580,7 @@ int doPeek() throws IOException { // In lenient mode, a 0-length literal in an array means 'null'. if (peekStack == JsonScope.EMPTY_ARRAY || peekStack == JsonScope.NONEMPTY_ARRAY) { checkLenient(); - pos--; + pos--; //#15 return peeked = PEEKED_NULL; } else { throw syntaxError("Unexpected value"); @@ -574,7 +597,6 @@ int doPeek() throws IOException { default: pos--; // Don't consume the first character in a literal value. } - int result = peekKeyword(); if (result != PEEKED_NONE) { return result; @@ -593,6 +615,12 @@ int doPeek() throws IOException { return peeked = PEEKED_UNQUOTED; } + /*if statement check if pos + i is less than limit #17 therefore #18 is safe*/ + /*loop #16 is valid traversal for both keyword and keywordUpper as they have same length, + therefore incrementing i in the loop leads to no unsafe access #19*/ + /*According to documentation buffer is of highest length required for any token, + therefore pos+length #20 is less that buffer.length.*/ + @SuppressWarnings({"array.access.unsafe.high","unary.increment.type.incompatible","compound.assignment.type.incompatible"}) private int peekKeyword() throws IOException { // Figure out which keyword we're matching against by its first character. char c = buffer[pos]; @@ -617,12 +645,12 @@ private int peekKeyword() throws IOException { // Confirm that chars [1..length) match the keyword. int length = keyword.length(); - for (int i = 1; i < length; i++) { - if (pos + i >= limit && !fillBuffer(i + 1)) { + for (@IndexFor({"keyword","keywordUpper"}) int i = 1; i < length; i++) {//#16 + if (pos + i >= limit && !fillBuffer(i + 1)) { //#17 return PEEKED_NONE; } - c = buffer[pos + i]; - if (c != keyword.charAt(i) && c != keywordUpper.charAt(i)) { + c = buffer[pos + i]; //#18 + if (c != keyword.charAt(i) && c != keywordUpper.charAt(i)) { //#19 return PEEKED_NONE; } } @@ -633,10 +661,15 @@ && isLiteral(buffer[pos + length])) { } // We've found the keyword followed either by EOF or by a non-literal character. - pos += length; + pos += length; //#20 return peeked = peeking; } + /*According to documentation buffer is of highest length required for any token, + therefore pos+i #24 is less that buffer.length.*/ + /*#21 ensures p+i < limit, therefore p+i is a valid index for buffer #23*/ + /*#22 ensures i < buffer.length therefore #25 is safe*/ + @SuppressWarnings({"compound.assignment.type.incompatible","array.access.unsafe.high","assignment.type.incompatible"}) private int peekNumber() throws IOException { // Like nextNonWhitespace, this uses locals 'p' and 'l' to save inner-loop field access. char[] buffer = this.buffer; @@ -648,12 +681,12 @@ private int peekNumber() throws IOException { boolean fitsInLong = true; int last = NUMBER_CHAR_NONE; - int i = 0; + @NonNegative int i = 0; charactersOfNumber: for (; true; i++) { - if (p + i == l) { - if (i == buffer.length) { + if (p + i == l) { //#21 + if (i == buffer.length) { //#22 // Though this looks like a well-formed number, it's too long to continue reading. Give up // and let the application handle this as an unquoted literal. return PEEKED_NONE; @@ -665,7 +698,7 @@ private int peekNumber() throws IOException { l = limit; } - char c = buffer[p + i]; + char c = buffer[p + i]; //#23 switch (c) { case '-': if (last == NUMBER_CHAR_NONE) { @@ -729,11 +762,11 @@ private int peekNumber() throws IOException { // We've read a complete number. Decide if it's a PEEKED_LONG or a PEEKED_NUMBER. if (last == NUMBER_CHAR_DIGIT && fitsInLong && (value != Long.MIN_VALUE || negative) && (value!=0 || false==negative)) { peekedLong = negative ? value : -value; - pos += i; + pos += i; //#24 return peeked = PEEKED_LONG; } else if (last == NUMBER_CHAR_DIGIT || last == NUMBER_CHAR_FRACTION_DIGIT || last == NUMBER_CHAR_EXP_DIGIT) { - peekedNumberLength = i; + peekedNumberLength = i; //#25 return peeked = PEEKED_NUMBER; } else { return PEEKED_NONE; @@ -772,10 +805,13 @@ private boolean isLiteral(char c) throws IOException { * @throws java.io.IOException if the next token in the stream is not a property * name. */ + /*#26 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #27 is safe*/ + @SuppressWarnings("array.access.unsafe.low") public String nextName() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#26 } String result; if (p == PEEKED_UNQUOTED_NAME) { @@ -788,7 +824,7 @@ public String nextName() throws IOException { throw new IllegalStateException("Expected a name but was " + peek() + locationString()); } peeked = PEEKED_NONE; - pathNames[stackSize - 1] = result; + pathNames[stackSize - 1] = result; //#27 return result; } @@ -800,10 +836,15 @@ public String nextName() throws IOException { * @throws IllegalStateException if the next token is not a string or if * this reader is closed. */ + /*#28 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #30 is safe*/ + /*According to documentation buffer is of highest length required for any token, + therefore pos+peekedNumberLength #29 is less that buffer.length.*/ + @SuppressWarnings({"array.access.unsafe.low","compound.assignment.type.incompatible"}) public String nextString() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#28 } String result; if (p == PEEKED_UNQUOTED) { @@ -819,12 +860,12 @@ public String nextString() throws IOException { result = Long.toString(peekedLong); } else if (p == PEEKED_NUMBER) { result = new String(buffer, pos, peekedNumberLength); - pos += peekedNumberLength; + pos += peekedNumberLength; //#29 } else { throw new IllegalStateException("Expected a string but was " + peek() + locationString()); } peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#30 return result; } @@ -835,18 +876,21 @@ public String nextString() throws IOException { * @throws IllegalStateException if the next token is not a boolean or if * this reader is closed. */ + /*#31 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #32 #33 is safe*/ + @SuppressWarnings("array.access.unsafe.low") public boolean nextBoolean() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#31 } if (p == PEEKED_TRUE) { peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#32 return true; } else if (p == PEEKED_FALSE) { peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#33 return false; } throw new IllegalStateException("Expected a boolean but was " + peek() + locationString()); @@ -859,14 +903,17 @@ public boolean nextBoolean() throws IOException { * @throws IllegalStateException if the next token is not null or if this * reader is closed. */ + /*#34 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #35 is safe*/ + @SuppressWarnings("array.access.unsafe.low") public void nextNull() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#34 } if (p == PEEKED_NULL) { peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#35 } else { throw new IllegalStateException("Expected null but was " + peek() + locationString()); } @@ -881,21 +928,26 @@ public void nextNull() throws IOException { * @throws NumberFormatException if the next literal value cannot be parsed * as a double, or is non-finite. */ + /*#36 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #37 #39 are safe*/ + /* According to documentatiom buffer is taken for highest length token, + pos + peekedNuberLength < buffer.length and safe #38*/ + @SuppressWarnings({"array.access.unsafe.low","compound.assignment.type.incompatible"}) public double nextDouble() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#36 } if (p == PEEKED_LONG) { peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#37 return (double) peekedLong; } if (p == PEEKED_NUMBER) { peekedString = new String(buffer, pos, peekedNumberLength); - pos += peekedNumberLength; + pos += peekedNumberLength; //#38 } else if (p == PEEKED_SINGLE_QUOTED || p == PEEKED_DOUBLE_QUOTED) { peekedString = nextQuotedValue(p == PEEKED_SINGLE_QUOTED ? '\'' : '"'); } else if (p == PEEKED_UNQUOTED) { @@ -912,7 +964,7 @@ public double nextDouble() throws IOException { } peekedString = null; peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#39 return result; } @@ -926,21 +978,26 @@ public double nextDouble() throws IOException { * @throws NumberFormatException if the next literal value cannot be parsed * as a number, or exactly represented as a long. */ + /*#40 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #41 #43 #44 are safe*/ + /* According to documentatiom buffer is taken for highest length token, + pos + peekedNuberLength < buffer.length and is safe #42*/ + @SuppressWarnings({"array.access.unsafe.low","compound.assignment.type.incompatible"}) public long nextLong() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#40 } if (p == PEEKED_LONG) { peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#41 return peekedLong; } if (p == PEEKED_NUMBER) { peekedString = new String(buffer, pos, peekedNumberLength); - pos += peekedNumberLength; + pos += peekedNumberLength; //#42 } else if (p == PEEKED_SINGLE_QUOTED || p == PEEKED_DOUBLE_QUOTED || p == PEEKED_UNQUOTED) { if (p == PEEKED_UNQUOTED) { peekedString = nextUnquotedValue(); @@ -950,7 +1007,7 @@ public long nextLong() throws IOException { try { long result = Long.parseLong(peekedString); peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#43 return result; } catch (NumberFormatException ignored) { // Fall back to parse as a double below. @@ -967,7 +1024,7 @@ public long nextLong() throws IOException { } peekedString = null; peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#44 return result; } @@ -981,21 +1038,26 @@ public long nextLong() throws IOException { * @throws NumberFormatException if any unicode escape sequences are * malformed. */ + //p > start due to #46, p - start > 0 and less than buffer.length - start, #47 #48 are safe + //as p > start, p-start is a valid argument #49 + @SuppressWarnings({"assignment.type.incompatible","argument.type.incompatible"}) private String nextQuotedValue(char quote) throws IOException { // Like nextNonWhitespace, this uses locals 'p' and 'l' to save inner-loop field access. char[] buffer = this.buffer; StringBuilder builder = null; while (true) { - int p = pos; + @NonNegative @LTLengthOf("buffer") int p = pos; int l = limit; /* the index of the first character not yet appended to the builder. */ int start = p; - while (p < l) { - int c = buffer[p++]; + while (p < l) { //#45 + //The while condition #45 ensures p < l and less than buffer.length, #46 is safe + @SuppressWarnings({"array.access.unsafe.high","unary.increment.type.incompatible"}) + int c = buffer[p++]; //#46 if (c == quote) { pos = p; - int len = p - start - 1; + @NonNegative @LTLengthOf(value="buffer", offset="start - 1") int len = p - start - 1; //#47 if (builder == null) { return new String(buffer, start, len); } else { @@ -1004,7 +1066,7 @@ private String nextQuotedValue(char quote) throws IOException { } } else if (c == '\\') { pos = p; - int len = p - start - 1; + @NonNegative @LTLengthOf(value="buffer", offset="start - 1") int len = p - start - 1; //#48 if (builder == null) { int estimatedLength = (len + 1) * 2; builder = new StringBuilder(Math.max(estimatedLength, 16)); @@ -1024,7 +1086,7 @@ private String nextQuotedValue(char quote) throws IOException { int estimatedLength = (p - start) * 2; builder = new StringBuilder(Math.max(estimatedLength, 16)); } - builder.append(buffer, start, p - start); + builder.append(buffer, start, p - start); //#49 pos = p; if (!fillBuffer(1)) { throw syntaxError("Unterminated string"); @@ -1035,14 +1097,18 @@ private String nextQuotedValue(char quote) throws IOException { /** * Returns an unquoted value as a string. */ - @SuppressWarnings("fallthrough") + /* According to documentatiom buffer is taken for highest length token, + therefore pos + i is less than buffer.length #52 #54*/ + /*i = 0 is valid as pos could have a maximum value of buffer.length - 1 #50 #53*/ + /* #51 is safe as the condition ensures that i < limit - pos in the loop*/ + @SuppressWarnings({"fallthrough","compound.assignment.type.incompatible","assignment.type.incompatible","unary.increment.type.incompatible"}) private String nextUnquotedValue() throws IOException { StringBuilder builder = null; - int i = 0; + @NonNegative @LTLengthOf(value="buffer", offset="this.pos-1") int i = 0; //#50 findNonLiteralCharacter: while (true) { - for (; pos + i < limit; i++) { + for (; pos + i < limit; i++) { //51 switch (buffer[pos + i]) { case '/': case '\\': @@ -1079,15 +1145,15 @@ private String nextUnquotedValue() throws IOException { builder = new StringBuilder(Math.max(i,16)); } builder.append(buffer, pos, i); - pos += i; - i = 0; + pos += i; //52 + i = 0; //#53 if (!fillBuffer(1)) { break; } } - + String result = (null == builder) ? new String(buffer, pos, i) : builder.append(buffer, pos, i).toString(); - pos += i; + pos += i; //#54 return result; } @@ -1098,7 +1164,9 @@ private void skipQuotedValue(char quote) throws IOException { int p = pos; int l = limit; /* the index of the first character not yet appended to the builder. */ - while (p < l) { + while (p < l) { //#55 + //The abouve while #55 ensure p < l and buffer.length + @SuppressWarnings("array.access.unsafe.high") int c = buffer[p++]; if (c == quote) { pos = p; @@ -1118,6 +1186,9 @@ private void skipQuotedValue(char quote) throws IOException { throw syntaxError("Unterminated string"); } + /* According to documentatiom buffer is taken for highest length token, + therefore pos + i is less than buffer.length #56*/ + @SuppressWarnings("compound.assignment.type.incompatible") private void skipUnquotedValue() throws IOException { do { int i = 0; @@ -1144,7 +1215,7 @@ private void skipUnquotedValue() throws IOException { return; } } - pos += i; + pos += i; //#56 } while (fillBuffer(1)); } @@ -1158,10 +1229,15 @@ private void skipUnquotedValue() throws IOException { * @throws NumberFormatException if the next literal value cannot be parsed * as a number, or exactly represented as an int. */ + /*#57 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #58 #60 #61 are safe*/ + /* According to documentatiom buffer is taken for highest length token, + pos + peekedNuberLength < buffer.length and is safe #59*/ + @SuppressWarnings({"array.access.unsafe.low","compound.assignment.type.incompatible"}) public int nextInt() throws IOException { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#57 } int result; @@ -1171,13 +1247,13 @@ public int nextInt() throws IOException { throw new NumberFormatException("Expected an int but was " + peekedLong + locationString()); } peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#58 return result; } if (p == PEEKED_NUMBER) { peekedString = new String(buffer, pos, peekedNumberLength); - pos += peekedNumberLength; + pos += peekedNumberLength; //#59 } else if (p == PEEKED_SINGLE_QUOTED || p == PEEKED_DOUBLE_QUOTED || p == PEEKED_UNQUOTED) { if (p == PEEKED_UNQUOTED) { peekedString = nextUnquotedValue(); @@ -1187,7 +1263,7 @@ public int nextInt() throws IOException { try { result = Integer.parseInt(peekedString); peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#60 return result; } catch (NumberFormatException ignored) { // Fall back to parse as a double below. @@ -1204,17 +1280,20 @@ public int nextInt() throws IOException { } peekedString = null; peeked = PEEKED_NONE; - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#61 return result; } /** * Closes this JSON reader and the underlying {@link java.io.Reader}. */ + /*#62 0 is less than length of stack*/ + /*stack has one element therefore stackSize = 1 is safe #63*/ + @SuppressWarnings({"array.access.unsafe.high.constant","assignment.type.incompatible"}) public void close() throws IOException { peeked = PEEKED_NONE; - stack[0] = JsonScope.CLOSED; - stackSize = 1; + stack[0] = JsonScope.CLOSED; //#62 + stackSize = 1; //#63 in.close(); } @@ -1223,12 +1302,18 @@ public void close() throws IOException { * elements are skipped. This method is intended for use when the JSON token * stream contains unrecognized or unhandled values. */ + /*#64 doPeek() returns the top of the stack, if it does not return one of the + expected values, exception is thrown therefore stackSize > 1 and #68 is safe*/ + /* According to documentatiom buffer is taken for highest length token, + pos + peekedNuberLength < buffer.length and is safe #67*/ + /*as stackSize > 1 #65 #66 is safe*/ + @SuppressWarnings({"array.access.unsafe.low","compound.assignment.type.incompatible","unary.decrement.type.incompatible"}) public void skipValue() throws IOException { int count = 0; do { int p = peeked; if (p == PEEKED_NONE) { - p = doPeek(); + p = doPeek(); //#64 } if (p == PEEKED_BEGIN_ARRAY) { @@ -1238,10 +1323,10 @@ public void skipValue() throws IOException { push(JsonScope.EMPTY_OBJECT); count++; } else if (p == PEEKED_END_ARRAY) { - stackSize--; + stackSize--; //#65 count--; } else if (p == PEEKED_END_OBJECT) { - stackSize--; + stackSize--; //#66 count--; } else if (p == PEEKED_UNQUOTED_NAME || p == PEEKED_UNQUOTED) { skipUnquotedValue(); @@ -1250,23 +1335,25 @@ public void skipValue() throws IOException { } else if (p == PEEKED_DOUBLE_QUOTED || p == PEEKED_DOUBLE_QUOTED_NAME) { skipQuotedValue('"'); } else if (p == PEEKED_NUMBER) { - pos += peekedNumberLength; + pos += peekedNumberLength; //#67 } peeked = PEEKED_NONE; } while (count != 0); - pathIndices[stackSize - 1]++; + pathIndices[stackSize - 1]++; //#68 pathNames[stackSize - 1] = "null"; } + //#69 ensures stackSize is less than stack.length, therefore #70 is safe + @SuppressWarnings({"array.access.unsafe.high","unary.increment.type.incompatible"}) private void push(int newTop) { - if (stackSize == stack.length) { + if (stackSize == stack.length) { //#69 int newLength = stackSize * 2; stack = Arrays.copyOf(stack, newLength); pathIndices = Arrays.copyOf(pathIndices, newLength); pathNames = Arrays.copyOf(pathNames, newLength); } - stack[stackSize++] = newTop; + stack[stackSize++] = newTop; //#70 } /** @@ -1274,24 +1361,30 @@ private void push(int newTop) { * exhausted before that many characters are available, this returns * false. */ + /*#73 ensured that total is no more than buffer.length - limit, + therefore #74 is safe*/ + /*#75 is safe as pos = 0 and incrementing pos once is less than buffer.length*/ + /*#73 has safe arguments as buffer.length > limit and buffer.length - limit > 0*/ + /*#72 arraycopy has valid arguments due to #71 as limit is less than buffer.length - pos*/ + @SuppressWarnings({"compound.assignment.type.incompatible","unary.increment.type.incompatible","argument.type.incompatible"}) private boolean fillBuffer(int minimum) throws IOException { char[] buffer = this.buffer; lineStart -= pos; if (limit != pos) { - limit -= pos; - System.arraycopy(buffer, pos, buffer, 0, limit); + limit -= pos; //#71 + System.arraycopy(buffer, pos, buffer, 0, limit); //#72 } else { limit = 0; } pos = 0; int total; - while ((total = in.read(buffer, limit, buffer.length - limit)) != -1) { - limit += total; + while ((total = in.read(buffer, limit, buffer.length - limit)) != -1) { //#73 + limit += total; //#74 // if this is the first read, consume an optional byte order mark (BOM) if it exists if (lineNumber == 0 && lineStart == 0 && limit > 0 && buffer[0] == '\ufeff') { - pos++; + pos++; //#75 lineStart++; minimum++; } @@ -1309,7 +1402,12 @@ private boolean fillBuffer(int minimum) throws IOException { * {@code buffer[pos-1]}; this means the caller can always push back the * returned character by decrementing {@code pos}. */ - private int nextNonWhitespace(boolean throwOnEof) throws IOException { + /*As #77 c is a character being read from buffer pos > 0 therefore #78 is safe*/ + /*as #78 pos was decremented to push'/' to buffer, #79 is a valid and safe operation to consume back '/'*/ + /*#80 reads a character from the buffer therefore pos incremented #81 #84 is safe and valid*/ + /*if #82 returns true, terminating characters of a comment are read by incrementing pos by 2, therefore #83 is safe*/ + @SuppressWarnings({"unary.decrement.type.incompatible","unary.increment.type.incompatible","assignment.type.incompatible"}) + private @GTENegativeOne int nextNonWhitespace(boolean throwOnEof) throws IOException { /* * This code uses ugly local variables 'p' and 'l' representing the 'pos' * and 'limit' fields respectively. Using locals rather than fields saves @@ -1319,10 +1417,10 @@ private int nextNonWhitespace(boolean throwOnEof) throws IOException { * 'p' and 'l' after any (potentially indirect) call to the same method. */ char[] buffer = this.buffer; - int p = pos; + @NonNegative @LTLengthOf("buffer") int p = pos; int l = limit; while (true) { - if (p == l) { + if (p == l) { //#76 pos = p; if (!fillBuffer(1)) { break; @@ -1331,7 +1429,11 @@ private int nextNonWhitespace(boolean throwOnEof) throws IOException { l = limit; } - int c = buffer[p++]; + /*c stores the ascii value of a character which is NonNegative + #76 ensures p < l therefore less than limit and buffer.length therefore buffer[p] is safe + as p < l, p++ is within valid range*/ + @SuppressWarnings({"assignment.type.incompatible","array.access.unsafe.high","unary.increment.type.incompatible"}) + @NonNegative int c = buffer[p++]; if (c == '\n') { lineNumber++; lineStart = p; @@ -1340,33 +1442,33 @@ private int nextNonWhitespace(boolean throwOnEof) throws IOException { continue; } - if (c == '/') { + if (c == '/') {//#77 pos = p; if (p == l) { - pos--; // push back '/' so it's still in the buffer when this method returns + pos--; // push back '/' so it's still in the buffer when this method returns #78 boolean charsLoaded = fillBuffer(2); - pos++; // consume the '/' again + pos++; // consume the '/' again #79 if (!charsLoaded) { return c; } } checkLenient(); - char peek = buffer[pos]; + char peek = buffer[pos]; //#80 switch (peek) { case '*': // skip a /* c-style comment */ - pos++; - if (!skipTo("*/")) { + pos++; //#81 + if (!skipTo("*/")) { //#82 throw syntaxError("Unterminated comment"); } - p = pos + 2; + p = pos + 2; //#83 l = limit; continue; case '/': // skip a // end-of-line comment - pos++; + pos++; //#84 skipToEndOfLine(); p = pos; l = limit; @@ -1409,9 +1511,11 @@ private void checkLenient() throws IOException { * is terminated by "\r\n", the '\n' must be consumed as whitespace by the * caller. */ + //pos is ensured to be < limit #85, therefore #86 is safe + @SuppressWarnings({"array.access.unsafe.high","unary.increment.type.incompatible"}) private void skipToEndOfLine() throws IOException { - while (pos < limit || fillBuffer(1)) { - char c = buffer[pos++]; + while (pos < limit || fillBuffer(1)) { //#85 + char c = buffer[pos++]; //#86 if (c == '\n') { lineNumber++; lineStart = pos; @@ -1425,17 +1529,19 @@ private void skipToEndOfLine() throws IOException { /** * @param toFind a string to search for. Must not contain a newline. */ + //pos+length is ensured to be less than limit #87 therefore #88 #88 are safe + @SuppressWarnings({"array.access.unsafe.high","array.access.unsafe.low","unary.increment.type.incompatible"}) private boolean skipTo(String toFind) throws IOException { int length = toFind.length(); outer: - for (; pos + length <= limit || fillBuffer(length); pos++) { - if (buffer[pos] == '\n') { + for (; pos + length <= limit || fillBuffer(length); pos++) { //#87 + if (buffer[pos] == '\n') { //#88 lineNumber++; lineStart = pos + 1; continue; } for (int c = 0; c < length; c++) { - if (buffer[pos + c] != toFind.charAt(c)) { + if (buffer[pos + c] != toFind.charAt(c)) { //#89 continue outer; } } @@ -1458,9 +1564,11 @@ String locationString() { * Returns a JsonPath to * the current location in the JSON value. */ + //Could not add annotation to i and not size #90 + @SuppressWarnings("assignment.type.incompatible") public String getPath() { StringBuilder result = new StringBuilder().append('$'); - for (int i = 0, size = stackSize; i < size; i++) { + for (@IndexFor("stack") int i = 0, size = stackSize; i < size; i++) { //#90 switch (stack[i]) { case JsonScope.EMPTY_ARRAY: case JsonScope.NONEMPTY_ARRAY: @@ -1494,20 +1602,28 @@ public String getPath() { * @throws NumberFormatException if any unicode escape sequences are * malformed. */ + /*According to documentation, buffer is of highest possible length of token, + and pos+4 was already ensured to be less than limit #92, therefore #94 is safe*/ + //the if #92 ensures 4 < buffer.length - pos therefore #93 is safe + @SuppressWarnings({"compound.assignment.type.incompatible","argument.type.incompatible"}) private char readEscapeCharacter() throws IOException { - if (pos == limit && !fillBuffer(1)) { + if (pos == limit && !fillBuffer(1)) { //#91 throw syntaxError("Unterminated escape sequence"); } + //The above if #91 ensures pos < limit + @SuppressWarnings({"unary.increment.type.incompatible"}) char escaped = buffer[pos++]; switch (escaped) { case 'u': - if (pos + 4 > limit && !fillBuffer(4)) { + if (pos + 4 > limit && !fillBuffer(4)) { //#92 throw syntaxError("Unterminated escape sequence"); } // Equivalent to Integer.parseInt(stringPool.get(buffer, pos, 4), 16); char result = 0; for (int i = pos, end = i + 4; i < end; i++) { + //if #92 ensures pos + 4 < limit, therefore index i is safe + @SuppressWarnings("array.access.unsafe.high") char c = buffer[i]; result <<= 4; if (c >= '0' && c <= '9') { @@ -1517,10 +1633,10 @@ private char readEscapeCharacter() throws IOException { } else if (c >= 'A' && c <= 'F') { result += (c - 'A' + 10); } else { - throw new NumberFormatException("\\u" + new String(buffer, pos, 4)); + throw new NumberFormatException("\\u" + new String(buffer, pos, 4)); //#93 } } - pos += 4; + pos += 4; //#94 return result; case 't': @@ -1546,7 +1662,7 @@ private char readEscapeCharacter() throws IOException { case '\'': case '"': case '\\': - case '/': + case '/': return escaped; default: // throw error when none of the above cases are matched @@ -1565,23 +1681,28 @@ private IOException syntaxError(String message) throws IOException { /** * Consumes the non-execute prefix if it exists. */ + //ALready been checked if p+5 < limit #96 therefore no unsafe access in #97 + //acc to doc returned character by nextNonWhitespace is always at pos-1 therefore decrementing is safe #95, as pos>0 + /*According to documentation buffer is of highest possible length of token, + and pos+5 was already ensured to be less than limit #96, therefore #98 is safe*/ + @SuppressWarnings({"array.access.unsafe.high","array.access.unsafe.low","compound.assignment.type.incompatible","unary.decrement.type.incompatible"}) private void consumeNonExecutePrefix() throws IOException { // fast forward through the leading whitespace nextNonWhitespace(true); - pos--; + pos--; //#95 int p = pos; - if (p + 5 > limit && !fillBuffer(5)) { + if (p + 5 > limit && !fillBuffer(5)) { //#96 return; } char[] buf = buffer; - if(buf[p] != ')' || buf[p + 1] != ']' || buf[p + 2] != '}' || buf[p + 3] != '\'' || buf[p + 4] != '\n') { + if(buf[p] != ')' || buf[p + 1] != ']' || buf[p + 2] != '}' || buf[p + 3] != '\'' || buf[p + 4] != '\n') { //#97 return; // not a security token! } // we consumed a security token! - pos += 5; + pos += 5; //#98 } static { diff --git a/gson/src/main/java/com/google/gson/stream/JsonWriter.java b/gson/src/main/java/com/google/gson/stream/JsonWriter.java index 84eaa0a7c4..9dc404fd30 100644 --- a/gson/src/main/java/com/google/gson/stream/JsonWriter.java +++ b/gson/src/main/java/com/google/gson/stream/JsonWriter.java @@ -29,6 +29,8 @@ import static com.google.gson.stream.JsonScope.NONEMPTY_ARRAY; import static com.google.gson.stream.JsonScope.NONEMPTY_DOCUMENT; import static com.google.gson.stream.JsonScope.NONEMPTY_OBJECT; +import org.checkerframework.checker.index.qual.IndexOrHigh; +import org.checkerframework.common.value.qual.ArrayLen; /** * Writes a JSON (RFC 7159) @@ -140,8 +142,8 @@ public class JsonWriter implements Closeable, Flushable { * newline characters. This prevents eval() from failing with a syntax * error. http://code.google.com/p/google-gson/issues/detail?id=341 */ - private static final String[] REPLACEMENT_CHARS; - private static final String[] HTML_SAFE_REPLACEMENT_CHARS; + private static final String @ArrayLen(128) [] REPLACEMENT_CHARS; + private static final String @ArrayLen(128) [] HTML_SAFE_REPLACEMENT_CHARS; static { REPLACEMENT_CHARS = new String[128]; for (int i = 0; i <= 0x1f; i++) { @@ -166,7 +168,7 @@ public class JsonWriter implements Closeable, Flushable { private final Writer out; private int[] stack = new int[32]; - private int stackSize = 0; + private @IndexOrHigh("stack") int stackSize = 0; { push(EMPTY_DOCUMENT); } @@ -333,6 +335,10 @@ private JsonWriter open(int empty, char openBracket) throws IOException { * Closes the current scope by appending any necessary whitespace and the * given bracket. */ + + /*close is a private function and is called after open() which pushes + empty to the stack therefore stackSize > 0 #1*/ + @SuppressWarnings("unary.decrement.type.incompatible") private JsonWriter close(int empty, int nonempty, char closeBracket) throws IOException { int context = peek(); @@ -343,7 +349,7 @@ private JsonWriter close(int empty, int nonempty, char closeBracket) throw new IllegalStateException("Dangling name: " + deferredName); } - stackSize--; + stackSize--; //#1 if (context == nonempty) { newline(); } @@ -351,11 +357,14 @@ private JsonWriter close(int empty, int nonempty, char closeBracket) return this; } + /*#2 ensures that if stack is full its size is doubled, + therefore #3 stackSize is within range of stack and code is safe*/ + @SuppressWarnings({"array.access.unsafe.high","unary.increment.type.incompatible"}) private void push(int newTop) { - if (stackSize == stack.length) { + if (stackSize == stack.length) { //#2 stack = Arrays.copyOf(stack, stackSize * 2); } - stack[stackSize++] = newTop; + stack[stackSize++] = newTop; //#3 } /** @@ -371,8 +380,10 @@ private int peek() { /** * Replace the value on the top of the stack with the given value. */ + //replaceTop is a private function and is called when stack is not empty, #4 is safe + @SuppressWarnings("array.access.unsafe.low") private void replaceTop(int topOfStack) { - stack[stackSize - 1] = topOfStack; + stack[stackSize - 1] = topOfStack; //#4 } /** @@ -560,6 +571,9 @@ public void close() throws IOException { stackSize = 0; } + /*c is a character having ascii value >= 0 therefore is a valid index #5 + * if ensures last < i #6 therefore the index sent is a safe index for value #7*/ + @SuppressWarnings({"array.access.unsafe.low","argument.type.incompatible"}) private void string(String value) throws IOException { String[] replacements = htmlSafe ? HTML_SAFE_REPLACEMENT_CHARS : REPLACEMENT_CHARS; out.write('\"'); @@ -569,7 +583,7 @@ private void string(String value) throws IOException { char c = value.charAt(i); String replacement; if (c < 128) { - replacement = replacements[c]; + replacement = replacements[c]; //#5 if (replacement == null) { continue; } @@ -580,8 +594,8 @@ private void string(String value) throws IOException { } else { continue; } - if (last < i) { - out.write(value, last, i - last); + if (last < i) { //#6 + out.write(value, last, i - last); //#7 } out.write(replacement); last = i + 1; diff --git a/gson/src/main/java/module-info.java b/gson/src/main/java/module-info.java index 161fbdba7f..a42440cb22 100644 --- a/gson/src/main/java/module-info.java +++ b/gson/src/main/java/module-info.java @@ -9,4 +9,5 @@ exports com.google.gson.stream; requires transitive java.sql; + requires org.checkerframework.checker; } diff --git a/pom.xml b/pom.xml index 1fb47fcde4..7312bb54e8 100644 --- a/pom.xml +++ b/pom.xml @@ -54,6 +54,16 @@ 4.12 test + + org.checkerframework + checker + 3.4.0 + + + org.checkerframework + jdk11 + 3.4.0 + @@ -70,8 +80,7 @@ 9 - - 9 + @@ -81,7 +90,7 @@ - module-info.java + @@ -90,8 +99,20 @@ [1.5,9) - 1.6 - 1.6 + 11 + + + 10000 + 10000 + + + org.checkerframework.checker.index.IndexChecker + + + + -J- -add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED + -AprintErrorStack +