diff options
| -rw-r--r-- | compiler/Errors.ml | 60 | ||||
| -rw-r--r-- | compiler/Main.ml | 22 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 1 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 3 |
4 files changed, 31 insertions, 55 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 41e841f0..04fd708b 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -6,50 +6,38 @@ let meta_to_string (span : Meta.span) = "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-" ^ loc_to_string span.end_loc -let format_error_message (meta : Meta.meta) msg = - msg ^ "\n" ^ meta_to_string meta.span +let format_error_message (meta : Meta.meta option) (msg : string) = + let meta = + match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span + in + msg ^ meta + +let format_error_message_with_file_line (file : string) (line : int) + (meta : Meta.meta option) (msg : string) = + "In file:" ^ file ^ ", line:" ^ string_of_int line ^ "\n" + ^ format_error_message meta msg -exception CFailure of string +exception CFailure of (Meta.meta option * string) let error_list : (Meta.meta option * string) list ref = ref [] -let push_error (file : string) (line : int) (meta : Meta.meta option) - (msg : string) = - error_list := - (meta, msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line) - :: !error_list +let push_error (meta : Meta.meta option) (msg : string) = + error_list := (meta, msg) :: !error_list -let save_error (file : string) (line : int) ?(b : bool = true) +(** Register an error, and throw an exception if [throw] is true *) +let save_error (file : string) (line : int) ?(throw : bool = false) (meta : Meta.meta option) (msg : string) = - push_error file line meta msg; - match meta with - | Some m -> - if !Config.fail_hard && not b then - raise - (Failure - (format_error_message m - (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line))) - | None -> if !Config.fail_hard && not b then raise (Failure msg) + push_error meta msg; + if !Config.fail_hard && throw then + raise (Failure (format_error_message_with_file_line file line meta msg)) let craise_opt_meta (file : string) (line : int) (meta : Meta.meta option) (msg : string) = - match meta with - | Some m -> - if !Config.fail_hard then - raise - (Failure - (format_error_message m - (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line))) - else - let () = push_error file line (Some m) msg in - raise (CFailure msg) - | None -> - if !Config.fail_hard then - raise - (Failure (msg ^ "\n In file:" ^ file ^ "\n Line:" ^ string_of_int line)) - else - let () = push_error file line None msg in - raise (CFailure msg) + if !Config.fail_hard then + raise (Failure (format_error_message_with_file_line file line meta msg)) + else + let () = push_error meta msg in + raise (CFailure (meta, msg)) let craise (file : string) (line : int) (meta : Meta.meta) (msg : string) = craise_opt_meta file line (Some meta) msg @@ -69,7 +57,7 @@ let sanity_check_opt_meta (file : string) (line : int) b meta = cassert_opt_meta file line b meta "Internal error, please file an issue" let internal_error (file : string) (line : int) meta = - craise file line meta "Internal error, please report an issue" + craise file line meta "Internal error, please file an issue" let exec_raise = craise let exec_assert = cassert diff --git a/compiler/Main.ml b/compiler/Main.ml index 798bcec3..64d8ae2b 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -267,6 +267,7 @@ let () = definitions"; fail ()); + (* There may be exceptions to catch *) (try (* Apply the pre-passes *) let m = Aeneas.PrePasses.apply_passes m in @@ -276,24 +277,11 @@ let () = (* Translate the functions *) Aeneas.Translate.translate_crate filename dest_dir m - with Errors.CFailure msg -> + with Errors.CFailure (meta, msg) -> (* In theory it shouldn't happen, but there may be uncaught errors - - note that we let the Failure errors go through *) - (* The error should have been saved *) - let meta = - match !Errors.error_list with - | (m, msg') :: _ -> - (* The last saved message should be the current error - but - good to check *) - if msg = msg' then m else None - | _ -> (* Want to be safe here *) None - in - let msg = - match meta with - | None -> msg - | Some m -> Errors.format_error_message m msg - in - log#serror msg; + note that we let the [Failure] exceptions go through (they are + send if we use the option [-abort-on-error] *) + log#serror (Errors.format_error_message meta msg); exit 1); (* Print total elapsed time *) diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index c3afe1c4..4bc90872 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -325,6 +325,7 @@ let destruct_apps (e : texpression) : texpression * texpression list = let mk_app (meta : Meta.meta) (app : texpression) (arg : texpression) : texpression = let raise_or_return msg = + (* We shouldn't get there, so we save an error (and eventually raise an exception) *) save_error __FILE__ __LINE__ (Some meta) msg; let e = App (app, arg) in (* Dummy type - TODO: introduce an error type *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index aeb03c34..ccb4f585 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2892,8 +2892,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) ^ pure_ty_to_string ctx true_e.ty ^ "\n\nfalse_e.ty: " ^ pure_ty_to_string ctx false_e.ty)); - save_error __FILE__ __LINE__ ~b:(ty = false_e.ty) (Some ctx.fun_decl.meta) - "Internal error, please file an issue"; + sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.fun_decl.meta; { e; ty } | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : |