Rename default methods to avoid name clashes

AeneasVerif · Feb 12, 2025 · e3490c1 · e3490c1
1 parent 22550f3
commit e3490c1
Show file tree

Hide file tree

Showing 7 changed files with 33 additions and 12 deletions.
diff --git a/src/PrePasses.ml b/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] *)

diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v
@@ -100,9 +100,9 @@ Definition no_borrows_sum (n : nat) (max : u32) : result u32 :=
   no_borrows_sum_loop n max 0%u32 0%u32
 .
 
-(** [rename_attribute::BoolTrait::ret_true]:
+(** [rename_attribute::BoolTrait::default::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-Definition boolTrait_retTest
+Definition boolTrait_default_retTest
   {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
   Ok true
 .

diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
@@ -705,9 +705,9 @@ Definition use_foo2
   Ok (foo_foo T traitInst)
 .
 
-(** [traits::BoolTrait::ret_true]:
+(** [traits::BoolTrait::default::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-Definition boolTrait_ret_true
+Definition boolTrait_default_ret_true
   {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
   Ok true
 .

diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
@@ -65,9 +65,9 @@ let rec no_borrows_sum_loop
 let no_borrows_sum (max : u32) : result u32 =
   no_borrows_sum_loop max 0 0
 
-(** [rename_attribute::BoolTrait::ret_true]:
+(** [rename_attribute::BoolTrait::default::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-let boolTrait_retTest
+let boolTrait_default_retTest
   (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
   result bool
   =

diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
@@ -531,9 +531,9 @@ let use_foo2
   =
   Ok (foo_foo t traitInst)
 
-(** [traits::BoolTrait::ret_true]:
+(** [traits::BoolTrait::default::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-let boolTrait_ret_true
+let boolTrait_default_ret_true
   (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
   result bool
   =

diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean
@@ -91,9 +91,9 @@ divergent def No_borrows_sum_loop
 def No_borrows_sum (max : U32) : Result U32 :=
   No_borrows_sum_loop max 0#u32 0#u32
 
-/- [rename_attribute::BoolTrait::ret_true]:
+/- [rename_attribute::BoolTrait::default::ret_true]:
    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/
-def BoolTrait.retTest
+def BoolTrait.default.retTest
   {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool :=
   Result.ok true
 

diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
@@ -550,9 +550,9 @@ def use_foo2
   :=
   Result.ok (Foo.FOO T TraitInst)
 
-/- [traits::BoolTrait::ret_true]:
+/- [traits::BoolTrait::default::ret_true]:
    Source: 'tests/src/traits.rs', lines 8:4-10:5 -/
-def BoolTrait.ret_true
+def BoolTrait.default.ret_true
   {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
   Result.ok true