Merge pull request #788 from Nadrieril/vtables

Generate explicit structs and values for trait vtables

Author: Nadrieril

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.121"
+let supported_charon_version = "0.1.122"

charon-ml/src/generated/Generated_GAst.ml

@@ -209,6 +209,9 @@ type trait_decl = {
           The binder contains the type parameters specific to the method. The
           [FunDeclRef] then provides a full list of arguments to the pointed-to
           function. *)
+  vtable : type_decl_ref option;
+      (** The virtual table struct for this trait, if it has one. It is
+          guaranteed that the trait has a vtable iff it is dyn-compatible. *)
 }
 [@@deriving
   show,
@@ -256,6 +259,9 @@ type trait_impl = {
       (** The associated types declared in the trait. *)
   methods : (trait_item_name * fun_decl_ref binder) list;
       (** The implemented methods *)
+  vtable : global_decl_ref option;
+      (** The virtual table instance for this trait implementation. This is
+          [Some] iff the trait is dyn-compatible. *)
 }
 [@@deriving
   show,

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1041,6 +1041,12 @@ and item_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* item_name = trait_item_name_of_json ctx item_name in
         let* reuses_default = bool_of_json ctx reuses_default in
         Ok (TraitImplItem (impl_ref, trait_ref, item_name, reuses_default))
+    | `Assoc [ ("VTableTy", `Assoc [ ("dyn_predicate", dyn_predicate) ]) ] ->
+        let* dyn_predicate = dyn_predicate_of_json ctx dyn_predicate in
+        Ok (VTableTyItem dyn_predicate)
+    | `Assoc [ ("VTableInstance", `Assoc [ ("impl_ref", impl_ref) ]) ] ->
+        let* impl_ref = trait_impl_ref_of_json ctx impl_ref in
+        Ok (VTableInstanceItem impl_ref)
     | _ -> Error "")
 
 and item_meta_of_json (ctx : of_json_ctx) (js : json) :
@@ -1569,6 +1575,7 @@ and trait_decl_of_json (ctx : of_json_ctx) (js : json) :
           ("type_defaults", _);
           ("type_clauses", _);
           ("methods", methods);
+          ("vtable", vtable);
         ] ->
         let* def_id = trait_decl_id_of_json ctx def_id in
         let* item_meta = item_meta_of_json ctx item_meta in
@@ -1589,6 +1596,7 @@ and trait_decl_of_json (ctx : of_json_ctx) (js : json) :
                (binder_of_json fun_decl_ref_of_json))
             ctx methods
         in
+        let* vtable = option_of_json type_decl_ref_of_json ctx vtable in
         Ok
           ({
              def_id;
@@ -1598,6 +1606,7 @@ and trait_decl_of_json (ctx : of_json_ctx) (js : json) :
              consts;
              types;
              methods;
+             vtable;
            }
             : trait_decl)
     | _ -> Error "")
@@ -1634,6 +1643,7 @@ and trait_impl_of_json (ctx : of_json_ctx) (js : json) :
           ("types", types);
           ("type_clauses", _);
           ("methods", methods);
+          ("vtable", vtable);
         ] ->
         let* def_id = trait_impl_id_of_json ctx def_id in
         let* item_meta = item_meta_of_json ctx item_meta in
@@ -1659,6 +1669,7 @@ and trait_impl_of_json (ctx : of_json_ctx) (js : json) :
                (binder_of_json fun_decl_ref_of_json))
             ctx methods
         in
+        let* vtable = option_of_json global_decl_ref_of_json ctx vtable in
         Ok
           ({
              def_id;
@@ -1669,6 +1680,7 @@ and trait_impl_of_json (ctx : of_json_ctx) (js : json) :
              consts;
              types;
              methods;
+             vtable;
            }
             : trait_impl)
     | _ -> Error "")

charon-ml/src/generated/Generated_Types.ml

@@ -717,6 +717,17 @@ and item_kind =
           - [reuses_default]: True if the trait decl had a default
             implementation for this function/const and this item is a copy of
             the default item. *)
