Skip to content

Commit

Permalink
track the source of nested goals
Browse files Browse the repository at this point in the history
  • Loading branch information
lcnr committed Dec 18, 2023
1 parent 321b656 commit ca718ff
Show file tree
Hide file tree
Showing 14 changed files with 173 additions and 81 deletions.
18 changes: 18 additions & 0 deletions compiler/rustc_middle/src/traits/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,24 @@ impl<'tcx> TypeVisitable<TyCtxt<'tcx>> for PredefinedOpaques<'tcx> {
}
}

/// Why a specific goal has to be proven.
///
/// This is necessary as we treat nested goals different depending on
/// their source.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
pub enum GoalSource {
Misc,
/// We're proving a where-bound of an impl.
///
/// FIXME(-Znext-solver=coinductive): Explain how and why this
/// changes whether cycles are coinductive.
///
/// This also impacts whether we erase constraints on overflow.
/// Erasing constraints is generally very useful for perf and also
/// results in better error messages by avoiding spurious errors.
ImplWhereBound,
}

#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, HashStable)]
pub enum IsNormalizesToHack {
Yes,
Expand Down
6 changes: 3 additions & 3 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@
//! [canonicalized]: https://rustc-dev-guide.rust-lang.org/solve/canonicalization.html

use super::{
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, IsNormalizesToHack, NoSolution,
QueryInput, QueryResult,
CandidateSource, Canonical, CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack,
NoSolution, QueryInput, QueryResult,
};
use crate::{infer::canonical::CanonicalVarValues, ty};
use format::ProofTreeFormatter;
Expand Down Expand Up @@ -115,7 +115,7 @@ impl Debug for Probe<'_> {
pub enum ProbeStep<'tcx> {
/// We added a goal to the `EvalCtxt` which will get proven
/// the next time `EvalCtxt::try_evaluate_added_goals` is called.
AddGoal(CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
AddGoal(GoalSource, CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
/// The inside of a `EvalCtxt::try_evaluate_added_goals` call.
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
/// A call to `probe` while proving the current goal. This is
Expand Down
8 changes: 7 additions & 1 deletion compiler/rustc_middle/src/traits/solve/inspect/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,13 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
self.nested(|this| {
for step in &probe.steps {
match step {
ProbeStep::AddGoal(goal) => writeln!(this.f, "ADDED GOAL: {goal:?}")?,
ProbeStep::AddGoal(source, goal) => {
let source = match source {
GoalSource::Misc => "misc",
GoalSource::ImplWhereBound => "impl where-bound",
};
writeln!(this.f, "ADDED GOAL ({source}): {goal:?}")?
}
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
ProbeStep::CommitIfOkStart => writeln!(this.f, "COMMIT_IF_OK START")?,
Expand Down
16 changes: 9 additions & 7 deletions compiler/rustc_trait_selection/src/solve/alias_relate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
//! * bidirectional-normalizes-to: If `A` and `B` are both projections, and both
//! may apply, then we can compute the "intersection" of both normalizes-to by
//! performing them together. This is used specifically to resolve ambiguities.
use super::EvalCtxt;
use super::{EvalCtxt, GoalSource};
use rustc_infer::infer::DefineOpaqueTypes;
use rustc_infer::traits::query::NoSolution;
use rustc_middle::traits::solve::{Certainty, Goal, QueryResult};
Expand Down Expand Up @@ -89,11 +89,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
ty::TermKind::Const(_) => {
if let Some(alias) = term.to_alias_ty(self.tcx()) {
let term = self.next_term_infer_of_kind(term);
self.add_goal(Goal::new(
self.tcx(),
param_env,
ty::NormalizesTo { alias, term },
));
self.add_goal(
GoalSource::Misc,
Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias, term }),
);
self.try_evaluate_added_goals()?;
Ok(Some(self.resolve_vars_if_possible(term)))
} else {
Expand All @@ -109,7 +108,10 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
opaque: ty::AliasTy<'tcx>,
term: ty::Term<'tcx>,
) -> QueryResult<'tcx> {
self.add_goal(Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias: opaque, term }));
self.add_goal(
GoalSource::Misc,
Goal::new(self.tcx(), param_env, ty::NormalizesTo { alias: opaque, term }),
);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}

Expand Down
23 changes: 15 additions & 8 deletions compiler/rustc_trait_selection/src/solve/assembly/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
//! Code shared by trait and projection goals for candidate assembly.

use super::{EvalCtxt, SolverMode};
use crate::solve::GoalSource;
use crate::traits::coherence;
use rustc_hir::def_id::DefId;
use rustc_infer::traits::query::NoSolution;
Expand Down Expand Up @@ -62,7 +63,9 @@ pub(super) trait GoalKind<'tcx>:
requirements: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> QueryResult<'tcx> {
Self::probe_and_match_goal_against_assumption(ecx, goal, assumption, |ecx| {
ecx.add_goals(requirements);
// FIXME(-Znext-solver=coinductive): check whether this should be
// `GoalSource::ImplWhereBound` for any caller.
ecx.add_goals(GoalSource::Misc, requirements);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
Expand Down Expand Up @@ -94,12 +97,16 @@ pub(super) trait GoalKind<'tcx>:
let ty::Dynamic(bounds, _, _) = *goal.predicate.self_ty().kind() else {
bug!("expected object type in `consider_object_bound_candidate`");
};
ecx.add_goals(structural_traits::predicates_for_object_candidate(
ecx,
goal.param_env,
goal.predicate.trait_ref(tcx),
bounds,
));
// FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
ecx.add_goals(
GoalSource::Misc,
structural_traits::predicates_for_object_candidate(
ecx,
goal.param_env,
goal.predicate.trait_ref(tcx),
bounds,
),
);
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
Expand Down Expand Up @@ -364,7 +371,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
let normalized_ty = ecx.next_ty_infer();
let normalizes_to_goal =
goal.with(tcx, ty::NormalizesTo { alias, term: normalized_ty.into() });
ecx.add_goal(normalizes_to_goal);
ecx.add_goal(GoalSource::Misc, normalizes_to_goal);
if let Err(NoSolution) = ecx.try_evaluate_added_goals() {
debug!("self type normalization failed");
return vec![];
Expand Down
34 changes: 21 additions & 13 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,15 @@ use rustc_middle::ty::{
use rustc_session::config::DumpSolverProofTree;
use rustc_span::DUMMY_SP;
use std::io::Write;
use std::iter;
use std::ops::ControlFlow;

use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};

use super::inspect::ProofTreeBuilder;
use super::SolverMode;
use super::{search_graph, GoalEvaluationKind};
use super::{search_graph::SearchGraph, Goal};
use super::{GoalSource, SolverMode};
pub use select::InferCtxtSelectExt;

mod canonical;
Expand Down Expand Up @@ -105,7 +106,7 @@ pub(super) struct NestedGoals<'tcx> {
/// can be unsound with more powerful coinduction in the future.
pub(super) normalizes_to_hack_goal: Option<Goal<'tcx, ty::NormalizesTo<'tcx>>>,
/// The rest of the goals which have not yet processed or remain ambiguous.
pub(super) goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
pub(super) goals: Vec<(GoalSource, Goal<'tcx, ty::Predicate<'tcx>>)>,
}

impl<'tcx> NestedGoals<'tcx> {
Expand Down Expand Up @@ -439,7 +440,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
} else {
let kind = self.infcx.instantiate_binder_with_placeholders(kind);
let goal = goal.with(self.tcx(), ty::Binder::dummy(kind));
self.add_goal(goal);
self.add_goal(GoalSource::Misc, goal);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}
}
Expand Down Expand Up @@ -488,6 +489,13 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let mut goals = core::mem::replace(&mut self.nested_goals, NestedGoals::new());

self.inspect.evaluate_added_goals_loop_start();

fn with_misc_source<'tcx>(
it: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) -> impl Iterator<Item = (GoalSource, Goal<'tcx, ty::Predicate<'tcx>>)> {
iter::zip(iter::repeat(GoalSource::Misc), it)
}

// If this loop did not result in any progress, what's our final certainty.
let mut unchanged_certainty = Some(Certainty::Yes);
if let Some(goal) = goals.normalizes_to_hack_goal.take() {
Expand All @@ -503,7 +511,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
unconstrained_goal,
)?;
self.nested_goals.goals.extend(instantiate_goals);
self.nested_goals.goals.extend(with_misc_source(instantiate_goals));

// Finally, equate the goal's RHS with the unconstrained var.
// We put the nested goals from this into goals instead of
Expand All @@ -512,7 +520,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// matters in practice, though.
let eq_goals =
self.eq_and_get_goals(goal.param_env, goal.predicate.term, unconstrained_rhs)?;
goals.goals.extend(eq_goals);
goals.goals.extend(with_misc_source(eq_goals));

// We only look at the `projection_ty` part here rather than
// looking at the "has changed" return from evaluate_goal,
Expand All @@ -533,20 +541,20 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}
}

for goal in goals.goals.drain(..) {
for (source, goal) in goals.goals.drain(..) {
let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
goal,
)?;
self.nested_goals.goals.extend(instantiate_goals);
self.nested_goals.goals.extend(with_misc_source(instantiate_goals));
if has_changed {
unchanged_certainty = None;
}

match certainty {
Certainty::Yes => {}
Certainty::Maybe(_) => {
self.nested_goals.goals.push(goal);
self.nested_goals.goals.push((source, goal));
unchanged_certainty = unchanged_certainty.map(|c| c.unify_with(certainty));
}
}
Expand Down Expand Up @@ -670,7 +678,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env)
.eq(DefineOpaqueTypes::No, lhs, rhs)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to equate");
Expand All @@ -689,7 +697,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env)
.sub(DefineOpaqueTypes::No, sub, sup)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to subtype");
Expand All @@ -709,7 +717,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
.at(&ObligationCause::dummy(), param_env)
.relate(DefineOpaqueTypes::No, lhs, variance, rhs)
.map(|InferOk { value: (), obligations }| {
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
})
.map_err(|e| {
debug!(?e, "failed to relate");
Expand Down Expand Up @@ -842,7 +850,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
true,
&mut obligations,
)?;
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
Ok(())
}

