The Pattern-Matching Bug: introduce a temporality heuristic to de-pessimize certain programs#13154
Conversation
4dbadd4 to
a3020d5
Compare
ncik-roberts
left a comment
There was a problem hiding this comment.
The approach looks correct. In a survey of a large codebase, I found only one instance where this PR de-pessimizes a program -- I would consider arguing against this change if it significantly complicated the matching.ml code, but given that the change is clear and well-structured, I'm in favor of merging it.
|
One reason I like this heuristic is that it helps me reason about "structural matches" that do not contain splits -- all possible cases are explored in full. For example: function
| None -> 0
| Some {contents = A} -> 1
| Some {contents = B _} -> 2
| Some {contents = C _} -> 3(assuming the type-checker finds this example exhaustive: For this fragment of pattern-matching programs, the type-checker exhaustiveness analysis is always correct, and the temporality heuristic guarantees that we generate good code. |
d727011 to
47c16ae
Compare
|
Rebasing this on top of #13338 (transitively) made the implementation quite a bit less invasive, because I can add the temporality as an extra field to the |
73fef1d to
522abfb
Compare
| (opaque *match*/298)) | ||
| *match*/298))) | ||
| *match*/305 =o (field_mut 0 (field_imm 1 param/297))) | ||
| (if (isint *match*/305) (if *match*/305 12 (exit 3)) (exit 3))))) |
There was a problem hiding this comment.
I did not understand why this test case changed -- there was a Match_failure case before and there is still one after, so what did the temporality change in the code? This is much easier to see in the -drawlambda output for this test:
(setglobal Test!
(let
(lazy_needs_partial/274 =
(function param/276 : int
(catch
(let (*match*/279 =a (field_imm 0 param/276))
(catch
(let
(*match*/280 =a (field_imm 1 param/276)
*match*/281 =o (field_mut 0 *match*/280))
- (if (isint *match*/281) (if *match*/281 (exit 2) 0)
- (exit 1)))
+ (switch* *match*/281 case int 0: 0
+ case int 1: (exit 2)))
with (2)
(let
(*match*/288 =
(let
(lzarg/282 = *match*/279
tag/283 =a (caml_obj_tag lzarg/282))
(if (== tag/283 250) (field_mut 0 lzarg/282)
(if (|| (== tag/283 246) (== tag/283 244))
(apply (field_imm 1 (global CamlinternalLazy!))
(opaque lzarg/282))
lzarg/282)))
*match*/289 =a (field_imm 1 param/276)
*match*/290 =o (field_mut 0 *match*/289))
(if (isint *match*/290) (if *match*/290 12 (exit 1))
(exit 1)))))
with (1)
(raise
(makeblock 0 (global Match_failure/20!) [0: "test.ml" 6 49])))))
(makeblock 0 lazy_needs_partial/274)))This is about the way that the check (_, {contents = True}) is compiled in the first clause. The GADT type declaration is as follows:
type _ t =
| Int : int -> int t
| True : bool t
| False : bool tBefore the compiled would do first an isint test to rule out Int, and then an if test to distinguish True from False. But with this commit, the compiler now trusts the totality information that tells it that the Int case is impossible, and generates a simpler check to differentiate True from False. (There is a similar check down below, after the lazy () pattern, and that ones is pessimized as it should.)
64e24b5 to
e5e2b95
Compare
lpw25
left a comment
There was a problem hiding this comment.
Approving on the basis of @ncik-roberts review
|
Thanks! The present PR sits on top of #13341, so I should wait for that PR to be merged before merging the present one. |
29a02bb to
9392e14
Compare
…DT+mutable combinations
9392e14 to
94a8158
Compare
|
This PR can be merged now that #13341 has been approved and merged. I am planning to do this after/if the CI passes. |
The Pattern-Matching Bug: introduce a temporality heuristic to de-pessimize certain programs (cherry picked from commit 9e72506)
(This PR sits on top of #13152 and #13153; for now it is best reviewed by looking only at the latest commit.)
#13152 pessimizes Total matches in transitively mutable position. It gives two examples of code that now generates worse code:
In the case A, the generated code first checks something about the argument root.0, then it checks a guard, then it goes back to the argument root.0. (We say that there are two "splits", resulting in three submatrices, that are checked in sequence.) When it goes back to root.0, its value could have changed in the meantime, so assuming that root.0.0 could only be
falseis wrong, and we really needed to make the code worse.In the case B, the generated code reads the mutable field root.0, then immediately checks all possible cases on this constructor. In this case there cannot have been any mutation "in the meantime", this is the first time ever that we are checking this value. So generating a
Match_failurecase here was not necessary, and we are generating worse code than we could.In general it is hard to know for sure "this is the first time we do something on this value". Tracking this precisely might be done with more context information, but it would be a tricky change with quickly diminishing returns. There is however a case where it is very easy to see that we are in this situation: where we have not generated any "split", any logic of the form "check this about the first value, and if that fails check that".
The present PR introduces a new piece of static context information used by the pattern-matching compiler to track this criterion. In code:
When deciding whether a switch on a given position should be pessimized, we now use a refined criterion: we are in a transitively mutable position and the current temporality is
Following, we have already accessed this position before.In particular, the example
gabove now produces good code again, as well as any reasonable usage of GADTs in mutable positions that I can think of.It is, of course, possible to build examples where the heuristic is too coarse-grained and which will generate worse code than they could. For example: