From c5ecd67917351b6277c285869fee245d89494ce1 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 30 Nov 2023 10:54:00 -0300 Subject: [PATCH] Normalize term in projection predicate (#565) --- crates/flux-middle/src/rty/fold.rs | 22 +++++++++++++++++-- crates/flux-middle/src/rty/mod.rs | 6 ++++- crates/flux-middle/src/rty/refining.rs | 5 +++++ crates/flux-middle/src/rustc/lowering.rs | 18 +++++++++++++-- crates/flux-middle/src/rustc/ty.rs | 7 ++++-- crates/flux-refineck/src/checker.rs | 5 +++-- crates/flux-refineck/src/constraint_gen.rs | 15 ++++++++----- .../flux-tests/tests/pos/surface/trait04.rs | 6 +++++ 8 files changed, 70 insertions(+), 14 deletions(-) create mode 100644 crates/flux-tests/tests/pos/surface/trait04.rs diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index f9e96d03be..5c9b65bac2 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -16,8 +16,9 @@ use super::{ subst::EVarSubstFolder, AliasTy, BaseTy, Binder, BoundVariableKind, Clause, ClauseKind, Constraint, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, GeneratorObligPredicate, GenericArg, Index, - Invariant, KVar, Name, OpaqueArgsMap, Opaqueness, PolyFuncSort, ProjectionPredicate, PtrKind, - Qualifier, ReLateBound, Region, Sort, TraitPredicate, TraitRef, Ty, TyKind, + Invariant, KVar, Name, OpaqueArgsMap, Opaqueness, OutlivesPredicate, PolyFuncSort, + ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, Sort, TraitPredicate, TraitRef, + Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -429,6 +430,7 @@ impl TypeVisitable for ClauseKind { ClauseKind::Trait(pred) => pred.visit_with(visitor), ClauseKind::Projection(pred) => pred.visit_with(visitor), ClauseKind::GeneratorOblig(pred) => pred.visit_with(visitor), + ClauseKind::TypeOutlives(pred) => pred.visit_with(visitor), } } } @@ -442,10 +444,26 @@ impl TypeFoldable for ClauseKind { ClauseKind::GeneratorOblig(pred) => { Ok(ClauseKind::GeneratorOblig(pred.try_fold_with(folder)?)) } + ClauseKind::TypeOutlives(pred) => { + Ok(ClauseKind::TypeOutlives(pred.try_fold_with(folder)?)) + } } } } +impl TypeVisitable for OutlivesPredicate { + fn visit_with(&self, visitor: &mut V) -> ControlFlow { + self.0.visit_with(visitor)?; + self.1.visit_with(visitor) + } +} + +impl TypeFoldable for OutlivesPredicate { + fn try_fold_with(&self, folder: &mut F) -> Result { + Ok(OutlivesPredicate(self.0.try_fold_with(folder)?, self.1.try_fold_with(folder)?)) + } +} + impl TypeVisitable for TraitPredicate { fn visit_with(&self, visitor: &mut V) -> ControlFlow { self.trait_ref.visit_with(visitor) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index fc8445e0bc..4bed1313f4 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -28,7 +28,7 @@ use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable}; use rustc_middle::ty::ParamConst; pub use rustc_middle::{ mir::Mutability, - ty::{AdtFlags, ClosureKind, FloatTy, IntTy, ParamTy, ScalarInt, UintTy}, + ty::{AdtFlags, ClosureKind, FloatTy, IntTy, OutlivesPredicate, ParamTy, ScalarInt, UintTy}, }; use rustc_span::Symbol; pub use rustc_target::abi::{VariantIdx, FIRST_VARIANT}; @@ -105,9 +105,12 @@ pub enum ClauseKind { FnTrait(FnTraitPredicate), Trait(TraitPredicate), Projection(ProjectionPredicate), + TypeOutlives(TypeOutlivesPredicate), GeneratorOblig(GeneratorObligPredicate), } +pub type TypeOutlivesPredicate = OutlivesPredicate; + #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct TraitPredicate { pub trait_ref: TraitRef, @@ -1695,6 +1698,7 @@ mod pretty { ClauseKind::Trait(pred) => w!("Trait ({pred:?})"), ClauseKind::Projection(pred) => w!("Projection ({pred:?})"), ClauseKind::GeneratorOblig(pred) => w!("Projection ({pred:?})"), + ClauseKind::TypeOutlives(pred) => w!("Outlives ({:?}, {:?})", &pred.0, &pred.1), } } } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 2c2e4d517f..ddd0dae6c0 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -130,6 +130,10 @@ impl<'a, 'tcx> Refiner<'a, 'tcx> { }; rty::ClauseKind::Projection(pred) } + rustc::ty::ClauseKind::TypeOutlives(pred) => { + let pred = rty::OutlivesPredicate(self.as_default().refine_ty(&pred.0)?, pred.1); + rty::ClauseKind::TypeOutlives(pred) + } }; let kind = rty::Binder::new(kind, List::empty()); Ok(Some(rty::Clause { kind })) @@ -282,6 +286,7 @@ impl<'a, 'tcx> Refiner<'a, 'tcx> { _ => Ok(rty::Ty::exists(ty)), } } + fn refine_alias_kind(kind: &rustc::ty::AliasKind) -> rty::AliasKind { match kind { rustc::ty::AliasKind::Projection => rty::AliasKind::Projection, diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 052b5a5ad1..86a3b66874 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -24,8 +24,8 @@ use super::{ ty::{ AdtDef, AdtDefData, AliasKind, Binder, BoundRegion, BoundVariableKind, Clause, ClauseKind, Const, FieldDef, FnSig, GenericArg, GenericParamDef, GenericParamDefKind, - GenericPredicates, Generics, PolyFnSig, TraitPredicate, TraitRef, Ty, ValueConst, - VariantDef, + GenericPredicates, Generics, PolyFnSig, TraitPredicate, TraitRef, Ty, + TypeOutlivesPredicate, ValueConst, VariantDef, }, }; use crate::{ @@ -849,6 +849,13 @@ fn lower_clause<'tcx>( .emit(sess)?; ClauseKind::Projection(ProjectionPredicate { projection_ty, term }) } + rustc_ty::ClauseKind::TypeOutlives(outlives_pred) => { + ClauseKind::TypeOutlives( + lower_type_outlives(tcx, outlives_pred) + .map_err(|err| errors::UnsupportedGenericBound::new(span, err.descr)) + .emit(sess)?, + ) + } _ => { return Err(sess.emit_err(errors::UnsupportedGenericBound::new( span, @@ -859,6 +866,13 @@ fn lower_clause<'tcx>( Ok(Clause::new(kind)) } +fn lower_type_outlives<'tcx>( + tcx: TyCtxt<'tcx>, + pred: rustc_ty::TypeOutlivesPredicate<'tcx>, +) -> Result { + Ok(rustc_ty::OutlivesPredicate(lower_ty(tcx, pred.0)?, lower_region(&pred.1)?)) +} + mod errors { use flux_macros::Diagnostic; use rustc_middle::mir as rustc_mir; diff --git a/crates/flux-middle/src/rustc/ty.rs b/crates/flux-middle/src/rustc/ty.rs index 7e70448c33..c65d9cd466 100644 --- a/crates/flux-middle/src/rustc/ty.rs +++ b/crates/flux-middle/src/rustc/ty.rs @@ -13,8 +13,8 @@ use rustc_middle::ty::{AdtFlags, ParamConst}; pub use rustc_middle::{ mir::Mutability, ty::{ - BoundRegionKind, BoundVar, DebruijnIndex, EarlyBoundRegion, FloatTy, IntTy, ParamTy, - RegionVid, ScalarInt, UintTy, + BoundRegionKind, BoundVar, DebruijnIndex, EarlyBoundRegion, FloatTy, IntTy, + OutlivesPredicate, ParamTy, RegionVid, ScalarInt, UintTy, }, }; use rustc_span::{symbol::kw, Symbol}; @@ -72,8 +72,11 @@ pub struct Clause { pub enum ClauseKind { Trait(TraitPredicate), Projection(ProjectionPredicate), + TypeOutlives(TypeOutlivesPredicate), } +pub type TypeOutlivesPredicate = OutlivesPredicate; + #[derive(PartialEq, Eq, Hash, Debug)] pub struct TraitPredicate { pub trait_ref: TraitRef, diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 1bc6993a8a..6dbb0bae9c 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -610,8 +610,9 @@ impl<'a, 'tcx, M: Mode> Checker<'a, 'tcx, M> { rty::ClauseKind::GeneratorOblig(gen_pred) => { self.check_oblig_generator_pred(rcx, &obligs.snapshot, gen_pred)?; } - rty::ClauseKind::Projection(_) => (), - rty::ClauseKind::Trait(_) => (), + rty::ClauseKind::Projection(_) + | rty::ClauseKind::Trait(_) + | rty::ClauseKind::TypeOutlives(_) => {} } } Ok(()) diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 85ec88f0e6..64bb0793e3 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -198,7 +198,6 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> { .collect_vec(); let genv = self.genv; - let callsite_def_id = self.def_id; let span = self.span; if let Some(did) = callee_def_id { @@ -228,7 +227,7 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> { }, |sort, mode| infcx.fresh_infer_var(sort, mode), ) - .normalize_projections(genv, infcx.region_infcx, callsite_def_id, infcx.refparams)?; + .normalize_projections(genv, infcx.region_infcx, infcx.def_id, infcx.refparams)?; let obligs = if let Some(did) = callee_def_id { mk_obligations(genv, did, &generic_args, &refine_args)? @@ -278,13 +277,19 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> { .normalize_projections( infcx.genv, infcx.region_infcx, - callsite_def_id, + infcx.def_id, infcx.refparams, )?; + let term = projection_pred.term.normalize_projections( + infcx.genv, + infcx.region_infcx, + infcx.def_id, + infcx.refparams, + )?; // TODO: does this really need to be invariant? https://github.com/flux-rs/flux/pull/478#issuecomment-1654035374 - infcx.subtyping(rcx, &impl_elem, &projection_pred.term)?; - infcx.subtyping(rcx, &projection_pred.term, &impl_elem)?; + infcx.subtyping(rcx, &impl_elem, &term)?; + infcx.subtyping(rcx, &term, &impl_elem)?; } } // Replace evars diff --git a/crates/flux-tests/tests/pos/surface/trait04.rs b/crates/flux-tests/tests/pos/surface/trait04.rs new file mode 100644 index 0000000000..4eae65ce33 --- /dev/null +++ b/crates/flux-tests/tests/pos/surface/trait04.rs @@ -0,0 +1,6 @@ +const A: &[i32] = &[0]; +const B: &[i32] = &[1]; + +fn test() -> Vec<&'static i32> { + A.iter().chain(B).collect() +}