Basic support for dyn

source/rust_verify/src/fn_call_to_vir.rs

@@ -241,6 +241,12 @@ pub(crate) fn fn_call_to_vir<'tcx>(
                     is_trait_default: true,
                 }
             }
+            ResolutionResult::Builtin(
+                rustc_trait_selection::traits::BuiltinImplSource::Object(_),
+            ) => {
+                // dyn T dispatch
+                vir::ast::CallTargetKind::Dynamic
+            }
             ResolutionResult::Builtin(b) => {
                 unsupported_err!(expr.span, format!("built-in instance {:?}", b));
             }

source/rust_verify/src/rust_to_vir.rs

@@ -550,6 +550,7 @@ pub fn crate_to_vir<'a, 'tcx>(
     )?;
 
     crate::rust_to_vir_adts::setup_type_invariants(&mut vir)?;
+    vir::traits::set_krate_dyn_compatibility(imported, &mut vir);
 
     Ok(Arc::new(vir))
 }

source/rust_verify/src/rust_to_vir_base.rs

@@ -855,13 +855,29 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>(
     ty: &rustc_middle::ty::Ty<'tcx>,
     allow_mut_ref: bool,
 ) -> Result<(Typ, bool), VirErr> {
+    use rustc_middle::ty::GenericArgs;
     use vir::ast::TypDecoration;
     let t_rec = |t: &rustc_middle::ty::Ty<'tcx>| {
         mid_ty_to_vir_ghost(tcx, verus_items, None, param_env_src, span, t, allow_mut_ref)
     };
     let t_rec_flags = |t: &rustc_middle::ty::Ty<'tcx>, allow_mut_ref: bool| {
         mid_ty_to_vir_ghost(tcx, verus_items, None, param_env_src, span, t, allow_mut_ref)
     };
+    let mk_typ_args = |args: &GenericArgs<'tcx>| -> Result<Vec<(Typ, bool)>, VirErr> {
+        let mut typ_args: Vec<(Typ, bool)> = Vec::new();
+        for arg in args.iter() {
+            match arg.kind() {
+                rustc_middle::ty::GenericArgKind::Type(t) => {
+                    typ_args.push(t_rec(&t)?);
+                }
+                rustc_middle::ty::GenericArgKind::Lifetime(_) => {}
+                rustc_middle::ty::GenericArgKind::Const(cnst) => {
+                    typ_args.push((mid_ty_const_to_vir(tcx, Some(span), &cnst)?, false));
+                }
+            }
+        }
+        Ok(typ_args)
+    };
     let t = match ty.kind() {
         TyKind::Bool => (Arc::new(TypX::Bool), false),
         TyKind::Uint(_) | TyKind::Int(_) => (Arc::new(TypX::Int(mk_range(verus_items, ty))), false),
@@ -951,18 +967,7 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>(
                     ));
                 }
 
-                let mut typ_args: Vec<(Typ, bool)> = Vec::new();
-                for arg in args.iter() {
-                    match arg.kind() {
-                        rustc_middle::ty::GenericArgKind::Type(t) => {
-                            typ_args.push(t_rec(&t)?);
-                        }
-                        rustc_middle::ty::GenericArgKind::Lifetime(_) => {}
-                        rustc_middle::ty::GenericArgKind::Const(cnst) => {
-                            typ_args.push((mid_ty_const_to_vir(tcx, Some(span), &cnst)?, false));
-                        }
-                    }
-                }
+                let typ_args = mk_typ_args(&args)?;
                 if Some(did) == tcx.lang_items().owned_box() && typ_args.len() == 2 {
                     let (t0, ghost) = &typ_args[0];
                     let alloc_dec = Some(TypDecorationArg { allocator_typ: typ_args[1].0.clone() });
@@ -1180,39 +1185,54 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>(
                 }
             };
 
