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

Jump to bottom

Add aliasing annotations #57

Merged
merged 11 commits into from
Jul 21, 2020
Merged

Add aliasing annotations #57

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
d762ff3
Transferring stubfile.astub annotations in jdk
aditya3434 Jun 20, 2020
2b20719
Transferring stubfile.astub annotations in jdk
aditya3434 Jun 20, 2020
4b31773
Fixing String.java
aditya3434 Jun 20, 2020
6cfb5ad
Fixing String.java
aditya3434 Jun 20, 2020
9d2e56f
Changing annotation position
aditya3434 Jun 24, 2020
048d592
Updating Object constructor
aditya3434 Jun 28, 2020
76fb25d
Merge branch 'master' into 3313-explicit-annotation-fix
aditya3434 Jun 28, 2020
211d04c
Annotating remaining constructors and some methods
aditya3434 Jun 28, 2020
d0cabbd
Fixing parameter
aditya3434 Jun 28, 2020
1df80aa
Annotating other append functions
aditya3434 Jun 28, 2020
dc87ebb
Merge branch 'master' into 3313-explicit-annotation-fix
aditya3434 Jul 17, 2020
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
13 changes: 7 additions & 6 deletions src/java.base/share/classes/java/lang/Exception.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.framework.qual.AnnotatedFor;
import org.checkerframework.common.aliasing.qual.Unique;

