Cleanup a bit and improve the error messages

12 files changed, 91 insertions, 82 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index f7d08fdb..985fb470 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
           ^ string_of_int (List.length types)
           ^ " type arguments"
         in
-        log#serror err;
+        save_error __FILE__ __LINE__ None err;
         Result.Error (types, err))
       else
         let types = List.combine filter types in
@@ -1884,6 +1884,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   let meta = body.meta in
   sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
   sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
+
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
   let name =
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e593ae75..a158ed9a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
             if bid' = bid then (
               (* Sanity check *)
               let expected_ty = ty in
-              if nv.ty <> expected_ty then (
-                log#serror
-                  ("give_back_value: improper type:\n- expected: "
-                 ^ ty_to_string ctx ty ^ "\n- received: "
-                 ^ ty_to_string ctx nv.ty);
+              if nv.ty <> expected_ty then
                 craise __FILE__ __LINE__ meta
-                  "Value given back doesn't have the proper type");
+                  ("Value given back doesn't have the proper type:\n\
+                    - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
+                 ^ ty_to_string ctx nv.ty);
               (* Replace *)
               set_replaced ();
               nv.value)
@@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                * see the comment at the level of the definition of
                * {!typed_avalue} *)
               let _, expected_ty, _ = ty_get_ref ty in
