Merge pull request #436 from Nadrieril/provided-methods3

AeneasVerif · Feb 11, 2025 · c15db3b · c15db3b
2 parents 91c7726 + e7fd388
commit c15db3b
Show file tree

Hide file tree

Showing 10 changed files with 130 additions and 132 deletions.
diff --git a/charon-pin b/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.
-ab692757d7033908c89bcc0e94d5ab1380b4f856
+91f411e4de52d2fb5c7a861a374a1b9676e03dd2
diff --git a/flake.lock b/flake.lock
diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml
@@ -2456,16 +2456,6 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
         (ctx, Some info)
   in
 
-  (* For now we do not support overriding provided methods *)
-  cassert __FILE__ __LINE__
-    (trait_impl.provided_methods = [])
-    trait_impl.item_meta.span
-    ("Overriding trait provided methods in trait implementations is not \
-      supported yet (trait impl: "
-    ^ name_to_string ctx trait_impl.item_meta.name
-    ^ ", overriden methods: "
-    ^ String.concat ", " (List.map fst trait_impl.provided_methods)
-    ^ ")");
   (* Everything is taken care of by {!extract_trait_decl_register_names} *but*
      the name of the implementation itself *)
   (* Compute the name *)

diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml
@@ -690,78 +690,40 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
              depending on whethere we call a top-level trait method impl or the
              method from a local clause *)
           match trait_ref.trait_id with
-          | TraitImpl (impl_id, impl_generics) -> (
+          | TraitImpl (impl_id, impl_generics) -> begin
               (* Lookup the trait impl *)
               let trait_impl = ctx_lookup_trait_impl ctx impl_id in
               log#ltrace
                 (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl));
-              (* First look in the required methods *)
+              (* Lookup the method *)
               let fn_ref =
-                Substitute.lookup_and_subst_trait_impl_required_method
-                  trait_impl method_name impl_generics func.generics
+                Option.get
+                  (Substitute.lookup_and_subst_trait_impl_method trait_impl
+                     method_name impl_generics func.generics)
+              in
+              let method_id = fn_ref.fun_id in
+              let generics = fn_ref.fun_generics in
+              let method_def = ctx_lookup_fun_decl ctx method_id in
+              (* Instantiate *)
+              let tr_self = trait_ref.trait_id in
+              let fid : fun_id = FRegular method_id in
+              let regions_hierarchy =
+                LlbcAstUtils.FunIdMap.find fid ctx.fun_ctx.regions_hierarchies
+              in
+              let inst_sg =
+                instantiate_fun_sig span ctx generics tr_self
+                  method_def.signature regions_hierarchy
               in
-              match fn_ref with
-              | Some fn_ref ->
-                  let method_id = fn_ref.fun_id in
-                  let generics = fn_ref.fun_generics in
-                  (* This is a required method *)
-                  let method_def = ctx_lookup_fun_decl ctx method_id in
-                  (* Instantiate *)
-                  let tr_self = trait_ref.trait_id in
-                  let fid : fun_id = FRegular method_id in
-                  let regions_hierarchy =
-                    LlbcAstUtils.FunIdMap.find fid
-                      ctx.fun_ctx.regions_hierarchies
-                  in
-                  let inst_sg =
-                    instantiate_fun_sig span ctx generics tr_self
-                      method_def.signature regions_hierarchy
-                  in
-                  (* Also update the function identifier: we want to forget
-                     the fact that we called a trait method, and treat it as
-                     a regular function call to the top-level function
-                     which implements the method. In order to do this properly,
-                     we also need to update the generics.
-                  *)
-                  let func = FunId fid in
-                  (* TODO: the `trait_method_generics` look fishy *)
-                  (func, generics, Some (generics, tr_self), method_def, inst_sg)
-              | None ->
-                  (* If not found, lookup the methods provided by the trait *declaration*
-                     (remember: for now, we forbid overriding provided methods) *)
-                  cassert __FILE__ __LINE__
-                    (trait_impl.provided_methods = [])
-                    span "Overriding provided methods is currently forbidden";
-                  let trait_decl =
-                    ctx_lookup_trait_decl ctx trait_decl_ref.trait_decl_id
-                  in
-                  let fn_ref =
-                    Option.get
-                      (Substitute.lookup_and_subst_trait_decl_provided_method
-                         trait_decl method_name trait_ref func.generics)
-                  in
-                  let method_id = fn_ref.fun_id in
-                  let method_def = ctx_lookup_fun_decl ctx method_id in
-                  let all_generics = fn_ref.fun_generics in
-                  log#ldebug
-                    (lazy
-                      ("provided method call:" ^ "\n- method name: "
-                     ^ method_name ^ "\n- all_generics:\n"
-                      ^ generic_args_to_string ctx all_generics));
-                  let regions_hierarchy =
-                    LlbcAstUtils.FunIdMap.find (FRegular method_id)
-                      ctx.fun_ctx.regions_hierarchies
-                  in
-                  let tr_self = trait_ref.trait_id in
-                  let inst_sg =
-                    instantiate_fun_sig span ctx all_generics tr_self
-                      method_def.signature regions_hierarchy
-                  in
-                  ( func.func,
-                    func.generics,
-                    Some (all_generics, tr_self),
-                    method_def,
-                    inst_sg ))
+              (* Also update the function identifier: we want to forget
+                 the fact that we called a trait method, and treat it as
+                 a regular function call to the top-level function
+                 which implements the method. In order to do this properly,
+                 we also need to update the generics.
+              *)
+              let func = FunId fid in
+              (* TODO: the `trait_method_generics` look fishy *)
+              (func, generics, Some (generics, tr_self), method_def, inst_sg)
+            end
           | _ ->
               (* We are using a local clause - we lookup the trait decl *)
               let trait_decl =

diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v
@@ -22,24 +22,21 @@ Arguments BoolTest_t_getTest { _ } _.
 Definition boolTraitBool_getTest (self : bool) : result bool :=
   Ok self.
 
+(** [rename_attribute::{rename_attribute::BoolTrait for bool}::ret_true]:
+    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
+Definition boolTraitBool_retTest (self : bool) : result bool :=
+  Ok true.
+
 (** Trait implementation: [rename_attribute::{rename_attribute::BoolTrait for bool}]
     Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 *)
 Definition BoolImpl : BoolTest_t bool := {|
   BoolTest_t_getTest := boolTraitBool_getTest;
 |}.
 
-(** [rename_attribute::BoolTrait::ret_true]:
-    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-Definition boolTrait_retTest
-  {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
-  Ok true
-.
-
 (** [rename_attribute::test_bool_trait]:
     Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *)
 Definition boolFn (T : Type) (x : bool) : result bool :=
-  b <- boolTraitBool_getTest x;
-  if b then boolTrait_retTest BoolImpl x else Ok false
+  b <- boolTraitBool_getTest x; if b then boolTraitBool_retTest x else Ok false
 .
 
 (** [rename_attribute::SimpleEnum]
@@ -100,4 +97,11 @@ 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]:
+    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
+Definition boolTrait_retTest
+  {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
+  Ok true
+.
+
 End RenameAttribute.
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
@@ -22,24 +22,22 @@ Arguments BoolTrait_t_get_bool { _ } _.
 Definition boolTraitBool_get_bool (self : bool) : result bool :=
   Ok self.
 
+(** [traits::{traits::BoolTrait for bool}::ret_true]:
+    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
+Definition boolTraitBool_ret_true (self : bool) : result bool :=
+  Ok true.
+
 (** Trait implementation: [traits::{traits::BoolTrait for bool}]
     Source: 'tests/src/traits.rs', lines 13:0-17:1 *)
 Definition BoolTraitBool : BoolTrait_t bool := {|
   BoolTrait_t_get_bool := boolTraitBool_get_bool;
 |}.
 
-(** [traits::BoolTrait::ret_true]:
-    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-Definition boolTrait_ret_true
-  {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
-  Ok true
-.
-
 (** [traits::test_bool_trait_bool]:
     Source: 'tests/src/traits.rs', lines 19:0-21:1 *)
 Definition test_bool_trait_bool (x : bool) : result bool :=
   b <- boolTraitBool_get_bool x;
-  if b then boolTrait_ret_true BoolTraitBool x else Ok false
+  if b then boolTraitBool_ret_true x else Ok false
 .
 
 (** [traits::{traits::BoolTrait for core::option::Option<T>}#1::get_bool]:
@@ -49,6 +47,13 @@ Definition boolTraitOption_get_bool
   match self with | None => Ok false | Some _ => Ok true end
 .
 
+(** [traits::{traits::BoolTrait for core::option::Option<T>}#1::ret_true]:
+    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
+Definition boolTraitOption_ret_true
+  {T : Type} (self : option T) : result bool :=
+  Ok true
+.
+
 (** Trait implementation: [traits::{traits::BoolTrait for core::option::Option<T>}#1]
     Source: 'tests/src/traits.rs', lines 24:0-31:1 *)
 Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
@@ -59,7 +64,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
     Source: 'tests/src/traits.rs', lines 33:0-35:1 *)
 Definition test_bool_trait_option {T : Type} (x : option T) : result bool :=
   b <- boolTraitOption_get_bool x;
-  if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false
+  if b then boolTraitOption_ret_true x else Ok false
 .
 
 (** [traits::test_bool_trait]:
@@ -696,6 +701,13 @@ Definition use_foo2
   Ok (foo_foo T traitInst)
 .
 
+(** [traits::BoolTrait::ret_true]:
+    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
+Definition boolTrait_ret_true
+  {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
+  Ok true
+.
+
 (** Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
     Source: 'tests/src/traits.rs', lines 130:8-132:9 *)
 Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t {

diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
@@ -12,23 +12,20 @@ include RenameAttribute.Clauses
 let boolTraitBool_getTest (self : bool) : result bool =
   Ok self
 
+(** [rename_attribute::{rename_attribute::BoolTrait for bool}::ret_true]:
+    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
+let boolTraitBool_retTest (self : bool) : result bool =
+  Ok true
+
 (** Trait implementation: [rename_attribute::{rename_attribute::BoolTrait for bool}]
     Source: 'tests/src/rename_attribute.rs', lines 21:0-25:1 *)
 let boolImpl : boolTest_t bool = { getTest = boolTraitBool_getTest; }
 
-(** [rename_attribute::BoolTrait::ret_true]:
-    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-let boolTrait_retTest
-  (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
-  result bool
-  =
-  Ok true
-
 (** [rename_attribute::test_bool_trait]:
     Source: 'tests/src/rename_attribute.rs', lines 28:0-30:1 *)
 let boolFn (t : Type0) (x : bool) : result bool =
   let* b = boolTraitBool_getTest x in
-  if b then boolTrait_retTest boolImpl x else Ok false
+  if b then boolTraitBool_retTest x else Ok false
 
 (** [rename_attribute::C]
     Source: 'tests/src/rename_attribute.rs', lines 50:0-50:28 *)
@@ -65,3 +62,11 @@ 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]:
+    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
+let boolTrait_retTest
+  (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
+  result bool
+  =
+  Ok true
+
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
@@ -14,29 +14,31 @@ noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; }
 let boolTraitBool_get_bool (self : bool) : result bool =
   Ok self
 
+(** [traits::{traits::BoolTrait for bool}::ret_true]:
+    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
+let boolTraitBool_ret_true (self : bool) : result bool =
+  Ok true
+
 (** Trait implementation: [traits::{traits::BoolTrait for bool}]
     Source: 'tests/src/traits.rs', lines 13:0-17:1 *)
 let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; }
 
-(** [traits::BoolTrait::ret_true]:
-    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
-let boolTrait_ret_true
-  (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
-  result bool
-  =
-  Ok true
-
 (** [traits::test_bool_trait_bool]:
     Source: 'tests/src/traits.rs', lines 19:0-21:1 *)
 let test_bool_trait_bool (x : bool) : result bool =
   let* b = boolTraitBool_get_bool x in
-  if b then boolTrait_ret_true boolTraitBool x else Ok false
+  if b then boolTraitBool_ret_true x else Ok false
 
 (** [traits::{traits::BoolTrait for core::option::Option<T>}#1::get_bool]:
     Source: 'tests/src/traits.rs', lines 25:4-30:5 *)
 let boolTraitOption_get_bool (#t : Type0) (self : option t) : result bool =
   begin match self with | None -> Ok false | Some _ -> Ok true end
 
+(** [traits::{traits::BoolTrait for core::option::Option<T>}#1::ret_true]:
+    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
+let boolTraitOption_ret_true (#t : Type0) (self : option t) : result bool =
+  Ok true
+
 (** Trait implementation: [traits::{traits::BoolTrait for core::option::Option<T>}#1]
     Source: 'tests/src/traits.rs', lines 24:0-31:1 *)
 let boolTraitOption (t : Type0) : boolTrait_t (option t) = {
@@ -47,7 +49,7 @@ let boolTraitOption (t : Type0) : boolTrait_t (option t) = {
     Source: 'tests/src/traits.rs', lines 33:0-35:1 *)
 let test_bool_trait_option (#t : Type0) (x : option t) : result bool =
   let* b = boolTraitOption_get_bool x in
-  if b then boolTrait_ret_true (boolTraitOption t) x else Ok false
+  if b then boolTraitOption_ret_true x else Ok false
 
 (** [traits::test_bool_trait]:
     Source: 'tests/src/traits.rs', lines 37:0-39:1 *)
@@ -522,6 +524,14 @@ let use_foo2
   =
   Ok (foo_foo t traitInst)
 
+(** [traits::BoolTrait::ret_true]:
+    Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
+let boolTrait_ret_true
+  (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
+  result bool
+  =
+  Ok true
+
 (** Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
     Source: 'tests/src/traits.rs', lines 130:8-132:9 *)
 noeq type testType_test_TestTrait_t (self : Type0) = {