Don't distinguish provided and required methods

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.
-91f411e4de52d2fb5c7a861a374a1b9676e03dd2
+821fe7c71300e00c23e47ae97de1e8dc4ac91f9d

src/PrePasses.ml

@@ -661,12 +661,33 @@ let decompose_str_borrows (f : fun_decl) : fun_decl =
   in
   { f with body }
 
+(** When a trait method has a default implementation, this becomes a `fun_decl`
+    that we may want to extract. By default, its name is `Trait::method`, which
+    for lean creates a name clash with the method name as a field in the trait
+    struct. We therefore rename these function items to avoid the name clash.
+ *)
+let rename_default_methods (def : fun_decl) : fun_decl =
+  match def.kind with
+  | TraitDeclItem (_, _, true) ->
+      let name = def.item_meta.name in
+      let rev_name = List.rev name in
+      let method_name = List.hd rev_name in
+      let name =
+        List.rev
+          (method_name
+          :: PeIdent ("default", Disambiguator.zero)
+          :: List.tl rev_name)
+      in
+      { def with item_meta = { def.item_meta with name } }
+  | _ -> def
+
 let apply_passes (crate : crate) : crate =
   let function_passes =
     [
       remove_loop_breaks crate;
       remove_shallow_borrows crate;
       decompose_str_borrows;
+      rename_default_methods;
     ]
   in
   (* Attempt to apply a pass: if it fails we replace the body by [None] *)

src/extract/Extract.ml

@@ -507,46 +507,24 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
       *)
       (match fun_id with
       | FromLlbc (TraitMethod (trait_ref, method_name, _fun_decl_id), lp_id) ->
-          (* We have to check whether the trait method is required or provided *)
           let trait_decl_id = trait_ref.trait_decl_ref.trait_decl_id in
           let trait_decl =
             TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls
           in
-          let method_id =
-            PureUtils.trait_decl_get_method trait_decl method_name
-          in
-
-          if not method_id.is_provided then (
-            (* Required method *)
-            sanity_check __FILE__ __LINE__ (lp_id = None)
-              trait_decl.item_meta.span;
-            extract_trait_ref trait_decl.item_meta.span ctx fmt
-              TypeDeclId.Set.empty true trait_ref;
-            let fun_name =
-              ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
-                method_name ctx
-            in
-            let add_brackets (s : string) =
-              if backend () = Coq then "(" ^ s ^ ")" else s
-            in
-            F.pp_print_string fmt ("." ^ add_brackets fun_name))
-          else
-            (* Provided method: we see it as a regular function call, and use
-               the function name *)
-            let fun_id = FromLlbc (FunId (FRegular method_id.id), lp_id) in
-            let fun_name =
-              ctx_get_function trait_decl.item_meta.span fun_id ctx
-            in
-            F.pp_print_string fmt fun_name;
-
-            (* Note that we do not need to print the generics for the trait
-               declaration: they are always implicit as they can be deduced
-               from the trait self clause.
 
-               Print the trait ref (to instantate the self clause) *)
-            F.pp_print_space fmt ();
-            extract_trait_ref trait_decl.item_meta.span ctx fmt
-              TypeDeclId.Set.empty true trait_ref
+          (* Required method *)
+          sanity_check __FILE__ __LINE__ (lp_id = None)
+            trait_decl.item_meta.span;
+          extract_trait_ref trait_decl.item_meta.span ctx fmt
+            TypeDeclId.Set.empty true trait_ref;
+          let fun_name =
+            ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
+              method_name ctx
+          in
+          let add_brackets (s : string) =
+            if backend () = Coq then "(" ^ s ^ ")" else s
+          in
+          F.pp_print_string fmt ("." ^ add_brackets fun_name)
       | _ ->
           let fun_name = ctx_get_function span fun_id ctx in
           F.pp_print_string fmt fun_name);
@@ -2323,7 +2301,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let required_methods = trait_decl.required_methods in
+  let methods = trait_decl.methods in
   (* Compute the names *)
   let method_names =
     match builtin_info with
