-
Notifications
You must be signed in to change notification settings - Fork 348
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.
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
Support unique classes (Fixes #3313) #3336
Changes from 6 commits
fd536c4
126014d
b2b91eb
1b756c0
4edfc68
dde03ef
22462e0
017082b
4b36609
fa03246
97ff12d
629a1a9
25b602a
91d8372
eb424fd
c324094
941cab0
d71f608
53a6c12
ff1b9e4
135b266
db149b9
e64f002
167d9cc
cf45fd6
f3d2479
9b60d82
1335ba2
1da4103
7b191e9
bd1fe05
37976e8
1523897
79f35f1
f6e67cc
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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"); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. You should try to avoid operations on strings. Is there no TypeKind to compare against? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ping. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I have used your suggested logic in my latest commit. There is no need for array TypeKind comparison in the code. |
||
boolean isNull = exp.getKind() == Kind.NULL_LITERAL; | ||
if (type.getUnderlyingType().toString().startsWith("java.lang") || isArray || isNull) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What is the motivation for this special logic? You should explain the logic here or at least in the PR description. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Also, do add tests that cover such special logic, in at least a few important cases. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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) { There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can you clarify what you mean with "user defined"? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 Also can you move the annotations from There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. |
||
return type.hasExplicitAnnotation(Unique.class) && !isMethodInvocation && !isNewClass; | ||
} else { | ||
return type.hasAnnotation(Unique.class) && !isMethodInvocation && !isNewClass; | ||
} | ||
} | ||
|
||
private boolean isInUniqueConstructor() { | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
import org.checkerframework.common.aliasing.qual.Unique; | ||
|
||
@Unique class Data { | ||
@SuppressWarnings("unique.leaked") | ||
Data() {} // All objects of Data are now @Unique | ||
} | ||
|
||
class Demo { | ||
void check(Data p) { // p is @Unique Data Object | ||
// :: error: (unique.leaked) | ||
Data y = p; // @Unique p is leaked | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is the type of the left-hand side important? Can you add another method that does
which I guess should also give a There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ping. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not sure how you mean this. Does There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
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. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ok, can you expand this test case with the |
||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You should also update the javadoc with the change in behavior.
Do you understand what
canBeLeaked
expresses? The documentation is rather unclear.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have changed the documentation for the canBeLeaked method in my latest commit