Skip to content

try evaluate nested goals with reduced depth first #143638

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

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all 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
10 changes: 8 additions & 2 deletions compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use rustc_type_ir::{
self as ty, Interner, TypeFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitableExt as _,
TypeVisitor, TypingMode, Upcast as _, elaborate,
};
use tracing::{debug, instrument};
use tracing::{debug, instrument, debug_span};

use super::trait_goals::TraitGoalProvenVia;
use super::{has_only_region_constraints, inspect};
Expand Down Expand Up @@ -958,13 +958,19 @@ where
// If the trait goal has been proven by using the environment, we want to treat
// aliases as rigid if there are no applicable projection bounds in the environment.
if considered_candidates.is_empty() {
let _span = debug_span!("inject_normalize_to_rigid_candidate");
let _span = _span.enter();
Comment on lines +961 to +962
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do we need this still? can't we just #[instrument] the inject fn?

if let Ok(response) = inject_normalize_to_rigid_candidate(self) {
considered_candidates.push(response);
}
}

if let Some(response) = self.try_merge_responses(&considered_candidates) {
Ok(response)
if response.value.certainty == Certainty::Yes && response.value.external_constraints.normalization_nested_goals.is_empty() {
Ok(response)
} else {
self.flounder(&considered_candidates)
}
} else {
self.flounder(&considered_candidates)
}
Expand Down
43 changes: 36 additions & 7 deletions compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -334,6 +334,19 @@ where
(result, proof_tree)
}

pub(super) fn with_capped_depth<R>(
&mut self,
max_depth: usize,
f: impl FnOnce(&mut Self) -> R,
) -> R {
let info = self.search_graph.with_capped_depth_start(max_depth);
let r = f(self);
if let Some(info) = info {
self.search_graph.with_capped_depth_end(info);
}
r
}

/// Creates a nested evaluation context that shares the same search graph as the
/// one passed in. This is suitable for evaluation, granted that the search graph
/// has had the nested goal recorded on its stack. This method only be used by
Expand Down Expand Up @@ -594,15 +607,31 @@ where
#[instrument(level = "trace", skip(self))]
pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
let mut response = Ok(Certainty::overflow(false));
for _ in 0..FIXPOINT_STEP_LIMIT {
// FIXME: This match is a bit ugly, it might be nice to change the inspect
// stuff to use a closure instead. which should hopefully simplify this a bit.
match self.evaluate_added_goals_step() {
for i in 0..FIXPOINT_STEP_LIMIT {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i'm tempted to say we should just unroll this loop somehow lol

debug!(?i, ?self.nested_goals, "try_evaluate_added_goals_step");
let evaluate_step_result = if i == 0 {
self.with_capped_depth(4, |this| this.evaluate_added_goals_step())
} else {
self.evaluate_added_goals_step()
};
match evaluate_step_result {
Ok(Some(cert)) => {
response = Ok(cert);
break;
if i == 0 {
for (_, _, stalled_on) in &mut self.nested_goals {
*stalled_on = None;
}
} else {
response = Ok(cert);
break;
}
}
Ok(None) => {
if i == 0 {
for (_, _, stalled_on) in &mut self.nested_goals {
*stalled_on = None;
}
}
}
Ok(None) => {}
Err(NoSolution) => {
response = Err(NoSolution);
break;
Expand Down
2 changes: 1 addition & 1 deletion compiler/rustc_next_trait_solver/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,7 @@ where
}

fn bail_with_ambiguity(&mut self, responses: &[CanonicalResponse<I>]) -> CanonicalResponse<I> {
debug_assert!(responses.len() > 1);
debug_assert!(responses.len() > 0);
let maybe_cause = responses.iter().fold(MaybeCause::Ambiguity, |maybe_cause, response| {
// Pull down the certainty of `Certainty::Yes` to ambiguity when combining
// these responses, b/c we're combining more than one response and this we
Expand Down
14 changes: 12 additions & 2 deletions compiler/rustc_next_trait_solver/src/solve/trait_goals.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1380,7 +1380,12 @@ where
.map(|c| c.result)
.collect();
return if let Some(response) = self.try_merge_responses(&where_bounds) {
Ok((response, Some(TraitGoalProvenVia::ParamEnv)))
let proven_via = if response.value.certainty == Certainty::Yes {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🤔 ?

Some(TraitGoalProvenVia::ParamEnv)
} else {
None
};
Ok((response, proven_via))
} else {
Ok((self.bail_with_ambiguity(&where_bounds), None))
};
Expand All @@ -1393,7 +1398,12 @@ where
.map(|c| c.result)
.collect();
return if let Some(response) = self.try_merge_responses(&alias_bounds) {
Ok((response, Some(TraitGoalProvenVia::AliasBound)))
let proven_via = if response.value.certainty == Certainty::Yes {
Some(TraitGoalProvenVia::AliasBound)
} else {
None
};
Ok((response, proven_via))
} else {
Ok((self.bail_with_ambiguity(&alias_bounds), None))
};
Expand Down
25 changes: 25 additions & 0 deletions compiler/rustc_type_ir/src/search_graph/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ use std::collections::hash_map::Entry;
use std::fmt::Debug;
use std::hash::Hash;
use std::marker::PhantomData;
use std::mem;

use derive_where::derive_where;
#[cfg(feature = "nightly")]
Expand Down Expand Up @@ -521,6 +522,11 @@ enum UpdateParentGoalCtxt<'a, X: Cx> {
ProvisionalCacheHit,
}

pub struct WithCappedDepthInfo {
encountered_overflow: bool,
available_depth: AvailableDepth,
}

impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
pub fn new(root_depth: usize) -> SearchGraph<D> {
Self {
Expand Down Expand Up @@ -594,6 +600,25 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
stack.cycle_step_kinds(head).fold(step_kind_to_head, |curr, step| curr.extend(step))
}

pub fn with_capped_depth_start(&mut self, max_depth: usize) -> Option<WithCappedDepthInfo> {
let entry = self.stack.last_mut().unwrap();
if max_depth < entry.available_depth.0 {
let encountered_overflow = entry.encountered_overflow;
let available_depth =
mem::replace(&mut entry.available_depth, AvailableDepth(max_depth));
Some(WithCappedDepthInfo { encountered_overflow, available_depth })
} else {
None
}
}

pub fn with_capped_depth_end(&mut self, info: WithCappedDepthInfo) {
let entry = self.stack.last_mut().unwrap();
entry.encountered_overflow = info.encountered_overflow;
entry.available_depth = info.available_depth;
self.provisional_cache.clear();
}

/// Probably the most involved method of the whole solver.
///
/// While goals get computed via `D::compute_goal`, this function handles
Expand Down
Loading