Don't crash on dyn Trait

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.17"
+let supported_charon_version = "0.1.18"

charon-ml/src/GAstOfJson.ml

@@ -372,6 +372,7 @@ let rec ty_of_json (js : json) : (ty, string) result =
         let* inputs = list_of_json ty_of_json inputs in
         let* output = ty_of_json output in
         Ok (TArrow (regions, inputs, output))
+    | `Assoc [ ("DynTrait", `Null) ] -> Ok (TDynTrait ())
     | `String "Never" -> Ok TNever
     | _ -> Error "")
 
@@ -450,6 +451,9 @@ and trait_instance_id_of_json (js : json) : (trait_instance_id, string) result =
         let* fid = FunDeclId.id_of_json fid in
         let* generics = generic_args_of_json generics in
         Ok (Closure (fid, generics))
+    | `Assoc [ ("Dyn", id) ] ->
+        let* id = TraitDeclId.id_of_json id in
+        Ok (Dyn id)
     | `Assoc [ ("Unsolved", `List [ decl_id; generics ]) ] ->
         let* decl_id = TraitDeclId.id_of_json decl_id in
         let* generics = generic_args_of_json generics in

charon-ml/src/NameMatcher.ml

@@ -866,6 +866,7 @@ and ty_to_pattern_aux (ctx : ctx) (c : to_pat_config) (m : constraints)
       EArrow (inputs, out)
   | TRawPtr (ty, RMut) -> ERawPtr (Mut, ty_to_pattern_aux ctx c m ty)
   | TRawPtr (ty, RShared) -> ERawPtr (Not, ty_to_pattern_aux ctx c m ty)
+  | TDynTrait _ -> raise (Failure "Unimplemented: DynTrait")
   | TNever -> raise (Failure "Unimplemented: Never")
 
 and trait_ref_item_with_generics_to_pattern (ctx : ctx) (c : to_pat_config)

charon-ml/src/PrintTypes.ml

@@ -167,6 +167,7 @@ and ty_to_string (env : ('a, 'b) fmt_env) (ty : ty) : string =
         "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> "
       in
       inputs ^ ty_to_string env output
+  | TDynTrait _ -> "dyn (TODO)"
 
 and params_to_string (env : ('a, 'b) fmt_env) (is_tuple : bool)
     (generics : generic_args) : string =
@@ -239,6 +240,7 @@ and trait_instance_id_to_string (env : ('a, 'b) fmt_env)
       ^ fun_decl_id_to_string env fid
       ^ generic_args_to_string env generics
       ^ ")"
+  | Dyn id -> "dyn(" ^ trait_decl_id_to_string env id ^ ")"
   | Unsolved (decl_id, generics) ->
       "unsolved("
       ^ trait_decl_id_to_string env decl_id

charon-ml/src/Types.ml

@@ -288,6 +288,7 @@ and ty =
   | TTraitType of trait_ref * string
       (** The string is for the name of the associated type *)
   | TArrow of region_var list * ty list * ty
+  | TDynTrait of unit
 
 and trait_ref = {
   trait_id : trait_instance_id;
@@ -331,6 +332,7 @@ and trait_instance_id =
        *)
   | FnPointer of ty
   | Closure of fun_decl_id * generic_args
