Improve error handling

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-2909a3c23b1abbc780aad5dca76a0f101fedc6ea
+4925c99ccab9613d6af784dd52d69fccaf3f5f5d

src/Config.ml

@@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a =
   | None -> default
   | Some _ -> f ()
 
+(** Print the source code span which emitted errors *)
+let print_error_emitters = ref false
+
 (** Print all the external definitions which are not listed in the builtin functions *)
 let print_unknown_externals = ref false
 

src/Errors.ml

@@ -8,12 +8,20 @@ let raw_span_to_string (raw_span : Meta.raw_span) =
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
   in
-  "Source: '" ^ file ^ "', lines "
+  "'" ^ file ^ "', lines "
   ^ loc_to_string raw_span.beg_loc
   ^ "-"
   ^ loc_to_string raw_span.end_loc
 
-let span_to_string (span : Meta.span) = raw_span_to_string span.span
+let span_to_string (span : Meta.span) =
+  let generated_from =
+    match span.generated_from_span with
+    | None -> ""
+    | Some span ->
+        "; this code is generated from a macro invocation at: "
+        ^ raw_span_to_string span
+  in
+  "Source: " ^ raw_span_to_string span.span ^ generated_from
 
 let format_error_message (span : Meta.span option) (msg : string) =
   let span =
@@ -28,35 +36,61 @@ let format_error_message_with_file_line (file : string) (line : int)
   "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n"
   ^ format_error_message span msg
 
-exception CFailure of (Meta.span option * string)
+type cfailure = {
+  span : Meta.span option;
+  file : string;
+  line : int;
+  msg : string;
+}
+[@@deriving show]
 
-let error_list : (Meta.span option * string) list ref = ref []
+exception CFailure of cfailure
 
-let push_error (span : Meta.span option) (msg : string) =
-  error_list := (span, msg) :: !error_list
+let error_list : (string * int * Meta.span option * string) list ref = ref []
+
+let push_error (file : string) (line : int) (span : Meta.span option)
+    (msg : string) =
+  error_list := (file, line, span, msg) :: !error_list
 
 (** Register an error, and throw an exception if [throw] is true *)
-let save_error (file : string) (line : int) (span : Meta.span option)
+let save_error_opt_span (file : string) (line : int) (span : Meta.span option)
     (msg : string) =
-  push_error span msg;
+  push_error file line span msg;
   if !Config.fail_hard then (
     let msg = format_error_message_with_file_line file line span msg in
     log#serror (msg ^ "\n");
     raise (Failure msg))
 
+let save_error (file : string) (line : int) (span : Meta.span) (msg : string) =
+  save_error_opt_span file line (Some span) msg
+
 let craise_opt_span (file : string) (line : int) (span : Meta.span option)
     (msg : string) =
   if !Config.fail_hard then (
     let msg = format_error_message_with_file_line file line span msg in
     log#serror (msg ^ "\n");
     raise (Failure msg))
   else
-    let () = push_error span msg in
-    raise (CFailure (span, msg))
+    let () = push_error file line span msg in
+    raise (CFailure { span; file; line; msg })
 
 let craise (file : string) (line : int) (span : Meta.span) (msg : string) =
   craise_opt_span file line (Some span) msg
 
+(** Throw an exception, but do not register an error *)
+let craise_opt_span_silent (file : string) (line : int)
+    (span : Meta.span option) (msg : string) =
+  if !Config.fail_hard then
+    let msg = format_error_message_with_file_line file line span msg in
+    raise (Failure msg)
+  else
+    let () = push_error file line span msg in
+    raise (CFailure { span; file; line; msg })
+
+let craise_silent (file : string) (line : int) (span : Meta.span) (msg : string)
+    =
+  craise_opt_span_silent file line (Some span) msg
+
 (** Lazy assert *)
 let classert_opt_span (file : string) (line : int) (b : bool)
     (span : Meta.span option) (msg : string Lazy.t) =
@@ -103,3 +137,26 @@ let cassert_warn (file : string) (line : int) (b : bool) (span : Meta.span)
 
 let exec_raise = craise
 let exec_assert = cassert
