Notice that in the xa = true case, we have performed an unnecessary read of x.(1) before returning 0.

I think this is not as bad as it sounds. The read is not required to be completed until we actually need the data (in this case we don't), so, assuming a normal out-of-order processor, we only consume memory bandwidth, but do not block subsequent operations. We would only be limited once we hit either our maximum memory bandwidth, or the maximum number of reads we can track. (we could also end up using extra registers/stack space, but I think the user would expect that if they have very complex matches)

The "Bind mutable fields earlier" feels a little more principled -- we're examining a "snapshot" of the variables taken at the time the match scrutinee is evaluated. This means it's much easier to reason about the results -- no "Match_failure" is required, and we can ensure that we retain the full power of exhaustiveness analysis, allowing even strangely written code to prevent having additional exception paths.

I'll open a PR with the "bind mutable fields earlier" approach so that you can compare. (There is more to say about the comparison but I will quote your (informative!) post and reply there.)

Edit: done, see #12556.

@gasche : Thanks for the very detailed and useful context! Does the solution proposed here address the case of mutations only from explicit when guards, or also those possibly happening when (1) forcing lazy fields, or (2) boxing floats extracted from float record (or from "unboxed float arrays").

I find @smuenzel arguments convincing, esp. if we can measure that the overhead of unneeded read is only tiny. With the solution proposed in this PR, if I understand correctly, there is also a potential overhead if we need to read multiple times and add extra tests.

The solution proposed fixes one aspect of the Pattern Matching Bug without making assumptions on where the source of mutation comes from, it merely assumes that reading a mutable field several times may return different results. It thus works for guards, lazy patterns, allocations, or multicore races. (There remain bugs due to the "incorrect partiality information", which is orthogonal and will be the topic of subsequent PRs, that also work for all mutation sources.)

I find @smuenzel arguments convincing, esp. if we can measure that the overhead of unneeded read is only tiny. With the solution proposed in this PR, if I understand correctly, there is also a potential overhead if we need to read multiple times and add extra tests.

I don't necessarily disagree, but note that:

• I think that we will get un-needed mutable reads relatively often on records with mutable fields -- whenever at least one clause uses the field, and at least another clauses does not use it. (Caveat: the extra reads only occur if the mutable field is not the first field in the type declaration -- for first fields the generated code is the same as they are matched right away.) On the other hand, the duplicated reads occur relatively less often -- you have to have a "split" in the pattern matrices, which is less common.
• The duplicated reads are already present in the code currently generated, so (they may be slower than other approaches, and I also wonder about the code-size impact but) they don't cause a performance regression that I would need to worry about.
• The extra checks have a cost (probably more costly than the extra reads), but again they only occur when the same field is read across splits, which is relatively uncommon.

This being said, we may be splitting hairs here: the difference that we are talking about only concerns records with a mutable field that is not the first field (in particular, it does not make any difference for single-field records). Pattern matching on record with mutable fields is relatively rare. I had a hard time finding a relevant example in the OCaml compiler codebase -- there are many records with several mutable fields, but they are accessed by field instead of deconstructed by pattern-matching.

The only one example that I could locate is the following, which occurs in several <arch>/emit.mlp files:

  Reg.Set.iter
    (function
      | {typ = Val; loc = Reg r} ->
          live_offset := ((r lsl 1) + 1) :: !live_offset
      | {typ = Val; loc = Stack s} as reg ->
          live_offset := slot_offset env s (register_class reg) :: !live_offset
      | {typ = Addr} as r ->
          Misc.fatal_error ("bad GC root " ^ Reg.name r)
      | _ -> ()
    )
    live

Here loc is a mutable field, and the "strict bindings" strategy will read it in all cases, even in the typ = Addr case where it was not necessary. (Obviously on this example there is no problem as the Addr case is not supposed to ever happen.) There is a split in the pattern matrix, but the second matrix is just for the catch-all case, and it will not read loc again. On this example, the "strict bindings" strategy generates slightly worse code than today, but the "context erasure" strategy keeps the code unchanged.

(One should also keep in mind that the "context erasure" implementation is simpler.)

I asked Luc Maranget, who also has the gut feeling that the "erase more often" approach is the better choice. One point that he made is that useless bindings keep memory alive in bytecode, so binding "earlier" may increase the memory footprint. (Native code is unaffected as it uses a liveness analysis.)

@ncik-roberts here is how to confirm that the testcase you propose is unrelated to the present PR and belongs to the totality-information territory. In trunk, activate the debug output for lambda/matching.ml by changing let dbg = false into let dbg = true, and then compile your testcase. I used the following command-line myself:

./runtime/ocamlrun ./ocamlc -nostdlib -I stdlib -dsource -dlambda -dno-locations test_nick.ml -stop-after lambda 2>&1 | less

There is a fair amount of output and it is not easy to work one's way inside it. But here are the relevant parts:

COMPILE:
  SPLIT
    false _ 
    _ {contents=None} 
    _ _ 
    true {contents=Some y} 
  INTO:
    First matrix:
      PM:
        false _ 
    Default matrix 2:
      PM:
        _ {contents=None} 
        _ _ 
    Default matrix 1:
      PM:
        true {contents=Some y} 

The testcase will be split into three matrices, one of the first line, one for the second and third line, one for the fourth line.

    COMPILE:
      MATCH Partial
      PM:
        None 
      Default environment:
        Matrix for 3:
          <_> 
        Matrix for 1:
          <Some y> 
      CTX:
        LEFT <{ _ }> <true> <{ _ }> RIGHT <_> 
      COMPILE:
        empty matrix
        COMBINE (mk_failaction_pos Partial)
          Default environment:
            Matrix for 3:
              <_> 
            Matrix for 1:
              <Some y> 
          FAIL PATTERNS:
            Some _
          POSITIVE JUMPS:
            jump for 3
            LEFT <{ _ }> <true> <{ _ }> RIGHT <Some _> 
      JUMPS:
        jump for 3
        LEFT <{ _ }> <true> <{ _ }> RIGHT <Some _> 
    JUMPS:
      jump for 3
      LEFT <true> <{ _ }> RIGHT <{ _ }> 

This is the match on the None constructor in the { contents = None } part. That match contains a sub-match on the empty matrix where mk_failaction_pos will compute (erroneous) context information RIGHT <Some _> for the failure case ("jump for 3"). This erroneous information is repeated in the first JUMPS block corresponding to the jump summary for the compilation of the empty matrix. But then the second JUMPS block at the end of the quote, with one less level of indentation, correspond to the { contents = None } jump summary, and it has RIGHT <{ _ }>. I believe that what we are seeing here is set_args_erase_mutable in action: as the context moves up, some information is erased (even today in trunk) on mutable fields, and at this point the context information is not incorrect anymore.

But then, later in the output we have:

    COMPILE:
      MATCH Total
      PM:
        Some y 
      CTX:
        LEFT <{ _ }> <true> <{ _ }> RIGHT <_> 
      COMPILE:
        MATCH Total
        PM:
          _ 
        CTX:
          LEFT <Some _> <{ _ }> <true> <{ _ }> RIGHT <_> 
        COMPILE:
          empty matrix
        NO JUMPS
        COMBINE (mk_failaction_pos Total)
          Default environment:
            empty
          FAIL PATTERNS:
            None
          POSITIVE JUMPS:
            empty
      NO JUMPS

This is the compilation of the Some y submatrix that is responsible for the segfault in your example -- it generates a direct access to the field, convinced that only the Some constructor is possible here, when the input is in fact None. The bug here is that mk_failaction_pos found a "fail pattern" None as it should (an input that is not matched in this switch), but decided to ignore this fail pattern due to the default environment being empty, and so computed no positive jumps (Positive jumps: empty; No jumps) to a failure case. (The default environment is empty because this matching is erroneously believed to be Total, but the relation between those two things is decided much earlier in the caller.)

The bulk of the code to fix this issue is in the matching-bug-final-exit branch mentioned in the overview comment, specifically gasche@f2044ed#diff-059d6544bdc63e5f278818ea9f50bef7aa3f855c4d5ce6fd726abee18b187f55R2813 (but that change is against the current-in-trunk version of mk_failaction_pos, so it would be more pleasant to review, I hope, after we manage to merge #12534 .)

On performance: Users might reasonably be concerned that this change will slow down existing pattern matches that involve mutable fields. Some light experimentation shows that indeed some extra switches are inserted. Do you have a sense of how big of an effect this change should have? (Or some characterization of the class of programs affected?)

A program generates different code under this PR when several matches on a given mutable position of the scrutinee occur across several split submatrices in the matching problem, and we need to reason about the former matches to convince ourselves that some of the later matches are exhaustive -- that at this point we have covered all cases.

(I don't know how to give an intuition for how matrices are split without going in the details of how pattern-matching compilation work, so this is not a proper language-level specification.)

My personal intuition is two-fold:

1. These cases where code is pessimized are going to be very rare.
2. The code we currently generate for these cases is unsound for OCaml 5 anyway, as they are always cases where a race on the mutable position could invalidate the assumption currently made by the code generator.

(Some other changes down in the tree of branches have a larger potential for performance regression on real-world program, I suspect, because they degrade totality information which is used to generate good code for GADTs in particular.)

These cases where code is pessimized are going to be very rare.

Some experimentation on a large code base appears to agree with this claim for the present PR.

Thanks!

To summarize my understanding:

• After reviewing the change carefully, @ncik-roberts was wondering if this PR missed some "bad cases". After discussion, we agree that the bad cases he had in mind are outside the scope of this PR, and are fixed by a following planned change (no PR submitted yet, but the code is in my branches).
• @ncik-roberts was wondering about the performance impact, and confirms my intuition that very little real-world code is affected by the change -- he did not find any instance when experimenting with the PR on internal codebases.

Now that @ncik-roberts has approved the PR, I wonder if a maintainer would be willing to approve as well, either by doing their own review or by approving on @ncik-roberts' behalf. (Maybe @Octachron or @lthls would be interested?) I would be interested in having a maintainer look at this relatively quickly, so that I can submit follow-up PRs as soon as possible and strike while the iron is hot.

Thanks! I now have to rebase, merge, and send a follow-up PR.