Fix a soundness bug in Simplif (#3832)

Ensure that Alias bindings are not substituted under lambda

This used to be the case, but the recent refactoring of Lletrec introduced a bug.
(Due to locals, this is a soundness issue rather than just poor optimisation)

Author: stedolan

lambda/lambda.mli

@@ -691,7 +691,8 @@ type let_kind = Strict | Alias | StrictOpt
       (If e is a simple expression, e.g. a variable or constant,
        we may still substitute e'[x/e].)
     Alias: e is pure, we can substitute e'[x/e] if x has 0 or 1 occurrences
-      in e'
+      in e', and these occurrences are definitely in the same region as
+      the binding (not inside a lambda nor an exclave)
     StrictOpt: e does not have side-effects, but depend on the store;
       we can discard e if x does not appear in e'
  *)

lambda/simplif.ml

@@ -465,8 +465,8 @@ let simplify_lets lam =
           end
       | _ -> no_opt ()
       end
-  | Lfunction {body} ->
-      count Ident.Map.empty body
+  | Lfunction fn ->
+      count_lfunction fn
   | Llet(_str, _k, v, Lvar w, l2) when optimize ->
       (* v will be replaced by w in l2, so each occurrence of v in l2
          increases w's refcount *)
@@ -480,7 +480,7 @@ let simplify_lets lam =
      count bv l1;
      count bv l2
   | Lletrec(bindings, body) ->
-      List.iter (fun { def } -> count bv def.body) bindings;
+      List.iter (fun { def } -> count_lfunction def) bindings;
       count bv body
   | Lprim(_p, ll, _) -> List.iter (count bv) ll
   | Lswitch(l, sw, _loc, _kind) ->
@@ -528,6 +528,8 @@ let simplify_lets lam =
       (* Don't move code into an exclave *)
       count Ident.Map.empty l2
 
+  and count_lfunction fn =
+    count Ident.Map.empty fn.body
 
   and count_default bv sw = match sw.sw_failaction with
   | None -> ()

testsuite/tests/typing-local/regression_simplif_letrec.ml

@@ -0,0 +1,40 @@
+(* TEST *)
+
+(* Regression test for incorrect Simplif substitution of Alias bindings
+   into Lletrec closures *)
+
+let ok () =
+  Gc.full_major ();
+  print_endline "ok"
+
+let[@inline never] test1 f =
+  match
+    if Sys.opaque_identity false
+    then (Sys.opaque_identity 1), 3
+    else (Sys.opaque_identity 2), 4
+  with
+  | a, b ->
+    let rec loop () =
+      let retry () =
+        ignore (Sys.opaque_identity b);
+        loop ()
+      in
+      f ();
+      if Sys.opaque_identity false then retry ()
+    in
+    loop ()
+
+let () = test1 ok
+
+type 'a g = { g: 'a @@ global }
+
+let[@inline never] test2 f =
+  let { g = r } = { g = ref 42 } in
+  let rec loop () =
+    f ();
+    ignore (Sys.opaque_identity r);
+    if Sys.opaque_identity false then loop ()
+  in
+  loop
+
+let () = test2 ok ()

testsuite/tests/typing-local/regression_simplif_letrec.reference

@@ -0,0 +1,2 @@
+ok
+ok