-
Notifications
You must be signed in to change notification settings - Fork 3
Implements SideEffectsOnly checking. #216
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
base: master
Are you sure you want to change the base?
Conversation
mernst
left a comment
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'm not sure what this pull request is doing. Could you please clarify?
...k/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/Refined.java
Outdated
Show resolved
Hide resolved
.../java/org/checkerframework/framework/testchecker/sideeffectsonly/SideEffectsOnlyChecker.java
Outdated
Show resolved
Hide resolved
Added this check in the latest commit. |
mernst
left a comment
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.
Thanks for this code. I have a few questions and suggestions.
framework/src/main/java/org/checkerframework/common/basetype/messages.properties
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
| * For methods annotated with {@link SideEffectsOnly}, computes expressions that are side-effected | ||
| * but not permitted by the annotation. | ||
| */ | ||
| public class SideEffectsOnlyAnnoChecker { |
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'm curious why this is a brand-new class rather than a modification to the existing mutation checker.
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 am not aware of a mutation checker and couldn’t find it in the manual either. Could you please point me to that class?
Although I think the PurityChecker can be modified to add all the functionality in the SideEffectsOnlyAnnoChecker. Do you think that's more appropriate?
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.
By "mutation checker" I meant PurityChecker. I'm sorry for being sloppy in my terminology. Thank you for setting me straight. Yes, I was thinking that merging the functionality in one place (maybe controlled by a switch) would be shorter, easier to understand, and less prone to code drift, compared to the two separate implementations. At least, I think that is worth trying to see whether it works out.
Thank you!
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.
Thank you for the suggestions. I tried merging the two functionalities into PurityChecker but wasn’t successful because of the following reason:
SideEffectsOnlyAnnoChecker (a part of the Checker Framework repository) needs to import org.checkerframework.common.basetype.BaseTypeChecker, which is not visible in the dataflow project (dataflow project contains the PurityChecker). Is there any other way around this?
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java
Outdated
Show resolved
Hide resolved
|
Thanks for the feedback Mike. I just have one question regarding your comment about the mutation checker. |
This PR adds an annotation
@SideEffectsOnlyto the set of dataflow qualifiers. For a method with this annotation, dataflow analysis unrefines just those expressions that are specified as annotation values of@SideEffectsOnlyinstead of the more conservative alternative of unrefining all expressions.