Commit eb96f1af authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_190' into 'master'

Fix issue #190

Closes #190

See merge request !27
parents 85fd313b c1dde87a
...@@ -567,7 +567,7 @@ let interpNotif (n: notification) = ...@@ -567,7 +567,7 @@ let interpNotif (n: notification) =
| Proof_error (_nid, s) -> | Proof_error (_nid, s) ->
PE.error_print_msg PE.error_print_msg
(Format.asprintf "Proof error on selected node: \"%s\"" s) (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 PE.error_print_msg
(Format.asprintf "Transformation error on selected node: \"%s\"" s) (Format.asprintf "Transformation error on selected node: \"%s\"" s)
| Strat_error (_nid, s) -> | Strat_error (_nid, s) ->
......
...@@ -1465,7 +1465,12 @@ let treat_message_notification msg = match msg with ...@@ -1465,7 +1465,12 @@ let treat_message_notification msg = match msg with
(* TODO: do something ! *) (* TODO: do something ! *)
| Proof_error (_id, s) -> | Proof_error (_id, s) ->
print_message ~kind:1 ~notif_kind:"Proof_error" "%s" 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 if arg = "" then
print_message ~kind:1 ~notif_kind:"Transformation Error" print_message ~kind:1 ~notif_kind:"Transformation Error"
"%s\nTransformation failed: \n%s\n\n%s" msg tr_name doc "%s\nTransformation failed: \n%s\n\n%s" msg tr_name doc
......
...@@ -12,6 +12,8 @@ ...@@ -12,6 +12,8 @@
open Format open Format
open Wstdlib open Wstdlib
open Session_itp open Session_itp
open Generic_arg_trans_utils
open Args_wrapper
let debug_sched = Debug.register_info_flag "scheduler" let debug_sched = Debug.register_info_flag "scheduler"
~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \ ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
...@@ -53,20 +55,24 @@ let print_status fmt st = ...@@ -53,20 +55,24 @@ let print_status fmt st =
type transformation_status = type transformation_status =
| TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn) | TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
| TSfatal of (proofNodeID * exn)
let print_trans_status fmt st = let print_trans_status fmt st =
match st with match st with
| TSscheduled -> fprintf fmt "TScheduled" | TSscheduled -> fprintf fmt "TScheduled"
| TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *) | TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
| TSfailed _e -> fprintf fmt "TSfailed" | TSfailed _e -> fprintf fmt "TSfailed"
| TSfatal _e -> fprintf fmt "TSfatal"
type strategy_status = STSgoto of proofNodeID * int | STShalt type strategy_status = STSgoto of proofNodeID * int | STShalt
| STSfatal of string * proofNodeID * exn
let print_strategy_status fmt st = let print_strategy_status fmt st =
match st with match st with
| STSgoto(id,n) -> | STSgoto(id,n) ->
fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id
| STShalt -> fprintf fmt "halt" | STShalt -> fprintf fmt "halt"
| STSfatal _ -> fprintf fmt "fatal"
type controller = type controller =
...@@ -716,7 +722,7 @@ let schedule_transformation c id name args ~callback ~notification = ...@@ -716,7 +722,7 @@ let schedule_transformation c id name args ~callback ~notification =
begin match s with begin match s with
| TSdone tid -> update_trans_node notification c.controller_session tid | TSdone tid -> update_trans_node notification c.controller_session tid
| TSscheduled | TSscheduled
| TSfailed _ -> () | TSfailed _ | TSfatal _ -> ()
end; end;
callback s callback s
in in
...@@ -733,10 +739,18 @@ let schedule_transformation c id name args ~callback ~notification = ...@@ -733,10 +739,18 @@ let schedule_transformation c id name args ~callback ~notification =
| NoProgress -> | NoProgress ->
(* if result is same as input task, consider it as a failure *) (* if result is same as input task, consider it as a failure *)
callback (TSfailed (id, NoProgress)) 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) -> | e when not (Debug.test_flag Debug.stack_trace) ->
(* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]" (* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
name Exn_printer.exn_printer e; TODO *) name Exn_printer.exn_printer e; TODO *)
callback (TSfailed (id, e)) callback (TSfatal (id, e))
end; end;
false false
in in
...@@ -782,6 +796,8 @@ let run_strategy_on_goal ...@@ -782,6 +796,8 @@ let run_strategy_on_goal
let callback ntr = let callback ntr =
callback_tr trname [] ntr; callback_tr trname [] ntr;
match ntr with match ntr with
| TSfatal (id, e) ->
callback (STSfatal (trname, id, e))
| TSfailed _e -> (* transformation failed *) | TSfailed _e -> (* transformation failed *)
callback (STSgoto (g,pc+1)); callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in 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 ...@@ -1184,6 +1200,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
begin match st with begin match st with
| TSscheduled -> () | TSscheduled -> ()
| TSfailed _ -> assert false | TSfailed _ -> assert false
| TSfatal _ -> assert false
| TSdone trid -> | TSdone trid ->
match get_sub_tasks ses trid with match get_sub_tasks ses trid with
| [pn] -> | [pn] ->
...@@ -1230,6 +1247,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i ...@@ -1230,6 +1247,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
debug debug
"[Bisect] transformation 'remove' scheduled@."; "[Bisect] transformation 'remove' scheduled@.";
callback_tr "remove" [rem] st; callback_tr "remove" [rem] st;
| TSfatal (_, exn)
| TSfailed(_,exn) -> | TSfailed(_,exn) ->
(* may happen if removing a type or a lsymbol that is used (* may happen if removing a type or a lsymbol that is used
later on. We do has if proof fails. *) later on. We do has if proof fails. *)
......
...@@ -34,10 +34,17 @@ type transformation_status = ...@@ -34,10 +34,17 @@ type transformation_status =
TSscheduled TSscheduled
| TSdone of transID | TSdone of transID
| TSfailed of (proofNodeID * exn) | 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 val print_trans_status : Format.formatter -> transformation_status -> unit
type strategy_status = STSgoto of proofNodeID * int | STShalt 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 val print_strategy_status : Format.formatter -> strategy_status -> unit
......
...@@ -36,7 +36,7 @@ type global_information = ...@@ -36,7 +36,7 @@ type global_information =
type message_notification = type message_notification =
| Proof_error of node_ID * string | 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 *) (* Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_trans *)
| Strat_error of node_ID * string | Strat_error of node_ID * string
| Replay_Info of string | Replay_Info of string
...@@ -155,7 +155,8 @@ let print_request fmt r = ...@@ -155,7 +155,8 @@ let print_request fmt r =
let print_msg fmt m = let print_msg fmt m =
match m with match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s | 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 | Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s | Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s | Query_Info (_ids, s) -> fprintf fmt "query info %s" s
......
...@@ -40,8 +40,8 @@ type global_information = ...@@ -40,8 +40,8 @@ type global_information =
type message_notification = type message_notification =
| Proof_error of node_ID * string | 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_transf *) (** Transf_error (is_fatal, nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf *)
| Strat_error of node_ID * string | Strat_error of node_ID * string
| Replay_Info of string | Replay_Info of string
| Query_Info of node_ID * string | Query_Info of node_ID * string
......
...@@ -1138,8 +1138,15 @@ end ...@@ -1138,8 +1138,15 @@ end
with | _ -> "" in with | _ -> "" in
let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e 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 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 apply_transform node_id t args =
let d = get_server_data () in let d = get_server_data () in
......
...@@ -261,8 +261,9 @@ let convert_message (m: message_notification) = ...@@ -261,8 +261,9 @@ let convert_message (m: message_notification) =
convert_record ["mess_notif", cc m; convert_record ["mess_notif", cc m;
"node_ID", Int nid; "node_ID", Int nid;
"error", String s] "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; convert_record ["mess_notif", cc m;
"is_fatal", Bool is_fatal;
"node_ID", Int nid; "node_ID", Int nid;
"tr_name", String tr; "tr_name", String tr;
"failing_arg", String arg; "failing_arg", String arg;
...@@ -665,12 +666,13 @@ let parse_message constr j = ...@@ -665,12 +666,13 @@ let parse_message constr j =
| "Transf_error" -> | "Transf_error" ->
let nid = get_int (get_field j "node_ID") in 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 tr_name = get_string (get_field j "tr_name") in
let arg = get_string (get_field j "failing_arg") in let arg = get_string (get_field j "failing_arg") in
let loc = parse_loc (get_field j "loc") in let loc = parse_loc (get_field j "loc") in
let error = get_string (get_field j "error") in let error = get_string (get_field j "error") in
let doc = get_string (get_field j "doc") 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" -> | "Strat_error" ->
let nid = get_int (get_field j "node_ID") in let nid = get_int (get_field j "node_ID") in
......
...@@ -105,7 +105,7 @@ module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell) ...@@ -105,7 +105,7 @@ module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)
let treat_message_notification fmt msg = match msg with let treat_message_notification fmt msg = match msg with
(* TODO: do something ! *) (* TODO: do something ! *)
| Proof_error (_id, s) -> fprintf fmt "%s@." s | 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 | Strat_error (_id, s) -> fprintf fmt "%s@." s
| Replay_Info s -> fprintf fmt "%s@." s | Replay_Info s -> fprintf fmt "%s@." s
| Query_Info (_id, s) -> fprintf fmt "%s@." s | Query_Info (_id, s) -> fprintf fmt "%s@." s
......
...@@ -26,6 +26,8 @@ exception Arg_expected_none of string ...@@ -26,6 +26,8 @@ exception Arg_expected_none of string
exception Arg_pr_not_found of Decl.prsymbol exception Arg_pr_not_found of Decl.prsymbol
exception Arg_qid_not_found of Ptree.qualid exception Arg_qid_not_found of Ptree.qualid
exception Arg_error of string 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 val build_naming_tables : Task.task -> Trans.naming_table
...@@ -98,9 +100,6 @@ type (_, _) trans_typ = ...@@ -98,9 +100,6 @@ type (_, _) trans_typ =
string is the keyword for that optional argument, its presence string is the keyword for that optional argument, its presence
meaning "true" *) meaning "true" *)
exception Arg_parse_type_error of Loc.position * string * exn
exception Unnecessary_arguments of string list
(** {2 parsing and typing of arguments} (** {2 parsing and typing of arguments}
the functions below wrap arguments of transformations, turning string 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