+  | VTableTyItem of dyn_predicate
+      (** This is a vtable struct for a trait.
+
+          Fields:
+          - [dyn_predicate]: The [dyn Trait] predicate implemented by this
+            vtable. *)
+  | VTableInstanceItem of trait_impl_ref
+      (** This is a vtable value for an impl.
+
+          Fields:
+          - [impl_ref] *)
 
 (** Meta information about an item (function, trait decl, trait impl, type decl,
     global). *)

charon/Cargo.lock

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

charon/Cargo.toml

@@ -471,6 +471,7 @@ impl From<FunDeclRef> for FnPtr {
 /// reading the constant `a.b` is translated to `{ _1 = const a; _2 = (_1.0) }`.
 #[derive(
     Debug,
+    Hash,
     PartialEq,
     Eq,
     Clone,
@@ -485,7 +486,6 @@ impl From<FunDeclRef> for FnPtr {
 #[charon::variants_prefix("C")]
 pub enum RawConstantExpr {
     Literal(Literal),
-    ///
     /// In most situations:
     /// Enumeration with one variant with no fields, structure with
     /// no fields, unit (encoded as a 0-tuple).
@@ -553,7 +553,7 @@ pub enum RawConstantExpr {
     Opaque(String),
 }
 
-#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
+#[derive(Debug, Hash, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
 pub struct ConstantExpr {
     pub value: RawConstantExpr,
     pub ty: Ty,

charon/src/ast/expressions.rs

@@ -127,6 +127,13 @@ pub enum ItemKind {
         #[drive(skip)]
         reuses_default: bool,
     },
+    /// This is a vtable struct for a trait.
+    VTableTy {
+        /// The `dyn Trait` predicate implemented by this vtable.
+        dyn_predicate: DynPredicate,
+    },
+    /// This is a vtable value for an impl.
+    VTableInstance { impl_ref: TraitImplRef },
 }
 
 /// A function definition
@@ -279,6 +286,9 @@ pub struct TraitDecl {
     /// The binder contains the type parameters specific to the method. The `FunDeclRef` then
     /// provides a full list of arguments to the pointed-to function.
     pub methods: Vec<(TraitItemName, Binder<FunDeclRef>)>,
+    /// The virtual table struct for this trait, if it has one.
+    /// It is guaranteed that the trait has a vtable iff it is dyn-compatible.
+    pub vtable: Option<TypeDeclRef>,
 }
 
 /// A trait **implementation**.
@@ -313,6 +323,9 @@ pub struct TraitImpl {
     pub type_clauses: Vec<(TraitItemName, Vector<TraitClauseId, TraitRef>)>,
     /// The implemented methods
     pub methods: Vec<(TraitItemName, Binder<FunDeclRef>)>,
+    /// The virtual table instance for this trait implementation. This is `Some` iff the trait is
+    /// dyn-compatible.
+    pub vtable: Option<GlobalDeclRef>,
 }
 
 /// A function operand is used in function calls.

charon/src/ast/gast.rs

@@ -412,6 +412,47 @@ impl GenericArgs {
     }
 }
 
+impl IntTy {
+    /// Important: this returns the target byte count for the types.
+    /// Must not be used for host types from rustc.
+    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
+        match self {
+            IntTy::Isize => ptr_size as usize,
+            IntTy::I8 => size_of::<i8>(),
+            IntTy::I16 => size_of::<i16>(),
+            IntTy::I32 => size_of::<i32>(),
+            IntTy::I64 => size_of::<i64>(),
+            IntTy::I128 => size_of::<i128>(),
+        }
+    }
+}
+impl UIntTy {
+    /// Important: this returns the target byte count for the types.
+    /// Must not be used for host types from rustc.
+    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
+        match self {
+            UIntTy::Usize => ptr_size as usize,
+            UIntTy::U8 => size_of::<u8>(),
+            UIntTy::U16 => size_of::<u16>(),
+            UIntTy::U32 => size_of::<u32>(),
+            UIntTy::U64 => size_of::<u64>(),
+            UIntTy::U128 => size_of::<u128>(),
+        }
+    }
+}
+impl FloatTy {
+    /// Important: this returns the target byte count for the types.
+    /// Must not be used for host types from rustc.
+    pub fn target_size(&self) -> usize {
+        match self {
+            FloatTy::F16 => size_of::<u16>(),
+            FloatTy::F32 => size_of::<u32>(),
+            FloatTy::F64 => size_of::<u64>(),
+            FloatTy::F128 => size_of::<u128>(),
+        }
+    }
+}
+
 impl IntegerTy {
     pub fn to_unsigned(&self) -> Self {
         match self {
@@ -429,18 +470,8 @@ impl IntegerTy {
     /// Must not be used for host types from rustc.
     pub fn target_size(&self, ptr_size: ByteCount) -> usize {
         match self {
-            IntegerTy::Signed(IntTy::Isize) => ptr_size as usize,
-            IntegerTy::Signed(IntTy::I8) => size_of::<i8>(),
-            IntegerTy::Signed(IntTy::I16) => size_of::<i16>(),
-            IntegerTy::Signed(IntTy::I32) => size_of::<i32>(),
-            IntegerTy::Signed(IntTy::I64) => size_of::<i64>(),
-            IntegerTy::Signed(IntTy::I128) => size_of::<i128>(),
-            IntegerTy::Unsigned(UIntTy::Usize) => ptr_size as usize,
-            IntegerTy::Unsigned(UIntTy::U8) => size_of::<u8>(),
-            IntegerTy::Unsigned(UIntTy::U16) => size_of::<u16>(),
-            IntegerTy::Unsigned(UIntTy::U32) => size_of::<u32>(),
-            IntegerTy::Unsigned(UIntTy::U64) => size_of::<u64>(),
-            IntegerTy::Unsigned(UIntTy::U128) => size_of::<u128>(),
+            IntegerTy::Signed(ty) => ty.target_size(ptr_size),
+            IntegerTy::Unsigned(ty) => ty.target_size(ptr_size),
         }
     }
 }
@@ -453,6 +484,18 @@ impl LiteralTy {
             _ => None,
         }
     }
+
+    /// Important: this returns the target byte count for the types.
+    /// Must not be used for host types from rustc.
+    pub fn target_size(&self, ptr_size: ByteCount) -> usize {
+        match self {
+            LiteralTy::Int(int_ty) => int_ty.target_size(ptr_size),
+            LiteralTy::UInt(uint_ty) => uint_ty.target_size(ptr_size),
+            LiteralTy::Float(float_ty) => float_ty.target_size(),
+            LiteralTy::Char => 4,
+            LiteralTy::Bool => 1,
+        }
+    }
 }
 
 /// A value of type `T` bound by the generic parameters of item

charon/src/ast/types_utils.rs

@@ -501,6 +501,25 @@ impl BodyTransCtx<'_, '_, '_> {
                             }
                             hax::UnsizingMetadata::VTablePtr(impl_expr) => {
                                 let tref = self.translate_trait_impl_expr(span, impl_expr)?;
+                                match &impl_expr.r#impl {
+                                    hax::ImplExprAtom::Concrete(tref) => {
+                                        // Ensure the vtable type is translated.
+                                        let _: GlobalDeclId = self.register_item(
+                                            span,
+                                            tref,
+                                            TransItemSourceKind::VTableInstance(
+                                                TraitImplSource::Normal,
+                                            ),
+                                        );
+                                    }
+                                    // TODO(dyn): more ways of registering vtable instance?
+                                    _ => {
+                                        trace!(
+                                            "impl_expr not triggering registering vtable: {:?}",
+                                            impl_expr
+                                        )
+                                    }
+                                };
                                 UnsizingMetadata::VTablePtr(tref)
                             }
                             hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown,