Translate dyn Trait method shims

.gitignore

@@ -55,3 +55,4 @@ nohup.out
 *#
 *.smt2
 .#*
+**/.DS_Store

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.133"
+let supported_charon_version = "0.1.134"

charon-ml/src/PrintExpressions.ml

@@ -79,6 +79,8 @@ and cast_kind_to_string (env : 'a fmt_env) (cast : cast_kind) : string =
       "cast<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
   | CastUnsize (src, tgt, _) ->
       "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
+  | CastConcretize (src, tgt) ->
+      "concretize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
 
 and nullop_to_string (env : 'a fmt_env) (op : nullop) : string =
   match op with

charon-ml/src/generated/Generated_Expressions.ml

@@ -139,6 +139,20 @@ and cast_kind =
   | CastTransmute of ty * ty
       (** Reinterprets the bits of a value of one type as another type, i.e.
           exactly what [[std::mem::transmute]] does. *)
+  | CastConcretize of ty * ty
+      (** Converts a receiver type with [dyn Trait<...>] to a concrete type [T],
+          used in vtable method shims. Valid conversions are references, raw
+          pointers, and (optionally) boxes:
+          - [&[mut] dyn Trait<...>] -> [&[mut] T]
+          - [*[mut] dyn Trait<...>] -> [*[mut] T]
+          - [Box<dyn Trait<...>>] -> [Box<T>] when no [--raw-boxes]
+
+          For possible receivers, see:
+          https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility.
+          Other receivers, e.g., [Rc] should be unpacked before the cast and
+          re-boxed after. FIXME(ssyram): but this is not implemented yet,
+          namely, there may still be something like
+          [Rc<dyn Trait<...>> -> Rc<T>] in the types. *)
 
 and constant_expr = { kind : constant_expr_kind; ty : ty }
 

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -279,6 +279,10 @@ and cast_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* x_0 = ty_of_json ctx x_0 in
         let* x_1 = ty_of_json ctx x_1 in
         Ok (CastTransmute (x_0, x_1))
+    | `Assoc [ ("Concretize", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = ty_of_json ctx x_0 in
+        let* x_1 = ty_of_json ctx x_1 in
+        Ok (CastConcretize (x_0, x_1))
     | _ -> Error "")
 
 and cli_options_of_json (ctx : of_json_ctx) (js : json) :
@@ -1098,6 +1102,7 @@ and item_source_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("VTableInstance", `Assoc [ ("impl_ref", impl_ref) ]) ] ->
         let* impl_ref = trait_impl_ref_of_json ctx impl_ref in
         Ok (VTableInstanceItem impl_ref)
+    | `String "VTableMethodShim" -> Ok VTableMethodShimItem
     | _ -> Error "")
 
 and layout_of_json (ctx : of_json_ctx) (js : json) : (layout, string) result =

charon-ml/src/generated/Generated_Types.ml

@@ -769,6 +769,10 @@ and item_source =
 
           Fields:
           - [impl_ref] *)
+  | VTableMethodShimItem
+      (** The method shim wraps a concrete implementation of a method into a
+          function that takes [dyn Trait] as its [Self] type. This shim casts
+          the receiver to the known concrete type and calls the real method. *)
 
 (** Simplified type layout information.
 

charon/Cargo.toml

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

charon/src/ast/expressions.rs

@@ -202,6 +202,17 @@ pub enum CastKind {
     /// Reinterprets the bits of a value of one type as another type, i.e. exactly what
     /// [`std::mem::transmute`] does.
     Transmute(Ty, Ty),
+    /// Converts a receiver type with `dyn Trait<...>` to a concrete type `T`, used in vtable method shims.
+    /// Valid conversions are references, raw pointers, and (optionally) boxes:
+    /// - `&[mut] dyn Trait<...>` -> `&[mut] T`
+    /// - `*[mut] dyn Trait<...>` -> `*[mut] T`
+    /// - `Box<dyn Trait<...>>` -> `Box<T>` when no `--raw-boxes`
+    ///
+    /// For possible receivers, see: https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility.
+    /// Other receivers, e.g., `Rc` should be unpacked before the cast and re-boxed after.
+    /// FIXME(ssyram): but this is not implemented yet, namely, there may still be
+    ///     something like `Rc<dyn Trait<...>> -> Rc<T>` in the types.
+    Concretize(Ty, Ty),
 }
 
 #[derive(

charon/src/ast/gast.rs

@@ -133,6 +133,10 @@ pub enum ItemSource {
     },
     /// This is a vtable value for an impl.
     VTableInstance { impl_ref: TraitImplRef },
+    /// The method shim wraps a concrete implementation of a method into a function that takes `dyn
+    /// Trait` as its `Self` type. This shim casts the receiver to the known concrete type and
+    /// calls the real method.
+    VTableMethodShim,
 }
 
 /// A function definition

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

@@ -1047,7 +1047,9 @@ impl BodyTransCtx<'_, '_, '_> {
                     // We ignore the arguments
                     return Ok(TerminatorKind::Abort(AbortKind::Panic(Some(name))));
                 } else {
-                    let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
+                    let fn_ptr = self
+                        .translate_fn_ptr(span, item, TransItemSourceKind::Fun)?
+                        .erase();
                     FnOperand::Regular(fn_ptr)
                 }
             }

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

@@ -129,7 +129,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                 expressions::ConstantExprKind::Var(var)
             }
             ConstantExprKind::FnPtr(item) => {
-                let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
+                let fn_ptr = self
+                    .translate_fn_ptr(span, item, TransItemSourceKind::Fun)?
+                    .erase();
                 expressions::ConstantExprKind::FnPtr(fn_ptr)
             }
             ConstantExprKind::Memory(bytes) => {

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

@@ -504,6 +504,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
         &mut self,
         span: Span,
         item: &hax::ItemRef,
+        kind: TransItemSourceKind,
     ) -> Result<MaybeBuiltinFunDeclRef, Error> {
         match self.recognize_builtin_fun(item)? {
             Some(id) => {
@@ -514,7 +515,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                     generics: Box::new(generics),
                 })
             }
-            None => self.translate_item(span, item, TransItemSourceKind::Fun),
+            None => self.translate_item(span, item, kind),
         }
     }
 
@@ -525,8 +526,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
         &mut self,
         span: Span,
         item: &hax::ItemRef,
+        kind: TransItemSourceKind,
     ) -> Result<RegionBinder<FnPtr>, Error> {
-        let fun_item = self.translate_fun_item(span, item)?;
+        let fun_item = self.translate_fun_item(span, item, kind)?;
         let late_bound = match self.hax_def(item)?.kind() {
             hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
                 Some(sig.as_ref().rebind(()))

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

@@ -165,11 +165,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                 self.translated.fun_decls.set_slot(id, fun_decl);
             }
             TransItemSourceKind::VTableMethod => {
-                // let Some(ItemId::Fun(id)) = trans_id else {
-                //     unreachable!()
-                // };
-                // let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
-                // self.translated.fun_decls.set_slot(id, fun_decl);
+                let Some(ItemId::Fun(id)) = trans_id else {
+                    unreachable!()
+                };
+                let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?;
+                self.translated.fun_decls.set_slot(id, fun_decl);
             }
         }
         Ok(())

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

@@ -362,6 +362,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                 name.name
                     .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
             }
+            TransItemSourceKind::VTableMethod => {
+                name.name.push(PathElem::Ident(
+                    "{vtable_method}".into(),
+                    Disambiguator::ZERO,
+                ));
+            }
             _ => {}
         }
         Ok(name)