Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
@bollu and I also ran into the double reset bug a while ago (sorry for not reporting this earlier -- we didn't have a good MWE and put it off at first). However, we fixed it slightly differently: The reference counting can still be sound if there are two reset instructions on the same variable, but then an
inc
has to be generated before the firstreset
.The underlying reason for the bug is thus that Figure 5 of https://pp.ipd.kit.edu/uploads/publikationen/ullrich19counting.pdf has a wrong
reset
case, where theO^+
function is not called onreset
s, even though the variable to be reset should be owned (compare to theTy-Reset
rule of https://lean-lang.org/papers/beans_appendix.pdf). In contrast, Koka used to callO^+
in this case before we switched to drop-guided reuse analysis.This PR fixes the issue by calling
O^+
onreset
. This might make the fix in #4028 easier to maintain since it prevents segfaults even if there are tworeset
instructions on the same variable.