summaryrefslogtreecommitdiffstats
path: root/vendor/chalk-solve-0.87.0/src/wf.rs
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/wf.rs')
-rw-r--r--vendor/chalk-solve-0.87.0/src/wf.rs1202
1 files changed, 0 insertions, 1202 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/wf.rs b/vendor/chalk-solve-0.87.0/src/wf.rs
deleted file mode 100644
index d552cdde7..000000000
--- a/vendor/chalk-solve-0.87.0/src/wf.rs
+++ /dev/null
@@ -1,1202 +0,0 @@
-use std::ops::ControlFlow;
-use std::{fmt, iter};
-
-use crate::{
- ext::*, goal_builder::GoalBuilder, rust_ir::*, solve::Solver, split::Split, RustIrDatabase,
-};
-use chalk_ir::{
- cast::*,
- fold::shift::Shift,
- interner::Interner,
- visit::{TypeVisitable, TypeVisitor},
- *,
-};
-use tracing::debug;
-
-#[derive(Debug)]
-pub enum WfError<I: Interner> {
- IllFormedTypeDecl(chalk_ir::AdtId<I>),
- IllFormedOpaqueTypeDecl(chalk_ir::OpaqueTyId<I>),
- IllFormedTraitImpl(chalk_ir::TraitId<I>),
-}
-
-impl<I: Interner> fmt::Display for WfError<I> {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- match self {
- WfError::IllFormedTypeDecl(id) => write!(
- f,
- "type declaration `{:?}` does not meet well-formedness requirements",
- id
- ),
- WfError::IllFormedOpaqueTypeDecl(id) => write!(
- f,
- "opaque type declaration `{:?}` does not meet well-formedness requirements",
- id
- ),
- WfError::IllFormedTraitImpl(id) => write!(
- f,
- "trait impl for `{:?}` does not meet well-formedness requirements",
- id
- ),
- }
- }
-}
-
-impl<I: Interner> std::error::Error for WfError<I> {}
-
-pub struct WfSolver<'a, I: Interner> {
- db: &'a dyn RustIrDatabase<I>,
- solver_builder: &'a dyn Fn() -> Box<dyn Solver<I>>,
-}
-
-struct InputTypeCollector<I: Interner> {
- types: Vec<Ty<I>>,
- interner: I,
-}
-
-impl<I: Interner> InputTypeCollector<I> {
- fn new(interner: I) -> Self {
- Self {
- types: Vec::new(),
- interner,
- }
- }
-
- fn types_in(interner: I, value: impl TypeVisitable<I>) -> Vec<Ty<I>> {
- let mut collector = Self::new(interner);
- value.visit_with(&mut collector, DebruijnIndex::INNERMOST);
- collector.types
- }
-}
-
-impl<I: Interner> TypeVisitor<I> for InputTypeCollector<I> {
- type BreakTy = ();
- fn as_dyn(&mut self) -> &mut dyn TypeVisitor<I, BreakTy = Self::BreakTy> {
- self
- }
-
- fn interner(&self) -> I {
- self.interner
- }
-
- fn visit_where_clause(
- &mut self,
- where_clause: &WhereClause<I>,
- outer_binder: DebruijnIndex,
- ) -> ControlFlow<()> {
- match where_clause {
- WhereClause::AliasEq(alias_eq) => alias_eq
- .alias
- .clone()
- .intern(self.interner)
- .visit_with(self, outer_binder),
- WhereClause::Implemented(trait_ref) => trait_ref.visit_with(self, outer_binder),
- WhereClause::TypeOutlives(TypeOutlives { ty, .. }) => ty.visit_with(self, outer_binder),
- WhereClause::LifetimeOutlives(..) => ControlFlow::Continue(()),
- }
- }
-
- fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> ControlFlow<()> {
- let interner = self.interner();
-
- let mut push_ty = || {
- self.types
- .push(ty.clone().shifted_out_to(interner, outer_binder).unwrap())
- };
- match ty.kind(interner) {
- TyKind::Adt(id, substitution) => {
- push_ty();
- id.visit_with(self, outer_binder);
- substitution.visit_with(self, outer_binder)
- }
- TyKind::AssociatedType(assoc_ty, substitution) => {
- push_ty();
- assoc_ty.visit_with(self, outer_binder);
- substitution.visit_with(self, outer_binder)
- }
- TyKind::Scalar(scalar) => {
- push_ty();
- scalar.visit_with(self, outer_binder)
- }
- TyKind::Str => {
- push_ty();
- ControlFlow::Continue(())
- }
- TyKind::Tuple(arity, substitution) => {
- push_ty();
- arity.visit_with(self, outer_binder);
- substitution.visit_with(self, outer_binder)
- }
- TyKind::OpaqueType(opaque_ty, substitution) => {
- push_ty();
- opaque_ty.visit_with(self, outer_binder);
- substitution.visit_with(self, outer_binder)
- }
- TyKind::Slice(substitution) => {
- push_ty();
- substitution.visit_with(self, outer_binder)
- }
- TyKind::FnDef(fn_def, substitution) => {
- push_ty();
- fn_def.visit_with(self, outer_binder);
- substitution.visit_with(self, outer_binder)
- }
- TyKind::Ref(mutability, lifetime, ty) => {
- push_ty();
- mutability.visit_with(self, outer_binder);
- lifetime.visit_with(self, outer_binder);
- ty.visit_with(self, outer_binder)
- }
- TyKind::Raw(mutability, substitution) => {
- push_ty();
- mutability.visit_with(self, outer_binder);
- substitution.visit_with(self, outer_binder)
- }
- TyKind::Never => {
- push_ty();
- ControlFlow::Continue(())
- }
- TyKind::Array(ty, const_) => {
- push_ty();
- ty.visit_with(self, outer_binder);
- const_.visit_with(self, outer_binder)
- }
- TyKind::Closure(_id, substitution) => {
- push_ty();
- substitution.visit_with(self, outer_binder)
- }
- TyKind::Generator(_generator, substitution) => {
- push_ty();
- substitution.visit_with(self, outer_binder)
- }
- TyKind::GeneratorWitness(_witness, substitution) => {
- push_ty();
- substitution.visit_with(self, outer_binder)
- }
- TyKind::Foreign(_foreign_ty) => {
- push_ty();
- ControlFlow::Continue(())
- }
- TyKind::Error => {
- push_ty();
- ControlFlow::Continue(())
- }
-
- TyKind::Dyn(clauses) => {
- push_ty();
- clauses.visit_with(self, outer_binder)
- }
-
- TyKind::Alias(AliasTy::Projection(proj)) => {
- push_ty();
- proj.visit_with(self, outer_binder)
- }
-
- TyKind::Alias(AliasTy::Opaque(opaque_ty)) => {
- push_ty();
- opaque_ty.visit_with(self, outer_binder)
- }
-
- TyKind::Placeholder(_) => {
- push_ty();
- ControlFlow::Continue(())
- }
-
- // Type parameters do not carry any input types (so we can sort of assume they are
- // always WF).
- TyKind::BoundVar(..) => ControlFlow::Continue(()),
-
- // Higher-kinded types such as `for<'a> fn(&'a u32)` introduce their own implied
- // bounds, and these bounds will be enforced upon calling such a function. In some
- // sense, well-formedness requirements for the input types of an HKT will be enforced
- // lazily, so no need to include them here.
- TyKind::Function(..) => ControlFlow::Continue(()),
-
- TyKind::InferenceVar(..) => {
- panic!("unexpected inference variable in wf rules: {:?}", ty)
- }
- }
- }
-}
-
-impl<'a, I> WfSolver<'a, I>
-where
- I: Interner,
-{
- /// Constructs a new `WfSolver`.
- pub fn new(
- db: &'a dyn RustIrDatabase<I>,
- solver_builder: &'a dyn Fn() -> Box<dyn Solver<I>>,
- ) -> Self {
- Self { db, solver_builder }
- }
-
- pub fn verify_adt_decl(&self, adt_id: AdtId<I>) -> Result<(), WfError<I>> {
- let interner = self.db.interner();
-
- // Given a struct like
- //
- // ```rust
- // struct Foo<T> where T: Eq {
- // data: Vec<T>
- // }
- // ```
- let adt_datum = self.db.adt_datum(adt_id);
- let is_enum = adt_datum.kind == AdtKind::Enum;
-
- let mut gb = GoalBuilder::new(self.db);
- let adt_data = adt_datum
- .binders
- .map_ref(|b| (&b.variants, &b.where_clauses));
-
- // We make a goal like...
- //
- // forall<T> { ... }
- let wg_goal = gb.forall(
- &adt_data,
- is_enum,
- |gb, _, (variants, where_clauses), is_enum| {
- let interner = gb.interner();
-
- // (FromEnv(T: Eq) => ...)
- gb.implies(
- where_clauses
- .iter()
- .cloned()
- .map(|wc| wc.into_from_env_goal(interner)),
- |gb| {
- let sub_goals: Vec<_> = variants
- .iter()
- .flat_map(|variant| {
- let fields = &variant.fields;
-
- // When checking if Enum is well-formed, we require that all fields of
- // each variant are sized. For `structs`, we relax this requirement to
- // all but the last field.
- let sized_constraint_goal =
- WfWellKnownConstraints::struct_sized_constraint(
- gb.db(),
- fields,
- is_enum,
- );
-
- // WellFormed(Vec<T>), for each field type `Vec<T>` or type that appears in the where clauses
- let types = InputTypeCollector::types_in(
- gb.interner(),
- (&fields, &where_clauses),
- );
-
- types
- .into_iter()
- .map(|ty| ty.well_formed().cast(interner))
- .chain(sized_constraint_goal.into_iter())
- })
- .collect();
-
- gb.all(sub_goals)
- },
- )
- },
- );
-
- let wg_goal = wg_goal.into_closed_goal(interner);
- let mut fresh_solver = (self.solver_builder)();
- let is_legal = fresh_solver.has_unique_solution(self.db, &wg_goal);
-
- if !is_legal {
- Err(WfError::IllFormedTypeDecl(adt_id))
- } else {
- Ok(())
- }
- }
-
- pub fn verify_trait_impl(&self, impl_id: ImplId<I>) -> Result<(), WfError<I>> {
- let interner = self.db.interner();
-
- let impl_datum = self.db.impl_datum(impl_id);
- let trait_id = impl_datum.trait_id();
-
- let impl_goal = Goal::all(
- interner,
- impl_header_wf_goal(self.db, impl_id).into_iter().chain(
- impl_datum
- .associated_ty_value_ids
- .iter()
- .filter_map(|&id| compute_assoc_ty_goal(self.db, id)),
- ),
- );
-
- if let Some(well_known) = self.db.trait_datum(trait_id).well_known {
- self.verify_well_known_impl(impl_id, well_known)?
- }
-
- debug!("WF trait goal: {:?}", impl_goal);
-
- let mut fresh_solver = (self.solver_builder)();
- let is_legal =
- fresh_solver.has_unique_solution(self.db, &impl_goal.into_closed_goal(interner));
-
- if is_legal {
- Ok(())
- } else {
- Err(WfError::IllFormedTraitImpl(trait_id))
- }
- }
-
- pub fn verify_opaque_ty_decl(&self, opaque_ty_id: OpaqueTyId<I>) -> Result<(), WfError<I>> {
- // Given an opaque type like
- // ```notrust
- // opaque type Foo<T>: Clone where T: Bar = Baz;
- // ```
- let interner = self.db.interner();
-
- let mut gb = GoalBuilder::new(self.db);
-
- let datum = self.db.opaque_ty_data(opaque_ty_id);
- let bound = &datum.bound;
-
- // We make a goal like
- //
- // forall<T>
- let goal = gb.forall(bound, opaque_ty_id, |gb, _, bound, opaque_ty_id| {
- let interner = gb.interner();
-
- let subst = Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id));
-
- let bounds = bound.bounds.clone().substitute(interner, &subst);
- let where_clauses = bound.where_clauses.clone().substitute(interner, &subst);
-
- let clauses = where_clauses
- .iter()
- .cloned()
- .map(|wc| wc.into_from_env_goal(interner));
-
- // if (WellFormed(T: Bar))
- gb.implies(clauses, |gb| {
- let interner = gb.interner();
-
- // all(WellFormed(Baz: Clone))
- gb.all(
- bounds
- .iter()
- .cloned()
- .map(|b| b.into_well_formed_goal(interner)),
- )
- })
- });
-
- debug!("WF opaque type goal: {:#?}", goal);
-
- let mut new_solver = (self.solver_builder)();
- let is_legal = new_solver.has_unique_solution(self.db, &goal.into_closed_goal(interner));
-
- if is_legal {
- Ok(())
- } else {
- Err(WfError::IllFormedOpaqueTypeDecl(opaque_ty_id))
- }
- }
-
- /// Verify builtin rules for well-known traits
- pub fn verify_well_known_impl(
- &self,
- impl_id: ImplId<I>,
- well_known: WellKnownTrait,
- ) -> Result<(), WfError<I>> {
- let mut solver = (self.solver_builder)();
- let impl_datum = self.db.impl_datum(impl_id);
-
- let is_legal = match well_known {
- WellKnownTrait::Copy => {
- WfWellKnownConstraints::copy_impl_constraint(&mut *solver, self.db, &impl_datum)
- }
- WellKnownTrait::Drop => {
- WfWellKnownConstraints::drop_impl_constraint(&mut *solver, self.db, &impl_datum)
- }
- WellKnownTrait::CoerceUnsized => {
- WfWellKnownConstraints::coerce_unsized_impl_constraint(
- &mut *solver,
- self.db,
- &impl_datum,
- )
- }
- WellKnownTrait::DispatchFromDyn => {
- WfWellKnownConstraints::dispatch_from_dyn_constraint(
- &mut *solver,
- self.db,
- &impl_datum,
- )
- }
- WellKnownTrait::Clone | WellKnownTrait::Unpin => true,
- // You can't add a manual implementation for the following traits:
- WellKnownTrait::Fn
- | WellKnownTrait::FnOnce
- | WellKnownTrait::FnMut
- | WellKnownTrait::Unsize
- | WellKnownTrait::Sized
- | WellKnownTrait::DiscriminantKind
- | WellKnownTrait::Generator
- | WellKnownTrait::Tuple => false,
- };
-
- if is_legal {
- Ok(())
- } else {
- Err(WfError::IllFormedTraitImpl(impl_datum.trait_id()))
- }
- }
-}
-
-fn impl_header_wf_goal<I: Interner>(
- db: &dyn RustIrDatabase<I>,
- impl_id: ImplId<I>,
-) -> Option<Goal<I>> {
- let impl_datum = db.impl_datum(impl_id);
-
- if !impl_datum.is_positive() {
- return None;
- }
-
- let impl_fields = impl_datum
- .binders
- .map_ref(|v| (&v.trait_ref, &v.where_clauses));
-
- let mut gb = GoalBuilder::new(db);
- // forall<P0...Pn> {...}
- let well_formed_goal = gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
- let interner = gb.interner();
-
- // if (WC && input types are well formed) { ... }
- gb.implies(
- impl_wf_environment(interner, where_clauses, trait_ref),
- |gb| {
- // We retrieve all the input types of the where clauses appearing on the trait impl,
- // e.g. in:
- // ```
- // impl<T, K> Foo for (T, K) where T: Iterator<Item = (HashSet<K>, Vec<Box<T>>)> { ... }
- // ```
- // we would retrieve `HashSet<K>`, `Box<T>`, `Vec<Box<T>>`, `(HashSet<K>, Vec<Box<T>>)`.
- // We will have to prove that these types are well-formed (e.g. an additional `K: Hash`
- // bound would be needed here).
- let types = InputTypeCollector::types_in(gb.interner(), &where_clauses);
-
- // Things to prove well-formed: input types of the where-clauses, projection types
- // appearing in the header, associated type values, and of course the trait ref.
- debug!(input_types=?types);
- let goals = types
- .into_iter()
- .map(|ty| ty.well_formed().cast(interner))
- .chain(Some((*trait_ref).clone().well_formed().cast(interner)));
-
- gb.all::<_, Goal<I>>(goals)
- },
- )
- });
-
- Some(well_formed_goal)
-}
-
-/// Creates the conditions that an impl (and its contents of an impl)
-/// can assume to be true when proving that it is well-formed.
-fn impl_wf_environment<'i, I: Interner>(
- interner: I,
- where_clauses: &'i [QuantifiedWhereClause<I>],
- trait_ref: &'i TraitRef<I>,
-) -> impl Iterator<Item = ProgramClause<I>> + 'i {
- // if (WC) { ... }
- let wc = where_clauses
- .iter()
- .cloned()
- .map(move |qwc| qwc.into_from_env_goal(interner).cast(interner));
-
- // We retrieve all the input types of the type on which we implement the trait: we will
- // *assume* that these types are well-formed, e.g. we will be able to derive that
- // `K: Hash` holds without writing any where clause.
- //
- // Example:
- // ```
- // struct HashSet<K> where K: Hash { ... }
- //
- // impl<K> Foo for HashSet<K> {
- // // Inside here, we can rely on the fact that `K: Hash` holds
- // }
- // ```
- let types = InputTypeCollector::types_in(interner, trait_ref);
-
- let types_wf = types
- .into_iter()
- .map(move |ty| ty.into_from_env_goal(interner).cast(interner));
-
- wc.chain(types_wf)
-}
-
-/// Associated type values are special because they can be parametric (independently of
-/// the impl), so we issue a special goal which is quantified using the binders of the
-/// associated type value, for example in:
-///
-/// ```ignore
-/// trait Foo {
-/// type Item<'a>: Clone where Self: 'a
-/// }
-///
-/// impl<T> Foo for Box<T> {
-/// type Item<'a> = Box<&'a T>;
-/// }
-/// ```
-///
-/// we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`.
-///
-/// Note that there is no binder for `T` in the above: the goal we
-/// generate is expected to be exected in the context of the
-/// larger WF goal for the impl, which already has such a
-/// binder. So the entire goal for the impl might be:
-///
-/// ```ignore
-/// forall<T> {
-/// WellFormed(Box<T>) /* this comes from the impl, not this routine */,
-/// forall<'a> { WellFormed(Box<&'a T>) },
-/// }
-/// ```
-fn compute_assoc_ty_goal<I: Interner>(
- db: &dyn RustIrDatabase<I>,
- assoc_ty_id: AssociatedTyValueId<I>,
-) -> Option<Goal<I>> {
- let mut gb = GoalBuilder::new(db);
- let assoc_ty = &db.associated_ty_value(assoc_ty_id);
-
- // Create `forall<T, 'a> { .. }`
- Some(gb.forall(
- &assoc_ty.value.map_ref(|v| &v.ty),
- assoc_ty_id,
- |gb, assoc_ty_substitution, value_ty, assoc_ty_id| {
- let interner = gb.interner();
- let db = gb.db();
-
- // Hmm, because `Arc<AssociatedTyValue>` does not implement `TypeFoldable`, we can't pass this value through,
- // just the id, so we have to fetch `assoc_ty` from the database again.
- // Implementing `TypeFoldable` for `AssociatedTyValue` doesn't *quite* seem right though, as that
- // would result in a deep clone, and the value is inert. We could do some more refatoring
- // (move the `Arc` behind a newtype, for example) to fix this, but for now doesn't
- // seem worth it.
- let assoc_ty = &db.associated_ty_value(assoc_ty_id);
-
- let (impl_parameters, projection) = db
- .impl_parameters_and_projection_from_associated_ty_value(
- assoc_ty_substitution.as_slice(interner),
- assoc_ty,
- );
-
- // If (/* impl WF environment */) { ... }
- let impl_id = assoc_ty.impl_id;
- let impl_datum = &db.impl_datum(impl_id);
- let ImplDatumBound {
- trait_ref: impl_trait_ref,
- where_clauses: impl_where_clauses,
- } = impl_datum
- .binders
- .clone()
- .substitute(interner, impl_parameters);
- let impl_wf_clauses =
- impl_wf_environment(interner, &impl_where_clauses, &impl_trait_ref);
- gb.implies(impl_wf_clauses, |gb| {
- // Get the bounds and where clauses from the trait
- // declaration, substituted appropriately.
- //
- // From our example:
- //
- // * bounds
- // * original in trait, `Clone`
- // * after substituting impl parameters, `Clone`
- // * note that the self-type is not yet supplied for bounds,
- // we will do that later
- // * where clauses
- // * original in trait, `Self: 'a`
- // * after substituting impl parameters, `Box<!T>: '!a`
- let assoc_ty_datum = db.associated_ty_data(projection.associated_ty_id);
- let AssociatedTyDatumBound {
- bounds: defn_bounds,
- where_clauses: defn_where_clauses,
- } = assoc_ty_datum
- .binders
- .clone()
- .substitute(interner, &projection.substitution);
-
- // Create `if (/* where clauses on associated type value */) { .. }`
- gb.implies(
- defn_where_clauses
- .iter()
- .cloned()
- .map(|qwc| qwc.into_from_env_goal(interner)),
- |gb| {
- let types = InputTypeCollector::types_in(gb.interner(), value_ty);
-
- // We require that `WellFormed(T)` for each type that appears in the value
- let wf_goals = types
- .into_iter()
- .map(|ty| ty.well_formed())
- .casted(interner);
-
- // Check that the `value_ty` meets the bounds from the trait.
- // Here we take the substituted bounds (`defn_bounds`) and we
- // supply the self-type `value_ty` to yield the final result.
- //
- // In our example, the bound was `Clone`, so the combined
- // result is `Box<!T>: Clone`. This is then converted to a
- // well-formed goal like `WellFormed(Box<!T>: Clone)`.
- let bound_goals = defn_bounds
- .iter()
- .cloned()
- .flat_map(|qb| qb.into_where_clauses(interner, (*value_ty).clone()))
- .map(|qwc| qwc.into_well_formed_goal(interner))
- .casted(interner);
-
- // Concatenate the WF goals of inner types + the requirements from trait
- gb.all::<_, Goal<I>>(wf_goals.chain(bound_goals))
- },
- )
- })
- },
- ))
-}
-
-/// Defines methods to compute well-formedness goals for well-known
-/// traits (e.g. a goal for all fields of struct in a Copy impl to be Copy)
-struct WfWellKnownConstraints;
-
-impl WfWellKnownConstraints {
- /// Computes a goal to prove Sized constraints on a struct definition.
- /// Struct is considered well-formed (in terms of Sized) when it either
- /// has no fields or all of it's fields except the last are proven to be Sized.
- pub fn struct_sized_constraint<I: Interner>(
- db: &dyn RustIrDatabase<I>,
- fields: &[Ty<I>],
- size_all: bool,
- ) -> Option<Goal<I>> {
- let excluded = if size_all { 0 } else { 1 };
-
- if fields.len() <= excluded {
- return None;
- }
-
- let interner = db.interner();
-
- let sized_trait = db.well_known_trait_id(WellKnownTrait::Sized)?;
-
- Some(Goal::all(
- interner,
- fields[..fields.len() - excluded].iter().map(|ty| {
- TraitRef {
- trait_id: sized_trait,
- substitution: Substitution::from1(interner, ty.clone()),
- }
- .cast(interner)
- }),
- ))
- }
-
- /// Verify constraints on a Copy implementation.
- /// Copy impl is considered well-formed for
- /// a) certain builtin types (scalar values, shared ref, etc..)
- /// b) adts which
- /// 1) have all Copy fields
- /// 2) don't have a Drop impl
- fn copy_impl_constraint<I: Interner>(
- solver: &mut dyn Solver<I>,
- db: &dyn RustIrDatabase<I>,
- impl_datum: &ImplDatum<I>,
- ) -> bool {
- let interner = db.interner();
-
- let mut gb = GoalBuilder::new(db);
-
- let impl_fields = impl_datum
- .binders
- .map_ref(|v| (&v.trait_ref, &v.where_clauses));
-
- // Implementations for scalars, pointer types and never type are provided by libcore.
- // User implementations on types other than ADTs are forbidden.
- match impl_datum
- .binders
- .skip_binders()
- .trait_ref
- .self_type_parameter(interner)
- .kind(interner)
- {
- TyKind::Scalar(_)
- | TyKind::Raw(_, _)
- | TyKind::Ref(Mutability::Not, _, _)
- | TyKind::Never => return true,
-
- TyKind::Adt(_, _) => (),
-
- _ => return false,
- };
-
- // Well fomedness goal for ADTs
- let well_formed_goal =
- gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
- let interner = gb.interner();
-
- let ty = trait_ref.self_type_parameter(interner);
-
- let (adt_id, substitution) = match ty.kind(interner) {
- TyKind::Adt(adt_id, substitution) => (*adt_id, substitution),
-
- _ => unreachable!(),
- };
-
- // if (WC) { ... }
- gb.implies(
- impl_wf_environment(interner, where_clauses, trait_ref),
- |gb| -> Goal<I> {
- let db = gb.db();
-
- // not { Implemented(ImplSelfTy: Drop) }
- let neg_drop_goal =
- db.well_known_trait_id(WellKnownTrait::Drop)
- .map(|drop_trait_id| {
- TraitRef {
- trait_id: drop_trait_id,
- substitution: Substitution::from1(interner, ty.clone()),
- }
- .cast::<Goal<I>>(interner)
- .negate(interner)
- });
-
- let adt_datum = db.adt_datum(adt_id);
-
- let goals = adt_datum
- .binders
- .map_ref(|b| &b.variants)
- .cloned()
- .substitute(interner, substitution)
- .into_iter()
- .flat_map(|v| {
- v.fields.into_iter().map(|f| {
- // Implemented(FieldTy: Copy)
- TraitRef {
- trait_id: trait_ref.trait_id,
- substitution: Substitution::from1(interner, f),
- }
- .cast(interner)
- })
- })
- .chain(neg_drop_goal.into_iter());
- gb.all(goals)
- },
- )
- });
-
- solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner))
- }
-
- /// Verifies constraints on a Drop implementation
- /// Drop implementation is considered well-formed if:
- /// a) it's implemented on an ADT
- /// b) The generic parameters of the impl's type must all be parameters
- /// of the Drop impl itself (i.e., no specialization like
- /// `impl Drop for S<Foo> {...}` is allowed).
- /// c) Any bounds on the genereic parameters of the impl must be
- /// deductible from the bounds imposed by the struct definition
- /// (i.e. the implementation must be exactly as generic as the ADT definition).
- ///
- /// ```rust,ignore
- /// struct S<T1, T2> { }
- /// struct Foo<T> { }
- ///
- /// impl<U1: Copy, U2: Sized> Drop for S<U2, Foo<U1>> { }
- /// ```
- ///
- /// generates the following:
- /// goal derived from c):
- ///
- /// ```notrust
- /// forall<U1, U2> {
- /// Implemented(U1: Copy), Implemented(U2: Sized) :- FromEnv(S<U2, Foo<U1>>)
- /// }
- /// ```
- ///
- /// goal derived from b):
- /// ```notrust
- /// forall <T1, T2> {
- /// exists<U1, U2> {
- /// S<T1, T2> = S<U2, Foo<U1>>
- /// }
- /// }
- /// ```
- fn drop_impl_constraint<I: Interner>(
- solver: &mut dyn Solver<I>,
- db: &dyn RustIrDatabase<I>,
- impl_datum: &ImplDatum<I>,
- ) -> bool {
- let interner = db.interner();
-
- let adt_id = match impl_datum.self_type_adt_id(interner) {
- Some(id) => id,
- // Drop can only be implemented on a nominal type
- None => return false,
- };
-
- let mut gb = GoalBuilder::new(db);
-
- let adt_datum = db.adt_datum(adt_id);
-
- let impl_fields = impl_datum
- .binders
- .map_ref(|v| (&v.trait_ref, &v.where_clauses));
-
- // forall<ImplP1...ImplPn> { .. }
- let implied_by_adt_def_goal =
- gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
- let interner = gb.interner();
-
- // FromEnv(ImplSelfType) => ...
- gb.implies(
- iter::once(
- FromEnv::Ty(trait_ref.self_type_parameter(interner))
- .cast::<DomainGoal<I>>(interner),
- ),
- |gb| {
- // All(ImplWhereClauses)
- gb.all(
- where_clauses
- .iter()
- .map(|wc| wc.clone().into_well_formed_goal(interner)),
- )
- },
- )
- });
-
- let impl_self_ty = impl_datum
- .binders
- .map_ref(|b| b.trait_ref.self_type_parameter(interner));
-
- // forall<StructP1..StructPN> {...}
- let eq_goal = gb.forall(
- &adt_datum.binders,
- (adt_id, impl_self_ty),
- |gb, substitution, _, (adt_id, impl_self_ty)| {
- let interner = gb.interner();
-
- let def_adt = TyKind::Adt(adt_id, substitution).intern(interner);
-
- // exists<ImplP1...ImplPn> { .. }
- gb.exists(&impl_self_ty, def_adt, |gb, _, impl_adt, def_adt| {
- let interner = gb.interner();
-
- // StructName<StructP1..StructPn> = ImplSelfType
- GoalData::EqGoal(EqGoal {
- a: GenericArgData::Ty(def_adt).intern(interner),
- b: GenericArgData::Ty(impl_adt.clone()).intern(interner),
- })
- .intern(interner)
- })
- },
- );
-
- let well_formed_goal = gb.all([implied_by_adt_def_goal, eq_goal].iter());
-
- solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner))
- }
-
- /// Verify constraints a CoerceUnsized impl.
- /// Rules for CoerceUnsized impl to be considered well-formed:
- /// 1) pointer conversions: `&[mut] T -> &[mut] U`, `&[mut] T -> *[mut] U`,
- /// `*[mut] T -> *[mut] U` are considered valid if
- /// 1) `T: Unsize<U>`
- /// 2) mutability is respected, i.e. immutable -> immutable, mutable -> immutable,
- /// mutable -> mutable conversions are allowed, immutable -> mutable is not.
- /// 2) struct conversions of structures with the same definition, `S<P0...Pn>` -> `S<Q0...Qn>`.
- /// To check if this impl is legal, we would walk down the fields of `S`
- /// and consider their types with both substitutes. We are looking to find
- /// exactly one (non-phantom) field that has changed its type (from `T` to `U`), and
- /// expect `T` to be unsizeable to `U`, i.e. `T: CoerceUnsized<U>`.
- ///
- /// As an example, consider a struct
- /// ```rust
- /// struct Foo<T, U> {
- /// extra: T,
- /// ptr: *mut U,
- /// }
- /// ```
- ///
- /// We might have an impl that allows (e.g.) `Foo<T, [i32; 3]>` to be unsized
- /// to `Foo<T, [i32]>`. That impl would look like:
- /// ```rust,ignore
- /// impl<T, U: Unsize<V>, V> CoerceUnsized<Foo<T, V>> for Foo<T, U> {}
- /// ```
- /// In this case:
- ///
- /// - `extra` has type `T` before and type `T` after
- /// - `ptr` has type `*mut U` before and type `*mut V` after
- ///
- /// Since just one field changed, we would then check that `*mut U: CoerceUnsized<*mut V>`
- /// is implemented. This will work out because `U: Unsize<V>`, and we have a libcore rule
- /// that `*mut U` can be coerced to `*mut V` if `U: Unsize<V>`.
- fn coerce_unsized_impl_constraint<I: Interner>(
- solver: &mut dyn Solver<I>,
- db: &dyn RustIrDatabase<I>,
- impl_datum: &ImplDatum<I>,
- ) -> bool {
- let interner = db.interner();
- let mut gb = GoalBuilder::new(db);
-
- let (binders, impl_datum) = impl_datum.binders.as_ref().into();
-
- let trait_ref: &TraitRef<I> = &impl_datum.trait_ref;
-
- let source = trait_ref.self_type_parameter(interner);
- let target = trait_ref
- .substitution
- .at(interner, 1)
- .assert_ty_ref(interner)
- .clone();
-
- let mut place_in_environment = |goal| -> Goal<I> {
- gb.forall(
- &Binders::new(
- binders.clone(),
- (goal, trait_ref, &impl_datum.where_clauses),
- ),
- (),
- |gb, _, (goal, trait_ref, where_clauses), ()| {
- let interner = gb.interner();
- gb.implies(
- impl_wf_environment(interner, where_clauses, trait_ref),
- |_| goal,
- )
- },
- )
- };
-
- match (source.kind(interner), target.kind(interner)) {
- (TyKind::Ref(s_m, _, source), TyKind::Ref(t_m, _, target))
- | (TyKind::Ref(s_m, _, source), TyKind::Raw(t_m, target))
- | (TyKind::Raw(s_m, source), TyKind::Raw(t_m, target)) => {
- if (*s_m, *t_m) == (Mutability::Not, Mutability::Mut) {
- return false;
- }
-
- let unsize_trait_id =
- if let Some(id) = db.well_known_trait_id(WellKnownTrait::Unsize) {
- id
- } else {
- return false;
- };
-
- // Source: Unsize<Target>
- let unsize_goal: Goal<I> = TraitRef {
- trait_id: unsize_trait_id,
- substitution: Substitution::from_iter(
- interner,
- [source.clone(), target.clone()].iter().cloned(),
- ),
- }
- .cast(interner);
-
- // ImplEnv -> Source: Unsize<Target>
- let unsize_goal = place_in_environment(unsize_goal);
-
- solver.has_unique_solution(db, &unsize_goal.into_closed_goal(interner))
- }
- (TyKind::Adt(source_id, subst_a), TyKind::Adt(target_id, subst_b)) => {
- let adt_datum = db.adt_datum(*source_id);
-
- if source_id != target_id || adt_datum.kind != AdtKind::Struct {
- return false;
- }
-
- let fields = adt_datum
- .binders
- .map_ref(|bound| &bound.variants.last().unwrap().fields)
- .cloned();
-
- let (source_fields, target_fields) = (
- fields.clone().substitute(interner, subst_a),
- fields.substitute(interner, subst_b),
- );
-
- // collect fields with unequal ids
- let uneq_field_ids: Vec<usize> = (0..source_fields.len())
- .filter(|&i| {
- // ignore phantom data fields
- if let Some(adt_id) = source_fields[i].adt_id(interner) {
- if db.adt_datum(adt_id).flags.phantom_data {
- return false;
- }
- }
-
- let eq_goal: Goal<I> = EqGoal {
- a: source_fields[i].clone().cast(interner),
- b: target_fields[i].clone().cast(interner),
- }
- .cast(interner);
-
- // ImplEnv -> Source.fields[i] = Target.fields[i]
- let eq_goal = place_in_environment(eq_goal);
-
- // We are interested in !UNEQUAL! fields
- !solver.has_unique_solution(db, &eq_goal.into_closed_goal(interner))
- })
- .collect();
-
- if uneq_field_ids.len() != 1 {
- return false;
- }
-
- let field_id = uneq_field_ids[0];
-
- // Source.fields[i]: CoerceUnsized<TargetFields[i]>
- let coerce_unsized_goal: Goal<I> = TraitRef {
- trait_id: trait_ref.trait_id,
- substitution: Substitution::from_iter(
- interner,
- [
- source_fields[field_id].clone(),
- target_fields[field_id].clone(),
- ]
- .iter()
- .cloned(),
- ),
- }
- .cast(interner);
-
- // ImplEnv -> Source.fields[i]: CoerceUnsized<TargetFields[i]>
- let coerce_unsized_goal = place_in_environment(coerce_unsized_goal);
-
- solver.has_unique_solution(db, &coerce_unsized_goal.into_closed_goal(interner))
- }
- _ => false,
- }
- }
-
- /// Verify constraints of a DispatchFromDyn impl.
- ///
- /// Rules for DispatchFromDyn impl to be considered well-formed:
- ///
- /// * Self and the type parameter must both be references or raw pointers with the same mutabilty
- /// * OR all the following hold:
- /// - Self and the type parameter must be structs
- /// - Self and the type parameter must have the same definitions
- /// - Self must not be `#[repr(packed)]` or `#[repr(C)]`
- /// - Self must have exactly one field which is not a 1-ZST (there may be any number of 1-ZST
- /// fields), and that field must have a different type in the type parameter (i.e., it is
- /// the field being coerced)
- /// - `DispatchFromDyn` is implemented for the type of the field being coerced.
- fn dispatch_from_dyn_constraint<I: Interner>(
- solver: &mut dyn Solver<I>,
- db: &dyn RustIrDatabase<I>,
- impl_datum: &ImplDatum<I>,
- ) -> bool {
- let interner = db.interner();
- let mut gb = GoalBuilder::new(db);
-
- let (binders, impl_datum) = impl_datum.binders.as_ref().into();
-
- let trait_ref: &TraitRef<I> = &impl_datum.trait_ref;
-
- // DispatchFromDyn specifies that Self (source) can be coerced to T (target; its single type parameter).
- let source = trait_ref.self_type_parameter(interner);
- let target = trait_ref
- .substitution
- .at(interner, 1)
- .assert_ty_ref(interner)
- .clone();
-
- let mut place_in_environment = |goal| -> Goal<I> {
- gb.forall(
- &Binders::new(
- binders.clone(),
- (goal, trait_ref, &impl_datum.where_clauses),
- ),
- (),
- |gb, _, (goal, trait_ref, where_clauses), ()| {
- let interner = gb.interner();
- gb.implies(
- impl_wf_environment(interner, &where_clauses, &trait_ref),
- |_| goal,
- )
- },
- )
- };
-
- match (source.kind(interner), target.kind(interner)) {
- (TyKind::Ref(s_m, _, _), TyKind::Ref(t_m, _, _))
- | (TyKind::Raw(s_m, _), TyKind::Raw(t_m, _))
- if s_m == t_m =>
- {
- true
- }
- (TyKind::Adt(source_id, subst_a), TyKind::Adt(target_id, subst_b)) => {
- let adt_datum = db.adt_datum(*source_id);
-
- // Definitions are equal and are structs.
- if source_id != target_id || adt_datum.kind != AdtKind::Struct {
- return false;
- }
-
- // Not repr(C) or repr(packed).
- let repr = db.adt_repr(*source_id);
- if repr.c || repr.packed {
- return false;
- }
-
- // Collect non 1-ZST fields; there must be exactly one.
- let fields = adt_datum
- .binders
- .map_ref(|bound| &bound.variants.last().unwrap().fields)
- .cloned();
-
- let (source_fields, target_fields) = (
- fields.clone().substitute(interner, subst_a),
- fields.substitute(interner, subst_b),
- );
-
- let mut non_zst_fields: Vec<_> = source_fields
- .iter()
- .zip(target_fields.iter())
- .filter(|(sf, _)| match sf.adt_id(interner) {
- Some(adt) => !db.adt_size_align(adt).one_zst(),
- None => true,
- })
- .collect();
-
- if non_zst_fields.len() != 1 {
- return false;
- }
-
- // The field being coerced (the interesting field).
- let (field_src, field_tgt) = non_zst_fields.pop().unwrap();
-
- // The interesting field is different in the source and target types.
- let eq_goal: Goal<I> = EqGoal {
- a: field_src.clone().cast(interner),
- b: field_tgt.clone().cast(interner),
- }
- .cast(interner);
- let eq_goal = place_in_environment(eq_goal);
- if solver.has_unique_solution(db, &eq_goal.into_closed_goal(interner)) {
- return false;
- }
-
- // Type(field_src): DispatchFromDyn<Type(field_tgt)>
- let field_dispatch_goal: Goal<I> = TraitRef {
- trait_id: trait_ref.trait_id,
- substitution: Substitution::from_iter(
- interner,
- [field_src.clone(), field_tgt.clone()].iter().cloned(),
- ),
- }
- .cast(interner);
- let field_dispatch_goal = place_in_environment(field_dispatch_goal);
- if !solver.has_unique_solution(db, &field_dispatch_goal.into_closed_goal(interner))
- {
- return false;
- }
-
- true
- }
- _ => false,
- }
- }
-}
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-11 22:49:06 +0000