Support unique classes (Fixes #3313) #3336

aditya3434 · 2020-05-28T17:32:19Z

The Aliasing Checker gives "unique.leaked" for local variables only when they are explicitly annotated. This is because of the calling of hasExplicitAnnotation() type method in AliasingVisitor.java, in the canbeLeaked() method. By annotating class Data with @unique, the local variables start as @MaybeAliased but eventually get refined to @unique, due to the upper bound. The class objects are unique but since they are not explicitly annotated, they bypass the canbeLeaked() method and don't report errors. Removing this explicit requirement fixes the issue, and gives the expected output without giving any side effects (under my testing).

This PR should be merged along with the annotated JDK pull request.
(typetools/jdk#57)

Fixes #3313.

…n-fix

This reverts commit fd536c4.

wmdietl · 2020-06-05T23:21:01Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

@@ -271,7 +271,13 @@ private boolean canBeLeaked(Tree exp) {
        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);
        boolean isMethodInvocation = exp.getKind() == Kind.METHOD_INVOCATION;
        boolean isNewClass = exp.getKind() == Kind.NEW_CLASS;
-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isArray = type.getUnderlyingType().getKind().toString().equalsIgnoreCase("array");


You should try to avoid operations on strings. Is there no TypeKind to compare against?

I have used your suggested logic in my latest commit. There is no need for array TypeKind comparison in the code.

wmdietl · 2020-06-05T23:21:50Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isArray = type.getUnderlyingType().getKind().toString().equalsIgnoreCase("array");
+        boolean isNull = exp.getKind() == Kind.NULL_LITERAL;
+        if (type.getUnderlyingType().toString().startsWith("java.lang") || isArray || isNull) {


What is the motivation for this special logic? You should explain the logic here or at least in the PR description.

Also, do add tests that cover such special logic, in at least a few important cases.

The main logic I was following that the Aliasing Checker doesn't check for explicit annotations for user defined classes. So only those classes that the user has specifically annotated as @unique would construct @unique classes. This would also prevent all trivial objects like strings, int, object, float, etc. from always becoming @unique (it is more convenient to explicitly annotate them).

However, I couldn't figure out how to make the AliasingVisitor check whether a class was user-defined or not. So, instead I listed classes and data types for which one would need explicit annotations. These included java.lang classes, arrays and null values. All this complicated conditions could be avoided if the Visitor could check for user-defined classes.

if (annotated class is user defined) {
return type.hasAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
}
else {
return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
}

Can you clarify what you mean with "user defined"?
Why should the handling of explicit annotations depend on whether the class is "user defined"?

In the stub file stubfile.astub in tests/aliasing, Object and String classes are annotated as @unique by default. So, if I don't check for explicit annotations for all classes, then, even trivial operations like string assignments give a "unique.leaked" error in the test cases.

// part of TypeRefinementTest.java in tests/aliasing
void rule1() {
String unique = new String();
isUnique(unique);
String notUnique = unique; // gives unique.leaked error even though @unique is never used
}

So I decided to limit this checking for "user-defined" classes (classes that are not part of any in-built java library, like java.lang or java.util). For example, in the code in the feature request #3313 (#3313), class Data and Demo are user-defined classes, and since Data is annotated as @unique, all its instances don't require explicit annotations to be unique as well.

We do not want different behavior for built-in classes and user-defined classes. The same logic should be applied to all source code, regardless of who wrote the code.

There is a difference between classes String and Data in these two examples.
In String the default constructor is annotated as returning a unique object. The class declaration is not annotated. Therefore, it is fine in the test case to have a non-unique String reference.
On the other hand class Data in this new test case is annotated as @Unique requiring that only @Unique references exist.
So your check should be for that difference between the two classes.

Also can you move the annotations from framework/tests/aliasing/stubfile.astub into typetools/jdk#52?

I have added a new method for the above requested logic. Now the code doesn't need to deal with the special cases of arrays, null and java.lang classes. I have used the getDeclAnnotations method to get the set of declared annotations of the class as a whole, and then searched for the unique annotation mirror in the set. The code now gives leaked errors without explicit annotations only when the class is annotated as @unique. Annotating just the constructor will allow non-unique object references.

wmdietl · 2020-06-05T23:23:42Z

framework/tests/aliasing/ExplicitAnnotationTest.java

+class Demo {
+    void check(Data p) { // p is @Unique Data Object
+        // :: error: (unique.leaked)
+        Data y = p; // @Unique p is leaked


Is the type of the left-hand side important? Can you add another method that does

Object check2(Data p) { return p; }

which I guess should also give a unique.leaked error.

No, the type of the left-hand side isn't important. However, the method doesn't give an error, even when Data is explicitly annotated as @unique.

I'm not sure how you mean this. Does Object z = p; not raise an error? Shouldn't it?

@Unique class Data { Object check2(Data p) { return p; } void check(Data p) { Object z = p; } }

In the code given above, Object z = p; does raise an error. Hence, the left hand side isn't important. However, the check2 function (where you are returning a @unique Data as an Object) doesn't raise an error both in the typetools/master and in my modified code, even if the Data p is explicitly annotated as @unique Data p.

Ok, can you expand this test case with the Object local variable and the expected error.
Then file an issue that shows the problem with the return version.

…tya3434/checker-framework into 3313-explicit-annotation-fix

This reverts commit fd536c4.

wmdietl · 2020-06-15T20:46:37Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

@@ -271,7 +271,13 @@ private boolean canBeLeaked(Tree exp) {
        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);
        boolean isMethodInvocation = exp.getKind() == Kind.METHOD_INVOCATION;
        boolean isNewClass = exp.getKind() == Kind.NEW_CLASS;
-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isArray = type.getUnderlyingType().getKind().toString().equalsIgnoreCase("array");


wmdietl · 2020-06-15T20:59:13Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isArray = type.getUnderlyingType().getKind().toString().equalsIgnoreCase("array");
+        boolean isNull = exp.getKind() == Kind.NULL_LITERAL;
+        if (type.getUnderlyingType().toString().startsWith("java.lang") || isArray || isNull) {


We do not want different behavior for built-in classes and user-defined classes. The same logic should be applied to all source code, regardless of who wrote the code.

There is a difference between classes String and Data in these two examples.
In String the default constructor is annotated as returning a unique object. The class declaration is not annotated. Therefore, it is fine in the test case to have a non-unique String reference.
On the other hand class Data in this new test case is annotated as @Unique requiring that only @Unique references exist.
So your check should be for that difference between the two classes.

Also can you move the annotations from framework/tests/aliasing/stubfile.astub into typetools/jdk#52?

wmdietl · 2020-06-15T20:59:31Z

framework/tests/aliasing/ExplicitAnnotationTest.java

+class Demo {
+    void check(Data p) { // p is @Unique Data Object
+        // :: error: (unique.leaked)
+        Data y = p; // @Unique p is leaked


This reverts commit fd536c4.

wmdietl · 2020-06-25T13:17:00Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

-import com.sun.source.tree.NewArrayTree;
-import com.sun.source.tree.ThrowTree;
-import com.sun.source.tree.Tree;
+import com.sun.source.tree.*;


Do not star import.

Instead of star import, I listed the library data types that were required in my latest commit

wmdietl · 2020-06-25T13:51:47Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

+     * @return boolean true if class if unique and false otherwise
+     */
+    private boolean isUniqueClass(Tree exp) {
+        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);


The caller already computed type and you don't seem to use exp in this method. So why not just pass the type as parameter?

I replaced exp with type as an argument in the isUniqueClass in my latest commit

wmdietl · 2020-06-25T14:08:11Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

+    private boolean isUniqueClass(Tree exp) {
+        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);
+        Element el = types.asElement(type.getUnderlyingType());
+        if (el != null) {


It might be easier as if (el == null) { return false; } and then the same for annoMirrors.

I have separated out el and annoMirrors checks instead of the nested if conditions. If either of them is null, the method returns false

wmdietl · 2020-06-25T14:14:04Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

+                    if (mirror.getAnnotationType()
+                            .asElement()
+                            .getSimpleName()
+                            .contentEquals("Unique")) {


Again, don't use Strings for things like this. Can you use AnnotationUtils.containsSameByClass https://github.com/typetools/checker-framework/blob/master/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java#L230 ? Then you don't need the for loop.

I have used the AnnotationUtils.containtsSameByClass method in my latest commit

wmdietl · 2020-06-25T14:16:11Z

framework/tests/aliasing/ExplicitAnnotationTest.java

+class Demo {
+    void check(Data p) { // p is @Unique Data Object
+        // :: error: (unique.leaked)
+        Data y = p; // @Unique p is leaked


I'm not sure how you mean this. Does Object z = p; not raise an error? Shouldn't it?

wmdietl · 2020-06-25T14:17:24Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isUniqueClassFlag = isUniqueClass(exp);
+        if (isUniqueClassFlag) {
+            return type.hasAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;


Why do you need the type.hasAnnotation again, if you already know that isUniqueClass?

Yes, I see that was a redundant check. I have not used it in my latest commits

wmdietl · 2020-06-25T14:17:44Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

@@ -271,7 +265,37 @@ private boolean canBeLeaked(Tree exp) {
        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);
        boolean isMethodInvocation = exp.getKind() == Kind.METHOD_INVOCATION;
        boolean isNewClass = exp.getKind() == Kind.NEW_CLASS;
-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isUniqueClassFlag = isUniqueClass(exp);


Remove the Flag part. Notice the style for the other is variables.

I have removed the flag part from the variable name in my latest commit

wmdietl · 2020-06-25T14:19:18Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

@@ -271,7 +265,37 @@ private boolean canBeLeaked(Tree exp) {
        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);
        boolean isMethodInvocation = exp.getKind() == Kind.METHOD_INVOCATION;
        boolean isNewClass = exp.getKind() == Kind.NEW_CLASS;
-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isUniqueClassFlag = isUniqueClass(exp);
+        if (isUniqueClassFlag) {


Could this just be return !isMethodInvocation && !isNewClass && (isUniqueClass || type.hasExplicitAnnotation(Unique.class));

Maybe extract the (isUniqueClass || type.hasExplicitAnnotation(Unique.class) into a separate local and document why that is the logic.

I have separated the (isUniqueClass || type.hasExplicitAnnotation(Unique.class) into a separate local variable and documented the logic.

wmdietl · 2020-06-25T14:20:49Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

@@ -271,7 +265,37 @@ private boolean canBeLeaked(Tree exp) {
        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);


You should also update the javadoc with the change in behavior.
Do you understand what canBeLeaked expresses? The documentation is rather unclear.

I have changed the documentation for the canBeLeaked method in my latest commit

smillst · 2020-06-30T17:19:46Z

@aditya3434 Is this ready to review again? If so, please remove your assignment and assign @wmdietl. Thanks!

aditya3434 · 2020-07-01T11:09:08Z

@aditya3434 Is this ready to review again? If so, please remove your assignment and assign @wmdietl. Thanks!

Thanks for the heads up! I have unassigned myself and assigned @wmdietl for the review.

wmdietl · 2020-07-20T13:56:33Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

-import javax.lang.model.element.ExecutableElement;
-import javax.lang.model.element.VariableElement;
+import java.util.Set;
+import javax.lang.model.element.*;


Do not use wildcard imports.

We had this before: #3336 (comment)
Look how to change your IDE configuration to not make such changes.

I have changed the import statement in my latest commit. Turns out my IDE automatically * imports whenever it imports more than 3 packages.

wmdietl · 2020-07-20T17:16:41Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

+    }
+
+    /**
+     * Returns true if class of annotated type {@code type} has annotation {@code @Unique}


The summary should end with a period.

Maybe use: Return true if the class declaration for annotated type ...

I have adjusted the summary in my latest commit

wmdietl · 2020-07-20T19:14:02Z

framework/src/main/java/org/checkerframework/common/aliasing/AliasingVisitor.java

     *
     * @param exp the Tree to check
     */
    private boolean canBeLeaked(Tree exp) {
        AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);
        boolean isMethodInvocation = exp.getKind() == Kind.METHOD_INVOCATION;
        boolean isNewClass = exp.getKind() == Kind.NEW_CLASS;
-        return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass;
+        boolean isUniqueType = (isUniqueClass(type) || type.hasExplicitAnnotation(Unique.class));


The outer parenthesis aren't necessary.

I have removed the parenthesis in my latest commit.

wmdietl · 2020-07-20T19:19:35Z

framework/tests/aliasing/ExplicitAnnotationTest.java

+class Demo {
+    void check(Data p) { // p is @Unique Data Object
+        // :: error: (unique.leaked)
+        Data y = p; // @Unique p is leaked


Ok, can you expand this test case with the Object local variable and the expected error.
Then file an issue that shows the problem with the return version.

aditya3434 · 2020-07-21T08:25:58Z

I have added the Object local variable error in the test case and have filed an issue with the return version.

Issue Link : #3486

wmdietl

Thanks, this looks good now!

aditya3434 added 3 commits May 28, 2020 12:00

Fix for feature request typetools#3313 in Aliasing Checker

fd536c4

Fix for explicit annotation check in Aliasing Checker

126014d

Adding test cases for removal of explicit annotation check

b2b91eb

smillst assigned wmdietl May 28, 2020

aditya3434 and others added 5 commits May 29, 2020 20:06

Ensuring all framework tests are passed

1b756c0

Formatting changes

4edfc68

Merge ../checker-framework-branch-master into 3313-explicit-annotatio…

dde03ef

…n-fix

Fix for feature request typetools#3313 in Aliasing Checker

22462e0

Revert "Fix for feature request typetools#3313 in Aliasing Checker"

017082b

This reverts commit fd536c4.

wmdietl requested changes Jun 5, 2020

View reviewed changes

wmdietl assigned aditya3434 and unassigned wmdietl Jun 5, 2020

aditya3434 added 4 commits June 6, 2020 16:12

Merge branch 'master' into 3313-explicit-annotation-fix

4b36609

Merge branch '3313-explicit-annotation-fix' of https://github.com/adi…

fa03246

…tya3434/checker-framework into 3313-explicit-annotation-fix

Fix for feature request typetools#3313 in Aliasing Checker

97ff12d

Revert "Fix for feature request typetools#3313 in Aliasing Checker"

629a1a9

This reverts commit fd536c4.

wmdietl requested changes Jun 15, 2020

View reviewed changes

smillst linked an issue Jun 15, 2020 that may be closed by this pull request

Feature request: @AlwaysUnique (?) to mark classes whose instances must always be @Unique #3313

Closed

aditya3434 added 11 commits June 16, 2020 17:19

Merge remote-tracking branch 'upstream/master'

25b602a

Merge branch 'master' into 3313-explicit-annotation-fix

91d8372

Fix for feature request typetools#3313 in Aliasing Checker

eb424fd

Revert "Fix for feature request typetools#3313 in Aliasing Checker"

c324094

This reverts commit fd536c4.

Fix for feature request typetools#3313 in Aliasing Checker

941cab0

Revert "Fix for feature request typetools#3313 in Aliasing Checker"

d71f608

This reverts commit fd536c4.

Merge remote-tracking branch 'upstream/master'

53a6c12

Merge branch 'master' into 3313-explicit-annotation-fix

ff1b9e4

Resolving review comments

135b266

Removing redundant variables

db149b9

Modifying documentation

e64f002

aditya3434 assigned wmdietl Jun 20, 2020

wmdietl requested changes Jun 25, 2020

View reviewed changes

wmdietl assigned aditya3434 and unassigned wmdietl Jun 25, 2020

aditya3434 added 5 commits June 27, 2020 21:04

Merge branch 'master' into 3313-explicit-annotation-fix

167d9cc

Making requested changes

cf45fd6

Modifying documentation

f3d2479

Deleting stubfile.astub

9b60d82

Removing stubfile.astub references

1335ba2

smillst mentioned this pull request Jun 30, 2020

Aliasing: test constructor declarations #3337

Merged

aditya3434 assigned wmdietl and unassigned aditya3434 Jul 1, 2020

aditya3434 added 5 commits July 11, 2020 14:58

Merge branch 'master' into 3313-explicit-annotation-fix

1da4103

Merge branch 'master' into 3313-explicit-annotation-fix

7b191e9

Merge branch 'master' into 3313-explicit-annotation-fix

bd1fe05

Merge branch 'master' into 3313-explicit-annotation-fix

37976e8

Merge branch 'master' into 3313-explicit-annotation-fix

1523897

wmdietl requested changes Jul 20, 2020

View reviewed changes

wmdietl assigned aditya3434 and unassigned wmdietl Jul 20, 2020

aditya3434 added 2 commits July 21, 2020 11:43

Merge branch 'master' into 3313-explicit-annotation-fix

79f35f1

Making requested changes

f6e67cc

aditya3434 assigned wmdietl and unassigned aditya3434 Jul 21, 2020

wmdietl changed the title ~~3313 explicit annotation fix~~ Support unique classes (Fixes #3313) Jul 21, 2020

wmdietl approved these changes Jul 21, 2020

View reviewed changes

wmdietl merged commit c44ded4 into typetools:master Jul 21, 2020

aditya3434 deleted the 3313-explicit-annotation-fix branch July 27, 2020 07:54

		@@ -271,7 +265,37 @@ private boolean canBeLeaked(Tree exp) {
		AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(exp);

Support unique classes (Fixes #3313) #3336

Support unique classes (Fixes #3313) #3336

Conversation

aditya3434 commented May 28, 2020 • edited by wmdietl

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aditya3434 Jun 6, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aditya3434 Jun 8, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aditya3434 Jun 20, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smillst commented Jun 30, 2020

aditya3434 commented Jul 1, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aditya3434 commented Jul 21, 2020

wmdietl left a comment

Choose a reason for hiding this comment

aditya3434 commented May 28, 2020 •

edited by wmdietl

aditya3434 Jun 6, 2020 •

edited

aditya3434 Jun 8, 2020 •

edited

aditya3434 Jun 20, 2020 •

edited