The Pattern-Matching Bug: remove check_partial#13153
Conversation
a4e732d to
ccdbcd2
Compare
ccdbcd2 to
8181ca4
Compare
ncik-roberts
left a comment
There was a problem hiding this comment.
I agree with the reasoning behind removing this old heuristic.
The testsuite output needs updating in light of this improvement. Compilation of this function in testsuite/tests/match-side-effects/check_partial.ml no longer produces a Match_failure case:
let lazy_total : _ * bool t -> int = function
| ({ contents = _ }, True) -> 0
| ({ contents = lazy () }, False) -> 12
(* This pattern-matching is in fact total: a Match_failure case is
not necessary for soundness. *)
8181ca4 to
04be000
Compare
|
I rebased this PR on top of the previous PR's rebase, and fixed the testsuite output, thanks! (Explanation for other people: the testsuite output recorded a case where no Match_failure case was necessary, but the compiler would conservatively insert one -- which is correct. Removing the check_partial heuristic (replacing it with the finer-grained checks in The Pattern-Matching Bug PRs) makes the compiler more clever about this case, and now there is no Match_failure case anymore. This is a small improvement, and/but both the previous and current test output are correct.) |
(no behavior change)
… default This un-does a small pessimization of ocaml#13076, which was analyzed in details in ocaml#13076 (comment), but at the time was believed to not affect any program in the wild. Since then Nick Roberts found instances of this pattern involving or-patterns and polymorphic variants. Thanks to the new presentation of partiality information that distingues the "global" and "current" information, the pessimization is now easy to undo, as done in this commit.
04be000 to
f965fcb
Compare
The [check_partial] heuristics are a coarse-grained approach degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns. It is not quite correct (it is not enough to prevent ocaml#7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects. This heuristic is subsumed by the recent changes to: - make context information accurate by binding mutable fields eagerly - make totality information accurate by tracking the mutability of the current position and can now be retired. Note: the [check_partial] function also contained hidden logic to deal with the pattern-matching programs with no cases at all (more precisely, those that have only refutation cases, like `function _ -> .`), we retain this logic and move it to `toplevel_handler`.
f965fcb to
a906f5a
Compare
lpw25
left a comment
There was a problem hiding this comment.
Approving on the basis of @ncik-roberts review
|
Thanks! I clicked "merge" without rebasing the PR (despite the PR being on an older branch than "trunk", it includes some commits that were not in trunk at submission time and have since been merged exactly as-is). Usually I would rebase first, check the CI results, and then merge. It looks like this is working fine -- the CI is being re-run on trunk after the merge, but I think it does this for all merges, even those that do not include commits already in trunk. |
(This PR sits on top of #13152, and is thus best review by looking at the last commit only.)
This is a non-obvious code simplification PR after #7241 is fixed. Before #7241 was reported and worked on, there already was a heuristic named
check_partialto degrade pattern-matching compilation in some cases involving side-effects during matching. Now that #7241 is fixed by other changes in the pattern-matching compiler, the heuristic is not necessary anymore and complicates the code, it can be removed.The testsuite
testsuite/tests/match-side-effects/check_partialwas introduced in #13121 to test various cases where thecheck_partialheuristic would fire. The code generated for these tests is not modified by the present PR, demonstrating that, on those tests, removingcheck_partialdoes not change the compiler behavior.Details
The
check_partialheuristics was a coarse-grained approach to degrade matching totality information in certain cases -- when clauses contain both reads of mutable fields and either guards or forcing of lazy patterns.This heuristic is unfortunately not quite correct (it is not enough to prevent #7241), and is not sufficient conceptually for OCaml Multicore. In a Multicore world, other domains may race to update values concurrently, so we cannot assume that only a fixed set of matching constructions may result in side-effects.