Merge branch 'fix/michele/output-messages' into 'master'

Rework output messages

See merge request laiser/caisar!36

src/main.ml

@@ -71,7 +71,7 @@ let log_level_is_debug () =
 let config detect () =
   if detect
   then (
-    Logs.debug (fun m -> m "Automatic detection.");
+    Logs.debug (fun m -> m "Automatic detection");
     let config =
       let debug = log_level_is_debug () in
       Autodetect.autodetection ~debug ()
@@ -95,7 +95,7 @@ let verify format loadpath memlimit timeout prover dataset_csv files =
     files
 
 let exec_cmd cmdname cmd =
-  Logs.debug (fun m -> m "Command `%s'." cmdname);
+  Logs.debug (fun m -> m "Command `%s'" cmdname);
   cmd ()
 
 (* -- Command line. *)
@@ -165,10 +165,9 @@ let verify_cmd =
       let all_provers = Prover.list_available () in
       let doc =
         Fmt.str
-          "Prover to use. Support is provided for the following provers: %s."
-          (Fmt.str "%a"
-             (Fmt.list ~sep:Fmt.comma Fmt.string)
-             (List.map ~f:Prover.to_string all_provers))
+          "Prover to use. Support is provided for the following provers: %a."
+          (Fmt.list ~sep:Fmt.comma Fmt.string)
+          (List.map ~f:Prover.to_string all_provers)
       in
       let provers =
         Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
@@ -215,9 +214,18 @@ let default_info =
 
 let default_cmd = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
 
+let () =
+  (* We register custom printers for a selection of exceptions otherwise Why3
+     will print the related messages as "anomaly: <exception with message>". *)
+  Why3.Exn_printer.register (fun fmt exn ->
+    match exn with
+    | Invalid_argument msg -> Fmt.pf fmt "Invalid argument: %s" msg
+    | Failure msg -> Fmt.pf fmt "Failure: %s" msg
+    | _ -> raise exn)
+
 let () =
   try
     Cmd.group ~default:default_cmd default_info [ config_cmd; verify_cmd ]
     |> Cmd.eval ~catch:false |> Caml.exit
   with exn when not (log_level_is_debug ()) ->
-    Fmt.epr "%a@." Why3.Exn_printer.exn_printer exn
+    Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)

src/verification.ml

@@ -77,7 +77,7 @@ let answer_saver limit config task env prover dataset_csv =
   let handle_task_saver task env dataset_csv command =
     let dataset_filename =
       match dataset_csv with
-      | None -> failwith "Error, no dataset provided for SAVer."
+      | None -> invalid_arg "No dataset provided for SAVer"
       | Some s -> s
     in
     let goal = Task.task_goal_fmla task in
@@ -104,13 +104,14 @@ let answer_saver limit config task env prover dataset_csv =
             let svm_filename =
               match Language.lookup_loaded_svms svm_app_sym with
               | Some t -> t.filename
-              | None -> failwith "SVM file not found in environment."
+              | None -> invalid_arg "No SVM model found in task"
             in
             (eps, svm_filename)
-          else failwith "Wrong predicate found."
-        (* no other predicate than robust_to is supported *)
-        | _ -> failwith "Unsupported by SAVer.")
-      | _ -> failwith "Unsupported by SAVer."
+          else failwith "Wrong predicate found"
+        | _ ->
+          (* no other predicate than robust_to is supported *)
+          failwith "Unsupported predicate by SAVer")
+      | _ -> failwith "Unsupported predicate by SAVer"
     in
     let svm_file = Unix.realpath svm_filename in
     let dataset_file = Unix.realpath dataset_filename in
@@ -175,7 +176,7 @@ let answer_generic limit config task driver (prover : Whyconf.config_prover) =
     match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
     | Some [ MAstr nn_file ] -> nn_file
     | Some _ -> assert false (* By construction of the meta. *)
-    | None -> invalid_arg (Fmt.str "No neural network model found in task")
+    | None -> invalid_arg "No neural network model found in task"
   in
   let nn_file = Unix.realpath nn_file in
   let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
@@ -198,8 +199,9 @@ let call_prover ~limit config (prover : Whyconf.config_prover) driver env
     then answer_saver limit config task env prover dataset_csv
     else answer_generic limit config task driver prover
   in
-  Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
-    Call_provers.print_prover_answer prover_answer
+  Logs.app (fun m ->
+    m "@[Goal %a:@ %a@]" Pretty.print_pr (Task.task_goal task)
+      Call_provers.print_prover_answer prover_answer)
 
 let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
   ?dataset_csv file =

tests/autodetect.t

@@ -21,8 +21,8 @@ Test autodetect
   $ PATH=$(pwd)/bin:$PATH
 
   $ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
-  [caisar][DEBUG] Command `config'.
-  [caisar][DEBUG] Automatic detection.
+  [caisar][DEBUG] Command `config'
+  [caisar][DEBUG] Automatic detection
   <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1

tests/marabou.t

@@ -34,7 +34,5 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
-  Goal G: Unknown
-  ()
-  Goal H: Unknown
-  ()
+  [caisar] Goal G: Unknown ()
+  [caisar] Goal H: Unknown ()

tests/simple.t

@@ -37,7 +37,5 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
-  Goal G: Unknown
-  ()
-  Goal H: Unknown
-  ()
+  [caisar] Goal G: Unknown ()
+  [caisar] Goal H: Unknown ()

tests/simple_onnx.t

@@ -29,5 +29,4 @@ Test verify
   >      (0.0:t) .< y1 .< (0.5:t)
   > end
   > EOF
-  Goal G: Unknown
-  ()
+  [caisar] Goal G: Unknown ()

tests/simple_ovo.t

@@ -34,4 +34,4 @@ Test verify
   >   goal G: forall a : input_type. robust_to svm_apply a (8.0:t)
   > end
   > EOF
-  Goal G: High failure
+  [caisar] Goal G: High failure