From aed06a73aea97e8d87eafa1d0e4853d8c24601b2 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Mon, 29 Jul 2024 06:05:43 -0700 Subject: [PATCH] Rudimentary support for dynamic trait objects (#664) * add stuff to generic_const test * next: onto lower type * next: into constraint_gen * yay, dyn00 works (doesn't keel over) * yay, dyn01 checks/fails as expected * allow region vars in dyn * Update crates/flux-middle/src/fhir/lift.rs * use Dynamic instead of PolyTraitRef * remove DynKind (only support Dyn) else panic * implement to_rustc for Dynamic/ExistentialPredicates * Update crates/flux-middle/src/rustc/lowering.rs * check dyn exi-preds are equal during subtyping * use span_bug * dont fill lifetimes in fill_generic_args Co-authored-by: Nico Lehmann --- .../flux-fhir-analysis/src/conv/fill_holes.rs | 7 +++ crates/flux-fhir-analysis/src/conv/mod.rs | 41 ++++++++++++++-- crates/flux-middle/src/fhir.rs | 5 ++ crates/flux-middle/src/fhir/lift.rs | 8 ++++ crates/flux-middle/src/fhir/visit.rs | 4 ++ crates/flux-middle/src/rty/fold.rs | 43 +++++++++++++++-- crates/flux-middle/src/rty/mod.rs | 47 ++++++++++++++++++- crates/flux-middle/src/rty/pretty.rs | 14 ++++++ crates/flux-middle/src/rty/refining.rs | 31 ++++++++++++ crates/flux-middle/src/rustc/lowering.rs | 36 ++++++++++++-- crates/flux-middle/src/rustc/ty.rs | 35 ++++++++++++-- crates/flux-middle/src/rustc/ty/subst.rs | 35 +++++++++++++- crates/flux-middle/src/sort_of.rs | 1 + crates/flux-refineck/src/checker.rs | 27 +++++++---- crates/flux-refineck/src/constraint_gen.rs | 4 ++ crates/flux-refineck/src/type_env.rs | 1 + tests/tests/neg/surface/dyn01.rs | 36 ++++++++++++++ tests/tests/pos/surface/dyn00.rs | 23 +++++++++ tests/tests/pos/surface/dyn02.rs | 8 ++++ tests/tests/pos/surface/dyn03.rs | 11 +++++ tests/tests/pos/surface/dyn04.rs | 10 ++++ 21 files changed, 400 insertions(+), 27 deletions(-) create mode 100644 tests/tests/neg/surface/dyn01.rs create mode 100644 tests/tests/pos/surface/dyn00.rs create mode 100644 tests/tests/pos/surface/dyn02.rs create mode 100644 tests/tests/pos/surface/dyn03.rs create mode 100644 tests/tests/pos/surface/dyn04.rs diff --git a/crates/flux-fhir-analysis/src/conv/fill_holes.rs b/crates/flux-fhir-analysis/src/conv/fill_holes.rs index 4738ef6a44..288ec0096a 100644 --- a/crates/flux-fhir-analysis/src/conv/fill_holes.rs +++ b/crates/flux-fhir-analysis/src/conv/fill_holes.rs @@ -216,6 +216,13 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { (rty::BaseTy::Param(pty_a), ty::TyKind::Param(pty_b)) => { debug_assert_eq!(pty_a, pty_b); } + ( + rty::BaseTy::Dynamic(poly_trait_refs, re_a), + ty::TyKind::Dynamic(poly_trait_refs_b, re_b), + ) => { + self.zip_region(re_a, re_b); + debug_assert_eq!(poly_trait_refs.len(), poly_trait_refs_b.len()); + } (rty::BaseTy::Closure(..), _) => { bug!("unexpected closure {a:?}"); } diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 123f43e101..0b6c8cd4ab 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -9,7 +9,6 @@ //! 3. Refinements are well-sorted. mod fill_holes; - use std::{borrow::Borrow, iter}; use flux_common::{bug, iter::IterExt, span_bug}; @@ -24,7 +23,7 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc, + rustc::{self}, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -435,6 +434,29 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { Ok(clauses) } + fn conv_poly_trait_ref_dyn( + &mut self, + env: &mut Env, + poly_trait_ref: &fhir::PolyTraitRef, + ) -> QueryResult> { + let trait_segment = poly_trait_ref.trait_ref.last_segment(); + + if !poly_trait_ref.bound_generic_params.is_empty() { + bug!( + "unexpected! conv_poly_dyn_trait_ref bound_generic_params={:?}", + poly_trait_ref.bound_generic_params + ); + } + + let def_id = poly_trait_ref.trait_def_id(); + let mut into = vec![]; + self.conv_generic_args_into(env, def_id, trait_segment.args, &mut into)?; + + let exi_trait_ref = rty::ExistentialTraitRef { def_id, args: into.into() }; + let exi_pred = rty::ExistentialPredicate::Trait(exi_trait_ref); + Ok(rty::Binder::new(exi_pred, List::empty())) + } + /// Converts a `T: Trait` bound fn conv_poly_trait_ref( &mut self, @@ -453,8 +475,8 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { vec![self.ty_to_generic_arg(self_param.kind, bounded_ty_span, bounded_ty)?]; self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; self.fill_generic_args_defaults(trait_id, &mut args)?; - let trait_ref = rty::TraitRef { def_id: trait_id, args: args.into() }; + let pred = rty::TraitPredicate { trait_ref: trait_ref.clone() }; let vars = poly_trait_ref .bound_generic_params @@ -788,6 +810,18 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let alias_ty = rty::AliasTy::new(def_id, args, refine_args); Ok(rty::Ty::alias(rty::AliasKind::Opaque, alias_ty)) } + fhir::TyKind::TraitObject(poly_traits, lft, syn) => { + let exi_preds: List<_> = poly_traits + .iter() + .map(|poly_trait| self.conv_poly_trait_ref_dyn(env, poly_trait)) + .try_collect()?; + let region = self.conv_lifetime(env, *lft); + if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) { + Ok(rty::Ty::dynamic(exi_preds, region)) + } else { + span_bug!(ty.span, "dyn* traits not supported yet") + } + } } } @@ -1161,7 +1195,6 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { bug!("unexpected generic param: {param:?}"); } } - Ok(()) } diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 53debd2536..c3aeb20b69 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -25,6 +25,7 @@ use flux_common::{bug, span_bug}; use flux_syntax::surface::ParamMode; pub use flux_syntax::surface::{BinOp, UnOp}; use itertools::Itertools; +use rustc_ast::TraitObjectSyntax; use rustc_data_structures::fx::{FxIndexMap, FxIndexSet}; use rustc_hash::FxHashMap; pub use rustc_hir::PrimTy; @@ -538,6 +539,7 @@ pub enum TyKind<'fhir> { Array(&'fhir Ty<'fhir>, ConstArg), RawPtr(&'fhir Ty<'fhir>, Mutability), OpaqueDef(ItemId, &'fhir [GenericArg<'fhir>], &'fhir [RefineArg<'fhir>], bool), + TraitObject(&'fhir [PolyTraitRef<'fhir>], Lifetime, TraitObjectSyntax), Never, Hole(FhirId), } @@ -1243,6 +1245,9 @@ impl fmt::Debug for Ty<'_> { "impl trait " ) } + TyKind::TraitObject(poly_traits, _lft, _syntax) => { + write!(f, "dyn {poly_traits:?}") + } } } } diff --git a/crates/flux-middle/src/fhir/lift.rs b/crates/flux-middle/src/fhir/lift.rs index 70f776556c..6ee791c94d 100644 --- a/crates/flux-middle/src/fhir/lift.rs +++ b/crates/flux-middle/src/fhir/lift.rs @@ -387,6 +387,14 @@ impl<'a, 'genv, 'tcx> LiftCtxt<'a, 'genv, 'tcx> { let args = self.lift_generic_args(args)?; fhir::TyKind::OpaqueDef(item_id, args, &[], in_trait_def) } + hir::TyKind::TraitObject(poly_traits, lft, syntax) => { + let poly_traits = try_alloc_slice!(self.genv, poly_traits, |poly_trait| { + self.lift_poly_trait_ref(*poly_trait) + })?; + + let lft = self.lift_lifetime(lft)?; + fhir::TyKind::TraitObject(poly_traits, lft, syntax) + } _ => { return self.emit_unsupported(&format!( "unsupported type: `{}`", diff --git a/crates/flux-middle/src/fhir/visit.rs b/crates/flux-middle/src/fhir/visit.rs index f39b05ba22..48432012f9 100644 --- a/crates/flux-middle/src/fhir/visit.rs +++ b/crates/flux-middle/src/fhir/visit.rs @@ -385,6 +385,10 @@ pub fn walk_ty<'v, V: Visitor<'v>>(vis: &mut V, ty: &Ty<'v>) { } TyKind::Never => {} TyKind::Hole(_) => {} + TyKind::TraitObject(poly_traits, lft, _) => { + walk_list!(vis, visit_poly_trait_ref, poly_traits); + vis.visit_lifetime(&lft); + } } } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 50a0f79906..1b5088e3eb 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -15,10 +15,10 @@ use super::{ projections, subst::EVarSubstFolder, AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Const, - CoroutineObligPredicate, Ensures, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, - GenericArg, Invariant, KVar, Lambda, Name, Opaqueness, OutlivesPredicate, PolyFuncSort, - ProjectionPredicate, PtrKind, Qualifier, ReBound, Region, Sort, SubsetTy, TraitPredicate, - TraitRef, Ty, TyKind, + CoroutineObligPredicate, Ensures, ExistentialPredicate, ExistentialTraitRef, Expr, ExprKind, + FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, + Opaqueness, OutlivesPredicate, PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReBound, + Region, Sort, SubsetTy, TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -488,6 +488,37 @@ impl TypeFoldable for TraitRef { } } +impl TypeVisitable for ExistentialTraitRef { + fn visit_with(&self, visitor: &mut V) -> ControlFlow { + self.args.visit_with(visitor) + } +} + +impl TypeFoldable for ExistentialTraitRef { + fn try_fold_with(&self, folder: &mut F) -> Result { + Ok(ExistentialTraitRef { def_id: self.def_id, args: self.args.try_fold_with(folder)? }) + } +} + +impl TypeVisitable for ExistentialPredicate { + fn visit_with(&self, visitor: &mut V) -> ControlFlow { + match self { + ExistentialPredicate::Trait(exi_trait_ref) => exi_trait_ref.visit_with(visitor), + } + } +} + +impl TypeFoldable for ExistentialPredicate { + fn try_fold_with(&self, folder: &mut F) -> Result { + match self { + ExistentialPredicate::Trait(exi_trait_ref) => { + let exi_trait_ref = exi_trait_ref.try_fold_with(folder)?; + Ok(ExistentialPredicate::Trait(exi_trait_ref)) + } + } + } +} + impl TypeVisitable for CoroutineObligPredicate { fn visit_with(&self, visitor: &mut V) -> ControlFlow { self.upvar_tys.visit_with(visitor)?; @@ -940,6 +971,7 @@ impl TypeSuperVisitable for BaseTy { | BaseTy::Closure(_, _) | BaseTy::Never | BaseTy::Param(_) => ControlFlow::Continue(()), + BaseTy::Dynamic(exi_preds, _) => exi_preds.visit_with(visitor), } } } @@ -979,6 +1011,9 @@ impl TypeSuperFoldable for BaseTy { args.try_fold_with(folder)?, ) } + BaseTy::Dynamic(exi_preds, region) => { + BaseTy::Dynamic(exi_preds.try_fold_with(folder)?, region.try_fold_with(folder)?) + } }; Ok(bty) } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index f4da559281..011a10fed5 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -13,7 +13,6 @@ mod pretty; pub mod projections; pub mod refining; pub mod subst; - use std::{borrow::Cow, hash::Hash, iter, slice, sync::LazyLock}; pub use evars::{EVar, EVarGen}; @@ -230,6 +229,36 @@ impl TraitRef { } } +#[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub enum ExistentialPredicate { + Trait(ExistentialTraitRef), +} + +impl Binder { + fn to_rustc<'tcx>( + &self, + tcx: TyCtxt<'tcx>, + ) -> rustc_middle::ty::Binder<'tcx, rustc_middle::ty::ExistentialPredicate<'tcx>> { + assert!(self.vars.is_empty()); + match self.value { + ExistentialPredicate::Trait(ref exi_trait_ref) => { + let exi_trait_ref = rustc_middle::ty::ExistentialTraitRef { + def_id: exi_trait_ref.def_id, + args: exi_trait_ref.args.to_rustc(tcx), + }; + let exi_pred = rustc_middle::ty::ExistentialPredicate::Trait(exi_trait_ref); + rustc_middle::ty::Binder::bind_with_vars(exi_pred, rustc_middle::ty::List::empty()) + } + } + } +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub struct ExistentialTraitRef { + pub def_id: DefId, + pub args: GenericArgs, +} + #[derive(PartialEq, Eq, Hash, Debug, Clone, TyEncodable, TyDecodable)] pub struct ProjectionPredicate { pub projection_ty: AliasTy, @@ -622,6 +651,10 @@ impl Ty { Self::alias(AliasKind::Projection, alias_ty) } + pub fn dynamic(preds: impl Into>>, region: Region) -> Ty { + BaseTy::Dynamic(preds.into(), region).to_ty() + } + pub fn strg_ref(re: Region, path: Path, ty: Ty) -> Ty { TyKind::StrgRef(re, path, ty).intern() } @@ -951,6 +984,7 @@ pub enum BaseTy { Never, Closure(DefId, /* upvar_tys */ List), Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List), + Dynamic(List>, Region), Param(ParamTy), } @@ -1099,6 +1133,7 @@ impl BaseTy { | BaseTy::Array(_, _) | BaseTy::Closure(_, _) | BaseTy::Coroutine(..) + | BaseTy::Dynamic(_, _) | BaseTy::Never => Sort::unit(), } } @@ -1131,6 +1166,14 @@ impl BaseTy { BaseTy::Array(_, _) => todo!(), BaseTy::Never => tcx.types.never, BaseTy::Closure(_, _) => todo!(), + BaseTy::Dynamic(exi_preds, re) => { + let preds: Vec<_> = exi_preds + .iter() + .map(|pred| pred.to_rustc(tcx)) + .collect_vec(); + let preds = tcx.mk_poly_existential_predicates(&preds); + ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx), rustc_middle::ty::DynKind::Dyn) + } BaseTy::Coroutine(def_id, resume_ty, upvars) => { todo!("Generator {def_id:?} {resume_ty:?} {upvars:?}") // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg)); @@ -2055,6 +2098,8 @@ impl_slice_internable!( InferMode, Sort, GenericParamDef, + TraitRef, + Binder, Clause, PolyVariant, Invariant, diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index 5493c65ecd..44a02bc0bc 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -337,6 +337,17 @@ impl Pretty for List { } } +impl Pretty for ExistentialPredicate { + fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(_cx, f); + match self { + ExistentialPredicate::Trait(exi_trait_ref) => { + w!("{exi_trait_ref:?}") + } + } + } +} + impl Pretty for BaseTy { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); @@ -388,6 +399,9 @@ impl Pretty for BaseTy { } Ok(()) } + BaseTy::Dynamic(exi_preds, _) => { + w!("dyn {:?}", join!(", ", exi_preds)) + } } } } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index f95a857a62..05b1056e66 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -170,6 +170,30 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::ClauseKind::FnTrait(pred)) } + pub fn refine_existential_predicate( + &self, + exi_pred: &rustc::ty::Binder, + ) -> QueryResult> { + assert!(exi_pred.vars().is_empty()); + let exi_pred = match exi_pred.as_ref().skip_binder() { + rustc::ty::ExistentialPredicate::Trait(exi_trait_ref) => { + rty::ExistentialPredicate::Trait(self.refine_exi_trait_ref(exi_trait_ref)?) + } + }; + Ok(rty::Binder::new(exi_pred, List::empty())) + } + + pub fn refine_exi_trait_ref( + &self, + exi_trait_ref: &rustc::ty::ExistentialTraitRef, + ) -> QueryResult { + let exi_trait_ref = rty::ExistentialTraitRef { + def_id: exi_trait_ref.def_id, + args: self.refine_generic_args(exi_trait_ref.def_id, &exi_trait_ref.args)?, + }; + Ok(exi_trait_ref) + } + pub fn refine_trait_ref(&self, trait_ref: &rustc::ty::TraitRef) -> QueryResult { let trait_ref = rty::TraitRef { def_id: trait_ref.def_id, @@ -358,6 +382,13 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::RawPtr(ty, mu) => { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } + rustc::ty::TyKind::Dynamic(exi_preds, r) => { + let exi_preds = exi_preds + .iter() + .map(|ty| self.refine_existential_predicate(ty)) + .try_collect()?; + rty::BaseTy::Dynamic(exi_preds, *r) + } }; Ok(TyOrBase::Base((self.refine)(bty))) } diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 500e2c1085..604f8ddf85 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -25,15 +25,15 @@ use super::{ }, ty::{ AdtDef, AdtDefData, AliasKind, Binder, BoundRegion, BoundVariableKind, Clause, ClauseKind, - Const, ConstKind, FieldDef, FnSig, GenericArg, GenericParamDef, GenericParamDefKind, - GenericPredicates, Generics, OutlivesPredicate, PolyFnSig, TraitPredicate, TraitRef, Ty, - TypeOutlivesPredicate, VariantDef, + Const, ConstKind, ExistentialPredicate, FieldDef, FnSig, GenericArg, GenericParamDef, + GenericParamDefKind, GenericPredicates, Generics, OutlivesPredicate, PolyFnSig, + TraitPredicate, TraitRef, Ty, TypeOutlivesPredicate, VariantDef, }, }; use crate::{ const_eval::scalar_int_to_constant, intern::List, - rustc::ty::{AliasTy, ProjectionPredicate, Region}, + rustc::ty::{AliasTy, ExistentialTraitRef, ProjectionPredicate, Region}, }; pub struct LoweringCtxt<'a, 'sess, 'tcx> { @@ -740,6 +740,18 @@ pub(crate) fn lower_ty<'tcx>( let args = lower_generic_args(tcx, args)?; Ok(Ty::mk_generator_witness(*did, args)) } + rustc_ty::Dynamic(predicates, region, rustc_ty::DynKind::Dyn) => { + let region = lower_region(region)?; + + let exi_preds = List::from_vec( + predicates + .iter() + .map(|pred| lower_existential_predicate(tcx, pred)) + .try_collect()?, + ); + + Ok(Ty::mk_dynamic(exi_preds, region)) + } _ => Err(UnsupportedReason::new(format!("unsupported type `{ty:?}`"))), } } @@ -772,6 +784,22 @@ fn lower_field(f: &rustc_ty::FieldDef) -> FieldDef { FieldDef { did: f.did, name: f.name } } +pub fn lower_existential_predicate<'tcx>( + tcx: TyCtxt<'tcx>, + pred: rustc_ty::Binder>, +) -> Result, UnsupportedReason> { + assert!(pred.bound_vars().is_empty()); + let pred = pred.skip_binder(); + if let rustc_ty::ExistentialPredicate::Trait(exi_trait_ref) = pred { + let def_id = exi_trait_ref.def_id; + let args = lower_generic_args(tcx, exi_trait_ref.args)?; + let exi_trait_ref = ExistentialTraitRef { def_id, args }; + Ok(Binder::bind_with_vars(ExistentialPredicate::Trait(exi_trait_ref), List::empty())) + } else { + Err(UnsupportedReason::new(format!("Unsupported existential predicate `{pred:?}`"))) + } +} + pub fn lower_generic_args<'tcx>( tcx: TyCtxt<'tcx>, args: rustc_middle::ty::GenericArgsRef<'tcx>, diff --git a/crates/flux-middle/src/rustc/ty.rs b/crates/flux-middle/src/rustc/ty.rs index 20d068e660..410b2d25b2 100644 --- a/crates/flux-middle/src/rustc/ty.rs +++ b/crates/flux-middle/src/rustc/ty.rs @@ -43,7 +43,7 @@ pub enum BoundVariableKind { Region(BoundRegionKind), } -#[derive(Debug, Hash, Eq, PartialEq)] +#[derive(Debug, Hash, Eq, PartialEq, TyEncodable, TyDecodable)] pub struct GenericParamDef { pub def_id: DefId, pub index: u32, @@ -57,7 +57,7 @@ impl GenericParamDef { } } -#[derive(Debug, Hash, Eq, PartialEq, Clone, Copy)] +#[derive(Debug, Hash, Eq, PartialEq, Clone, Copy, TyEncodable, TyDecodable)] pub enum GenericParamDefKind { Type { has_default: bool }, Lifetime, @@ -93,7 +93,7 @@ pub struct TraitPredicate { pub trait_ref: TraitRef, } -#[derive(PartialEq, Eq, Hash, Debug)] +#[derive(PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)] pub struct TraitRef { pub def_id: DefId, pub args: GenericArgs, @@ -182,6 +182,18 @@ pub enum TyKind { CoroutineWitness(DefId, GenericArgs), Alias(AliasKind, AliasTy), RawPtr(Ty, Mutability), + Dynamic(List>, Region), +} + +#[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub enum ExistentialPredicate { + Trait(ExistentialTraitRef), +} + +#[derive(PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)] +pub struct ExistentialTraitRef { + pub def_id: DefId, + pub args: GenericArgs, } #[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] @@ -630,6 +642,10 @@ impl Ty { TyKind::Param(param).intern() } + pub fn mk_dynamic(exi_preds: impl Into>>, r: Region) -> Ty { + TyKind::Dynamic(exi_preds.into(), r).intern() + } + pub fn mk_ref(region: Region, ty: Ty, mutability: Mutability) -> Ty { TyKind::Ref(region, ty, mutability).intern() } @@ -721,13 +737,21 @@ impl Ty { TyKind::Coroutine(_, _) => todo!(), TyKind::CoroutineWitness(_, _) => todo!(), TyKind::Alias(_, _) => todo!(), + TyKind::Dynamic(_, _) => todo!(), }; rustc_ty::Ty::new(tcx, kind) } } impl_internable!(TyS, AdtDefData); -impl_slice_internable!(Ty, GenericArg, GenericParamDef, BoundVariableKind, Clause); +impl_slice_internable!( + Ty, + GenericArg, + GenericParamDef, + BoundVariableKind, + Clause, + Binder, +); impl fmt::Debug for GenericArg { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { @@ -836,6 +860,9 @@ impl fmt::Debug for Ty { write!(f, ")")?; Ok(()) } + TyKind::Dynamic(exi_preds, _r) => { + write!(f, "dyn {exi_preds:?}") + } } } } diff --git a/crates/flux-middle/src/rustc/ty/subst.rs b/crates/flux-middle/src/rustc/ty/subst.rs index 90222d449c..cc52b761b2 100644 --- a/crates/flux-middle/src/rustc/ty/subst.rs +++ b/crates/flux-middle/src/rustc/ty/subst.rs @@ -1,5 +1,11 @@ -use super::{Binder, Const, ConstKind, FnSig, GenericArg, Region, Ty, TyKind}; -use crate::intern::{Internable, List}; +use super::{ + Binder, Const, ConstKind, ExistentialPredicate, ExistentialTraitRef, FnSig, GenericArg, Region, + Ty, TyKind, +}; +use crate::{ + intern::{Internable, List}, + rustc::ty::TraitRef, +}; pub(super) trait Subst { fn subst(&self, args: &[GenericArg]) -> Self; @@ -40,6 +46,7 @@ impl Subst for Ty { TyKind::RawPtr(ty, mutbl) => Ty::mk_raw_ptr(ty.subst(args), *mutbl), TyKind::Param(param_ty) => args[param_ty.index as usize].expect_type().clone(), TyKind::FnPtr(fn_sig) => Ty::mk_fn_ptr(fn_sig.subst(args)), + TyKind::Dynamic(exi_preds, re) => Ty::mk_dynamic(exi_preds.subst(args), *re), TyKind::Bool | TyKind::Uint(_) | TyKind::Str @@ -51,6 +58,30 @@ impl Subst for Ty { } } +impl Subst for TraitRef { + fn subst(&self, args: &[GenericArg]) -> Self { + let def_id = self.def_id; + TraitRef { def_id, args: self.args.subst(args) } + } +} + +impl Subst for ExistentialTraitRef { + fn subst(&self, args: &[GenericArg]) -> Self { + let def_id = self.def_id; + ExistentialTraitRef { def_id, args: self.args.subst(args) } + } +} + +impl Subst for ExistentialPredicate { + fn subst(&self, args: &[GenericArg]) -> Self { + match self { + ExistentialPredicate::Trait(exi_trait_ref) => { + ExistentialPredicate::Trait(exi_trait_ref.subst(args)) + } + } + } +} + impl Subst for GenericArg { fn subst(&self, args: &[GenericArg]) -> Self { match self { diff --git a/crates/flux-middle/src/sort_of.rs b/crates/flux-middle/src/sort_of.rs index f8498c3af0..edf42397aa 100644 --- a/crates/flux-middle/src/sort_of.rs +++ b/crates/flux-middle/src/sort_of.rs @@ -104,6 +104,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { | fhir::TyKind::Ref(_, _) | fhir::TyKind::Tuple(_) | fhir::TyKind::Array(_, _) + | fhir::TyKind::TraitObject(_, _, _) | fhir::TyKind::Never => Ok(Some(rty::Sort::unit())), fhir::TyKind::Hole(_) | fhir::TyKind::StrgRef(..) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 69f90e46dc..7585550e73 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -959,19 +959,30 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { } } } - // &mut [T; n] -> &mut [T][n] and &[T; n] -> &[T][n] CastKind::Pointer(mir::PointerCast::Unsize) => { if let TyKind::Indexed(BaseTy::Ref(_, src_ty, src_mut), _) = from.kind() - && let TyKind::Indexed(BaseTy::Array(src_arr_ty, src_n), _) = src_ty.kind() + && let TyKind::Indexed(src_base_ty, _) = src_ty.kind() && let rustc::ty::TyKind::Ref(dst_re, dst_ty, dst_mut) = to.kind() - && let rustc::ty::TyKind::Slice(_) = dst_ty.kind() - && src_mut == dst_mut { - let idx = Expr::from_const(self.genv.tcx(), src_n); - let dst_slice = Ty::indexed(BaseTy::Slice(src_arr_ty.clone()), idx); - Ty::mk_ref(*dst_re, dst_slice, *dst_mut) + // &mut [T; n] -> &mut [T][n] and &[T; n] -> &[T][n] + if let rustc::ty::TyKind::Slice(_) = dst_ty.kind() + && let BaseTy::Array(src_arr_ty, src_n) = src_base_ty + && src_mut == dst_mut + { + let idx = Expr::from_const(self.genv.tcx(), src_n); + let dst_slice = Ty::indexed(BaseTy::Slice(src_arr_ty.clone()), idx); + Ty::mk_ref(*dst_re, dst_slice, *dst_mut) + } else + // &T -> & dyn U + if let rustc::ty::TyKind::Dynamic(_, _) = dst_ty.kind() { + self.genv + .refine_default(&self.generics, to) + .with_span(self.body.span())? + } else { + tracked_span_bug!("unsupported Unsize cast: from {from:?} to {to:?}") + } } else { - tracked_span_bug!("unsupported Unsize cast") + tracked_span_bug!("unsupported Unsize cast: from {from:?} to {to:?}") } } CastKind::FloatToInt diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 615da96d95..315a3487a4 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -584,6 +584,10 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { | (BaseTy::Str, BaseTy::Str) | (BaseTy::Char, BaseTy::Char) | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) => Ok(()), + (BaseTy::Dynamic(preds1, _), BaseTy::Dynamic(preds2, _)) => { + assert_eq!(preds1, preds2); + Ok(()) + } (BaseTy::Closure(did1, tys1), BaseTy::Closure(did2, tys2)) if did1 == did2 => { debug_assert_eq!(tys1.len(), tys2.len()); for (ty1, ty2) in iter::zip(tys1, tys2) { diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 3af5e9e643..609ed25279 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -373,6 +373,7 @@ impl BasicBlockEnvShape { | BaseTy::Char | BaseTy::Never | BaseTy::Closure(_, _) + | BaseTy::Dynamic(_, _) | BaseTy::Coroutine(..) => bty.clone(), } } diff --git a/tests/tests/neg/surface/dyn01.rs b/tests/tests/neg/surface/dyn01.rs new file mode 100644 index 0000000000..f821ed0ed3 --- /dev/null +++ b/tests/tests/neg/surface/dyn01.rs @@ -0,0 +1,36 @@ +#![allow(unused)] + +// ------------------------------------------------------ + +trait Shape { + #[flux::sig(fn(self: _) -> i32{v: 0 <= v})] + fn vertices(&self) -> i32; +} + +// ------------------------------------------------------ + +struct Circle {} + +impl Shape for Circle { + fn vertices(&self) -> i32 { + 0 + } +} + +// ------------------------------------------------------ + +#[flux::sig(fn(shape: _) -> i32{v: 0 <= v})] +fn count(shape: &dyn Shape) -> i32 { + shape.vertices() +} + +#[flux::sig(fn(shape: _) -> i32{v: 10 <= v})] +fn count_bad(shape: &dyn Shape) -> i32 { + shape.vertices() //~ ERROR: refinement type +} + +fn main() { + let c = Circle {}; + count(&c); + count_bad(&c); +} diff --git a/tests/tests/pos/surface/dyn00.rs b/tests/tests/pos/surface/dyn00.rs new file mode 100644 index 0000000000..6be59a67dd --- /dev/null +++ b/tests/tests/pos/surface/dyn00.rs @@ -0,0 +1,23 @@ +#![allow(unused)] + +trait Animal { + fn noise(&self); +} + +struct Cow {} + +impl Animal for Cow { + fn noise(&self) { + println!("moooooo!"); + } +} + +fn make_two_noises(animal: &dyn Animal) { + animal.noise(); + animal.noise(); +} + +fn main() { + let cow = Cow {}; + make_two_noises(&cow); +} diff --git a/tests/tests/pos/surface/dyn02.rs b/tests/tests/pos/surface/dyn02.rs new file mode 100644 index 0000000000..fe0dd607c8 --- /dev/null +++ b/tests/tests/pos/surface/dyn02.rs @@ -0,0 +1,8 @@ +pub trait Animal { + fn noise(&self); +} + +#[flux::trusted] +pub fn get_animal() -> &'static dyn Animal { + unimplemented!() +} diff --git a/tests/tests/pos/surface/dyn03.rs b/tests/tests/pos/surface/dyn03.rs new file mode 100644 index 0000000000..e24b9c931f --- /dev/null +++ b/tests/tests/pos/surface/dyn03.rs @@ -0,0 +1,11 @@ +#![allow(dead_code)] + +pub struct Cow {} + +pub trait CowContainer<'apple> { + fn get_cow(&self) -> &'apple Cow; +} + +pub struct CowCell<'banana> { + inner: &'banana dyn CowContainer<'banana>, +} diff --git a/tests/tests/pos/surface/dyn04.rs b/tests/tests/pos/surface/dyn04.rs new file mode 100644 index 0000000000..34602e4272 --- /dev/null +++ b/tests/tests/pos/surface/dyn04.rs @@ -0,0 +1,10 @@ +pub trait Animal { + fn noise(&self); +} + +pub fn apply_closure_to_animal(closure: F, animal: &'static dyn Animal) +where + F: FnOnce(&dyn Animal), +{ + closure(animal); +}