Commit c1dde87a authored by Sylvain Dailler's avatar Sylvain Dailler

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
parent 64b9237d
......@@ -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) ->
......
......@@ -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
......
......@@ -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. *)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment