Merge pull request #88 from AeneasVerif/son/clashes

Improve the name generation for code extraction

1 files changed, 46 insertions, 18 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 794a1bfa..46f6a1ca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -19,7 +19,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
      only use their type for the fields of the records we generate for the trait
      declarations *)
   match def.f.kind with
-  | TraitMethodDecl _ -> ctx
+  | TraitItemDecl _ -> ctx
   | _ -> (
       (* Check if the function is builtin *)
       let builtin =
@@ -48,6 +48,9 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
           ctx_add (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
       | None ->
           (* Not builtin *)
+          (* If this is a trait method implementation, we prefix the name with the
+             name of the trait implementation. We need to do so because there
+             can be clashes otherwise. *)
           (* Register the decrease clauses, if necessary *)
           let register_decreases ctx def =
             if has_decreases_clause def then
@@ -1105,7 +1108,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   *)
   let ctx, trait_decl =
     match def.kind with
-    | TraitMethodProvided (decl_id, _) ->
+    | TraitItemProvided (decl_id, _) ->
         let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
         let ctx, _ = ctx_add_trait_self_clause ctx in
         let ctx = { ctx with is_provided_method = true } in
@@ -1204,9 +1207,14 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
-    def.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not def.is_local then
+       Some def.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+     name def.meta.span);
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1267,9 +1275,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
-    def.meta.span;
+    None def.meta.span;
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1322,9 +1330,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span fmt
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
-    def.meta.span;
+    None def.meta.span;
   F.pp_print_space fmt ();
   F.pp_open_hvbox fmt 0;
   F.pp_print_string fmt "syntax \"";
@@ -1364,7 +1372,12 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     in
     [ comment_pre ^ loop_comment ]
   in
-  extract_comment_with_span fmt comment def.meta.span
+  let name =
+    if !Config.extract_external_name_patterns && not def.is_local then
+      Some def.llbc_name
+    else None
+  in
+  extract_comment_with_span ctx fmt comment name def.meta.span
 
 (** Extract a function declaration.
 
@@ -1813,9 +1826,14 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span fmt
+  let name =
+    if !Config.extract_external_name_patterns && not global.is_local then
+      Some global.name
+    else None
+  in
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx global.name ^ "]" ]
-    global.meta.span;
+    name global.meta.span;
   F.pp_print_space fmt ();
 
   let decl_name = ctx_get_global global.def_id ctx in
@@ -2207,9 +2225,14 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
-    decl.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not decl.is_local then
+       Some decl.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+     name decl.meta.span);
   F.pp_print_break fmt 0 0;
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
      one line and indents are correct.
@@ -2490,9 +2513,14 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
-    impl.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not impl.is_local then
+       Some impl.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+     name impl.meta.span);
   F.pp_print_break fmt 0 0;
 
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on