+  | Dyn of trait_decl_id
   | Unsolved of trait_decl_id * generic_args
   | UnknownTrait of string
       (** Not present in the Rust version of Charon.

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.17"
+version = "0.1.18"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 

charon/src/ast/types.rs

@@ -134,14 +134,9 @@ pub enum Region {
     Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd, Drive, DriveMut,
 )]
 pub enum TraitInstanceId {
-    ///
-    /// A specific implementation
+    /// A specific top-level implementation item.
     TraitImpl(TraitImplId),
-    ///
-    /// A specific builtin trait implementation like [core::marker::Sized] or
-    /// auto trait implementation like [core::marker::Syn].
-    BuiltinOrAuto(TraitDeclId),
-    ///
+
     /// One of the local clauses.
     ///
     /// Example:
@@ -151,7 +146,7 @@ pub enum TraitInstanceId {
     ///                    Clause(0)
     /// ```
     Clause(TraitClauseId),
-    ///
+
     /// A parent clause
     ///
     /// Remark: the [TraitDeclId] gives the trait declaration which is
@@ -179,7 +174,7 @@ pub enum TraitInstanceId {
     /// }
     /// ```
     ParentClause(Box<TraitInstanceId>, TraitDeclId, TraitClauseId),
-    ///
+
     /// A clause bound in a trait item (typically a trait clause in an
     /// associated type).
     ///
@@ -213,22 +208,28 @@ pub enum TraitInstanceId {
         TraitItemName,
         TraitClauseId,
     ),
-    ///
+
     /// Self, in case of trait declarations/implementations.
     ///
     /// Putting [Self] at the end on purpose, so that when ordering the clauses
     /// we start with the other clauses (in particular, the local clauses). It
     /// is useful to give priority to the local clauses when solving the trait
     /// obligations which are fullfilled by the trait parameters.
     SelfId,
+
+    /// A specific builtin trait implementation like [core::marker::Sized] or
+    /// auto trait implementation like [core::marker::Syn].
+    BuiltinOrAuto(TraitDeclId),
+
+    /// The automatically-generated implementation for `dyn Trait`.
+    Dyn(TraitDeclId),
+
     /// For error reporting.
     Unknown(String),
 }
 
 /// A reference to a trait
-#[derive(
-    Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd, Drive, DriveMut,
-)]
+#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
 pub struct TraitRef {
     pub trait_id: TraitInstanceId,
     pub generics: GenericArgs,
@@ -245,9 +246,7 @@ pub struct TraitRef {
 /// ```
 ///
 /// The substitution is: `[String, bool]`.
-#[derive(
-    Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Ord, PartialOrd, Drive, DriveMut,
-)]
+#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
 pub struct TraitDeclRef {
     pub trait_id: TraitDeclId,
     pub generics: GenericArgs,
@@ -292,9 +291,7 @@ pub struct TraitTypeConstraint {
     pub ty: Ty,
 }
 
-#[derive(
-    Debug, Clone, Eq, PartialEq, Serialize, Deserialize, Hash, Ord, PartialOrd, Drive, DriveMut,
-)]
+#[derive(Debug, Clone, Eq, PartialEq, Serialize, Deserialize, Hash, Drive, DriveMut)]
 pub struct GenericArgs {
     pub regions: Vec<Region>,
     pub types: Vec<Ty>,
@@ -325,6 +322,12 @@ pub struct GenericParams {
     pub trait_type_constraints: Vec<TraitTypeConstraint>,
 }
 
+/// A predicate of the form `exists<T> where T: Trait`.
+///
+/// TODO: store something useful here
+#[derive(Debug, Default, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
+pub struct ExistentialPredicate;
+
 generate_index_type!(TraitClauseId, "TraitClause");
 generate_index_type!(TraitDeclId, "TraitDecl");
 generate_index_type!(TraitImplId, "TraitImpl");
@@ -611,8 +614,6 @@ pub enum ConstGeneric {
     Deserialize,
     Drive,
     DriveMut,
-    Ord,
-    PartialOrd,
 )]
 pub enum Ty {
     /// An ADT.
@@ -655,6 +656,13 @@ pub enum Ty {
     /// }
     /// ```
     TraitType(TraitRef, TraitItemName),
+    /// `dyn Trait`
+    ///
+    /// This carries an existentially quantified list of predicates, e.g. `exists<T> where T:
+    /// Into<u64>`. The predicate must quantify over a single type and no any regions or constants.
+    ///
+    /// TODO: we don't translate this properly yet.
+    DynTrait(ExistentialPredicate),
     /// Arrow type, used in particular for the local function pointers.
     /// This is essentially a "constrained" function signature:
     /// arrow types can only contain generic lifetime parameters

charon/src/ast/types_utils.rs

@@ -275,25 +275,6 @@ impl Ty {
     }
 }
 
-impl Ty {
-    // TODO: reimplement this with visitors
-    pub fn contains_never(&self) -> bool {
-        match self {
-            Ty::Never => true,
-            Ty::Adt(_, args) => {
-                // For the trait type case: we are checking the projected type,
-                // so we don't need to explore the trait ref
-                args.types.iter().any(|ty| ty.contains_never())
-            }
-            Ty::TraitType(..) | Ty::TypeVar(_) | Ty::Literal(_) => false,
-            Ty::Ref(_, ty, _) | Ty::RawPtr(ty, _) => ty.contains_never(),
-            Ty::Arrow(_, inputs, box output) => {
-                inputs.iter().any(|ty| ty.contains_never()) || output.contains_never()
-            }
-        }
-    }
-}
-
 pub struct TySubst {
     pub ignore_regions: bool,
     /// This map is from regions to regions, not from region ids to regions.

charon/src/pretty/fmt_with_ctx.rs

@@ -135,6 +135,12 @@ impl<C: AstFormatter> FmtWithCtx<C> for DeclarationGroup {
     }
 }
 
+impl<C: AstFormatter> FmtWithCtx<C> for ExistentialPredicate {
+    fn fmt_with_ctx(&self, _ctx: &C) -> String {
+        format!("exists(TODO)")
+    }
+}
+
 impl<C: AstFormatter> FmtWithCtx<C> for Field {
     fn fmt_with_ctx(&self, ctx: &C) -> String {
         match &self.name {
@@ -1234,7 +1240,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitInstanceId {
             }
             TraitInstanceId::TraitImpl(id) => ctx.format_object(*id),
             TraitInstanceId::Clause(id) => ctx.format_object(*id),
-            TraitInstanceId::BuiltinOrAuto(id) => ctx.format_object(*id),
+            TraitInstanceId::BuiltinOrAuto(id) | TraitInstanceId::Dyn(id) => ctx.format_object(*id),
             TraitInstanceId::Unknown(msg) => format!("UNKNOWN({msg})"),
         }
     }
@@ -1289,6 +1295,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for Ty {
             Ty::TraitType(trait_ref, name) => {
                 format!("{}::{name}", trait_ref.fmt_with_ctx(ctx),)
             }
+            Ty::DynTrait(pred) => format!("dyn ({})", pred.with_ctx(ctx)),
             Ty::Arrow(regions, inputs, box output) => {
                 // Update the bound regions
                 let ctx = &ctx.push_bound_regions(regions);

charon/src/translate/translate_predicates.rs

@@ -663,14 +663,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let trait_decl_id = self.register_trait_decl_id(span, def_id)?.unwrap();
 
                 // Retrieve the arguments
+                assert!(nested.is_empty());
                 let generics = self.translate_substs_and_trait_refs(
                     span,
                     erase_regions,
                     None,
                     &trait_ref.generic_args,
                     nested,
                 )?;
-                assert!(generics.trait_refs.is_empty());
 
                 // If we are refering to a trait clause, we need to find the
                 // relevant one.
@@ -734,9 +734,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     trait_decl_ref,
                 }
             }
-            ImplExprAtom::Dyn { .. } => {
-                error_or_panic!(self, span, "Unsupported trait impl source kind: object")
-            }
+            ImplExprAtom::Dyn => TraitRef {
+                trait_id: TraitInstanceId::Dyn(trait_decl_ref.trait_id),
+                generics: GenericArgs::empty(),
+                trait_decl_ref,
+            },
             ImplExprAtom::Builtin { r#trait: trait_ref } => {
                 let def_id = DefId::from(&trait_ref.def_id);
                 // Remark: we already filtered the marker traits when translating

charon/src/translate/translate_types.rs

@@ -337,9 +337,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 error_or_panic!(self, span, "Unsupported type: infer type")
             }
 
-            hax::Ty::Dynamic(_, _, _) => {
+            hax::Ty::Dynamic(_existential_preds, _region, _) => {
+                // TODO: we don't translate the predicates yet because our machinery can't handle
+                // it.
                 trace!("Dynamic");
-                error_or_panic!(self, span, "Dynamic types are not supported yet")
+                Ok(Ty::DynTrait(ExistentialPredicate))
             }
 
             hax::Ty::Coroutine(..) => {

charon/tests/ui/dyn-trait.out

@@ -0,0 +1,86 @@
+# Final LLBC before serialization:
+
+opaque type core::fmt::Formatter<'a>
+  where
+      'a : 'a,
+
+enum core::result::Result<T, E> =
+|  Ok(T)
+|  Err(E)
+
+
+struct core::fmt::Error = {}
+
+trait core::fmt::Display<Self>
+{
+    fn fmt : core::fmt::Display::fmt
+}
+
+fn test_crate::construct<T>(@1: T) -> alloc::boxed::Box<dyn (exists(TODO))>
+where
+    [@TraitClause0]: core::fmt::Display<T>,
+
+opaque type alloc::string::String
+
+trait alloc::string::ToString<Self>
+{
+    fn to_string : alloc::string::ToString::to_string
+}
+
+fn alloc::string::{impl alloc::string::ToString for T#32}::to_string<'_0, T>(@1: &'_0 (T)) -> alloc::string::String
+where
+    // Inherited clauses:
+    [@TraitClause0]: core::fmt::Display<T>,
+
+impl<T> alloc::string::{impl alloc::string::ToString for T#32}<T> : alloc::string::ToString<T>
+where
+    [@TraitClause0]: core::fmt::Display<T>,
+{
+    fn to_string = alloc::string::{impl alloc::string::ToString for T#32}::to_string
+}
+
+fn alloc::string::ToString::to_string<'_0, Self>(@1: &'_0 (Self)) -> alloc::string::String
+
+fn test_crate::destruct<'_0>(@1: &'_0 (dyn (exists(TODO)))) -> alloc::string::String
+{
+    let @0: alloc::string::String; // return
+    let x@1: &'_ (dyn (exists(TODO))); // arg #1
+    let @2: &'_ (dyn (exists(TODO))); // anonymous local
+
+    @2 := &*(x@1)
+    @0 := alloc::string::{impl alloc::string::ToString for T#32}<dyn (exists(TODO))>[core::fmt::Display]::to_string(move (@2))
+    drop @2
+    return
+}
+
+fn test_crate::combine()
+
+fn test_crate::foo<'_0, '_1, T>(@1: &'_0 (dyn (exists(TODO))), @2: &'_1 (dyn (exists(TODO))))
+{
+    let @0: (); // return
+    let @1: &'_ (dyn (exists(TODO))); // arg #1
+    let @2: &'_ (dyn (exists(TODO))); // arg #2
+    let @3: (); // anonymous local
+
+    @3 := ()
+    @0 := move (@3)
+    @0 := ()
+    return
+}
+
+fn test_crate::bar<'_0>(@1: &'_0 (dyn (exists(TODO))))
+{
+    let @0: (); // return
+    let @1: &'_ (dyn (exists(TODO))); // arg #1
+    let @2: (); // anonymous local
+
+    @2 := ()
+    @0 := move (@2)
+    @0 := ()
+    return
+}
+
+fn core::fmt::Display::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>
+
+
+