-            let mut typ_args: Vec<(Typ, bool)> = Vec::new();
-            for arg in args.iter() {
-                match arg.kind() {
-                    rustc_middle::ty::GenericArgKind::Type(t) => {
-                        typ_args.push(mid_ty_to_vir_ghost(
-                            tcx,
-                            verus_items,
-                            None,
-                            param_env_src,
-                            span,
-                            &t,
-                            allow_mut_ref,
-                        )?);
-                    }
-                    rustc_middle::ty::GenericArgKind::Lifetime(_) => {}
-                    rustc_middle::ty::GenericArgKind::Const(cnst) => {
-                        typ_args.push((mid_ty_const_to_vir(tcx, Some(span), &cnst)?, false));
-                    }
-                }
-            }
+            let typ_args = mk_typ_args(&args)?;
             let typ_args = typ_args.into_iter().map(|(t, _)| t).collect();
             let path = def_id_to_vir_path(tcx, verus_items, *def_id, None);
             let fun = Arc::new(vir::ast::FunX { path });
 
             let typx = TypX::FnDef(fun, Arc::new(typ_args), resolved);
             (Arc::new(typx), false)
         }
+        TyKind::Dynamic(preds, _, rustc_middle::ty::DynKind::Dyn) => {
+            use rustc_middle::ty::ExistentialPredicate;
+            if preds.len() != 1 {
+                unsupported_err!(span, "dyn with more that one trait");
+            }
+            match preds[0].skip_binder() {
+                ExistentialPredicate::Trait(trait_ref) => {
+                    let trait_did = trait_ref.def_id;
+                    let args = trait_ref.args;
+                    let trait_path = def_id_to_vir_path(tcx, verus_items, trait_did, None);
+                    let self_arg = GenericArg::from(*ty);
+                    let mut ty_args_with_self = vec![self_arg];
+                    ty_args_with_self.extend(args.into_iter());
+                    let args_with_self = tcx.mk_args(&ty_args_with_self);
+                    let typ_args = mk_typ_args(&args)?;
+                    let typ_args = typ_args.into_iter().map(|(t, _)| t).collect();
+                    let impl_paths = get_impl_paths(
+                        tcx,
+                        verus_items,
+                        param_env_src,
+                        trait_did,
+                        args_with_self,
+                        None,
+                    );
+                    let typx = TypX::Dyn(trait_path, Arc::new(typ_args), impl_paths);
+                    (Arc::new(typx), false)
+                }
+                ExistentialPredicate::Projection(_) => {
+                    unsupported_err!(span, "dyn with projections");
+                }
+                ExistentialPredicate::AutoTrait(_def_id) => {
+                    unsupported_err!(span, "dyn with auto-traits");
+                }
+            }
+        }
         TyKind::Foreign(..) => unsupported_err!(span, "foreign types"),
         TyKind::Ref(_, _, rustc_ast::Mutability::Mut) => {
             unsupported_err!(span, "&mut types, except in special cases")
         }
         TyKind::FnPtr(..) => unsupported_err!(span, "function pointer types"),
-        TyKind::Dynamic(..) => unsupported_err!(span, "dynamic types"),
         TyKind::Coroutine(..) => unsupported_err!(span, "generator types"),
         TyKind::CoroutineWitness(..) => unsupported_err!(span, "generator witness types"),
         TyKind::Bound(..) => unsupported_err!(span, "for<'a> types"),

source/rust_verify/src/rust_to_vir_expr.rs

@@ -53,6 +53,7 @@ use vir::ast_util::{
 };
 use vir::def::{field_ident_from_rust, positional_field_ident};
 
+#[derive(Clone, Debug)]
 pub(crate) enum ExprOrPlace {
     Expr(vir::ast::Expr),
     Place(Place),
@@ -1281,6 +1282,18 @@ pub(crate) fn expr_to_vir_with_adjustments<'tcx>(
                 adjustment_idx - 1,
             )?;
 
+            let (tyr1, tyr2) = remove_decoration_typs_for_unsizing(bctx.ctxt.tcx, ty1, ty2);
+            let op = match (tyr1.kind(), tyr2.kind()) {
+                (_, TyKind::Dynamic(_, _, rustc_middle::ty::DynKind::Dyn)) => Some(UnaryOp::ToDyn),
+                _ => None,
+            };
+            if let Some(op) = op {
+                let arg = arg.consume(bctx, get_inner_ty());
+                let x = ExprX::Unary(op, arg);
+                let expr_typ = bctx.mid_ty_to_vir(expr.span, &ty2, false)?;
+                return Ok(ExprOrPlace::Expr(bctx.spanned_typed_new(expr.span, &expr_typ, x)));
+            }
+
             let f = match (ty1.kind(), ty2.kind()) {
                 (TyKind::RawPtr(t1, _), TyKind::RawPtr(t2, _)) => {
                     match (t1.kind(), t2.kind()) {

source/rust_verify/src/rust_to_vir_trait.rs

@@ -468,6 +468,7 @@ pub(crate) fn translate_trait<'tcx>(
             Safety::Safe => false,
             Safety::Unsafe => true,
         },
+        dyn_compatible: None,
         external_trait_extension,
     };
     vir.traits.push(ctxt.spanned_new(trait_span, traitx));

source/rust_verify/src/trait_check.rs

@@ -130,6 +130,7 @@ fn index_set<Idx, V>(&mut self, index: Idx, val: V) { panic!() }
 impl<A:?Sized> IndexSet for A {}
 struct C<const N: usize, A: ?Sized>(Box<A>);
 struct Arr<A: ?Sized, const N: usize>(Box<A>);
+struct Dyn<const N: usize, A>(Box<A>, [bool]);
 fn use_type_invariant<A>(a: A) -> A { a }
 
 struct FnProof<'a, P, M, N, A, O>(PhantomData<P>, PhantomData<M>, PhantomData<N>, PhantomData<&'a fn(A) -> O>);

source/rust_verify/src/trait_check_ast.rs

