From c1dde87a8982599619f9d602cf9e86820c1d310b Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Tue, 2 Oct 2018 15:10:00 +0200
Subject: [PATCH] Fix issue #190
Exceptions from transformations are of two kinds:
- fatal exception which are then raised into a popup in the ide
- normal exception which appears in the message view
---
src/ide/why3_js.ml | 2 +-
src/ide/why3ide.ml | 7 ++++++-
src/session/controller_itp.ml | 22 ++++++++++++++++++++--
src/session/controller_itp.mli | 7 +++++++
src/session/itp_communication.ml | 5 +++--
src/session/itp_communication.mli | 4 ++--
src/session/itp_server.ml | 11 +++++++++--
src/session/json_util.ml | 6 ++++--
src/tools/why3shell.ml | 2 +-
src/transform/args_wrapper.mli | 5 ++---
10 files changed, 55 insertions(+), 16 deletions(-)
diff --git a/src/ide/why3_js.ml b/src/ide/why3_js.ml
index b184ae462..3fb4ea00f 100644
--- a/src/ide/why3_js.ml
+++ b/src/ide/why3_js.ml
@@ -567,7 +567,7 @@ let interpNotif (n: notification) =
| Proof_error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Proof error on selected node: \"%s\"" s)
- | Transf_error (_ids, _tr, _args, _loc, s, _d) ->
+ | Transf_error (_b, _ids, _tr, _args, _loc, s, _d) ->
PE.error_print_msg
(Format.asprintf "Transformation error on selected node: \"%s\"" s)
| Strat_error (_nid, s) ->
diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml
index 0bf9726fd..02dd70d4e 100644
--- a/src/ide/why3ide.ml
+++ b/src/ide/why3ide.ml
@@ -1465,7 +1465,12 @@ let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) ->
print_message ~kind:1 ~notif_kind:"Proof_error" "%s" s
- | Transf_error (_id, tr_name, arg, loc, msg, doc) ->
+ | Transf_error (true, _id, tr_name, _arg, _loc, msg, _doc) ->
+ (* When the error reported by the transformation is fatal, we notify the
+ user with a popup. *)
+ let msg = Format.sprintf "Please report:\nTransformation %s failed: \n%s\n" tr_name msg in
+ GToolbox.message_box ~title:"Why3 fatal error" msg
+ | Transf_error (false, _id, tr_name, arg, loc, msg, doc) ->
if arg = "" then
print_message ~kind:1 ~notif_kind:"Transformation Error"
"%s\nTransformation failed: \n%s\n\n%s" msg tr_name doc
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index ea1615c44..df2bdcd9d 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -12,6 +12,8 @@
open Format
open Wstdlib
open Session_itp
+open Generic_arg_trans_utils
+open Args_wrapper
let debug_sched = Debug.register_info_flag "scheduler"
~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
@@ -53,20 +55,24 @@ let print_status fmt st =
type transformation_status =
| TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
+ | TSfatal of (proofNodeID * exn)
let print_trans_status fmt st =
match st with
| TSscheduled -> fprintf fmt "TScheduled"
| TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
| TSfailed _e -> fprintf fmt "TSfailed"
+ | TSfatal _e -> fprintf fmt "TSfatal"
type strategy_status = STSgoto of proofNodeID * int | STShalt
+ | STSfatal of string * proofNodeID * exn
let print_strategy_status fmt st =
match st with
| STSgoto(id,n) ->
fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id
| STShalt -> fprintf fmt "halt"
+ | STSfatal _ -> fprintf fmt "fatal"
type controller =
@@ -716,7 +722,7 @@ let schedule_transformation c id name args ~callback ~notification =
begin match s with
| TSdone tid -> update_trans_node notification c.controller_session tid
| TSscheduled
- | TSfailed _ -> ()
+ | TSfailed _ | TSfatal _ -> ()
end;
callback s
in
@@ -733,10 +739,18 @@ let schedule_transformation c id name args ~callback ~notification =
| NoProgress ->
(* if result is same as input task, consider it as a failure *)
callback (TSfailed (id, NoProgress))
+ | (Arg_trans _ | Arg_trans_decl _
+ | Arg_trans_term _ | Arg_trans_term2 _
+ | Arg_trans_pattern _ | Arg_trans_type _ | Arg_bad_hypothesis _
+ | Cannot_infer_type _ | Unnecessary_terms _ | Parse_error _
+ | Arg_expected _ | Arg_theory_not_found _ | Arg_expected_none _
+ | Arg_qid_not_found _ | Arg_pr_not_found _ | Arg_error _
+ | Arg_parse_type_error _ | Unnecessary_arguments _) as e ->
+ callback (TSfailed (id, e))
| e when not (Debug.test_flag Debug.stack_trace) ->
(* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
name Exn_printer.exn_printer e; TODO *)
- callback (TSfailed (id, e))
+ callback (TSfatal (id, e))
end;
false
in
@@ -782,6 +796,8 @@ let run_strategy_on_goal
let callback ntr =
callback_tr trname [] ntr;
match ntr with
+ | TSfatal (id, e) ->
+ callback (STSfatal (trname, id, e))
| TSfailed _e -> (* transformation failed *)
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
@@ -1184,6 +1200,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
begin match st with
| TSscheduled -> ()
| TSfailed _ -> assert false
+ | TSfatal _ -> assert false
| TSdone trid ->
match get_sub_tasks ses trid with
| [pn] ->
@@ -1230,6 +1247,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
debug
"[Bisect] transformation 'remove' scheduled@.";
callback_tr "remove" [rem] st;
+ | TSfatal (_, exn)
| TSfailed(_,exn) ->
(* may happen if removing a type or a lsymbol that is used
later on. We do has if proof fails. *)
diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli
index 21e7c44fa..c4205eecd 100644
--- a/src/session/controller_itp.mli
+++ b/src/session/controller_itp.mli
@@ -34,10 +34,17 @@ type transformation_status =
TSscheduled
| TSdone of transID
| TSfailed of (proofNodeID * exn)
+ (* We distinguish normal usage exception of transformation from fatal
+ exception like assertion failure that should not be raised *)
+ | TSfatal of (proofNodeID * exn)
val print_trans_status : Format.formatter -> transformation_status -> unit
type strategy_status = STSgoto of proofNodeID * int | STShalt
+ (* When a transformation fatally returns, we have to
+ fatally fail the strategy
+ [transformation_name, pid, exn] *)
+ | STSfatal of string * proofNodeID * exn
val print_strategy_status : Format.formatter -> strategy_status -> unit
diff --git a/src/session/itp_communication.ml b/src/session/itp_communication.ml
index e0f85166f..64e309e1c 100644
--- a/src/session/itp_communication.ml
+++ b/src/session/itp_communication.ml
@@ -36,7 +36,7 @@ type global_information =
type message_notification =
| Proof_error of node_ID * string
- | Transf_error of node_ID * string * string * Loc.position * string * string
+ | Transf_error of bool * node_ID * string * string * Loc.position * string * string
(* Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_trans *)
| Strat_error of node_ID * string
| Replay_Info of string
@@ -155,7 +155,8 @@ let print_request fmt r =
let print_msg fmt m =
match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
- | Transf_error (_ids, _tr, _args, _loc, s, _d) -> fprintf fmt "transf error %s" s
+ | Transf_error (b, _ids, _tr, _args, _loc, s, _d) ->
+ fprintf fmt "transf error (is fatal = %b) %s" b s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
diff --git a/src/session/itp_communication.mli b/src/session/itp_communication.mli
index 10de2a128..4d9e41cd3 100644
--- a/src/session/itp_communication.mli
+++ b/src/session/itp_communication.mli
@@ -40,8 +40,8 @@ type global_information =
type message_notification =
| Proof_error of node_ID * string
- | Transf_error of node_ID * string * string * Loc.position * string * string
- (** Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf *)
+ | Transf_error of bool * node_ID * string * string * Loc.position * string * string
+ (** Transf_error (is_fatal, nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf *)
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 39b748530..12f01043f 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -1138,8 +1138,15 @@ end
with | _ -> "" in
let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
- P.notify (Message (Transf_error (node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
- | _ -> ()
+ P.notify (Message (Transf_error (false, node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
+ | TSscheduled -> ()
+ | TSfatal (id, e) ->
+ let doc = try
+ Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
+ with | _ -> "" in
+ let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
+ let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
+ P.notify (Message (Transf_error (true, node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
let apply_transform node_id t args =
let d = get_server_data () in
diff --git a/src/session/json_util.ml b/src/session/json_util.ml
index 2bd660d76..b7f86bb29 100644
--- a/src/session/json_util.ml
+++ b/src/session/json_util.ml
@@ -261,8 +261,9 @@ let convert_message (m: message_notification) =
convert_record ["mess_notif", cc m;
"node_ID", Int nid;
"error", String s]
- | Transf_error (nid, tr, arg, loc, s, doc) ->
+ | Transf_error (is_fatal, nid, tr, arg, loc, s, doc) ->
convert_record ["mess_notif", cc m;
+ "is_fatal", Bool is_fatal;
"node_ID", Int nid;
"tr_name", String tr;
"failing_arg", String arg;
@@ -665,12 +666,13 @@ let parse_message constr j =
| "Transf_error" ->
let nid = get_int (get_field j "node_ID") in
+ let is_fatal = get_bool (get_field j "is_fatal") in
let tr_name = get_string (get_field j "tr_name") in
let arg = get_string (get_field j "failing_arg") in
let loc = parse_loc (get_field j "loc") in
let error = get_string (get_field j "error") in
let doc = get_string (get_field j "doc") in
- Transf_error (nid, tr_name, arg, loc, error, doc)
+ Transf_error (is_fatal, nid, tr_name, arg, loc, error, doc)
| "Strat_error" ->
let nid = get_int (get_field j "node_ID") in
diff --git a/src/tools/why3shell.ml b/src/tools/why3shell.ml
index 38511eadf..5cb35ca79 100644
--- a/src/tools/why3shell.ml
+++ b/src/tools/why3shell.ml
@@ -105,7 +105,7 @@ module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)
let treat_message_notification fmt msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) -> fprintf fmt "%s@." s
- | Transf_error (_id, _tr_name, _arg, _loc, s, _) -> fprintf fmt "%s@." s
+ | Transf_error (_b, _id, _tr_name, _arg, _loc, s, _) -> fprintf fmt "%s@." s
| Strat_error (_id, s) -> fprintf fmt "%s@." s
| Replay_Info s -> fprintf fmt "%s@." s
| Query_Info (_id, s) -> fprintf fmt "%s@." s
diff --git a/src/transform/args_wrapper.mli b/src/transform/args_wrapper.mli
index 1133993d9..7cb8e93cf 100644
--- a/src/transform/args_wrapper.mli
+++ b/src/transform/args_wrapper.mli
@@ -26,6 +26,8 @@ exception Arg_expected_none of string
exception Arg_pr_not_found of Decl.prsymbol
exception Arg_qid_not_found of Ptree.qualid
exception Arg_error of string
+exception Arg_parse_type_error of Loc.position * string * exn
+exception Unnecessary_arguments of string list
val build_naming_tables : Task.task -> Trans.naming_table
@@ -98,9 +100,6 @@ type (_, _) trans_typ =
string is the keyword for that optional argument, its presence
meaning "true" *)
-exception Arg_parse_type_error of Loc.position * string * exn
-exception Unnecessary_arguments of string list
-
(** {2 parsing and typing of arguments}
the functions below wrap arguments of transformations, turning string
--
GitLab