-              if nv.ty <> expected_ty then (
-                log#serror
-                  ("give_back_avalue_to_same_abstraction: improper type:\n\
+              if nv.ty <> expected_ty then
+                craise __FILE__ __LINE__ meta
+                  ("Value given back doesn't have the proper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise __FILE__ __LINE__ meta
-                  "Value given back doesn't have the proper type");
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
@@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
       match lookup_borrow_opt ek_all l ctx with
       | None -> () (* Ok *)
       | Some _ ->
-          log#lerror
+          log#ltrace
             (lazy
               (fun_name ^ ": " ^ BorrowId.to_string l
              ^ ": borrow didn't disappear:\n- original context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx0
               ^ "\n\n- new context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-          craise __FILE__ __LINE__ meta "Borrow not eliminated"
+          internal_error __FILE__ __LINE__ meta
     in
     match lookup_loan_opt meta ek_all l ctx with
     | None -> () (* Ok *)
     | Some _ ->
-        log#lerror
+        log#ltrace
           (lazy
             (fun_name ^ ": " ^ BorrowId.to_string l
            ^ ": loan didn't disappear:\n- original context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx0
             ^ "\n\n- new context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-        craise __FILE__ __LINE__ meta "Loan not eliminated"
+        internal_error __FILE__ __LINE__ meta
   in
   unit_to_cm_fun check_disappeared
 
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6e65b11d..a01be046 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
       sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
       default
   | _ ->
-      log#lerror
+      log#ltrace
         (lazy
           ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1
          ^ "\n- ty2: " ^ show_ty ty2));
-      craise __FILE__ __LINE__ meta "Unreachable"
+      internal_error __FILE__ __LINE__ meta
 
 (** Check if two different projections intersect. This is necessary when
     giving a symbolic value to an abstraction: we need to check that
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index f2c0bcb1..ab3daa72 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
       let nv = update v in
       (* Type checking *)
       if nv.ty <> v.ty then (
-        log#lerror
+        log#ltrace
           (lazy
             ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
            ^ show_ety v.ty));
@@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           let pe = "- pe: " ^ show_projection_elem pe in
           let v = "- v:\n" ^ show_value v in
           let ty = "- ty:\n" ^ show_ety ty in
-          log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
-          craise __FILE__ __LINE__ meta "Inconsistent projection")
+          craise __FILE__ __LINE__ meta
+            ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
 
 (** Generic function to access (read/write) the value at a given place.
 
@@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if !Config.sanity_checks then
-        if ctx1 <> ctx then (
-          let msg =
-            "Unexpected environment update:\nNew environment:\n"
-            ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
-          in
-          log#serror msg;
-          craise __FILE__ __LINE__ meta "Unexpected environment update");
+      (if !Config.sanity_checks then
+         if ctx1 <> ctx then
+           let msg =
+             "Unexpected environment update:\nNew environment:\n"
+             ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
+           in
+           craise __FILE__ __LINE__ meta msg);
       Ok read_value
 
 let read_place (meta : Meta.meta) (access : access_kind) (p : place)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 6e86e6a4..3993d845 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
               meta);
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
-          log#lerror
+          log#ltrace
             (lazy
               ("apply_proj_borrows: unexpected inputs:\n- input value: "
               ^ typed_value_to_string ~meta:(Some meta) ctx v
               ^ "\n- proj rty: " ^ ty_to_string ctx ty));
-          craise __FILE__ __LINE__ meta "Unreachable"
+          internal_error __FILE__ __LINE__ meta
     in
     { value; ty }
 
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 642d7a37..2ccf3ad4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
           "find_info: could not find the representant of borrow "
           ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
         in
-        log#serror err;
         craise __FILE__ __LINE__ meta err
   in
 
@@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
         | AIgnored, _ -> ()
         | _ ->
-            log#lerror
+            log#ltrace
               (lazy
                 ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
                ^ "\n- value: "
                 ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
                 ^ "\n- type: " ^ ty_to_string ctx atv.ty));
-            craise __FILE__ __LINE__ meta "Erroneous typing");
+            internal_error __FILE__ __LINE__ meta);
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
     end
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 416f3a07..6161f2f2 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -283,7 +283,9 @@ let () =
       if !Errors.error_list <> [] then (
         List.iter
           (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
-          !Errors.error_list;
+          (* Reverse the list of error messages so that we print them from the
+             earliest to the latest. *)
+          (List.rev !Errors.error_list);
         exit 1);
 
       (* Print total elapsed time *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 0b39f64a..a46ef79c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
       method! visit_Sequence env st1 st2 =
         match st1.content with
         | Loop _ ->
-            sanity_check __FILE__ __LINE__
+            cassert __FILE__ __LINE__
               (statement_has_no_loop_break_continue st2)
-              st2.meta;
+              st2.meta "Sequences of loops are not supported yet";
             (replace_breaks_with st1 st2).content
         | _ -> super#visit_Sequence env st1 st2
     end
@@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
 
 let apply_passes (crate : crate) : crate =
   let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
+  (* Attempt to apply a pass: if it fails we replace the body by [None] *)
+  let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
+    try pass f
+    with CFailure (_, _) ->
+      (* The error was already registered, we don't need to register it twice.
+         However, we replace the body of the function, and save an error to
+         report to the user the fact that we will ignore the function body *)
+      let fmt = Print.Crate.crate_to_fmt_env crate in
+      let name = Print.name_to_string fmt f.name in
+      save_error __FILE__ __LINE__ (Some f.meta)
+        ("Ignoring the body of '" ^ name ^ "' because of previous error");
+      { f with body = None }
+  in
   let fun_decls =
     List.fold_left
-      (fun fl pass -> FunDeclId.Map.map pass fl)
+      (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl)
       crate.fun_decls passes
   in
   let crate = { crate with fun_decls } in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dad1aea3..51286553 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,4 +1,5 @@
 include Charon.PrintUtils
+include Charon.PrintTypes
 include Charon.PrintLlbcAst
 open Charon.PrintTypes
 open Charon.PrintExpressions
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 098e2564..27044c27 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx)
         get_adt_field_types meta ctx.type_decls type_id av.variant_id generics
       in
       let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
-        if ty <> v.ty then (
+        if ty <> v.ty then
           (* TODO: we need to normalize the types *)
-          log#serror
-            ("check_typed_pattern: not the same types:" ^ "\n- ty: "
-           ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
-          craise __FILE__ __LINE__ meta "Inconsistent types");
+          craise __FILE__ __LINE__ meta
+            ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: "
+           ^ show_ty v.ty);
         check_typed_pattern meta ctx v
       in
       (* Check the field types: check that the field patterns have the expected
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 607da445..93f9ef75 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3867,11 +3867,9 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
       with CFailure (meta, _) ->
         let env = PrintPure.decls_ctx_to_fmt_env ctx in
         let name = PrintPure.name_to_string env a.name in
-        let () =
-          save_error __FILE__ __LINE__ meta
-            ("Could not translate type decl '" ^ name
-           ^ "' because of previous error")
-        in
+        save_error __FILE__ __LINE__ meta
+          ("Could not translate type decl '" ^ name
+         ^ "' because of previous error");
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2fcf5b43..870f8a22 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -204,10 +204,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
   with CFailure (meta, _) ->
     let name = name_to_string trans_ctx fdef.name in
-    let () =
-      save_error __FILE__ __LINE__ meta
-        ("Could not translate function '" ^ name ^ "' because of previous error")
-    in
+    save_error __FILE__ __LINE__ meta
+      ("Could not translate the function '" ^ name
+     ^ "' because of previous error");
     None
 
 (* TODO: factor out the return type *)
@@ -231,6 +230,7 @@ let translate_crate_to_pure (crate : crate) :
     Pure.TypeDeclId.Map.of_list
       (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
   in
+
   (* Compute the decomposed fun sigs for the whole crate *)
   let fun_dsigs =
     FunDeclId.Map.of_list
@@ -243,11 +243,9 @@ let translate_crate_to_pure (crate : crate) :
                    trans_ctx fdef )
            with CFailure (meta, _) ->
              let name = name_to_string trans_ctx fdef.name in
-             let () =
-               save_error __FILE__ __LINE__ meta
-                 ("Could not translate function signature '" ^ name
-                ^ "' because of previous error")
-             in
+             save_error __FILE__ __LINE__ meta
+               ("Could not translate the function signature of '" ^ name
+              ^ "' because of previous error");
              None)
          (FunDeclId.Map.values crate.fun_decls))
   in
@@ -266,11 +264,9 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
         with CFailure (meta, _) ->
           let name = name_to_string trans_ctx a.name in
-          let () =
-            save_error __FILE__ __LINE__ meta
-              ("Could not translate trait decl '" ^ name
-             ^ "' because of previous error")
-          in
+          save_error __FILE__ __LINE__ meta
+            ("Could not translate the trait declaration '" ^ name
+           ^ "' because of previous error");
           None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
   in
@@ -282,11 +278,9 @@ let translate_crate_to_pure (crate : crate) :
         try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
         with CFailure (meta, _) ->
           let name = name_to_string trans_ctx a.name in
-          let () =
-            save_error __FILE__ __LINE__ meta
-              ("Could not translate trait impl '" ^ name
-             ^ "' because of previous error")
-          in
+          save_error __FILE__ __LINE__ meta
+            ("Could not translate the trait instance '" ^ name
+           ^ "' because of previous error");
           None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
@@ -516,12 +510,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     let global =
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (meta, _) ->
-        let () =
-          let name = name_to_string ctx.trans_ctx global.name in
-          save_error __FILE__ __LINE__ meta
-            ("Could not translate global '" ^ name
-           ^ "' because of previous error")
-        in
+        let name = name_to_string ctx.trans_ctx global.name in
+        save_error __FILE__ __LINE__ meta
+          ("Could not translate the global declaration '" ^ name
+         ^ "' because of previous error");
         None
     in
     Extract.extract_global_decl ctx fmt global body config.interface
@@ -778,22 +770,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     | TypeGroup (RecGroup ids) ->
         if config.extract_types then export_types_group true ids
     | FunGroup (NonRecGroup id) -> (
-        (* Lookup *)
-        let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+        (* Lookup - the translated function may not be in the map if we had
+           to ignore it because of errors *)
+        let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in
         (* Special case: we skip trait method *declarations* (we will
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match pure_fun.f.Pure.kind with
-        | TraitItemDecl _ -> ()
-        | _ ->
-            (* Translate *)
-            export_functions_group [ pure_fun ])
+        match pure_fun with
+        | Some pure_fun -> (
+            match pure_fun.f.Pure.kind with
+            | TraitItemDecl _ -> ()
+            | _ ->
+                (* Translate *)
+                export_functions_group [ pure_fun ])
+        | None -> ())
     | FunGroup (RecGroup ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
         let pure_funs =
-          List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+          List.filter_map
+            (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs)
+            ids
         in
         (* Translate *)
         export_functions_group pure_funs
@@ -951,7 +949,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
 
   (* Some logging *)
-  log#linfo (lazy ("Generated: " ^ fi.filename));
+  if !Errors.error_list <> [] then
+    log#linfo
+      (lazy ("Generated the partial file (because of errors): " ^ fi.filename))
+  else log#linfo (lazy ("Generated: " ^ fi.filename));
 
   (* Flush and close the file *)
   close_out out