Uncaught `Exit` exception in Alt-Ergo JS

[Halbaroth]

While working on #1325, I found a bug on both v2.6.x and next.

To reproduce the bug:

1. Save the following file as input.psmt2: input.txt
2. Build Alt-Ergo with jsoo in release mode:

   dune build --release _build/default/src/bin/js/main_text_js.bc.js
   ln -sf _build/default/src/bin/js/main_text_js.bc.js ./alt-ergo.js

3. Run Alt-Ergo with node on input.psmt2: node ./alt-ergo.js ./input.psmt2

Alt-Ergo immediately stops without error and exit status 0. If you run it with native Alt-Ergo, it will loop.

Alt-Ergo raises Exit to early leave some functions and the frontend catches it to invoke Stdlib.exit:

  let handle_exn st bt = function
    | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) ->
      recoverable_error "%t" msg; st
    | Util.Timeout ->
      Printer.print_status_timeout None None None None;
      exit_as_timeout ()
    | Errors.Error e ->
      recoverable_error "%a" Errors.report e;
      st
    | Exit -> raise (Exit_with_code 0)
    | _ as exn -> Printexc.raise_with_backtrace exn bt
  in

Unfortunately, Stdlib.Exit is used by several functions and in particular in Satml_types.mk_or, we have the following exception handler:

  let rec mk_or hcons l =
    try
      ...
      let delta_u = match delta_inv with
        | [] -> delta_inv
        | e::l ->
          let _, delta_u =
            List.fold_left
              (fun ((c,l) as acc) e ->
                 if complements c e then raise Exit;
                 if equal c e then acc
                 else (e, e::l)
              )(e,[e]) l
          in
          delta_u
      in
      ...
    with Exit -> vrai

On both native and bytecode, the handler catches Exit as expected but jsoo 6.2.0 fails to translate this code correctly in JS. You can apply this patch if you don't believe me ;)

diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml
index 7e87404bcf..e6b76e70de 100644
--- a/src/lib/structures/satml_types.ml
+++ b/src/lib/structures/satml_types.ml
@@ -830,6 +830,8 @@ module Flat_Formula : FLAT_FORMULA = struct
         try Some (common, List.rev_map (diff_list common) ands)
         with Not_included -> assert false
 
+  exception Kamoulox
+
   let rec mk_or hcons l =
     try
       let so, nso =
@@ -855,7 +857,7 @@ module Flat_Formula : FLAT_FORMULA = struct
           let _, delta_u =
             List.fold_left
               (fun ((c,l) as acc) e ->
-                 if complements c e then raise Exit;
+                 if complements c e then raise Kamoulox;
                  if equal c e then acc
                  else (e, e::l)
               )(e,[e]) l
@@ -883,7 +885,12 @@ module Flat_Formula : FLAT_FORMULA = struct
         | Some (com,ands) ->
           let ands = List.rev_map (mk_and hcons) ands in
           mk_and hcons ((mk_or hcons ands) :: com)
-    with Exit -> vrai
+    with Exit | Kamoulox -> vrai
+
+  let mk_or x y =
+    match mk_or x y with
+    | exception Kamoulox -> vrai
+    | r -> r
 
   (* translation from E.t *)

[Halbaroth]

The bug is fixed after js_of_ocaml 6.3.0. The following file is a MRE to check it:

exception Exn

let fake x = assert false

let mre l =
  try
    let _, y = List.fold_left (fun _ _ -> [], l) ([],[]) l in
    let () =
      match y with
      | [] -> ()
      | _ :: _ -> raise Exn
    in
    fake (List.map Fun.id l)
  with Exn -> 0

let () = ignore @@ mre [1]

and

ocamlc mre.ml -o mre.bc && js_of_ocaml compile mre.bc && node ./mre.js

should exit with 0 exit status.

[bclement-ocp]

Not actually fixed by #1349 as we removed that part of the patch – this is a bug in js_of_ocaml that was fixed upstream and we are waiting for a new release of js_of_ocaml with the fix.