Include method signatures in the trait decl

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.160"
+let supported_charon_version = "0.1.161"

charon-ml/src/generated/Generated_GAst.ml

@@ -269,6 +269,7 @@ and trait_decl = {
 (** A trait method. *)
 and trait_method = {
   name : trait_item_name;
+  signature : fun_sig region_binder;
   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_GAstOfJson.ml

@@ -1987,10 +1987,11 @@ 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); ("item", item) ] ->
+    | `Assoc [ ("name", name); ("signature", signature); ("item", item) ] ->
         let* name = trait_item_name_of_json ctx name in
+        let* signature = region_binder_of_json fun_sig_of_json ctx signature in
         let* item = fun_decl_ref_of_json ctx item in
-        Ok ({ name; item } : trait_method)
+        Ok ({ name; signature; item } : trait_method)
     | _ -> Error "")
 
 and trait_param_of_json (ctx : of_json_ctx) (js : json) :

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.160"
+version = "0.1.161"
 authors = [
     "Son Ho <[email protected]>",
     "Guillaume Boisseau <[email protected]>",

charon/src/ast/gast.rs

@@ -362,6 +362,7 @@ pub struct TraitAssocTy {
 #[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
 pub struct TraitMethod {
     pub name: TraitItemName,
+    pub signature: RegionBinder<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_drops.rs

@@ -87,6 +87,7 @@ impl ItemTransCtx<'_, '_> {
             .unwrap()
             .clone();
 
+        let signature = self.drop_in_place_method_sig(self_ty.clone());
         let src = match impl_kind {
             Some(impl_kind) => {
                 let destruct_impl_id =
@@ -115,13 +116,6 @@ impl ItemTransCtx<'_, '_> {
             self.translate_drop_in_place_method_body(span, def, &self_ty)?
         };
 
-        let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
-        let signature = FunSig {
-            is_unsafe: true,
-            inputs: vec![input],
-            output: Ty::mk_unit(),
-        };
-
         Ok(FunDecl {
             def_id,
             item_meta,
@@ -133,6 +127,16 @@ impl ItemTransCtx<'_, '_> {
         })
     }
 
+    // Small helper to deduplicate. Generates the signature `*mut self_ty -> ()`.
+    pub fn drop_in_place_method_sig(&self, self_ty: Ty) -> FunSig {
+        let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
+        FunSig {
+            is_unsafe: true,
+            inputs: [self_ptr].into(),
+            output: Ty::mk_unit(),
+        }
+    }
+
     // Small helper to deduplicate.
     pub fn prepare_drop_in_place_method(
         &mut self,

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

@@ -667,21 +667,15 @@ 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();
         let mut types = Vec::new();
         let mut methods = Vec::new();
 
-        for &(item_name, ref 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
@@ -745,8 +739,13 @@ impl ItemTransCtx<'_, '_> {
                                 id: method_id,
                                 generics: Box::new(fun_generics),
                             };
+                            let hax::AssocKind::Fn { sig, .. } = &hax_item.kind else {
+                                unreachable!()
+                            };
+                            let signature = bt_ctx.translate_poly_fun_sig(span, sig)?;
                             Ok(TraitMethod {
                                 name: item_name.clone(),
+                                signature,
                                 item: fn_ref,
                             })
                         },
@@ -853,9 +852,20 @@ 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,
-                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 sig = self.drop_in_place_method_sig(self_ty);
+                TraitMethod {
+                    name: method_name,
+                    item: fn_ref,
+                    signature: RegionBinder::empty(sig),
+                }
             }));
         }
 

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

@@ -315,8 +315,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 impl_id = self.register_item(

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

@@ -298,12 +298,9 @@ impl ItemTransCtx<'_, '_> {
                 TrVTableField::Drop => {
                     let self_ty =
                         TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
-                    let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
-                    let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(FunSig {
-                        is_unsafe: true,
-                        inputs: [self_ptr].into(),
-                        output: Ty::mk_unit(),
-                    })));
+                    let drop_ty = Ty::new(TyKind::FnPtr(RegionBinder::empty(
+                        self.drop_in_place_method_sig(self_ty),
+                    )));
                     ("drop".into(), drop_ty)
                 }
                 TrVTableField::Method(item_name, sig) => {
@@ -994,30 +991,24 @@ impl ItemTransCtx<'_, '_> {
             raise_error!(
                 self,
                 span,
-                "Trying to generate a vtable drop shim for a non-trait impl"
+                "Trying to generate a vtable drop shim for a non-dyn-compatible trait impl"
             );
         };
 
-        // `*mut dyn Trait`
-        let ref_dyn_self =
-            TyKind::RawPtr(self.translate_ty(span, dyn_self)?, RefKind::Mut).into_ty();
+        let dyn_self = self.translate_ty(span, dyn_self)?;
+        // `*mut dyn Trait -> ()`
+        let signature = self.drop_in_place_method_sig(dyn_self.clone());
+
         // `*mut T` for `impl Trait for T`
-        let ref_target_self = {
+        let target_self_ptr = {
             let impl_trait = self.translate_trait_ref(span, &trait_pred.trait_ref)?;
             TyKind::RawPtr(impl_trait.generics.types[0].clone(), RefKind::Mut).into_ty()
         };
 
-        // `*mut dyn Trait -> ()`
-        let signature = FunSig {
-            is_unsafe: true,
-            inputs: vec![ref_dyn_self.clone()],
-            output: Ty::mk_unit(),
-        };
-
         let body: Body = self.translate_vtable_drop_shim_body(
             span,
-            &ref_dyn_self,
-            &ref_target_self,
+            &signature.inputs[0],
+            &target_self_ptr,
             trait_pred,
         )?;
 

charon/src/transform/control_flow/duplicated-statement.rs

@@ -0,0 +1,8 @@
+fn rej_sample(a: &[u8]) -> usize {
+    let mut sampled = 0;
+    if a[0] < 42 && a[1] < 16 {
+        sampled += 100;
+    }
+    sampled += 101; // This statement is duplicated.
+    sampled
+}

charon/tests/ptr-metadata.json

@@ -41,6 +41,7 @@
   "alloc::alloc::Global": "None",
   "core::cmp::Ordering": "None",
   "core::option::Option": "None",
+  "core::ops::control_flow::ControlFlow": "None",
   "core::fmt::Formatter": "None",
   "core::result::Result": "None",
   "core::fmt::Error": "None",