From ba9fc85b8444fcb90af14c3d89acbba123d3a207 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Mon, 26 Feb 2024 11:23:32 +0100 Subject: [PATCH] Make exception output consistent across the interpreters --- compiler/driver.ml | 8 +-- compiler/lcalc/compile_without_exceptions.ml | 2 +- compiler/lcalc/to_ocaml.ml | 2 +- compiler/scalc/to_c.ml | 2 +- compiler/scalc/to_python.ml | 2 +- compiler/scalc/to_r.ml | 4 +- compiler/shared_ast/definitions.ml | 7 +- compiler/shared_ast/interpreter.ml | 71 +++++++++++++------- compiler/shared_ast/interpreter.mli | 2 +- compiler/shared_ast/optimizations.ml | 5 +- compiler/shared_ast/print.ml | 2 +- 11 files changed, 66 insertions(+), 41 deletions(-) diff --git a/compiler/driver.ml b/compiler/driver.ml index 4b5ab7d9..d164b0b7 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -676,13 +676,7 @@ module Commands = struct let print_interpretation_results options interpreter prg scope_uid = Message.emit_debug "Starting interpretation..."; - let results = - try interpreter prg scope_uid - with Shared_ast.Interpreter.CatalaException exn -> - Message.raise_error - "During interpretation, the error %a has been raised but not caught!" - Shared_ast.Print.except exn - in + let results = interpreter prg scope_uid in Message.emit_debug "End of interpretation"; let results = List.sort (fun ((v1, _), _) ((v2, _), _) -> String.compare v1 v2) results diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 13a962fe..1779fd3a 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -26,7 +26,7 @@ module A = Ast function calls. The resulting function is not more difficult than what we had when translating without exceptions. - The typing translation is to simply trnsform defult type into option types. *) + The typing translation is to simply trnsform default type into option types. *) let rec translate_typ (tau : typ) : typ = Mark.copy tau diff --git a/compiler/lcalc/to_ocaml.ml b/compiler/lcalc/to_ocaml.ml index 3fdeb7bc..1fcdf9cd 100644 --- a/compiler/lcalc/to_ocaml.ml +++ b/compiler/lcalc/to_ocaml.ml @@ -241,7 +241,7 @@ let needs_parens (e : 'm expr) : bool = let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit = match Mark.remove exc with - | ConflictError -> + | ConflictError _ -> let pos = Mark.get exc in Format.fprintf fmt "(ConflictError@ @[{filename = \"%s\";@\n\ diff --git a/compiler/scalc/to_c.ml b/compiler/scalc/to_c.ml index 8064b6dd..109769ec 100644 --- a/compiler/scalc/to_c.ml +++ b/compiler/scalc/to_c.ml @@ -452,7 +452,7 @@ let rec format_statement catala_fatal_error_raised.position.end_column = %d;@,\ longjmp(catala_fatal_error_jump_buffer, 0);" (match e with - | ConflictError -> "catala_conflict" + | ConflictError _ -> "catala_conflict" | EmptyError -> "catala_empty" | NoValueProvided -> "catala_no_value_provided" | Crash -> "catala_crash") diff --git a/compiler/scalc/to_python.ml b/compiler/scalc/to_python.ml index 1606a1a9..8886a399 100644 --- a/compiler/scalc/to_python.ml +++ b/compiler/scalc/to_python.ml @@ -258,7 +258,7 @@ let format_func_name (fmt : Format.formatter) (v : FuncName.t) : unit = let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit = let pos = Mark.get exc in match Mark.remove exc with - | ConflictError -> + | ConflictError _ -> Format.fprintf fmt "ConflictError(@[SourcePosition(@[filename=\"%s\",@ \ start_line=%d,@ start_column=%d,@ end_line=%d,@ end_column=%d,@ \ diff --git a/compiler/scalc/to_r.ml b/compiler/scalc/to_r.ml index f56ceb07..4a3dcde2 100644 --- a/compiler/scalc/to_r.ml +++ b/compiler/scalc/to_r.ml @@ -249,7 +249,7 @@ let format_func_name (fmt : Format.formatter) (v : FuncName.t) : unit = let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit = let pos = Mark.get exc in match Mark.remove exc with - | ConflictError -> + | ConflictError _ -> Format.fprintf fmt "catala_conflict_error(@[catala_position(@[filename=\"%s\",@ start_line=%d,@ start_column=%d,@ end_line=%d,@ \ @@ -270,7 +270,7 @@ let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit = let format_exception_name (fmt : Format.formatter) (exc : except) : unit = match exc with - | ConflictError -> Format.fprintf fmt "catala_conflict_error" + | ConflictError _ -> Format.fprintf fmt "catala_conflict_error" | EmptyError -> Format.fprintf fmt "catala_empty_error" | Crash -> Format.fprintf fmt "catala_crash" | NoValueProvided -> Format.fprintf fmt "catala_no_value_provided_error" diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml index 5e2d8184..d61ca201 100644 --- a/compiler/shared_ast/definitions.ml +++ b/compiler/shared_ast/definitions.ml @@ -383,7 +383,12 @@ module Op = struct end type 'a operator = 'a Op.t -type except = ConflictError | EmptyError | NoValueProvided | Crash + +type except = + | ConflictError of Pos.t list + | EmptyError + | NoValueProvided + | Crash (** {2 Markings} *) diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index 1a510bda..e03e578f 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -59,7 +59,15 @@ let print_log lang entry infos pos e = Message.emit_log "%s%a %a" !indent_str Print.log_entry entry Print.uid_list infos -exception CatalaException of except +exception CatalaException of except * Pos.t + +let () = + Printexc.register_printer (function + | CatalaException (e, _pos) -> + Some + (Format.asprintf "uncaught exception %a raised during interpretation" + Print.except e) + | _ -> None) (* Todo: this should be handled early when resolving overloads. Here we have proper structural equality, but the OCaml backend for example uses the @@ -372,7 +380,7 @@ let rec evaluate_operator List.filter_map (fun e -> try Some (evaluate_expr (Expr.unthunk_term_nobox e m)) - with CatalaException EmptyError -> None) + with CatalaException (EmptyError, _) -> None) excepts with | [] -> ( @@ -381,7 +389,7 @@ let rec evaluate_operator | ELit (LBool true) -> Mark.remove (evaluate_expr (Expr.unthunk_term_nobox cons (Mark.get cons))) - | ELit (LBool false) -> raise (CatalaException EmptyError) + | ELit (LBool false) -> raise (CatalaException (EmptyError, pos)) | _ -> Message.raise_spanned_error pos "Default justification has not been reduced to a boolean at \ @@ -389,14 +397,7 @@ let rec evaluate_operator %a@." Expr.format just) | [e] -> Mark.remove e - | es -> - Message.raise_multispanned_error - (List.map - (fun except -> - Some "This consequence has a valid justification:", Expr.pos except) - es) - "There is a conflict between multiple valid consequences for assigning \ - the same variable.") + | es -> raise (CatalaException (ConflictError (List.map Expr.pos es), pos))) | HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> ( let valid_exceptions = ListLabels.filter exps ~f:(function @@ -432,7 +433,8 @@ let rec evaluate_operator && EnumConstructor.equal cons Expr.some_constr -> e | [_] -> err () - | _ -> raise (CatalaException ConflictError)) + | excs -> + raise (CatalaException (ConflictError (List.map Expr.pos excs), pos))) | ( ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int | ToRat_mon | ToMoney_rat | Round_rat | Round_mon | Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Sub_int_int | Sub_rat_rat @@ -567,7 +569,7 @@ and val_to_runtime : let tys = List.map (fun a -> Expr.maybe_ty (Mark.get a)) args in val_to_runtime eval_expr ctx tret (try eval_expr ctx (EApp { f = v; args; tys }, m) - with CatalaException EmptyError -> raise Runtime.EmptyError) + with CatalaException (EmptyError, _) -> raise Runtime.EmptyError) | targ :: targs -> Obj.repr (fun x -> curry (runtime_to_val eval_expr ctx m targ x :: acc) targs) @@ -756,8 +758,7 @@ let rec evaluate_expr : | EEmptyError, _ -> Message.raise_spanned_error (Expr.pos e') "This variable evaluated to an empty term (no rule that defined it \ - applied in this situation): %a" - Expr.format e + applied in this situation)" | e -> e) | EDefault { excepts; just; cons } -> ( let excepts = List.map (evaluate_expr ctx lang) excepts in @@ -774,18 +775,17 @@ let rec evaluate_expr : evaluation (should not happen if the term was well-typed") | 1 -> List.find (fun sub -> not (is_empty_error sub)) excepts | _ -> - Message.raise_multispanned_error - (List.map - (fun except -> - Some "This consequence has a valid justification:", Expr.pos except) - (List.filter (fun sub -> not (is_empty_error sub)) excepts)) - "There is a conflict between multiple valid consequences for assigning \ - the same variable.") + let poslist = + List.filter_map + (fun ex -> if is_empty_error ex then None else Some (Expr.pos ex)) + excepts + in + raise (CatalaException (ConflictError poslist, pos))) | EPureDefault e -> evaluate_expr ctx lang e - | ERaise exn -> raise (CatalaException exn) + | ERaise exn -> raise (CatalaException (exn, pos)) | ECatch { body; exn; handler } -> ( try evaluate_expr ctx lang body - with CatalaException caught when Expr.equal_except caught exn -> + with CatalaException (caught, _) when Expr.equal_except caught exn -> evaluate_expr ctx lang handler) | _ -> . @@ -886,6 +886,25 @@ let delcustom e = nodes. *) Expr.unbox (f e) +let interp_failure_message ~pos = function + | NoValueProvided -> + Message.raise_spanned_error pos + "This variable evaluated to an empty term (no rule that defined it \ + applied in this situation)" + | ConflictError cpos -> + Message.raise_multispanned_error + (List.map + (fun pos -> Some "This consequence has a valid justification:", pos) + cpos) + "There is a conflict between multiple valid consequences for assigning \ + the same variable." + | Crash -> + (* This constructor seems to be never used *) + Message.raise_spanned_error pos "Internal error, the interpreter crashed" + | EmptyError -> + Message.raise_spanned_error pos + "Internal error, a variable without valid definition escaped" + let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list = let e = Expr.unbox @@ Program.to_expr p s in @@ -956,6 +975,8 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list List.map (fun (fld, e) -> StructField.get_info fld, e) (StructField.Map.bindings fields) + | exception CatalaException (except, pos) -> + interp_failure_message ~pos except | _ -> Message.raise_spanned_error (Expr.pos e) "The interpretation of a program should always yield a struct \ @@ -1011,6 +1032,8 @@ let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list List.map (fun (fld, e) -> StructField.get_info fld, e) (StructField.Map.bindings fields) + | exception CatalaException (except, pos) -> + interp_failure_message ~pos except | _ -> Message.raise_spanned_error (Expr.pos e) "The interpretation of a program should always yield a struct \ diff --git a/compiler/shared_ast/interpreter.mli b/compiler/shared_ast/interpreter.mli index fa85f788..d52aaa87 100644 --- a/compiler/shared_ast/interpreter.mli +++ b/compiler/shared_ast/interpreter.mli @@ -20,7 +20,7 @@ open Catala_utils open Definitions -exception CatalaException of except +exception CatalaException of except * Pos.t val evaluate_operator : ((((_, _, _) interpr_kind as 'a), 'm) gexpr -> ('a, 'm) gexpr) -> diff --git a/compiler/shared_ast/optimizations.ml b/compiler/shared_ast/optimizations.ml index 6a3c670c..99c29c81 100644 --- a/compiler/shared_ast/optimizations.ml +++ b/compiler/shared_ast/optimizations.ml @@ -88,7 +88,10 @@ let rec optimize_expr : (* We proceed bottom-up, first apply on the subterms *) let e = Expr.map ~f:(optimize_expr ctx) ~op:Fun.id e in let mark = Mark.get e in - (* Then reduce the parent node *) + (* Fixme: when removing enclosing expressions, it would be better if we were + able to keep the inner position (see the division_by_zero test) *) + (* Then reduce the parent node (this is applied through Box.apply, therefore + delayed to unbinding time: no need to be concerned about reboxing) *) let reduce (e : ((a, b) dcalc_lcalc, 'm) gexpr) = (* Todo: improve the handling of eapp(log,elit) cases here, it obfuscates the matches and the log calls are not preserved, which would be a good diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index dda7fc0e..268221d8 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -351,7 +351,7 @@ let except (fmt : Format.formatter) (exn : except) : unit = op_style fmt (match exn with | EmptyError -> "EmptyError" - | ConflictError -> "ConflictError" + | ConflictError _ -> "ConflictError" | Crash -> "Crash" | NoValueProvided -> "NoValueProvided")