njit-jerse / specimin

SPECIfication MINimizer. A different kind of slicer for Java.
MIT License
3 stars 5 forks source link

Avoid crashing when encountering method references #290

Closed kelloggm closed 4 months ago

kelloggm commented 4 months ago

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.

LoiNguyenCS commented 4 months ago

I think we can probably solve this problem in a general way by writing code to handle that

I think the most challenging part is to handle the parameters. For example, given something like Person::compareByAge, it is difficult to know which parameters compareByAge should have. As far as I remember, I couldn't solve cf-3032 in the past due to this implicit parameters issue.

kelloggm commented 4 months ago

@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., https://github.com/javaparser/javaparser/issues/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.

LoiNguyenCS commented 4 months ago

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.

kelloggm commented 4 months ago

@LoiNguyenCS sorry I missed your comment on this PR last week.

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.

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.

LoiNguyenCS commented 4 months ago

However, the user also has an easy tool to check this: they can run javac on Specimin's output, and if it fails then they know that Specimin has failed.

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.

kelloggm commented 4 months ago

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.

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 JavaTypeCorrect finds any compilation errors. I would not be against adding a mode that always crashes rather than producing non-compilable output (actually, that's a very good idea!), but Specimin doesn't currently have one. By the principle of least surprise, I think it's better if Specimin's behavior when it gets the wrong answer is consistent (in this case, consistently "produce a non-compilable output") rather than inconsistent (sometimes produce non-compilable output, sometimes crash).

LoiNguyenCS commented 4 months ago

Thank you for the explanation. The principle of least surprise makes sense for me.