@@ -2361,7 +2339,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
         List.map
           (fun (name, bound_fn) ->
             compute_item_name name bound_fn.binder_value.fun_id)
-          required_methods
+          methods
     | Some info ->
         (* This is a builtin *)
         let funs_map = StringMap.of_list info.methods in
@@ -2371,7 +2349,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
             let info = StringMap.find item_name funs_map in
             let fun_name = info.extract_name in
             (item_name, fun_name))
-          required_methods
+          methods
   in
   (* Register the names *)
   List.fold_left
@@ -2615,9 +2593,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     Option.get
       (type_decl_kind_to_qualif decl.item_meta.span SingleNonRec (Some Struct))
   in
-  (* When checking if the trait declaration is empty: we ignore the provided
-     methods, because for now they are extracted separately *)
-  let is_empty = trait_decl_is_empty { decl with provided_methods = [] } in
+  let is_empty = trait_decl_is_empty decl in
   if backend () = FStar && not is_empty then (
     F.pp_print_string fmt "noeq";
     F.pp_print_space fmt ());
@@ -2711,7 +2687,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (* The required methods *)
     List.iter
       (fun (name, fn) -> extract_trait_decl_method_items ctx fmt decl name fn)
-      decl.required_methods;
+      decl.methods;
 
     (* Close the outer boxes for the definition *)
     if backend () <> Lean then F.pp_close_box fmt ();
@@ -2772,7 +2748,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
       in
       extract_coq_arguments_instruction ctx fmt item_name params)
     decl.parent_clauses;
-  (* The required methods *)
+  (* The  methods *)
   List.iter
     (fun (item_name, bound_fn) ->
       let explicit_info = bound_fn.binder_explicit_info in
@@ -2790,7 +2766,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
         ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
       in
       extract_coq_arguments_instruction ctx fmt item_name params)
-    decl.required_methods;
+    decl.methods;
   (* Add a space *)
   F.pp_print_space fmt ()
 
@@ -2923,9 +2899,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   extract_trait_decl_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty false
     impl.impl_trait;
 
-  (* When checking if the trait impl is empty: we ignore the provided
-     methods, because for now they are extracted separately *)
-  let is_empty = trait_impl_is_empty { impl with provided_methods = [] } in
+  let is_empty = trait_impl_is_empty impl in
 
   F.pp_print_space fmt ();
   if is_empty && backend () = FStar then (
@@ -3011,11 +2985,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
         extract_trait_impl_item ctx fmt item_name ty)
       (List.combine trait_decl.parent_clauses impl.parent_trait_refs);
 
-    (* The required methods *)
+    (* The methods *)
     List.iter
       (fun (name, bound_fn) ->
         extract_trait_impl_method_items ctx fmt impl name bound_fn)
-      impl.required_methods;
+      impl.methods;
 
     (* Close the outer boxes for the definition, as well as the brackets *)
     F.pp_close_box fmt ();

src/extract/ExtractBase.ml

