-
Notifications
You must be signed in to change notification settings - Fork 7
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
Avoid crashing when encountering method references #290
Conversation
…t the proximate cause of the crash
…oblem: method references don't tell you what their arity is the way that lambdas do...
I think the most challenging part is to handle the parameters. For example, given something like |
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.
There is a part of codes that I think we can omit.
src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
Outdated
Show resolved
Hide resolved
@LoiNguyenCS can you take another look at this? This change is really unsatisfying but it does avoid the crash in #154 (even though it definitely gets the wrong answer). Because the expected output doesn't compile, I tried several approaches to change the expected output to something that would compile, but I couldn't get Specimin to reliably produce the right output using any strategy. The key problem appears to be that Java Parser doesn't really support resolution of method references in many contexts, e.g., javaparser/javaparser#4188 (and similar bugs - Java Parser has a bunch of open issues related to method references). I suspect we'll never be able to handle method references properly using the current design of Specimin unless we:
Both of those are infeasible right now, so I'm ok with settling for producing non-compilable output but avoiding the crash in Specimin. |
Professor, would it be better to throw an exception whenever a method reference is found within a target member? We could include an error message like: "Please check back later for the next version of Specimin." Hopefully, JavaParser will resolve this issue in its upcoming release. I think this approach is better than returning an incorrect result. |
@LoiNguyenCS sorry I missed your comment on this PR last week.
Your point is a good one. This is a question of priorities: when we encounter some code that we know that Specimin won't be able to handle properly, different situations/users of Specimin demand different behaviors:
Both of these cases are legitimate, and you're right that this PR supports the second over the first. |
I am still a bit confused about our choice here. Isn't software supposed to be correct? I mean, it is true that softwares usually have some bugs, but it seems counter-intuitive to intentionally write a software that return the wrong answers. For the case of ASHE, what if the owner of ASHE writes some scripts that skip projects which can not be minimized by Specimin? It seems to be a better choice than we as the owners of Specimin intentionally let Specimin return the wrong result. |
Software is supposed to be correct, but absent a proof it usually isn't. In my experience, good engineering means accepting that and planning for it rather than trying to get everything perfect. Of course, if you can instead write a proof of correctness, that works too :) In cases like this one, though, the question is not "is the software correct?" - we know for certain that it isn't. The question is, "when the software encounters something that we know will cause it to get the wrong answer, what should we do?". I am advocating for an approximate answer: we try to do the best that we can, even if it isn't always quite correct. You are advocating for crashing rather than producing an approximate answer when we encounter a situation where we know the answer will be approximate. As I said before, both positions are legitimate, and reasonable people can disagree about which they'd prefer. I prefer the former because Specimin already behaves that way, most of the time: after all, we don't crash if the last run of |
Thank you for the explanation. The principle of least surprise makes sense for me. |
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.
LGTM
Fixes the proximate cause of #154. However, this fix is extremely incomplete. I'll open a separate issue detailing all of the problems that I've found with how we handle method references if we decide to merge this PR.
At a high-level, the problem is that a method reference that's not solvable is basically equivalent to a lambda, but unlike a lambda it doesn't come with an arity. So, we have no way to decide what the type should be. In this PR, I arbitrarily chose
java.util.Supplier<?>
, which is correct for the example here (and prevents crashes), but will cause the output not to be compilable if the method reference has a different arity.I also manually confirmed that if I change the arity, we do have the ability to detect the problem in JavaTypeCorrect (we get a
incompatible types: invalid method reference
error). I think we can probably solve this problem in a general way by writing code to handle that, but I don't have time today to do that, and this partial fix prevents the crash, so I decided that this was worth PR'ing separately.