+
+let silent_unwrap_opt_span (file : string) (line : int)
+    (span : Meta.span option) (x : 'a option) : 'a =
+  match x with
+  | Some x -> x
+  | None ->
+      craise_opt_span_silent file line span
+        "Internal error: please file an issue"
+
+let silent_unwrap (file : string) (line : int) (span : Meta.span)
+    (x : 'a option) : 'a =
+  silent_unwrap_opt_span file line (Some span) x
+
+let opt_raise_opt_span (file : string) (line : int) (span : Meta.span option)
+    (msg : string) : unit =
+  if !Config.fail_hard then (
+    let msg = format_error_message_with_file_line file line span msg in
+    log#serror (msg ^ "\n");
+    raise (Failure msg))
+
+let opt_raise (file : string) (line : int) (span : Meta.span) (msg : string) :
+    unit =
+  opt_raise_opt_span file line (Some span) msg

src/Main.ml

@@ -100,6 +100,10 @@ let () =
 
   let spec_ls =
     [
+      ( "-print-error-emitters",
+        Arg.Set print_error_emitters,
+        " Whenever reporting an error, print the span of the source code of \
+         Aeneas which emitted the error" );
       ( "-borrow-check",
         Arg.Set borrow_check,
         " Only borrow-check the program and do not generate any translation" );
@@ -496,26 +500,23 @@ let () =
               @ trait_impls)));
         ());
 