Expand All @@ -862,7 +870,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
hidden_ty,
&mut obligations,
);
self.add_goals(obligations.into_iter().map(|o| o.into()));
self.add_goals(GoalSource::Misc, obligations.into_iter().map(|o| o.into()));
}

// Do something for each opaque/hidden pair defined with `def_id` in the
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
) {
for step in &probe.steps {
match step {
&inspect::ProbeStep::AddGoal(goal) => nested_goals.push(goal),
&inspect::ProbeStep::AddGoal(_source, goal) => nested_goals.push(goal),
inspect::ProbeStep::NestedProbe(ref probe) => {
// Nested probes have to prove goals added in their parent
// but do not leak them, so we truncate the added goals
Expand Down
16 changes: 11 additions & 5 deletions compiler/rustc_trait_selection/src/solve/inspect/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use std::mem;

use rustc_middle::traits::query::NoSolution;
use rustc_middle::traits::solve::{
CanonicalInput, Certainty, Goal, IsNormalizesToHack, QueryInput, QueryResult,
CanonicalInput, Certainty, Goal, GoalSource, IsNormalizesToHack, QueryInput, QueryResult,
};
use rustc_middle::ty::{self, TyCtxt};
use rustc_session::config::DumpSolverProofTree;
Expand Down Expand Up @@ -216,7 +216,7 @@ impl<'tcx> WipProbe<'tcx> {

#[derive(Eq, PartialEq, Debug)]
enum WipProbeStep<'tcx> {
AddGoal(inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
AddGoal(GoalSource, inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
NestedProbe(WipProbe<'tcx>),
CommitIfOkStart,
Expand All @@ -226,7 +226,7 @@ enum WipProbeStep<'tcx> {
impl<'tcx> WipProbeStep<'tcx> {
fn finalize(self) -> inspect::ProbeStep<'tcx> {
match self {
WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
WipProbeStep::CommitIfOkStart => inspect::ProbeStep::CommitIfOkStart,
Expand Down Expand Up @@ -428,7 +428,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
}
}

pub fn add_goal(ecx: &mut EvalCtxt<'_, 'tcx>, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
pub fn add_goal(
ecx: &mut EvalCtxt<'_, 'tcx>,
source: GoalSource,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) {
// Can't use `if let Some(this) = ecx.inspect.as_mut()` here because
// we have to immutably use the `EvalCtxt` for `make_canonical_state`.
if ecx.inspect.is_noop() {
Expand All @@ -442,7 +446,9 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
evaluation: WipProbe { steps, .. },
..
})
| DebugSolver::Probe(WipProbe { steps, .. }) => steps.push(WipProbeStep::AddGoal(goal)),
| DebugSolver::Probe(WipProbe { steps, .. }) => {
steps.push(WipProbeStep::AddGoal(source, goal))
}
s => unreachable!("tried to add {goal:?} to {s:?}"),
}
}
Expand Down
22 changes: 13 additions & 9 deletions compiler/rustc_trait_selection/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ use rustc_infer::infer::DefineOpaqueTypes;
use rustc_infer::traits::query::NoSolution;
use rustc_middle::infer::canonical::CanonicalVarInfos;
use rustc_middle::traits::solve::{
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, IsNormalizesToHack, QueryResult,
Response,
CanonicalResponse, Certainty, ExternalConstraintsData, Goal, GoalSource, IsNormalizesToHack,
QueryResult, Response,
};
use rustc_middle::ty::{self, OpaqueTypeKey, Ty, TyCtxt, UniverseIndex};
use rustc_middle::ty::{
Expand Down Expand Up @@ -157,7 +157,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
) -> QueryResult<'tcx> {
match self.well_formed_goals(goal.param_env, goal.predicate) {
Some(goals) => {
self.add_goals(goals);
self.add_goals(GoalSource::Misc, goals);
self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
}
None => self.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS),
Expand Down Expand Up @@ -223,15 +223,19 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
}

#[instrument(level = "debug", skip(self))]
fn add_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
inspect::ProofTreeBuilder::add_goal(self, goal);
self.nested_goals.goals.push(goal);
fn add_goal(&mut self, source: GoalSource, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
inspect::ProofTreeBuilder::add_goal(self, source, goal);
self.nested_goals.goals.push((source, goal));
}

#[instrument(level = "debug", skip(self, goals))]
fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>) {
fn add_goals(
&mut self,
source: GoalSource,
goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>,
) {
for goal in goals {
self.add_goal(goal);
self.add_goal(source, goal);
}
}

Expand Down Expand Up @@ -335,7 +339,7 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
param_env,
ty::NormalizesTo { alias, term: normalized_ty.into() },
);
this.add_goal(normalizes_to_goal);
this.add_goal(GoalSource::Misc, normalizes_to_goal);
this.try_evaluate_added_goals()?;
let ty = this.resolve_vars_if_possible(normalized_ty);
Ok(this.try_normalize_ty_recur(param_env, define_opaque_types, depth + 1, ty))
Expand Down
Loading

0 comments on commit ca718ff

Please sign in to comment.