Skip to content
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

value letrec: fix a bug in analysis of inner mutually-recursive bindings #2244

Merged
merged 1 commit into from Mar 1, 2019

Conversation

Projects
None yet
4 participants
@gasche
Copy link
Member

commented Feb 11, 2019

On Friday I found a bug in my own proof of correctness of the recursive-value-declarations analysis of #1942, and @yallop swiftly turned it into a example that crashes 4.08+dev. The present PR (explains and) fixes the issue in the same way that I fixed the type system and the proof.

The issue is in the handling of inner let rec bindings with mutual recursion going on (single-definitions let rec are fine). Read the comments and testsuite entries for the details. There are two potential fixes, a fixpoint (precise/complete, slightly more complex to implement), and an overapproximation (rejects safe programs, shorter to implement). The paper, the new proof and this PR use the fixpoint approach.

The new unsafe program in the testsuite is rejected in 4.07.1, which still uses @yallop's pre-#1942 implementation, which is more conservative -- it is equivalent to the "overapproximation" mentioned above. On the other hand, the new safe program in the testsuite was rejected in 4.07.1, because the overapproximation is too conservative there -- maybe it's okay.

We should have a fix for this issue in 4.08.

@gasche gasche force-pushed the gasche:mutual-rec-fix branch from 339ee28 to 23fc88d Feb 11, 2019

@gasche

This comment has been minimized.

Copy link
Member Author

commented Feb 24, 2019

@yallop: would you be able to review this PR in the next few weeks?

@yallop

This comment has been minimized.

Copy link
Member

commented Feb 25, 2019

@gasche: I think it's quite unlikely.

@gasche

This comment has been minimized.

Copy link
Member Author

commented Feb 25, 2019

Thanks; I'll try to find another victim.

@Armael
Copy link
Member

left a comment

A couple typos.

Show resolved Hide resolved typing/rec_check.ml Outdated
Show resolved Hide resolved typing/rec_check.ml Outdated

@gasche gasche force-pushed the gasche:mutual-rec-fix branch 2 times, most recently from c41dcc2 to cc60d17 Feb 28, 2019

@gasche

This comment has been minimized.

Copy link
Member Author

commented Feb 28, 2019

@Armael and @damiendoligez agreed to review the PR. I just fixed a couple of typos spotted by @Armael, and implemented a different, hopefully less-confusing naming schemes for multi-index families of modes.

@damiendoligez
Copy link
Member

left a comment

After getting a white-board explanation of the bug and the fix from @gasche, I had a good look at the code and I believe this patch is correct.
P.S. the new naming scheme is indeed much better.

Show resolved Hide resolved typing/rec_check.ml Outdated

@gasche gasche force-pushed the gasche:mutual-rec-fix branch 3 times, most recently from 27e902c to 1e4d40b Mar 1, 2019

@gasche

This comment has been minimized.

Copy link
Member Author

commented Mar 1, 2019

Thanks to the reviews of @Armael and @damiendoligez, I will merge and cherry-pick in 4.08 once the CI turns green again.

@gasche gasche force-pushed the gasche:mutual-rec-fix branch from 1e4d40b to 56c6786 Mar 1, 2019

value letrec: fix a bug in analysis of inner mutually-recursive bindings
Jeremy Yallop and myself found this bug while trying to prove the
soudness of the analysis.

@gasche gasche merged commit f785be3 into ocaml:trunk Mar 1, 2019

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

gasche added a commit that referenced this pull request Mar 1, 2019

Merge pull request #2244 from gasche/mutual-rec-fix
value letrec: fix a bug in analysis of inner mutually-recursive bindings

(cherry picked from commit f785be3)
@gasche

This comment has been minimized.

Copy link
Member Author

commented Mar 1, 2019

Cherry-picked as 8d7d758.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.