Segmentation fault on non-exhaustive pattern-matching in let rec

[lupjo]

The following code causes a segmentation fault when compiled in bytecode (not in native):

let rec f =
	let [| f0 |] = [| 0 |] in
	function
	| 0 -> f0
	| n -> f (n - 1)

let _ = f 1

Even weirder, the issue still stands when replacing the code by this:

let rec f =
	let 0 = 0 in
	function
	| 0 -> 0
	| n -> f (n - 1)

let _ = f 1

It seems the conjunction of a non-exhaustive pattern-matching and a let rec doesn't work very well. To be fair, the manual only describes the case let rec f = let x = _ in _, and not the case where x is replaced by a pattern, but it seems that replacing it by any exhaustive non-constructor pattern (tuples, records, polymorphic variant, lazy) causes no such issue.

[lthls]

Good catch! The issue is that the following definition is forbidden, and rejected by the type-checker (more specifically, Rec_check):

let rec f =
  if 0 = 0 then
    function
    | 0 -> 0
    | n -> f (n - 1)
  else assert false

The versions with partial matches are compiled to something equivalent, but the conditional is only introduced later in the pipeline, so Rec_check accepts the definition. Then, the parts of the compiler that are actually compiling recursive definitions do see a conditional, assume that it must not be a real recursive definition otherwise Rec_check would have complained, and generate wrong code.
Here is a slightly modified example that will fail also with the native backend:

let rec f =
	let 0 = Sys.opaque_identity 0 in
	function
	| 0 -> 0
	| n -> f (n - 1)

let _ = f 1

I don't know of any easy way to fix this, but maybe @gasche will have some ideas.

[gasche]

It took me a bit of time to understand that the problem was not in the tying-the-knot operational semantics itself (which should work perfectly fine on both examples), but in the fact that our code-generation strategy uses the notion of statically-known vs. dynamically-known size, and in the case of code introducing conditionals makes incorrect assumptions. This was mentioned in @lthls analysis, but I needed to compare the two following outputs to understand the issue.

$ cat good.ml
let rec good =
  let x = Sys.opaque_identity 0 in
  function
  | 0 -> 0
  | n -> good (n - 1)

$ ocamlopt -dno-locations -dno-unique-ids -dcmm -c good.ml 2>&1 | grep __entry -A 100
(function camlGood__entry ()
 (let good (extcall "caml_alloc_dummy" 7 ->val)
   (extcall "caml_update_dummy" good
     (let x (opaque 1)
       (alloc 3319 "camlGood__fun_345" 72057594037927941 good))
     ->unit)
   (extcall "caml_initialize" "camlGood" good ->unit))
 1)

$ cat bad.ml
let rec bad =
  let 0 = Sys.opaque_identity 0 in
  function
  | 0 -> 0
  | n -> bad (n - 1)

$ ocamlopt -dno-locations -dno-unique-ids -dcmm -c bad.ml 2>&1 | grep __entry -A 100
(function camlBad__entry ()
 (let
   (bad 1
    bad
      (let *match* (opaque 1)
        (if (!= *match* 1)
          (raise_notrace (alloc 2048 "caml_exn_Match_failure" "camlBad__2"))
          (alloc 3319 "camlBad__fun_346" 72057594037927941 bad))))
   (extcall "caml_initialize" "camlBad" bad ->unit))
 1)

The problem with bad is that the caml_alloc_dummy call is gone.

[gasche]

I think that a possible fix would be to teach the size-computation logic to work through conditionals when either both sides have the same size, or one does not return.

Note: we could have a check in the compiler that the main Rec_check information, which computes how recursive values depend on each other, agrees with the "size analysis" information, which is separate (and not the part that I have worked on). The bug arises because they make assumptions about each other that are not checked by anyone. If we had a check, we would have failed at compile-time instead of generating incorrect code.

[gasche]

This particular issue should be fixed by #12059.