/**
* The class {@code Exception} and its subclasses are a form of
Expand All @@ -46,7 +47,7 @@
* @jls 11.2 Compile-Time Checking of Exceptions
* @since 1.0
*/
@AnnotatedFor({"nullness"})
@AnnotatedFor({"aliasing", "nullness"})
public class Exception extends Throwable {
static final long serialVersionUID = -3387516993124229948L;

Expand All @@ -56,7 +57,7 @@ public class Exception extends Throwable {
* call to {@link #initCause}.
*/
@SideEffectFree
public Exception() {
public @Unique Exception() {
Copy link
Member

Choose a reason for hiding this comment

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

There are other constructors for this class. Shouldn't they also return a @Unique object?
Can you just look through the whole class bodies for the two methods and see whether other annotations are missing?

Copy link
Author

@aditya3434 aditya3434 Jun 28, 2020 •
edited
Loading

Choose a reason for hiding this comment

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

I have annotated the remaining constructors as @unique in my latest commit.

super();
}

Expand All @@ -69,7 +70,7 @@ public Exception() {
* later retrieval by the {@link #getMessage()} method.
*/
@SideEffectFree
public Exception(@Nullable String message) {
public @Unique Exception(@Nullable String message) {
super(message);
}

Expand All @@ -88,7 +89,7 @@ public Exception(@Nullable String message) {
* @since 1.4
*/
@SideEffectFree
public Exception(@Nullable String message, @Nullable Throwable cause) {
public @Unique Exception(@Nullable String message, @Nullable Throwable cause) {
super(message, cause);
}

Expand All @@ -107,7 +108,7 @@ public Exception(@Nullable String message, @Nullable Throwable cause) {
* @since 1.4
*/
@SideEffectFree
public Exception(@Nullable Throwable cause) {
public @Unique Exception(@Nullable Throwable cause) {
super(cause);
}

Expand All @@ -125,7 +126,7 @@ public Exception(@Nullable Throwable cause) {
* be writable
* @since 1.7
*/
protected Exception(@Nullable String message, @Nullable Throwable cause,
protected @Unique Exception(@Nullable String message, @Nullable Throwable cause,
boolean enableSuppression,
boolean writableStackTrace) {
super(message, cause, enableSuppression, writableStackTrace);
Expand Down
33 changes: 17 additions & 16 deletions src/java.base/share/classes/java/lang/String.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.framework.qual.AnnotatedFor;
import org.checkerframework.framework.qual.CFComment;
import org.checkerframework.common.aliasing.qual.Unique;

import java.io.ObjectStreamField;
import java.io.UnsupportedEncodingException;
Expand Down Expand Up @@ -153,7 +154,7 @@
* @jls 15.18.1 String Concatenation Operator +
*/

@AnnotatedFor({"formatter", "index", "interning", "lock", "nullness", "regex", "signature", "signedness", "value"})
@AnnotatedFor({"aliasing", "formatter", "index", "interning", "lock", "nullness", "regex", "signature", "signedness"})
Copy link
Member

Choose a reason for hiding this comment

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

Did you go through all methods and make sure uniqueness is correctly annotated? Same for StringBuffer.

Copy link
Author

Choose a reason for hiding this comment

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

I went through all the methods, however, I don't think any of them should return @unique results. Hence, I annotated the constructors of the data types for the most part. In StringBuffer, I also annotated the append function as they were annotated in the now deleted stubfile.

public final class String
implements java.io.Serializable, Comparable<String>, CharSequence {

Expand Down Expand Up @@ -250,7 +251,7 @@ public final class String
*/
@SideEffectFree
@StaticallyExecutable
public @StringVal("") String() {
public @StringVal("") @Unique String() {
Copy link
Member

Choose a reason for hiding this comment

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

Also for this class and StringBuffer below, annotate the other constructors and see whether any other methods should be annotated.

Copy link
Author

@aditya3434 aditya3434 Jun 28, 2020 •
edited
Loading

Choose a reason for hiding this comment

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

I have annotated the remaining constructors as @unique in my latest commit. I also annotated the append function for the StringBuffer data type as they were annotated in the stub file.

this.value = "".value;
this.coder = "".coder;
}
Expand All @@ -268,7 +269,7 @@ public final class String
@SideEffectFree
@StaticallyExecutable
@HotSpotIntrinsicCandidate
public @PolyValue String(@PolyValue String original) {
public @PolyValue @Unique String(@PolyValue String original) {
this.value = original.value;
this.coder = original.coder;
this.hash = original.hash;
Expand All @@ -285,7 +286,7 @@ public final class String
*/
@SideEffectFree
@StaticallyExecutable
public @PolyValue String(char value @GuardSatisfied @PolyValue []) {
public @PolyValue @Unique String(char value @GuardSatisfied @PolyValue []) {
this(value, 0, value.length, null);
}

Expand All @@ -312,7 +313,7 @@ public final class String
*/
@SideEffectFree
@StaticallyExecutable
public String(char value @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int count) {
public @Unique String(char value @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int count) {
this(value, offset, count, rangeCheck(value, offset, count));
}

Expand Down Expand Up @@ -351,7 +352,7 @@ private static Void rangeCheck(char[] value, int offset, int count) {
*/
@SideEffectFree
@StaticallyExecutable
public String(int @GuardSatisfied [] codePoints, @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int count) {
public @Unique String(int @GuardSatisfied [] codePoints, @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int count) {
checkBoundsOffCount(offset, count, codePoints.length);
if (count == 0) {
this.value = "".value;
Expand Down Expand Up @@ -413,7 +414,7 @@ public String(int @GuardSatisfied [] codePoints, @IndexOrHigh({"#1"}) int offset
@SideEffectFree
@StaticallyExecutable
@Deprecated(since="1.1")
public String(byte ascii @GuardSatisfied [], int hibyte, @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int count) {
public @Unique String(byte ascii @GuardSatisfied [], int hibyte, @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int count) {
checkBoundsOffCount(offset, count, ascii.length);
if (count == 0) {
this.value = "".value;
Expand Down Expand Up @@ -467,7 +468,7 @@ public String(byte ascii @GuardSatisfied [], int hibyte, @IndexOrHigh({"#1"}) in
@SideEffectFree
@StaticallyExecutable
@Deprecated(since="1.1")
public String(byte ascii @GuardSatisfied [], int hibyte) {
public @Unique String(byte ascii @GuardSatisfied [], int hibyte) {
this(ascii, hibyte, 0, ascii.length);
}

Expand Down Expand Up @@ -506,7 +507,7 @@ public String(byte ascii @GuardSatisfied [], int hibyte) {
*/
@SideEffectFree
@StaticallyExecutable
public String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int length, String charsetName)
public @Unique String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int length, String charsetName)
throws UnsupportedEncodingException {
if (charsetName == null)
throw new NullPointerException("charsetName");
Expand Down Expand Up @@ -549,7 +550,7 @@ public String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) in
*/
@SideEffectFree
@StaticallyExecutable
public String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int length, Charset charset) {
public @Unique String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int length, Charset charset) {
if (charset == null)
throw new NullPointerException("charset");
checkBoundsOffCount(offset, length, bytes.length);
Expand Down Expand Up @@ -584,7 +585,7 @@ public String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) in
*/
@SideEffectFree
@StaticallyExecutable
public String(@PolySigned byte bytes @GuardSatisfied [], String charsetName)
public @Unique String(@PolySigned byte bytes @GuardSatisfied [], String charsetName)
throws UnsupportedEncodingException {
this(bytes, 0, bytes.length, charsetName);
}
Expand All @@ -611,7 +612,7 @@ public String(@PolySigned byte bytes @GuardSatisfied [], String charsetName)
*/
@SideEffectFree
@StaticallyExecutable
public String(@PolySigned byte bytes @GuardSatisfied [], Charset charset) {
public @Unique String(@PolySigned byte bytes @GuardSatisfied [], Charset charset) {
this(bytes, 0, bytes.length, charset);
}

Expand Down Expand Up @@ -643,7 +644,7 @@ public String(@PolySigned byte bytes @GuardSatisfied [], Charset charset) {
*/
@SideEffectFree
@StaticallyExecutable
public String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int length) {
public @Unique String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) int offset, @LTLengthOf(value={"#1"}, offset={"#2 - 1"}) @NonNegative int length) {
checkBoundsOffCount(offset, length, bytes.length);
StringCoding.Result ret = StringCoding.decode(bytes, offset, length);
this.value = ret.value;
Expand All @@ -668,7 +669,7 @@ public String(@PolySigned byte bytes @GuardSatisfied [], @IndexOrHigh({"#1"}) in
*/
@SideEffectFree
@StaticallyExecutable
public String(@PolySigned byte @GuardSatisfied [] bytes) {
public @Unique String(@PolySigned byte @GuardSatisfied [] bytes) {
this(bytes, 0, bytes.length);
}

Expand All @@ -683,7 +684,7 @@ public String(@PolySigned byte @GuardSatisfied [] bytes) {
*/
@SideEffectFree
@StaticallyExecutable
public String(@GuardSatisfied StringBuffer buffer) {
public @Unique String(@GuardSatisfied StringBuffer buffer) {
this(buffer.toString());
}

Expand All @@ -704,7 +705,7 @@ public String(@GuardSatisfied StringBuffer buffer) {
*/
@SideEffectFree
@StaticallyExecutable
public String(@GuardSatisfied StringBuilder builder) {
public @Unique String(@GuardSatisfied StringBuilder builder) {
this(builder, null);
}

Expand Down
41 changes: 22 additions & 19 deletions src/java.base/share/classes/java/lang/StringBuffer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,9 @@
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
import org.checkerframework.framework.qual.AnnotatedFor;
import org.checkerframework.common.aliasing.qual.Unique;
import org.checkerframework.common.aliasing.qual.LeakedToResult;
import org.checkerframework.common.aliasing.qual.NonLeaked;

import java.util.Arrays;
import jdk.internal.HotSpotIntrinsicCandidate;
Expand Down Expand Up @@ -112,7 +115,7 @@
* @see java.lang.String
* @since 1.0
*/
@AnnotatedFor({"lock", "nullness", "index"})
@AnnotatedFor({"aliasing", "lock", "nullness", "index"})
public final class StringBuffer
extends AbstractStringBuilder
implements java.io.Serializable, Comparable<StringBuffer>, CharSequence
Expand All @@ -132,7 +135,7 @@ public final class StringBuffer
* initial capacity of 16 characters.
*/
@HotSpotIntrinsicCandidate
public StringBuffer() {
public @Unique StringBuffer() {
super(16);
}

Expand All @@ -145,7 +148,7 @@ public StringBuffer() {
* argument is less than {@code 0}.
*/
@HotSpotIntrinsicCandidate
public StringBuffer(@NonNegative int capacity) {
public @Unique StringBuffer(@NonNegative int capacity) {
super(capacity);
}

Expand All @@ -157,7 +160,7 @@ public StringBuffer(@NonNegative int capacity) {
* @param str the initial contents of the buffer.
*/
@HotSpotIntrinsicCandidate
public StringBuffer(String str) {
public @Unique StringBuffer(String str) {
super(str.length() + 16);
append(str);
}
Expand All @@ -175,7 +178,7 @@ public StringBuffer(String str) {
* @param seq the sequence to copy.
* @since 1.5
*/
public StringBuffer(CharSequence seq) {
public @Unique StringBuffer(CharSequence seq) {
this(seq.length() + 16);
append(seq);
}
Expand Down Expand Up @@ -310,15 +313,15 @@ public synchronized void setCharAt(int index, char ch) {
}

@Override
public synchronized StringBuffer append(@Nullable Object obj) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked @Nullable Object obj) {
toStringCache = null;
super.append(String.valueOf(obj));
return this;
}

@Override
@HotSpotIntrinsicCandidate
public synchronized StringBuffer append(@Nullable String str) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked @Nullable String str) {
toStringCache = null;
super.append(str);
return this;
Expand Down Expand Up @@ -348,7 +351,7 @@ public synchronized StringBuffer append(@Nullable String str) {
* @return a reference to this object.
* @since 1.4
*/
public synchronized StringBuffer append(@Nullable StringBuffer sb) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked @Nullable StringBuffer sb) {
toStringCache = null;
super.append(sb);
return this;
Expand All @@ -358,7 +361,7 @@ public synchronized StringBuffer append(@Nullable StringBuffer sb) {
* @since 1.8
*/
@Override
synchronized StringBuffer append(AbstractStringBuilder asb) {
synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked AbstractStringBuilder asb) {
toStringCache = null;
super.append(asb);
return this;
Expand Down Expand Up @@ -386,7 +389,7 @@ synchronized StringBuffer append(AbstractStringBuilder asb) {
* @since 1.5
*/
@Override
public synchronized StringBuffer append(@Nullable CharSequence s) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked @Nullable CharSequence s) {
toStringCache = null;
super.append(s);
return this;
Expand All @@ -397,15 +400,15 @@ public synchronized StringBuffer append(@Nullable CharSequence s) {
* @since 1.5
*/
@Override
public synchronized StringBuffer append(@Nullable CharSequence s, @IndexOrHigh({"#1"}) int start, @IndexOrHigh({"#1"}) int end)
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked @Nullable CharSequence s, @IndexOrHigh({"#1"}) int start, @IndexOrHigh({"#1"}) int end)
{
toStringCache = null;
super.append(s, start, end);
return this;
}

@Override
public synchronized StringBuffer append(char[] str) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked char[] str) {
toStringCache = null;
super.append(str);
return this;
Expand All @@ -415,30 +418,30 @@ public synchronized StringBuffer append(char[] str) {
* @throws IndexOutOfBoundsException {@inheritDoc}
*/
@Override
public synchronized StringBuffer append(char[] str, @IndexOrHigh({"#1"}) int offset, @IndexOrHigh({"#1"}) int len) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked char[] str, @IndexOrHigh({"#1"}) int offset, @IndexOrHigh({"#1"}) int len) {
toStringCache = null;
super.append(str, offset, len);
return this;
}

@Override
public synchronized StringBuffer append(boolean b) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked boolean b) {
toStringCache = null;
super.append(b);
return this;
}

@Override
@HotSpotIntrinsicCandidate
public synchronized StringBuffer append(char c) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked char c) {
toStringCache = null;
super.append(c);
return this;
}

@Override
@HotSpotIntrinsicCandidate
public synchronized StringBuffer append(int i) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked int i) {
toStringCache = null;
super.append(i);
return this;
Expand All @@ -455,21 +458,21 @@ public synchronized StringBuffer appendCodePoint(int codePoint) {
}

@Override
public synchronized StringBuffer append(long lng) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked long lng) {
toStringCache = null;
super.append(lng);
return this;
}

@Override
public synchronized StringBuffer append(float f) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked float f) {
toStringCache = null;
super.append(f);
return this;
}

@Override
public synchronized StringBuffer append(double d) {
public synchronized StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked double d) {
toStringCache = null;
super.append(d);
return this;
Expand Down