@@ -36,6 +36,9 @@ pub(crate) enum TypX {
     TraitSelf,
     Tuple(Vec<Typ>),
     Datatype(Id, Vec<Id>, Vec<Typ>),
+    Dyn(Id, Vec<Typ>),
+    Slice(Typ),
+    StrSlice,
     Projection {
         self_typ: Typ,
         // use Datatype(Id, Vec<Typ>) to represent (trait_path, trait_typ_args)

source/rust_verify/src/trait_check_emit.rs

@@ -85,6 +85,13 @@ impl ToString for TypX {
             TypX::Datatype(path, lifetimes, args) => {
                 typ_args_to_string(Some(path), lifetimes, args, &None)
             }
+            TypX::Dyn(path, args) => {
+                format!("dyn {}", typ_args_to_string(Some(path), &vec![], args, &None))
+            }
+            TypX::Slice(elem) => {
+                format!("[{}]", elem.to_string())
+            }
+            TypX::StrSlice => "str".to_string(),
             TypX::Projection { self_typ, trait_as_datatype: tr, name, assoc_typ_args } => {
                 format!(
                     "<{} as {}>::{}",

source/rust_verify/src/trait_conflicts.rs

@@ -40,8 +40,6 @@ use vir::ast::{
 #[derive(Copy, Clone)]
 enum TypNum {
     SpecFn,
-    Slice,
-    StrSlice,
     Ptr,
     Ref,
     MutRef,
@@ -101,6 +99,10 @@ fn gen_typ(state: &mut State, typ: &vir::ast::Typ) -> Typ {
         vir::ast::TypX::Datatype(Dt::Path(path), typs, _) => {
             Box::new(TypX::Datatype(state.datatype_name(path), vec![], gen_typs(state, typs)))
         }
+        vir::ast::TypX::Dyn(path, typs, _) => {
+            let id = state.trait_name(path);
+            Box::new(TypX::Dyn(id, gen_typs(state, typs)))
+        }
         vir::ast::TypX::Primitive(Primitive::Array, ts) => {
             assert!(ts.len() == 2);
             Box::new(TypX::Datatype(
@@ -109,11 +111,20 @@ fn gen_typ(state: &mut State, typ: &vir::ast::Typ) -> Typ {
                 gen_typs(state, ts),
             ))
         }
+        // Handle Slice and StrSlice specially to preserve unsizedness
+        vir::ast::TypX::Primitive(Primitive::Slice, ts) => {
+            assert!(ts.len() == 1);
+            Box::new(TypX::Slice(gen_typ(state, &ts[0])))
+        }
+        vir::ast::TypX::Primitive(Primitive::StrSlice, ts) => {
+            assert!(ts.len() == 0);
+            Box::new(TypX::StrSlice)
+        }
         vir::ast::TypX::Primitive(prim, ts) => {
             let n = match prim {
                 Primitive::Array => unreachable!(),
-                Primitive::Slice => TypNum::Slice,
-                Primitive::StrSlice => TypNum::StrSlice,
+                Primitive::Slice => unreachable!(),
+                Primitive::StrSlice => unreachable!(),
                 Primitive::Ptr => TypNum::Ptr,
                 Primitive::Global => TypNum::Global,
             };
@@ -165,7 +176,10 @@ fn gen_typ(state: &mut State, typ: &vir::ast::Typ) -> Typ {
         vir::ast::TypX::TypeId | vir::ast::TypX::Air(..) => {
             panic!("internal error: unexpected type")
         }
-        vir::ast::TypX::MutRef(_) => todo!(),
+        vir::ast::TypX::MutRef(t) => {
+            let ts = vec![t.clone()];
+            gen_num_typ(TypNum::MutRef, gen_typs(state, &ts))
+        }
     }
 }
 
@@ -319,6 +333,14 @@ pub(crate) fn gen_check_trait_impl_conflicts(
                 fields.push(Box::new(TypX::Datatype(box_name, Vec::new(), vec![t])));
             }
         }
+        if d.x.variants.len() == 1 {
+            let variant = &d.x.variants[0];
+            if let Some(field) = variant.fields.last() {
+                // For structs, we need to preserve the last field so Rust can
+                // determine the sizedness of the struct
+                fields.push(gen_typ(state, &field.a.0));
+            }
+        }
         let decl = DatatypeDecl {
             name: state.datatype_name(path),
             span: spans.from_air_span(&d.span, None),
@@ -408,4 +430,64 @@ pub(crate) fn gen_check_trait_impl_conflicts(
         };
         state.trait_impls.push(decl);
     }
+
+    // For each trait T<A: TA, ...> { type X: TX; ... } for which there is a dyn T,
+    // declare an impl modeling dyn T's blanket impl:
+    //   impl<A: TA, ...X: TX, ...> T<A, ...> for Dyn<n_T, (Box<A>, ..., Box<X>, ...)> { type X = X; ... }
+    // This works around https://github.com/rust-lang/rust/issues/57893 .
+    // This (and vir::traits::get_dyn_traits) can be removed when that issue is fixed.
+    let dyn_traits: HashSet<Path> = vir::traits::get_dyn_traits(vir_crate);
+    let mut n_trait: usize = 0;
+    for t in &vir_crate.traits {
+        if !dyn_traits.contains(&t.x.name) {
+            continue;
+        }
+        let name = state.trait_name(&t.x.name);
+        let span = spans.from_air_span(&t.span, None);
+        let (mut generic_params, mut generic_bounds) = gen_generics(
+            state,
+            &t.x.typ_params.iter().map(|(x, _)| x.clone()).collect(),
+            &t.x.typ_bounds,
+            None,
+        );
+        let t_args =
+            generic_params.iter().map(|p| Box::new(TypX::TypParam(p.name.clone()))).collect();
+        let (a_params, a_bounds) =
+            gen_generics(state, &t.x.assoc_typs, &t.x.assoc_typs_bounds, None);
+        let mut assoc_typs: Vec<(Id, Vec<GenericParam>, Typ)> = Vec::new();
+        for x in &a_params {
+            // TODO: test associated types once we support "dyn with more than one trait"
+            generic_params.push(x.clone());
+            assoc_typs.push((x.name.clone(), vec![], Box::new(TypX::TypParam(x.name.clone()))));
+        }
+        generic_bounds.extend(a_bounds);
+
+        let t1 = Box::new(TypX::Primitive(n_trait.to_string()));
+        let box_name = Id::new(IdKind::Builtin, 0, "Box".to_owned());
+        let ts = generic_params
+            .iter()
+            .map(|x| Box::new(TypX::TypParam(x.name.clone())))
+            .map(|t| Box::new(TypX::Datatype(box_name.clone(), Vec::new(), vec![t])))
+            .collect();
+        let t2 = Box::new(TypX::Tuple(ts));
+        let self_typ = Box::new(TypX::Datatype(
+            Id::new(IdKind::Builtin, 0, "Dyn".to_owned()),
+            vec![],
+            vec![t1, t2],
+        ));
+        let trait_as_datatype = Box::new(TypX::Datatype(name, Vec::new(), t_args));
+        let trait_polarity = rustc_middle::ty::ImplPolarity::Positive;
+        let decl = TraitImpl {
+            span,
+            self_typ,
+            generic_params,
+            generic_bounds,
+            trait_as_datatype,
+            assoc_typs,
+            trait_polarity,
+            is_clone: false,
+        };
+        state.trait_impls.push(decl);
+        n_trait += 1;
+    }
 }