Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added annotations to org.apache.dubbo.common.io #1

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Added annotations to org.apache.dubbo.common.io #1

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
bdc4403
Added annotations
Maxi17 Jun 5, 2019
c42444f
Updated pom.xml file
Maxi17 Jun 7, 2019
34eb60e
Updated pom.xml
Maxi17 Jun 7, 2019
34b3627
Updated pom.xml and improved annotations
Maxi17 Jun 10, 2019
90f08fe
Improved annotations
Maxi17 Jun 11, 2019
37ecbee
Improved annotations
Maxi17 Jun 11, 2019
489a4e1
Improved annotations
Maxi17 Jun 13, 2019
95b7927
Improved annotations
Maxi17 Jun 14, 2019
702acd8
Improved pom.xml file
Maxi17 Jun 14, 2019
c6fddfb
Improved pom.xml file
Maxi17 Jun 14, 2019
100aac8
Improved annotations
Maxi17 Jun 21, 2019
e861190
Improved annotation
Maxi17 Jun 22, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 35 additions & 1 deletion dubbo-common/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,5 +77,39 @@
<groupId>de.ruedigermoeller</groupId>
<artifactId>fst</artifactId>
</dependency>
<dependency>
<groupId>org.checkerframework</groupId>
<artifactId>checker</artifactId>
<version>2.8.1</version>
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be latest release when this is merged (so 2.8.2 right now)

</dependency>
<dependency>
<groupId>org.checkerframework</groupId>
<artifactId>jdk8</artifactId>
<version>2.8.1</version>
</dependency>
</dependencies>
</project>
<build>
<plugins>
<plugin>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.3</version>
<configuration>
<source>1.8</source>
<target>1.8</target>
<compilerArguments>
<Xmaxerrs>10000</Xmaxerrs>
<Xmaxwarns>10000</Xmaxwarns>
</compilerArguments>
<annotationProcessors>
<annotationProcessor>org.checkerframework.checker.index.IndexChecker</annotationProcessor>
</annotationProcessors>
<compilerArgs>
<arg>-Xbootclasspath/p:$CHECKERFRAMEWORK/checker/dist/jdk8.jar</arg>
<arg>-AprintErrorStack</arg>
<arg>-AonlyDefs=^org\.apache\.dubbo\.common\.io\.</arg>
</compilerArgs>
</configuration>
</plugin>
</plugins>
</build>
</project>
187 changes: 110 additions & 77 deletions dubbo-common/src/main/java/org/apache/dubbo/common/io/Bytes.java
View file
Open in desktop

Large diffs are not rendered by default.

18 changes: 10 additions & 8 deletions dubbo-common/src/main/java/org/apache/dubbo/common/io/StreamUtils.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@
*/
package org.apache.dubbo.common.io;

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

import java.io.IOException;
import java.io.InputStream;

Expand All @@ -31,7 +33,7 @@ public static InputStream limitedInputStream(final InputStream is, final int lim
private int mPosition = 0, mMark = 0, mLimit = Math.min(limit, is.available());

@Override
public int read() throws IOException {
public @GTENegativeOne int read() throws IOException {
if (mPosition < mLimit) {
mPosition++;
return is.read();
Expand All @@ -40,7 +42,7 @@ public int read() throws IOException {
}

@Override
public int read(byte[] b, int off, int len) throws IOException {
public @GTENegativeOne @LTEqLengthOf("#1") int read(byte[] b, @IndexOrHigh("#1") int off, @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int len) throws IOException {
if (b == null) {
throw new NullPointerException();
}
Expand All @@ -67,7 +69,7 @@ public int read(byte[] b, int off, int len) throws IOException {
}

@Override
public long skip(long len) throws IOException {
public @NonNegative long skip(long len) throws IOException {
if (mPosition + len > mLimit) {
len = mLimit - mPosition;
}
Expand All @@ -82,7 +84,7 @@ public long skip(long len) throws IOException {
}

@Override
public int available() {
public @NonNegative int available() {
return mLimit - mPosition;
}

Expand All @@ -92,7 +94,7 @@ public boolean markSupported() {
}

@Override
public void mark(int readlimit) {
public void mark(@NonNegative int readlimit) {
is.mark(readlimit);
mMark = mPosition;
}
Expand All @@ -110,7 +112,7 @@ public void close() throws IOException {
};
}

public static InputStream markSupportedInputStream(final InputStream is, final int markBufferSize) {
public static InputStream markSupportedInputStream(final InputStream is, final @NonNegative int markBufferSize) {
if (is.markSupported()) {
return is;
}
Expand All @@ -125,7 +127,7 @@ public static InputStream markSupportedInputStream(final InputStream is, final i
private int mCount = 0;

@Override
public int read() throws IOException {
public @GTENegativeOne int read() throws IOException {
if (!mInMarked) {
return is.read();
} else {
Expand Down Expand Up @@ -202,7 +204,7 @@ public boolean markSupported() {
}

@Override
public int available() throws IOException {
public @NonNegative int available() throws IOException {
int available = is.available();

if (mInMarked && mInReset) {
Expand Down
36 changes: 25 additions & 11 deletions dubbo-common/src/main/java/org/apache/dubbo/common/io/UnsafeByteArrayInputStream.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,35 +19,48 @@
import java.io.IOException;
import java.io.InputStream;

import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;

/**
* UnsafeByteArrayInputStream.
*/
public class UnsafeByteArrayInputStream extends InputStream {
protected byte[] mData;

protected int mPosition, mLimit, mMark = 0;
protected @IndexOrHigh("this.mData") int mPosition, mMark, mLimit = 0;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not annotated mPosition as @LessThan("this.mLimit")? You use that fact to justify several warning suppressions later in the file.


public UnsafeByteArrayInputStream(byte[] buf) {
this(buf, 0, buf.length);
}

public UnsafeByteArrayInputStream(byte[] buf, int offset) {
@SuppressWarnings("argument.type.incompatible") // The length of the array is always greater than the index used to access it.
public UnsafeByteArrayInputStream(byte[] buf, @IndexOrHigh("#1") int offset) {
this(buf, offset, buf.length - offset);
}

public UnsafeByteArrayInputStream(byte[] buf, int offset, int length) {
public UnsafeByteArrayInputStream(byte[] buf, @IndexOrHigh("#1") int offset, @NonNegative int length) {
mData = buf;
mPosition = mMark = offset;
mLimit = Math.min(offset + length, buf.length);
}

@Override
public int read() {
public @GTENegativeOne int read() {
return (mPosition < mLimit) ? (mData[mPosition++] & 0xff) : -1;
}

@Override
public int read(byte[] b, int off, int len) {
@SuppressWarnings({"assignment.type.incompatible", "argument.type.incompatible", "return.type.incompatible"}) /*
#1. mLimit is greater than mPosition and after the assignment the value can only decrease, so it stays valid.
#2. The call is safe because len has been verified before.
#3. The return type is safe because len has been verified.
*/
public @GTENegativeOne @LTEqLengthOf("#1") int read(byte[] b, @IndexOrHigh("#1") int off, @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int len) {
if (b == null) {
throw new NullPointerException();
}
Expand All @@ -58,18 +71,18 @@ public int read(byte[] b, int off, int len) {
return -1;
}
if (mPosition + len > mLimit) {
len = mLimit - mPosition;
len = mLimit - mPosition; // #1
}
if (len <= 0) {
return 0;
}
System.arraycopy(mData, mPosition, b, off, len);
System.arraycopy(mData, mPosition, b, off, len); // #2
mPosition += len;
return len;
return len; // #3
}

@Override
public long skip(long len) {
public @NonNegative long skip(long len) {
if (mPosition + len > mLimit) {
len = mLimit - mPosition;
}
Expand All @@ -81,7 +94,8 @@ public long skip(long len) {
}

@Override
public int available() {
@SuppressWarnings("return.type.incompatible") // mPosition is always lower than mLimit
public @NonNegative int available() {
return mLimit - mPosition;
}

Expand All @@ -108,7 +122,7 @@ public int position() {
return mPosition;
}

public void position(int newPosition) {
public void position(@IndexFor("this.mData") int newPosition) {
mPosition = newPosition;
}

Expand Down
14 changes: 11 additions & 3 deletions dubbo-common/src/main/java/org/apache/dubbo/common/io/UnsafeByteArrayOutputStream.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,26 +21,32 @@
import java.io.UnsupportedEncodingException;
import java.nio.ByteBuffer;

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;

/**
* UnsafeByteArrayOutputStream.
*/
public class UnsafeByteArrayOutputStream extends OutputStream {
protected byte[] mBuffer;

protected int mCount;
protected @IndexOrHigh("this.mBuffer") int mCount;

public UnsafeByteArrayOutputStream() {
this(32);
}

public UnsafeByteArrayOutputStream(int size) {
public UnsafeByteArrayOutputStream(@NonNegative int size) {
if (size < 0) {
throw new IllegalArgumentException("Negative initial size: " + size);
}
mBuffer = new byte[size];
}

@Override
@SuppressWarnings({"array.access.unsafe", "assignment.type.incompatible"}) // If mCount becomes mBuffer.length, then the array is extended before accessing it
public void write(int b) {
int newcount = mCount + 1;
if (newcount > mBuffer.length) {
Expand All @@ -51,7 +57,9 @@ public void write(int b) {
}

@Override
public void write(byte[] b, int off, int len) {
@SuppressWarnings({"argument.type.incompatible", "assignment.type.incompatible"}) // len is valid because if mCount + len exceeds mBuffer.length, then
// the array is extended
public void write(byte[] b, @IndexOrHigh("#1") int off, @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int len) {
if ((off < 0) || (off > b.length) || (len < 0) || ((off + len) > b.length) || ((off + len) < 0)) {
throw new IndexOutOfBoundsException();
}
Expand Down
29 changes: 21 additions & 8 deletions dubbo-common/src/main/java/org/apache/dubbo/common/io/UnsafeStringReader.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,13 +19,19 @@
import java.io.IOException;
import java.io.Reader;

import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;

/**
* Thread-unsafe StringReader.
*/
public class UnsafeStringReader extends Reader {
private String mString;

private int mPosition, mLimit, mMark;
private @IndexOrHigh("this.mString") int mPosition,mLimit, mMark;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing space in this line


public UnsafeStringReader(String str) {
mString = str;
Expand All @@ -34,7 +40,9 @@ public UnsafeStringReader(String str) {
}

@Override
public int read() throws IOException {
@SuppressWarnings({"return.type.incompatible", "argument.type.incompatible", "compound.assignment.type.incompatible"})
// A char is always greater than 0 and it has been previously verified that mPosition is less than the length of mString
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Where/how was that verified? If it's a precondition of the method, you should express it as an annotation instead.

public @GTENegativeOne int read() throws IOException {
ensureOpen();
if (mPosition >= mLimit) {
return -1;
Expand All @@ -44,7 +52,11 @@ public int read() throws IOException {
}

@Override
public int read(char[] cs, int off, int len) throws IOException {
@SuppressWarnings({"argument.type.incompatible", "compound.assignment.type.incompatible", "return.type.incompatible"}) /*
#1 and #2. mPosition + n is at most mLimit, which is a valid index
#3. Both mLimit - mPosition and len have been verified, so the returned variable is correct
*/
public @GTENegativeOne @LTEqLengthOf("#1") int read(char[] cs, @IndexOrHigh("#1") int off, @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int len) throws IOException {
ensureOpen();
if ((off < 0) || (off > cs.length) || (len < 0) ||
((off + len) > cs.length) || ((off + len) < 0)) {
Expand All @@ -60,13 +72,14 @@ public int read(char[] cs, int off, int len) throws IOException {
}

int n = Math.min(mLimit - mPosition, len);
mString.getChars(mPosition, mPosition + n, cs, off);
mPosition += n;
return n;
mString.getChars(mPosition, mPosition + n, cs, off); // #1
mPosition += n; // #2
return n; // #3
}

@Override
public long skip(long ns) throws IOException {
@SuppressWarnings("compound.assignment.type.incompatible") // n is valid because it was previously verified
public @NonNegative long skip(long ns) throws IOException {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not convinced that this is the right specification for this method: I would expect that the argument ns should be @NonNegative. Why isn't that the case here?

ensureOpen();
if (mPosition >= mLimit) {
return 0;
Expand All @@ -90,7 +103,7 @@ public boolean markSupported() {
}

@Override
public void mark(int readAheadLimit) throws IOException {
public void mark(@NonNegative int readAheadLimit) throws IOException {
if (readAheadLimit < 0) {
throw new IllegalArgumentException("Read-ahead limit < 0");
}
Expand Down
13 changes: 9 additions & 4 deletions dubbo-common/src/main/java/org/apache/dubbo/common/io/UnsafeStringWriter.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,10 @@
import java.io.IOException;
import java.io.Writer;

import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;

/**
* Thread-unsafe StringWriter.
*/
Expand All @@ -29,7 +33,7 @@ public UnsafeStringWriter() {
lock = mBuffer = new StringBuilder();
}

public UnsafeStringWriter(int size) {
public UnsafeStringWriter(@NonNegative int size) {
if (size < 0) {
throw new IllegalArgumentException("Negative buffer size");
}
Expand All @@ -48,7 +52,7 @@ public void write(char[] cs) throws IOException {
}

@Override
public void write(char[] cs, int off, int len) throws IOException {
public void write(char[] cs, @IndexOrHigh("#1") int off, @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int len) throws IOException {
if ((off < 0) || (off > cs.length) || (len < 0) ||
((off + len) > cs.length) || ((off + len) < 0)) {
throw new IndexOutOfBoundsException();
Expand All @@ -65,7 +69,7 @@ public void write(String str) {
}

@Override
public void write(String str, int off, int len) {
public void write(String str, @IndexOrHigh("#1") int off, @NonNegative @LTLengthOf(value = "#1", offset = "#2 - 1") int len) {
mBuffer.append(str.substring(off, off + len));
}

Expand All @@ -80,7 +84,8 @@ public Writer append(CharSequence csq) {
}

@Override
public Writer append(CharSequence csq, int start, int end) {
@SuppressWarnings("argument.type.incompatible") // The documentation is inherited from the overridden method.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand what you mean by this? Are you saying that the spec on the inherited method is wrong?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried to say that the implementation of this method is similar to the overridden one, which is part of the JDK. That one has a documentation and specifies that the method can throw an IndexOutOfBoundsException

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you clarify in the comment exactly where the warning is being suppressed, and how the exception can be thrown? Alternatively, you could add a link to the JDK documentation on the web so that a reader can easily read it themselves. As it is now, it's very confusing.

public Writer append(CharSequence csq, @IndexOrHigh("#1") int start, @IndexOrHigh("#1") int end) {
CharSequence cs = (csq == null ? "null" : csq);
write(cs.subSequence(start, end).toString());
return this;
Expand Down
Loading