Use an exception to leave Solving_loop.process_source. (#1256)

* Use an exception to leave `Solving_loop.process_source`.

This function cannot call the system call `exit` because this system
call is not supported in browsers (it works in Node).

This commit uses a new exception `Exit_with_code` and catch it at the
toplevel of binaries.

src/bin/common/solving_loop.ml

@@ -32,6 +32,8 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
+exception Exit_with_code of int
+
 type solver_ctx = {
   ctx    : Commands.sat_tdecl list;
   local  : Commands.sat_tdecl list;
@@ -58,10 +60,13 @@ let recoverable_error ?(code = 1) =
           | Smtlib2 _ -> Printer.print_smtlib_err "%s" msg
           | _ -> Printer.print_err "%s" msg
       in
-      if Options.get_exit_on_error () then exit code)
+      if Options.get_exit_on_error () then raise (Exit_with_code code))
 
 let fatal_error ?(code = 1) =
-  Format.kasprintf (fun msg -> recoverable_error ~code "%s" msg; exit code)
+  Format.kasprintf
+    (fun msg ->
+       recoverable_error ~code "%s" msg;
+       raise (Exit_with_code code))
 
 let exit_as_timeout () = fatal_error ~code:142 "timeout"
 
@@ -252,7 +257,7 @@ let process_source ?selector_inst ~print_status src =
     | Errors.Error e ->
       recoverable_error "%a" Errors.report e;
       st
-    | Exit -> exit 0
+    | Exit -> raise (Exit_with_code 0)
     | _ as exn -> Printexc.raise_with_backtrace exn bt
   in
   let finally ~handle_exn st e =
@@ -892,7 +897,9 @@ let process_source ?selector_inst ~print_status src =
 
 let main () =
   let path = Options.get_file () in
-  if String.equal path "" then
-    process_source ~print_status:Frontend.print_status `Stdin
-  else
-    process_source ~print_status:Frontend.print_status @@ (`File path)
+  try
+    if String.equal path "" then
+      process_source ~print_status:Frontend.print_status `Stdin
+    else
+      process_source ~print_status:Frontend.print_status @@ (`File path)
+  with Exit_with_code code -> exit code

src/bin/common/solving_loop.mli

@@ -25,6 +25,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+exception Exit_with_code of int
+(** Exception raised to notify that [process_source] cannot continue.
+    The integer corresponds to an error code. *)
+
 val main : unit -> unit
 (** Main function solve the input problem. The processed source is given
     by the file located at [Options.get_file ()]. *)
@@ -36,4 +40,8 @@ val process_source :
   unit
 (** [process_source ?selector_inst ~print_status src] processes the
     input source [src] and call [print_status] on each answers.
-    The hook [selector_inst] allows to track generated instantiations. *)
+    The hook [selector_inst] allows to track generated instantiations.
+
+    @raise Exit_with_code c with c <> 0 if a fatal error occurs.
+           Recovarable errors raise this exception if
+           [Options.get_exit_on_error ()] is [true]. *)

src/bin/js/main_text_js.ml

@@ -34,11 +34,6 @@ let parse_cmdline () =
   with Parse_command.Exit_parse_command i -> exit i
 
 let () =
-  (* Currently, the main function of [Solving_loop] calls the [exit] function in
-     case of recoverable error, which is not supported in Javascript. We
-     turn off this feature as we do not support it correctly. See issue
-     https://github.com/OCamlPro/alt-ergo/issues/1250 *)
-  AltErgoLib.Options.set_exit_on_error false;
   parse_cmdline ();
   AltErgoLib.Printer.init_colors ();
   AltErgoLib.Printer.init_output_format ();

src/bin/js/worker_js.ml

@@ -146,6 +146,13 @@ let main worker_id filename filecontent =
       Worker_interface.diagnostic =
         Some [Format.asprintf "%a" Errors.report e]
     }
+  | Solving_loop.Exit_with_code code ->
+    let res = Worker_interface.init_results () in
+    let msg = Fmt.str "exit code %d" code in
+    { res with
+      Worker_interface.worker_id = worker_id;
+      Worker_interface.status = Error msg;
+    }
   | exn ->
     let res = Worker_interface.init_results () in
     let msg = Fmt.str "Unknown error: %s" (Printexc.to_string exn) in
@@ -170,7 +177,6 @@ let () =
           (* Extract options and set them *)
           let options = Worker_interface.options_from_json json_options in
           Options_interface.set_options options;
-          Options.set_exit_on_error false;
 
           (* Run the worker on the input file (filecontent) *)
           let filename = Option.get filename_opt in