@@ -2181,11 +2181,10 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
           with
           | None -> def.item_meta
           | Some trait_decl -> (
-              let methods =
-                trait_decl.required_methods @ trait_decl.provided_methods
-              in
               match
-                List.find_opt (fun (name, _) -> name = item_name) methods
+                List.find_opt
+                  (fun (name, _) -> name = item_name)
+                  trait_decl.methods
               with
               | None -> def.item_meta
               | Some (_, bound_fn) ->

src/pure/Pure.ml

@@ -1353,8 +1353,7 @@ type trait_decl = {
   llbc_parent_clauses : Types.trait_clause list;
   consts : (trait_item_name * ty) list;
   types : trait_item_name list;
-  required_methods : (trait_item_name * fun_decl_ref binder) list;
-  provided_methods : (trait_item_name * fun_decl_ref binder) list;
+  methods : (trait_item_name * fun_decl_ref binder) list;
 }
 [@@deriving show]
 
@@ -1378,7 +1377,6 @@ type trait_impl = {
   parent_trait_refs : trait_ref list;
   consts : (trait_item_name * global_decl_ref) list;
   types : (trait_item_name * ty) list;
-  required_methods : (trait_item_name * fun_decl_ref binder) list;
-  provided_methods : (trait_item_name * fun_decl_ref binder) list;
+  methods : (trait_item_name * fun_decl_ref binder) list;
 }
 [@@deriving show]

src/pure/PureUtils.ml

@@ -794,24 +794,6 @@ let rec typed_pattern_to_texpression (span : Meta.span) (pat : typed_pattern) :
   | None -> None
   | Some e -> Some { e; ty = pat.ty }
 
-type trait_decl_method_decl_id = { is_provided : bool; id : fun_decl_id }
-
-let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) :
-    trait_decl_method_decl_id =
-  (* First look in the required methods *)
-  let bound_method =
-    List.find_opt (fun (s, _) -> s = method_name) trait_decl.required_methods
-  in
-  match bound_method with
-  | Some (_, bound_method) ->
-      { is_provided = false; id = bound_method.binder_value.fun_id }
-  | None ->
-      (* Must be a provided method *)
-      let _, bound_method =
-        List.find (fun (s, _) -> s = method_name) trait_decl.provided_methods
-      in
-      { is_provided = true; id = bound_method.binder_value.fun_id }
-
 let trait_decl_is_empty (trait_decl : trait_decl) : bool =
   let {
     def_id = _;
@@ -825,13 +807,11 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
     llbc_parent_clauses = _;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } =
     trait_decl
   in
-  parent_clauses = [] && consts = [] && types = [] && required_methods = []
-  && provided_methods = []
+  parent_clauses = [] && consts = [] && types = [] && methods = []
 
 let trait_impl_is_empty (trait_impl : trait_impl) : bool =
   let {
@@ -847,13 +827,11 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
     parent_trait_refs;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } =
     trait_impl
   in
-  parent_trait_refs = [] && consts = [] && types = [] && required_methods = []
-  && provided_methods = []
+  parent_trait_refs = [] && consts = [] && types = [] && methods = []
 
 (** Return true if a type declaration should be extracted as a tuple, because
     it is a non-recursive structure with unnamed fields. *)

src/symbolic/SymbolicToPure.ml

@@ -4791,8 +4791,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     parent_clauses = llbc_parent_clauses;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } : A.trait_decl =
     trait_decl
   in
@@ -4810,17 +4809,11 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     List.map (translate_trait_clause span) llbc_parent_clauses
   in
   let consts = List.map (fun (name, ty) -> (name, translate_ty ty)) consts in
-  let required_methods =
+  let methods =
     List.map
       (fun (name, bound_fn) ->
         (name, translate_trait_method span translate_ty bound_fn))
-      required_methods
-  in
-  let provided_methods =
-    List.map
-      (fun (name, bound_fn) ->
-        (name, translate_trait_method span translate_ty bound_fn))
-      provided_methods
+      methods
   in
   {
     def_id;
@@ -4834,8 +4827,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     llbc_parent_clauses;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   }
 
 let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
@@ -4848,8 +4840,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     parent_trait_refs;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   } =
     trait_impl
   in
@@ -4876,17 +4867,11 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
       consts
   in
   let types = List.map (fun (name, ty) -> (name, translate_ty ty)) types in
-  let required_methods =
-    List.map
-      (fun (name, bound_fn) ->
-        (name, translate_trait_method span translate_ty bound_fn))
-      required_methods
-  in
-  let provided_methods =
+  let methods =
     List.map
       (fun (name, bound_fn) ->
         (name, translate_trait_method span translate_ty bound_fn))
-      provided_methods
+      methods
   in
   {
     def_id;
@@ -4901,8 +4886,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     parent_trait_refs;
     consts;
     types;
-    required_methods;
-    provided_methods;
+    methods;
   }
 
 let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :