Skip to content

Implement stable overlap check considering negative traits #93175

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 12 commits into from
Jan 25, 2022
Merged
Show file tree
Hide file tree
Changes from 8 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions compiler/rustc_feature/src/builtin_attrs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -697,6 +697,7 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
rustc_attr!(TEST, rustc_capture_analysis, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_insignificant_dtor, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_strict_coherence, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_with_negative_coherence, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_variance, Normal, template!(Word), WarnFollowing),
rustc_attr!(TEST, rustc_layout, Normal, template!(List: "field1, field2, ..."), WarnFollowing),
rustc_attr!(TEST, rustc_regions, Normal, template!(Word), WarnFollowing),
Expand Down
1 change: 1 addition & 0 deletions compiler/rustc_span/src/symbol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1203,6 +1203,7 @@ symbols! {
rustc_trivial_field_reads,
rustc_unsafe_specialization_marker,
rustc_variance,
rustc_with_negative_coherence,
rustdoc,
rustdoc_internals,
rustfmt,
Expand Down
246 changes: 189 additions & 57 deletions compiler/rustc_trait_selection/src/traits/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@
use crate::infer::{CombinedSnapshot, InferOk, TyCtxtInferExt};
use crate::traits::query::evaluate_obligation::InferCtxtExt;
use crate::traits::select::IntercrateAmbiguityCause;
use crate::traits::util::impl_trait_ref_and_oblig;
use crate::traits::SkipLeakCheck;
use crate::traits::{
self, Normalized, Obligation, ObligationCause, PredicateObligation, SelectionContext,
self, FulfillmentContext, Normalized, Obligation, ObligationCause, PredicateObligation,
SelectionContext,
};
use rustc_hir::def_id::{DefId, LOCAL_CRATE};
use rustc_middle::ty::fast_reject::{self, SimplifyParams, StripReferences};
Expand Down Expand Up @@ -135,68 +137,131 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
header
}

enum OverlapMode {
Stable,
WithNegative,
Strict,
}

fn overlap_mode<'tcx>(tcx: TyCtxt<'tcx>, impl1_def_id: DefId, impl2_def_id: DefId) -> OverlapMode {
if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
!= tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence)
{
bug!("Use strict coherence on both impls",);
}

if tcx.has_attr(impl1_def_id, sym::rustc_with_negative_coherence)
!= tcx.has_attr(impl2_def_id, sym::rustc_with_negative_coherence)
{
bug!("Use with negative coherence on both impls",);
}

if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence) {
OverlapMode::Strict
} else if tcx.has_attr(impl1_def_id, sym::rustc_with_negative_coherence) {
OverlapMode::WithNegative
} else {
OverlapMode::Stable
}
}

/// Can both impl `a` and impl `b` be satisfied by a common type (including
/// where-clauses)? If so, returns an `ImplHeader` that unifies the two impls.
fn overlap<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
skip_leak_check: SkipLeakCheck,
a_def_id: DefId,
b_def_id: DefId,
impl1_def_id: DefId,
impl2_def_id: DefId,
) -> Option<OverlapResult<'tcx>> {
debug!("overlap(a_def_id={:?}, b_def_id={:?})", a_def_id, b_def_id);
debug!("overlap(impl1_def_id={:?}, impl2_def_id={:?})", impl1_def_id, impl2_def_id);

selcx.infcx().probe_maybe_skip_leak_check(skip_leak_check.is_yes(), |snapshot| {
overlap_within_probe(selcx, skip_leak_check, a_def_id, b_def_id, snapshot)
overlap_within_probe(selcx, skip_leak_check, impl1_def_id, impl2_def_id, snapshot)
})
}

fn overlap_within_probe<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
skip_leak_check: SkipLeakCheck,
a_def_id: DefId,
b_def_id: DefId,
impl1_def_id: DefId,
impl2_def_id: DefId,
snapshot: &CombinedSnapshot<'_, 'tcx>,
) -> Option<OverlapResult<'tcx>> {
fn loose_check<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
!selcx.predicate_may_hold_fatal(o)
}

fn strict_check<'cx, 'tcx>(
selcx: &SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
let infcx = selcx.infcx();
let tcx = infcx.tcx;
o.flip_polarity(tcx)
.as_ref()
.map(|o| selcx.infcx().predicate_must_hold_modulo_regions(o))
.unwrap_or(false)
}
let infcx = selcx.infcx();
let tcx = infcx.tcx;

// For the purposes of this check, we don't bring any placeholder
// types into scope; instead, we replace the generic types with
// fresh type variables, and hence we do our evaluations in an
// empty environment.
let param_env = ty::ParamEnv::empty();

let a_impl_header = with_fresh_ty_vars(selcx, param_env, a_def_id);
let b_impl_header = with_fresh_ty_vars(selcx, param_env, b_def_id);
let impl1_header = with_fresh_ty_vars(selcx, param_env, impl1_def_id);
let impl2_header = with_fresh_ty_vars(selcx, param_env, impl2_def_id);

match overlap_mode(tcx, impl1_def_id, impl2_def_id) {
OverlapMode::Stable => {
if stable_disjoint(selcx, param_env, &impl1_header, impl2_header) {
return None;
}
}
OverlapMode::Strict => {
if strict_disjoint(selcx, impl1_def_id, impl2_def_id) {
return None;
}

// Equate for error reporting
let _ = selcx
.infcx()
.at(&ObligationCause::dummy(), param_env)
.eq_impl_headers(&impl1_header, &impl2_header);
}
OverlapMode::WithNegative => {
if stable_disjoint(selcx, param_env, &impl1_header, impl2_header)
|| strict_disjoint(selcx, impl1_def_id, impl2_def_id)
{
return None;
}
}
}

if !skip_leak_check.is_yes() {
if infcx.leak_check(true, snapshot).is_err() {
debug!("overlap: leak check failed");
return None;
}
}

let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);

let involves_placeholder =
matches!(selcx.infcx().region_constraints_added_in_snapshot(snapshot), Some(true));

debug!("overlap: a_impl_header={:?}", a_impl_header);
debug!("overlap: b_impl_header={:?}", b_impl_header);
let impl_header = selcx.infcx().resolve_vars_if_possible(impl1_header);
Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
}

/// Given impl1 and impl2 check if both impls can be satisfied by a common type (including
/// where-clauses) If so, return false, otherwise return true, they are disjoint.
fn stable_disjoint<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
param_env: ty::ParamEnv<'tcx>,
impl1_header: &ty::ImplHeader<'tcx>,
impl2_header: ty::ImplHeader<'tcx>,
) -> bool {
debug!("overlap: impl1_header={:?}", impl1_header);
debug!("overlap: impl2_header={:?}", impl2_header);

// Do `a` and `b` unify? If not, no overlap.
let obligations = match selcx
.infcx()
.at(&ObligationCause::dummy(), param_env)
.eq_impl_headers(&a_impl_header, &b_impl_header)
.eq_impl_headers(&impl1_header, &impl2_header)
{
Ok(InferOk { obligations, value: () }) => obligations,
Err(_) => {
return None;
return true;
}
};

Expand Down Expand Up @@ -225,11 +290,11 @@ fn overlap_within_probe<'cx, 'tcx>(
// at some point an impl for `&'?a str: Error` could be added.
let infcx = selcx.infcx();
let tcx = infcx.tcx;
let opt_failing_obligation = a_impl_header
let opt_failing_obligation = impl1_header
.predicates
.iter()
.copied()
.chain(b_impl_header.predicates)
.chain(impl2_header.predicates)
.map(|p| infcx.resolve_vars_if_possible(p))
.map(|p| Obligation {
cause: ObligationCause::dummy(),
Expand All @@ -238,41 +303,108 @@ fn overlap_within_probe<'cx, 'tcx>(
predicate: p,
})
.chain(obligations)
.find(|o| {
// if both impl headers are set to strict coherence it means that this will be accepted
// only if it's stated that T: !Trait. So only prove that the negated obligation holds.
if tcx.has_attr(a_def_id, sym::rustc_strict_coherence)
&& tcx.has_attr(b_def_id, sym::rustc_strict_coherence)
{
strict_check(selcx, o)
} else {
loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
}
});
.find(|o| loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o));
// FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported
// to the canonical trait query form, `infcx.predicate_may_hold`, once
// the new system supports intercrate mode (which coherence needs).

if let Some(failing_obligation) = opt_failing_obligation {
debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
return None;
true
} else {
false
}
}

if !skip_leak_check.is_yes() {
if infcx.leak_check(true, snapshot).is_err() {
debug!("overlap: leak check failed");
return None;
}
}
/// Given impl1 and impl2 check if both impls are never satisfied by a common type (including
/// where-clauses) If so, return true, they are disjoint and false otherwise.
fn strict_disjoint<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
impl1_def_id: DefId,
impl2_def_id: DefId,
) -> bool {
explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
|| explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
}