-      (* There may be exceptions to catch *)
-      (try
-         (* Apply the pre-passes *)
-         let m = Aeneas.PrePasses.apply_passes m in
+      (* Apply the pre-passes *)
+      let m = Aeneas.PrePasses.apply_passes m in
 
-         (* Test the unit functions with the concrete interpreter *)
-         if !test_unit_functions then Test.test_unit_functions m;
+      (* Test the unit functions with the concrete interpreter *)
+      if !test_unit_functions then Test.test_unit_functions m;
 
-         (* Translate or borrow-check the crate *)
-         if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m
-         else Aeneas.Translate.translate_crate filename dest_dir m
-       with Errors.CFailure (_, _) ->
-         (* In theory it shouldn't happen, but there may be uncaught errors -
-            note that we let the [Failure] exceptions go through (they are
-            send if we use the option [-abort-on-error] *)
-         ());
+      (* Translate or borrow-check the crate *)
+      if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m
+      else Aeneas.Translate.translate_crate filename dest_dir m;
 
       if !Errors.error_list <> [] then (
         List.iter
-          (fun (span, msg) -> log#serror (Errors.format_error_message span msg))
+          (fun (file, line, span, msg) ->
+            if !print_error_emitters then
+              log#serror
+                (Errors.format_error_message_with_file_line file line span msg)
+            else log#serror (Errors.format_error_message span msg))
           (* Reverse the list of error messages so that we print them from the
              earliest to the latest. *)
           (List.rev !Errors.error_list);

src/PrePasses.ml

@@ -520,20 +520,165 @@ let filter_type_aliases (crate : crate) : crate =
         crate.declarations;
   }
 
+(** Whenever we write a string literal in Rust, rustc actually
+    introduces a constant of type [&str].
+    Generally speaking, because [str] is unsized, it doesn't
+    make sense to manipulate values of type [str] directly.
+    But in the context of Aeneas, it is reasonable to decompose
+    those literals into: a string stored in a local variable,
+    then a borrow of this variable.
+ *)
+let decompose_str_borrows (f : fun_decl) : fun_decl =
+  (* Map  *)
+  let body =
+    match f.body with
+    | Some body ->
+        let new_locals = ref [] in
+        let _, gen =
+          VarId.mk_stateful_generator_starting_at_id
+            (VarId.of_int (List.length body.locals.vars))
+        in
+        let fresh_local ty =
+          let local = { index = gen (); var_ty = ty; name = None } in
+          new_locals := local :: !new_locals;
+          local.index
+        in
+
+        (* Function to decompose a constant literal *)
+        let decompose_rvalue (span : Meta.span) (lv : place) (rv : rvalue)
+            (next : statement option) : raw_statement =
+          let new_statements = ref [] in
+
+          (* Visit the rvalue *)
+          let visitor =
+            object
+              inherit [_] map_statement as super
+
+              (* We have to visit all the constant operands.
+                 As we might need to replace them with borrows, while borrows
+                 are rvalues (i.e., not operands) we have to introduce two
+                 intermediate statements: the string initialization, then
+                 the borrow, that we can finally move.
+              *)
+              method! visit_Constant env cv =
+                match (cv.value, cv.ty) with
+                | ( CLiteral (VStr str),
+                    TRef (_, (TAdt (TBuiltin TStr, _) as str_ty), ref_kind) ) ->
+                    (* We need to introduce intermediate assignments *)
+                    (* First the string initialization *)
+                    let local_id =
+                      let local_id = fresh_local str_ty in
+                      let new_cv : constant_expr =
+                        { value = CLiteral (VStr str); ty = str_ty }
+                      in
+                      let st =
+                        {
+                          span;
+                          content =
+                            Assign
+                              ( { kind = PlaceBase local_id; ty = str_ty },
+                                Use (Constant new_cv) );
+                          comments_before = [];
+                        }
+                      in
+                      new_statements := st :: !new_statements;
+                      local_id
+                    in
+                    (* Then the borrow *)
+                    let local_id =
+                      let nlocal_id = fresh_local cv.ty in
+                      let bkind =
+                        match ref_kind with
+                        | RMut -> BMut
+                        | RShared -> BShared
+                      in
+                      let rv =
+                        RvRef ({ kind = PlaceBase local_id; ty = str_ty }, bkind)
+                      in
+                      let lv = { kind = PlaceBase nlocal_id; ty = cv.ty } in
+                      let st =
+                        {
+                          span;
+                          content = Assign (lv, rv);
+                          comments_before = [];
+                        }
+                      in
+                      new_statements := st :: !new_statements;
+                      nlocal_id
+                    in
+                    (* Finally we can move the value *)
+                    Move { kind = PlaceBase local_id; ty = cv.ty }
+                | _ -> super#visit_Constant env cv
+            end
+          in
+
+          let rv = visitor#visit_rvalue () rv in
+
+          (* Construct the sequence *)
+          let assign =
+            { span; content = Assign (lv, rv); comments_before = [] }
+          in
+          let statements, last =
+            match next with
+            | None -> (!new_statements, assign)
+            | Some st -> (assign :: !new_statements, st)
+          in
+          (* Note that the new statements are in reverse order *)
+          (List.fold_left
+             (fun st nst ->
+               { span; content = Sequence (nst, st); comments_before = [] })
+             last statements)
+            .content
+        in
+
+        (* Visit all the statements and decompose the literals *)
+        let visitor =
+          object
+            inherit [_] map_statement as super
+            method! visit_statement _ st = super#visit_statement st.span st
+
+            method! visit_Sequence span st1 st2 =
+              match st1.content with
+              | Assign (lv, rv) -> decompose_rvalue st1.span lv rv (Some st2)
+              | _ -> super#visit_Sequence span st1 st2
+
+            method! visit_Assign span lv rv = decompose_rvalue span lv rv None
+          end
+        in
+
+        let body_body = visitor#visit_statement body.body.span body.body in
+        Some
+          {
+            body with
+            body = body_body;
+            locals =
+              {
+                body.locals with
+                vars = body.locals.vars @ List.rev !new_locals;
+              };
+          }
+    | None -> None
+  in
+  { f with body }
+
 let apply_passes (crate : crate) : crate =
   let function_passes =
-    [ remove_loop_breaks crate; remove_shallow_borrows crate ]
+    [
+      remove_loop_breaks crate;
+      remove_shallow_borrows crate;
+      decompose_str_borrows;
+    ]
   in
   (* Attempt to apply a pass: if it fails we replace the body by [None] *)
   let apply_function_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
     try pass f
-    with CFailure (_, _) ->
+    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.item_meta.name in
-      save_error __FILE__ __LINE__ (Some f.item_meta.span)
+      save_error __FILE__ __LINE__ f.item_meta.span
         ("Ignoring the body of '" ^ name ^ "' because of previous error");
       { f with body = None }
   in