Include method signatures in the trait decl

Author: Nadrieril

charon-ml/src/GAstUtils.ml

@@ -57,20 +57,26 @@ let bound_fun_sig_of_decl (def : fun_decl) : bound_fun_sig =
     reflect that there are two binding levels: the trait generics and the method
     generics. *)
 let lookup_trait_decl_method (tdecl : trait_decl) (name : trait_item_name) :
+    trait_method binder item_binder option =
+  Option.map
+    (fun m -> { item_binder_params = tdecl.generics; item_binder_value = m })
+    (List.find_opt
+       (fun (m : trait_method binder) -> m.binder_value.name = name)
+       tdecl.methods)
+
+let lookup_trait_decl_method_ref (tdecl : trait_decl) (name : trait_item_name) :
     fun_decl_ref binder item_binder option =
   Option.map
     (fun m ->
       {
-        item_binder_params = tdecl.generics;
+        item_binder_params = m.item_binder_params;
         item_binder_value =
           {
-            binder_params = m.binder_params;
-            binder_value = m.binder_value.item;
+            binder_params = m.item_binder_value.binder_params;
+            binder_value = m.item_binder_value.binder_value.item;
           };
       })
-    (List.find_opt
-       (fun (m : trait_method binder) -> m.binder_value.name = name)
-       tdecl.methods)
+    (lookup_trait_decl_method tdecl name)
 
 (** Lookup a method in this trait impl. The two levels of binders in the output
     reflect that there are two binding levels: the impl generics and the method

charon-ml/src/Substitute.ml

@@ -562,12 +562,12 @@ let fuse_binders (substitutor : subst -> 'a -> 'a)
 (** Helper *)
 let instantiate_method (trait_self : trait_ref_kind)
     (item_generics : generic_args) (method_generics : generic_args)
-    (bound_fn : fun_decl_ref binder item_binder) : fun_decl_ref =
+    (bound_method : fun_decl_ref binder item_binder) : fun_decl_ref =
   let bound_fn =
     apply_args_to_item_binder trait_self item_generics
       (st_substitute_visitor#visit_binder
          st_substitute_visitor#visit_fun_decl_ref)
-      bound_fn
+      bound_method
   in
   apply_args_to_binder method_generics st_substitute_visitor#visit_fun_decl_ref
     bound_fn
@@ -585,7 +585,7 @@ let lookup_and_subst_trait_decl_method (tdecl : trait_decl)
     (method_generics : generic_args) : fun_decl_ref option =
   Option.map
     (instantiate_trait_method trait_ref method_generics)
-    (lookup_trait_decl_method tdecl name)
+    (lookup_trait_decl_method_ref tdecl name)
 
 (** Like lookup_trait_impl_method, but also correctly substitutes the generics.
 *)
@@ -606,26 +606,17 @@ let lookup_method_sig (crate : crate) (trait_id : trait_decl_id)
   let* tdecl = TraitDeclId.Map.find_opt trait_id crate.trait_decls in
   let* {
          item_binder_params : generic_params = trait_params;
-         item_binder_value : fun_decl_ref binder = bound_method;
+         item_binder_value : trait_method binder =
+           { binder_params = method_params; binder_value = trait_method };
        } =
     lookup_trait_decl_method tdecl name
   in
-  let method_decl_id = bound_method.binder_value.id in
-  let* method_decl =
-    LlbcAst.FunDeclId.Map.find_opt method_decl_id crate.fun_decls
-  in
-  (* Substitute the signature to be valid under the binder. *)
-  let signature =
-    st_substitute_visitor#visit_fun_sig
-      (make_subst_from_generics method_decl.generics
-         bound_method.binder_value.generics Self)
-      method_decl.signature
-  in
-  (* Rebind everything *)
-  let bound_sig =
-    { binder_params = bound_method.binder_params; binder_value = signature }
-  in
-  Some { item_binder_params = trait_params; item_binder_value = bound_sig }
+  Some
+    {
+      item_binder_params = trait_params;
+      item_binder_value =
+        { binder_params = method_params; binder_value = trait_method.signature };
+    }
 
 (* Like [lookup_method_sig], but with no binder shenanigans: the returned
    binder binds the concatenation of trait generics and method generics. *)

charon-ml/src/generated/Generated_GAst.ml

@@ -301,6 +301,7 @@ and trait_decl = {
 and trait_method = {
   name : trait_item_name;
   attr_info : attr_info;
+  signature : fun_sig;
   item : fun_decl_ref;
       (** Each method declaration is represented by a function item. That
           function contains the signature of the method as well as information

charon-ml/src/generated/Generated_OfJson.ml

@@ -2782,11 +2782,18 @@ and trait_method_of_json (ctx : of_json_ctx) (js : json) :
     (trait_method, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("name", name); ("attr_info", attr_info); ("item", item) ] ->
+    | `Assoc
+        [
+          ("name", name);
+          ("attr_info", attr_info);
+          ("signature", signature);
+          ("item", item);
+        ] ->
         let* name = trait_item_name_of_json ctx name in
         let* attr_info = attr_info_of_json ctx attr_info in
+        let* signature = fun_sig_of_json ctx signature in
         let* item = fun_decl_ref_of_json ctx item in
-        Ok ({ name; attr_info; item } : trait_method)
+        Ok ({ name; attr_info; signature; item } : trait_method)
     | _ -> Error "")
 
 and translated_crate_of_json (ctx : of_json_ctx) (js : json) :

charon/src/ast/gast.rs

@@ -399,6 +399,7 @@ pub struct TraitMethod {
     #[drive(skip)]
     #[serde_state(stateless)]
     pub attr_info: AttrInfo,
+    pub signature: FunSig,
     /// Each method declaration is represented by a function item. That function contains the
     /// signature of the method as well as information like attributes. It has a body iff the
     /// method declaration has a default implementation; otherwise it has an `Opaque` body.

charon/src/bin/charon-driver/translate/translate_items.rs

@@ -672,13 +672,6 @@ impl ItemTransCtx<'_, '_> {
             TraitRefKind::SelfId,
             RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?),
         );
-        let items: Vec<(TraitItemName, &hax::AssocItem)> = items
-            .iter()
-            .map(|item| -> Result<_, Error> {
-                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
-                Ok((name, item))
-            })
-            .try_collect()?;
 
         // Translate the associated items
         let mut consts = Vec::new();
@@ -701,8 +694,9 @@ impl ItemTransCtx<'_, '_> {
             });
         }
 
-        for &(item_name, hax_item) in &items {
+        for hax_item in items {
             let item_def_id = &hax_item.def_id;
+            let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?;
             let item_span = self.def_span(item_def_id);
 
             // In --mono mode, we keep only non-polymorphic items; in not-mono mode, we use the
@@ -718,7 +712,7 @@ impl ItemTransCtx<'_, '_> {
             let attr_info = self.translate_attr_info(&item_def);
 
             match item_def.kind() {
-                hax::FullDefKind::AssocFn { .. } => {
+                hax::FullDefKind::AssocFn { sig, .. } => {
                     let method_id = self.register_no_enqueue(item_span, &item_src);
                     // Register this method.
                     self.register_method_impl(def_id, item_name, method_id);
@@ -752,9 +746,14 @@ impl ItemTransCtx<'_, '_> {
                                 id: method_id,
                                 generics: Box::new(fun_generics),
                             };
+                            // `skip_binder` is allowed because `translate_binder_for_def` puts the
+                            // late bound params in scope.
+                            let signature =
+                                bt_ctx.translate_fun_sig(span, sig.hax_skip_binder_ref())?;
                             Ok(TraitMethod {
                                 name: item_name,
                                 attr_info,
+                                signature,
                                 item: fn_ref,
                             })
                         },
@@ -884,10 +883,21 @@ impl ItemTransCtx<'_, '_> {
             let (method_name, method_binder) =
                 self.prepare_drop_in_place_method(def, span, def_id, None);
             self.mark_method_as_used(def_id, method_name);
-            methods.push(method_binder.map(|fn_ref| TraitMethod {
-                name: method_name,
-                attr_info: AttrInfo::dummy_public(),
-                item: fn_ref,
+            methods.push(method_binder.map(|fn_ref| {
+                let self_ty = if self.monomorphize() {
+                    // FIXME: put something real here
+                    Ty::mk_unit()
+                } else {
+                    TyKind::TypeVar(DeBruijnVar::bound(DeBruijnId::one(), TypeVarId::ZERO))
+                        .into_ty()
+                };
+                let signature = self.drop_in_place_method_sig(self_ty);
+                TraitMethod {
+                    name: method_name,
+                    item: fn_ref,
+                    attr_info: AttrInfo::dummy_public(),
+                    signature,
+                }
             }));
         }
 

charon/src/bin/charon-driver/translate/translate_predicates.rs

@@ -331,8 +331,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                 ..
             } => {
                 let tref = &impl_source.r#trait;
-                let trait_def =
-                    self.hax_def(&tref.hax_skip_binder_ref().erase(self.hax_state_with_id()))?;
+                let trait_def = self.poly_hax_def(&tref.hax_skip_binder_ref().def_id)?;
                 let kind = if let hax::FullDefKind::TraitAlias { .. } = trait_def.kind() {
                     // We reuse the same `def_id` to generate a blanket impl for the trait.
                     let mut impl_ref: TraitImplRef = self.translate_item(

charon/tests/ptr-metadata.json

@@ -46,5 +46,6 @@
   "core::fmt::Formatter": "None",
   "core::fmt::Error": "None",
   "core::cmp::Ordering": "None",
-  "core::option::Option": "None"
+  "core::option::Option": "None",
+  "core::ops::control_flow::ControlFlow": "None"
 }

charon/tests/ui/control-flow/loops.out

@@ -321,25 +321,24 @@ where
     [@TraitClause0]: Iterator<Self>,
 = <opaque>
 
-// Full name: core::slice::index::private_slice_index::Sealed
-pub trait Sealed<Self>
+pub trait core::slice::index::private_slice_index::Sealed<Self>
 {
     parent_clause0 : [@TraitClause0]: MetaSized<Self>
     vtable: core::slice::index::private_slice_index::Sealed::{vtable}
 }
 
-// Full name: core::slice::index::private_slice_index::{impl Sealed for usize}
-impl Sealed for usize {
+// Full name: core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for usize}
+impl core::slice::index::private_slice_index::Sealed for usize {
     parent_clause0 = {built_in impl MetaSized for usize}
-    vtable: {impl Sealed for usize}::{vtable}
+    vtable: {impl core::slice::index::private_slice_index::Sealed for usize}::{vtable}
 }
 
 // Full name: core::slice::index::SliceIndex
 #[lang_item("SliceIndex")]
 pub trait SliceIndex<Self, T>
 {
     parent_clause0 : [@TraitClause0]: MetaSized<Self>
-    parent_clause1 : [@TraitClause1]: Sealed<Self>
+    parent_clause1 : [@TraitClause1]: core::slice::index::private_slice_index::Sealed<Self>
     parent_clause2 : [@TraitClause2]: MetaSized<T>
     parent_clause3 : [@TraitClause3]: MetaSized<Self::Output>
     type Output
@@ -424,7 +423,7 @@ where
     [@TraitClause0]: Sized<T>,
 {
     parent_clause0 = {built_in impl MetaSized for usize}
-    parent_clause1 = {impl Sealed for usize}
+    parent_clause1 = {impl core::slice::index::private_slice_index::Sealed for usize}
     parent_clause2 = {built_in impl MetaSized for [T]}
     parent_clause3 = @TraitClause0::parent_clause0
     type Output = T

charon/tests/ui/monomorphization/dyn-trait.out

@@ -1,5 +1,5 @@
 
-thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:1696:13:
+thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:1687:13:
 Could not determine method index for drop in vtable
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `core::fmt::Display`.
@@ -11,7 +11,7 @@ note: the error occurred when translating `core::fmt::Display::{vtable_drop_pres
 12 |     let _ = dyn_to_string(&str);
    |                           ----
 
-thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:1574:13:
+thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:1565:13:
 Could not determine method index for method_fmt in vtable
 error: Thread panicked when extracting item `core::fmt::Display`.
  --> /rustc/library/core/src/fmt/mod.rs:1186:1