let impl_header = selcx.infcx().resolve_vars_if_possible(a_impl_header);
let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
fn explicit_disjoint<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
impl1_def_id: DefId,
impl2_def_id: DefId,
) -> bool {
let tcx = selcx.infcx().tcx;

let involves_placeholder =
matches!(selcx.infcx().region_constraints_added_in_snapshot(snapshot), Some(true));
// create a parameter environment corresponding to a (placeholder) instantiation of impl1
let impl1_env = tcx.param_env(impl1_def_id);
let impl1_trait_ref = tcx.impl_trait_ref(impl1_def_id).unwrap();

Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
// Create an infcx, taking the predicates of impl1 as assumptions:
tcx.infer_ctxt().enter(|infcx| {
// Normalize the trait reference. The WF rules ought to ensure
// that this always succeeds.
let impl1_trait_ref = match traits::fully_normalize(
&infcx,
FulfillmentContext::new(),
ObligationCause::dummy(),
impl1_env,
impl1_trait_ref,
) {
Ok(impl1_trait_ref) => impl1_trait_ref,
Err(err) => {
bug!("failed to fully normalize {:?}: {:?}", impl1_trait_ref, err);
}
};

// Attempt to prove that impl2 applies, given all of the above.
let selcx = &mut SelectionContext::new(&infcx);
let impl2_substs = infcx.fresh_substs_for_item(DUMMY_SP, impl2_def_id);
let (impl2_trait_ref, obligations) =
impl_trait_ref_and_oblig(selcx, impl1_env, impl2_def_id, impl2_substs);

// do the impls unify? If not, not disjoint.
let more_obligations = match infcx
.at(&ObligationCause::dummy(), impl1_env)
.eq(impl1_trait_ref, impl2_trait_ref)
{
Ok(InferOk { obligations, .. }) => obligations,
Err(_) => {
debug!(
"explicit_disjoint: {:?} does not unify with {:?}",
impl1_trait_ref, impl2_trait_ref
);
return false;
}
};

let opt_failing_obligation =
obligations.into_iter().chain(more_obligations).find(|o| strict_check(selcx, o));

if let Some(failing_obligation) = opt_failing_obligation {
debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
true
} else {
false
}
})
}

fn loose_check<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
!selcx.predicate_may_hold_fatal(o)
}

fn strict_check<'cx, 'tcx>(
selcx: &SelectionContext<'cx, 'tcx>,
o: &PredicateObligation<'tcx>,
) -> bool {
let infcx = selcx.infcx();
let tcx = infcx.tcx;
o.flip_polarity(tcx)
.as_ref()
.map(|o| selcx.infcx().predicate_must_hold_modulo_regions(o))
.unwrap_or(false)
}

pub fn trait_ref_is_knowable<'tcx>(
Expand Down
8 changes: 8 additions & 0 deletions src/test/ui/coherence/auxiliary/option_future.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#![crate_type = "lib"]
#![feature(negative_impls)]
#![feature(rustc_attrs)]

pub trait Future {}

#[rustc_with_negative_coherence]
impl<E> !Future for Option<E> where E: Sized {}
18 changes: 18 additions & 0 deletions src/test/ui/coherence/coherence-overlap-negative-trait2.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// check-pass
// aux-build:option_future.rs
//
// Check that if we promise to not impl what would overlap it doesn't actually overlap

#![feature(rustc_attrs)]

extern crate option_future as lib;
use lib::Future;

trait Termination {}

#[rustc_with_negative_coherence]
impl<E> Termination for Option<E> where E: Sized {}
#[rustc_with_negative_coherence]
impl<F> Termination for F where F: Future + Sized {}

fn main() {}