Properly exiting in the main loop

src/bin/common/parse_command.ml

@@ -324,7 +324,8 @@ let mk_execution_opt input_format parse_only ()
   set_preludes preludes;
   `Ok()
 
-let mk_internal_opt disable_weaks enable_assertions warning_as_error gc_policy
+let mk_internal_opt
+    disable_weaks enable_assertions warning_as_error continue_on_error gc_policy
   =
   let gc_policy = match gc_policy with
     | 0 | 1 | 2 -> gc_policy
@@ -335,6 +336,7 @@ let mk_internal_opt disable_weaks enable_assertions warning_as_error gc_policy
   set_disable_weaks disable_weaks;
   set_enable_assertions enable_assertions;
   set_warning_as_error warning_as_error;
+  set_exit_on_error (not continue_on_error);
   `Ok(gc_policy)
 
 let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
@@ -779,6 +781,10 @@ let parse_internal_opt =
     let doc = "Enable warning as error" in
     Arg.(value & flag & info ["warning-as-error"] ~docs ~doc) in
 
+  let continue_on_error =
+    let doc = "Sets Alt-ergo's behavior to continue on errors" in
+    Arg.(value & flag & info ["continue-on-error"] ~docs ~doc) in
+
   let gc_policy =
     let doc =
       "Set the gc policy allocation. 0 = next-fit policy, 1 = \
@@ -788,7 +794,8 @@ let parse_internal_opt =
     Arg.(value & opt int 0 & info ["gc-policy"] ~docv ~docs ~doc) in
 
   Term.(ret (const mk_internal_opt $
-             disable_weaks $ enable_assertions $ warning_as_error $ gc_policy
+             disable_weaks $ enable_assertions $
+             warning_as_error $ continue_on_error $ gc_policy
             ))
 
 let parse_limit_opt =

src/bin/common/solving_loop.ml

@@ -50,8 +50,51 @@ let empty_solver_ctx = {
   global = [];
 }
 
-let unsupported_opt () =
-  Printer.print_std "unsupported"
+let custom_error
+    (type a)
+    ?(default : a option)
+    err_code
+    (msg : ('a, Format.formatter, unit, unit, unit, a) format6)
+  : 'a =
+  let pp_reporter =
+    match Options.get_output_format () with
+    | Options.Smtlib2 -> Printer.print_smtlib_err ~flushed:true
+    | _ ->
+      Printer.print_err ~flushed:true ~header:true ~error:true
+  in
+  Format.kasprintf
+    ( fun msg ->
+        if msg <> "" then pp_reporter "%s" msg;
+        if Options.get_exit_on_error () then
+          exit err_code
+        else
+          match default with
+          | None -> exit err_code
+          | Some d -> d
+    )
+    msg
+
+let error
+    (type a)
+    ?(default : a option)
+    (msg : ('a, Format.formatter, unit, unit, unit, a) format6) : 'a =
+  custom_error ?default 1 msg
+
+let exit_as_timeout () = custom_error 142 "timeout"
+
+let warning (msg : ('a, Format.formatter, unit, unit, unit, 'b) format6) : 'a =
+  if Options.get_warning_as_error () then
+    error msg
+  else
+    Printer.print_wrn msg
+
+let unsupported_opt opt =
+  let () =
+    match Options.get_output_format () with
+    | Options.Smtlib2 -> Printer.print_std "unsupported"
+    | _ -> ()
+  in
+  warning "unsupported option %s" opt
 
 let main () =
   let () = Dolmen_loop.Code.init [] in
@@ -104,7 +147,7 @@ let main () =
         Some partial_model
       | `Unsat -> None
     with Util.Timeout ->
-      if not (Options.get_timelimit_per_goal()) then exit 142;
+      if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
       None
   in
 
@@ -182,14 +225,15 @@ let main () =
       with
       | Util.Timeout ->
         FE.print_status (FE.Timeout None) 0;
-        exit 142
+        exit_as_timeout ()
       | Parsing.Parse_error ->
-        Printer.print_err "%a" Errors.report
-          (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""));
-        exit 1
+        (* TODO: display a better error message *)
+        error
+          "%a"
+          Errors.report
+          (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""))
       | Errors.Error e ->
-        Printer.print_err "%a" Errors.report e;
-        exit 1
+        error "%a" Errors.report e;
     in
 
     let all_used_context = FE.init_all_used_context () in
@@ -204,8 +248,9 @@ let main () =
         with
         | Errors.Error e ->
           if e != Warning_as_error then
-            Printer.print_err "%a" Errors.report e;
-          exit 1
+            error ~default:state "%a" Errors.report e
+          else
+            error ~default:state ""
       end
     in
 
@@ -219,7 +264,7 @@ let main () =
       Options.Time.unset_timeout ();
     with Util.Timeout ->
       FE.print_status (FE.Timeout None) 0;
-      exit 142
+      exit_as_timeout ()
   in
 
   let solver_ctx_key: solver_ctx State.key =
@@ -250,21 +295,18 @@ let main () =
     else
       st, `Continue stmt
   in
-  let handle_exn _ bt = function
+  let handle_exn st bt = function
     | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) ->
-      Printer.print_err "%t" msg;
-      exit 1
+      error ~default:st "%t" msg
     | Util.Timeout ->
       Printer.print_status_timeout None None None None;
-      exit 142
-    | Errors.Error e ->
-      Printer.print_err "%a" Errors.report e;
-      exit 1
+      exit_as_timeout ()
+    | Errors.Error e -> error ~default:st "%a" Errors.report e
     | _ as exn -> Printexc.raise_with_backtrace exn bt
   in
   let finally ~handle_exn st e =
     match e with
-    | Some (bt, exn) -> handle_exn st bt exn; st
+    | Some (bt, exn) -> handle_exn st bt exn
     | _ -> st
   in
   let set_output_format fmt =
@@ -273,8 +315,7 @@ let main () =
       | ".ae" -> Options.set_output_format Native
       | ".smt2" | ".psmt2" -> Options.set_output_format Smtlib2
       | s ->
-        Printer.print_wrn
-          "The output format %s is not supported by the Dolmen frontend." s
+        warning "The output format %s is not supported by the Dolmen frontend." s
   in
   (* The function In_channel.input_all is not available before OCaml 4.14. *)
   let read_all ch =
@@ -348,7 +389,8 @@ let main () =
   in
 
   let print_wrn_opt ~name loc ty value =
-    Printer.print_wrn "%a The option %s expects a %s, got %a"
+    warning
+      "%a The option %s expects a %s, got %a"
       Loc.report loc name ty DStd.Term.print value
   in
 
@@ -369,9 +411,11 @@ let main () =
          solver Tableaux. *)
       if Stdlib.(Options.get_sat_solver () = Tableaux) then
         Options.set_unsat_core true
-      else Printer.print_wrn "%a The generation of unsat cores is not \
-                              supported for the current SAT solver. Please \
-                              choose the SAT solver Tableaux."
+      else
+        warning
+          "%a The generation of unsat cores is not \
+           supported for the current SAT solver. Please \
+           choose the SAT solver Tableaux."
           Loc.report st_loc
     | ":produce-unsat-cores", Symbol { name = Simple "false"; _ } ->
       Options.set_unsat_core false
@@ -403,11 +447,9 @@ let main () =
       | ":print-success"
       | ":random-seed"), _
       ->
-      unsupported_opt ();
-      Printer.print_wrn "unsupported option '%s'" name
+      unsupported_opt name
     | _ ->
-      unsupported_opt ();
-      Printer.print_err "unknown option '%s'" name
+      unsupported_opt name
   in
 
   let handle_get_info (st : State.t) (name: string) =
@@ -417,8 +459,7 @@ let main () =
     in
     let pp_reason_unknown st =
       let err () =
-        let msg = "Invalid (get-info :reason-unknown)" in
-        Printer.print_smtlib_err "%s" msg
+        error ~default:() "Invalid (get-info :reason-unknown)"
       in
       match State.get partial_model_key st with
       | None -> err ()
@@ -434,7 +475,13 @@ let main () =
     | ":authors" ->
       print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
     | ":error-behavior" ->
-      print_std Fmt.string "immediate-exit"
+      let behavior =
+        if Options.get_exit_on_error () then
+          "immediate-exit"
+        else
+          "continued-execution"
+      in
+      print_std Fmt.string behavior
     | ":name" ->
       print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
     | ":reason-unknown" ->
@@ -443,11 +490,9 @@ let main () =
       print_std Fmt.string Version._version
     | ":all-statistics"
     | ":assertion-stack-levels" ->
-      unsupported_opt ();
-      Printer.print_wrn "unsupported option '%s'" name
+      unsupported_opt name
     | _ ->
-      unsupported_opt ();
-      Printer.print_err "unknown option '%s'" name
+      unsupported_opt name
   in
 
   let handle_stmt :
@@ -541,15 +586,10 @@ let main () =
             end
           | None ->
             (* TODO: add the location of the statement. *)
-            Printer.print_smtlib_err "No model produced.";
-            st
+            error ~default:st "No model produced."
         else
-          begin
             (* TODO: add the location of the statement. *)
-            Printer.print_smtlib_err
-              "Model generation disabled (try --produce-models)";
-            st
-          end
+          error ~default:st "Model generation disabled (try --produce-models)"
 
       | {contents = `Get_info kind; _ } ->
         handle_get_info st kind;
@@ -611,7 +651,7 @@ let main () =
       State.flush st () |> ignore
     with exn ->
       let bt = Printexc.get_raw_backtrace () in
-      handle_exn st bt exn
+      ignore (handle_exn st bt exn)
   in
 
   let filename = get_file () in

src/lib/util/options.ml

@@ -302,14 +302,17 @@ let get_type_smt2 () = !type_smt2
 let disable_weaks = ref false
 let enable_assertions = ref false
 let warning_as_error = ref false
+let exit_on_error = ref true
 
 let set_disable_weaks b = disable_weaks := b
 let set_enable_assertions b = enable_assertions := b
 let set_warning_as_error b = warning_as_error := b
+let set_exit_on_error b = exit_on_error := b
 
 let get_disable_weaks () = !disable_weaks
 let get_enable_assertions () = !enable_assertions
 let get_warning_as_error () = !warning_as_error
+let get_exit_on_error () = !exit_on_error
 
 (** Limit options *)
 

src/lib/util/options.mli

@@ -359,6 +359,9 @@ val set_enable_assertions : bool -> unit
 (** Set [warning_as_error] accessible with {!val:get_warning_as_error} *)
 val set_warning_as_error : bool -> unit
 
+(** Set [exit_on_error] accessible with {!val:get_exit_on_error} *)
+val set_exit_on_error : bool -> unit
+
 (** Set [timelimit_interpretation] accessible with
     {!val:get_timelimit_interpretation} *)
 val set_timelimit_interpretation : float -> unit
@@ -658,6 +661,10 @@ val get_enable_assertions : unit -> bool
 val get_warning_as_error : unit -> bool
 (** Default to [false] *)
 
+(** [true] if alt-ergo exits on all errors. *)
+val get_exit_on_error : unit -> bool
+(** Default to [true] *)
+
 (** {4 Limit options} *)
 
 (** Value specifying the age limit bound. *)

tests/cram.t/run.t

@@ -50,21 +50,21 @@ combinations of produce-models et al.
 First, if model generation is not enabled, we should error out when a
 `(get-model)` statement is issued:
 
-  $ echo '(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 --continue-on-error
   (error "Model generation disabled (try --produce-models)")
 
 This should be the case Tableaux solver as well:
 
-  $ echo '(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error
   (error "Model generation disabled (try --produce-models)")
 
 The messages above mention `--produce-models`, but we can also use
 `set-option`.
 
-  $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 --continue-on-error
   (error "No model produced.")
 
-  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error
   (error "No model produced.")
 
 And now some cases where it should work (using either `--produce-models` or `set-option`):