Support for renaming using the rename attribute in charon (#239)

* support for renaming using the rename attribute in charon

* support for global decl

* add support for renaming field

* applied suggested changes and began adding support for variant

* finished support for renaming variant

* applied suggested changes

* add tests

* fixed variant and field renaming

* update charon-pin

* update flake.lock

* Update the charon pin

* Fix an issue with renaming trait method implementations

* Fix an issue with the renaming of trait implementations

* Fix an issue when renaming enumerations

* Update the Charon pin

* Fix the F* tests

* Fix an issue with the spans for the loops

* Fix the tests

* Update a comment

* Use fuel in the coq tests

* Generate the template decreases clauses by default

---------

Co-authored-by: Escherichia <escherichia@charlotte>
Co-authored-by: Son Ho <hosonmarc@gmail.com>

1 files changed, 36 insertions, 23 deletions

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 8b95f729..543b2bee 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -224,7 +224,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   let register_var (ctx : pn_ctx) (v : var) : pn_ctx =
     sanity_check __FILE__ __LINE__
       (not (VarId.Map.mem v.id ctx.pure_vars))
-      def.span;
+      def.item_meta.span;
     match v.basename with
     | None -> ctx
     | Some name ->
@@ -614,7 +614,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
         | App _ -> (
             let app, args = destruct_apps e in
             let ignore () =
-              mk_apps def.span
+              mk_apps def.item_meta.span
                 (self#visit_texpression env app)
                 (List.map (self#visit_texpression env) args)
             in
@@ -759,7 +759,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
             else if variant_id = result_fail_id then
               (* Fail case *)
               self#visit_expression env rv.e
-            else craise __FILE__ __LINE__ def.span "Unexpected"
+            else craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
         | App _ ->
             (* This might be the tuple case *)
             if not monadic then
@@ -914,7 +914,7 @@ let inline_useless_var_reassignments (ctx : trans_ctx) ~(inline_named : bool)
               } ) ->
             (* Second case: we deconstruct a structure with one field that we will
                extract as tuple. *)
-            let adt_id, _ = PureUtils.ty_as_adt def.span re.ty in
+            let adt_id, _ = PureUtils.ty_as_adt def.item_meta.span re.ty in
             (* Update the rhs (we may perform substitutions inside, and it is
              * better to do them *before* we inline it *)
             let re = self#visit_texpression env re in
@@ -1152,7 +1152,7 @@ let simplify_let_then_ok _ctx (def : fun_decl) =
               | Some e ->
                   if match_pattern_and_expr lv e then
                     (* We need to wrap the right-value in a ret *)
-                    (mk_result_ok_texpression def.span rv).e
+                    (mk_result_ok_texpression def.item_meta.span rv).e
                   else not_simpl_e
               | None ->
                   if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
@@ -1203,13 +1203,14 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 let fields =
                   match adt_decl.kind with
                   | Enum _ | Alias _ | Opaque ->
-                      craise __FILE__ __LINE__ def.span "Unreachable"
+                      craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
                   | Struct fields -> fields
                 in
                 let num_fields = List.length fields in
                 (* In order to simplify, there must be as many arguments as
                  * there are fields *)
-                sanity_check __FILE__ __LINE__ (num_fields > 0) def.span;
+                sanity_check __FILE__ __LINE__ (num_fields > 0)
+                  def.item_meta.span;
                 if num_fields = List.length args then
                   (* We now need to check that all the arguments are of the form:
                    * [x.field] for some variable [x], and where the projection
@@ -1249,7 +1250,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                         (List.for_all
                            (fun (generics1, _) -> generics1 = generics)
                            args)
-                        def.span;
+                        def.item_meta.span;
                       { e with e = Var x })
                     else super#visit_texpression env e
                   else super#visit_texpression env e
@@ -1406,7 +1407,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
             in
             sanity_check __FILE__ __LINE__
               (fun_sig_info_is_wf loop_fwd_sig_info)
-              def.span;
+              def.item_meta.span;
 
             let inputs_tys =
               let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in
@@ -1449,7 +1450,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
                 sanity_check __FILE__ __LINE__
                   (loop_fwd_effect_info.stateful
                   = Option.is_some loop.input_state)
-                  def.span;
+                  def.item_meta.span;
                 match loop.input_state with
                 | None -> ([], [])
                 | Some input_state ->
@@ -1486,17 +1487,20 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
               match fuel_vars with
               | None -> loop.loop_body
               | Some (fuel0, fuel) ->
-                  SymbolicToPure.wrap_in_match_fuel def.span fuel0 fuel
-                    loop.loop_body
+                  SymbolicToPure.wrap_in_match_fuel def.item_meta.span fuel0
+                    fuel loop.loop_body
             in
 
             let loop_body = { inputs; inputs_lvs; body = loop_body } in
+            (* We retrieve the meta information from the parent function
+               *but* replace its span with the span of the loop *)
+            let item_meta = { def.item_meta with span = loop.span } in
 
             let loop_def : fun_decl =
               {
                 def_id = def.def_id;
                 is_local = def.is_local;
-                span = loop.span;
+                item_meta;
                 kind = def.kind;
                 backend_attributes = def.backend_attributes;
                 num_loops;
@@ -1581,9 +1585,10 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 match aid with
                 | BoxNew ->
                     let arg, args = Collections.List.pop args in
-                    mk_apps def.span arg args
+                    mk_apps def.item_meta.span arg args
                 | BoxFree ->
-                    sanity_check __FILE__ __LINE__ (args = []) def.span;
+                    sanity_check __FILE__ __LINE__ (args = [])
+                      def.item_meta.span;
                     mk_unit_rvalue
                 | SliceIndexShared | SliceIndexMut | ArrayIndexShared
                 | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
@@ -1777,8 +1782,10 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               *)
               (* TODO: this information should be computed in SymbolicToPure and
                * store in an enum ("monadic" should be an enum, not a bool). *)
-              let re_ty = Option.get (opt_destruct_result def.span re.ty) in
-              sanity_check __FILE__ __LINE__ (lv.ty = re_ty) def.span;
+              let re_ty =
+                Option.get (opt_destruct_result def.item_meta.span re.ty)
+              in
+              sanity_check __FILE__ __LINE__ (lv.ty = re_ty) def.item_meta.span;
               let err_vid = fresh_id () in
               let err_var : var =
                 {
@@ -1790,7 +1797,9 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               let err_pat = mk_typed_pattern_from_var err_var None in
               let fail_pat = mk_result_fail_pattern err_pat.value lv.ty in
               let err_v = mk_texpression_from_var err_var in
-              let fail_value = mk_result_fail_texpression def.span err_v e.ty in
+              let fail_value =
+                mk_result_fail_texpression def.item_meta.span err_v e.ty
+              in
               let fail_branch = { pat = fail_pat; branch = fail_value } in
               let success_pat = mk_result_ok_pattern lv in
               let success_branch = { pat = success_pat; branch = e } in
@@ -2031,7 +2040,9 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
         ^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix)
         ^ "\n"));
     let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
-    sanity_check __FILE__ __LINE__ (Option.is_some decl.loop_id) decl.span;
+    sanity_check __FILE__ __LINE__
+      (Option.is_some decl.loop_id)
+      decl.item_meta.span;
 
     let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
 
@@ -2183,7 +2194,9 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
           in
 
           let fwd_info = { fwd_info; effect_info; ignore_output } in
-          sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf fwd_info) decl.span;
+          sanity_check __FILE__ __LINE__
+            (fun_sig_info_is_wf fwd_info)
+            decl.item_meta.span;
           let signature =
             {
               generics;
@@ -2249,17 +2262,17 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
                                 in
 
                                 (* Rebuild *)
-                                mk_apps decl.span e_app args)
+                                mk_apps decl.item_meta.span e_app args)
                         | _ ->
                             let e_app = self#visit_texpression env e_app in
                             let args =
                               List.map (self#visit_texpression env) args
                             in
-                            mk_apps decl.span e_app args)
+                            mk_apps decl.item_meta.span e_app args)
                     | _ ->
                         let e_app = self#visit_texpression env e_app in
                         let args = List.map (self#visit_texpression env) args in
-                        mk_apps decl.span e_app args)
+                        mk_apps decl.item_meta.span e_app args)
                 | _ -> super#visit_texpression env e
             end
           in