Skip to content
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

remove proof tree formatting, make em shallow #125510

Merged
merged 1 commit into from
May 25, 2024
Merged
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
5 changes: 1 addition & 4 deletions compiler/rustc_interface/src/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -799,10 +799,7 @@ fn test_unstable_options_tracking_hash() {
tracked!(mir_opt_level, Some(4));
tracked!(move_size_limit, Some(4096));
tracked!(mutable_noalias, false);
tracked!(
next_solver,
Some(NextSolverConfig { coherence: true, globally: false, dump_tree: Default::default() })
);
tracked!(next_solver, Some(NextSolverConfig { coherence: true, globally: false }));
tracked!(no_generate_arange_section, true);
tracked!(no_jump_tables, true);
tracked!(no_link, true);
Expand Down
5 changes: 4 additions & 1 deletion compiler/rustc_middle/src/arena.rs
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,10 @@ macro_rules! arena_types {
[] dtorck_constraint: rustc_middle::traits::query::DropckConstraint<'tcx>,
[] candidate_step: rustc_middle::traits::query::CandidateStep<'tcx>,
[] autoderef_bad_ty: rustc_middle::traits::query::MethodAutoderefBadTy<'tcx>,
[] canonical_goal_evaluation: rustc_next_trait_solver::solve::inspect::GoalEvaluationStep<rustc_middle::ty::TyCtxt<'tcx>>,
[] canonical_goal_evaluation:
rustc_next_trait_solver::solve::inspect::CanonicalGoalEvaluationStep<
rustc_middle::ty::TyCtxt<'tcx>
>,
[] query_region_constraints: rustc_middle::infer::canonical::QueryRegionConstraints<'tcx>,
[] type_op_subtype:
rustc_middle::infer::canonical::Canonical<'tcx,
Expand Down
6 changes: 3 additions & 3 deletions compiler/rustc_middle/src/traits/solve/cache.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ pub struct EvaluationCache<'tcx> {
#[derive(Debug, PartialEq, Eq)]
pub struct CacheData<'tcx> {
pub result: QueryResult<'tcx>,
pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
pub additional_depth: usize,
pub encountered_overflow: bool,
}
Expand All @@ -28,7 +28,7 @@ impl<'tcx> EvaluationCache<'tcx> {
&self,
tcx: TyCtxt<'tcx>,
key: CanonicalInput<'tcx>,
proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
additional_depth: usize,
encountered_overflow: bool,
cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
Expand Down Expand Up @@ -107,7 +107,7 @@ struct Success<'tcx> {
#[derive(Clone, Copy)]
pub struct QueryData<'tcx> {
pub result: QueryResult<'tcx>,
pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
}

/// The cache entry for a goal `CanonicalInput`.
Expand Down
3 changes: 2 additions & 1 deletion compiler/rustc_middle/src/ty/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,8 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
type PredefinedOpaques = solve::PredefinedOpaques<'tcx>;
type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
type ExternalConstraints = ExternalConstraints<'tcx>;
type GoalEvaluationSteps = &'tcx [solve::inspect::GoalEvaluationStep<TyCtxt<'tcx>>];
type CanonicalGoalEvaluationStepRef =
&'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>;

type Ty = Ty<'tcx>;
type Tys = &'tcx List<Ty<'tcx>>;
Expand Down
10 changes: 0 additions & 10 deletions compiler/rustc_session/src/config.rs
Original file line number Diff line number Diff line change
Expand Up @@ -796,16 +796,6 @@ pub struct NextSolverConfig {
/// Whether the new trait solver should be enabled everywhere.
/// This is only `true` if `coherence` is also enabled.
pub globally: bool,
/// Whether to dump proof trees after computing a proof tree.
pub dump_tree: DumpSolverProofTree,
}

#[derive(Default, Debug, Copy, Clone, Hash, PartialEq, Eq)]
pub enum DumpSolverProofTree {
Always,
OnError,
#[default]
Never,
}

#[derive(Clone)]
Expand Down
26 changes: 4 additions & 22 deletions compiler/rustc_session/src/options.rs
Original file line number Diff line number Diff line change
Expand Up @@ -399,7 +399,8 @@ mod desc {
pub const parse_instrument_xray: &str = "either a boolean (`yes`, `no`, `on`, `off`, etc), or a comma separated list of settings: `always` or `never` (mutually exclusive), `ignore-loops`, `instruction-threshold=N`, `skip-entry`, `skip-exit`";
pub const parse_unpretty: &str = "`string` or `string=string`";
pub const parse_treat_err_as_bug: &str = "either no value or a non-negative number";
pub const parse_next_solver_config: &str = "a comma separated list of solver configurations: `globally` (default), `coherence`, `dump-tree`, `dump-tree-on-error";
pub const parse_next_solver_config: &str =
"a comma separated list of solver configurations: `globally` (default), and `coherence`";
pub const parse_lto: &str =
"either a boolean (`yes`, `no`, `on`, `off`, etc), `thin`, `fat`, or omitted";
pub const parse_linker_plugin_lto: &str =
Expand Down Expand Up @@ -1058,39 +1059,20 @@ mod parse {
if let Some(config) = v {
let mut coherence = false;
let mut globally = true;
let mut dump_tree = None;
for c in config.split(',') {
match c {
"globally" => globally = true,
"coherence" => {
globally = false;
coherence = true;
}
"dump-tree" => {
if dump_tree.replace(DumpSolverProofTree::Always).is_some() {
return false;
}
}
"dump-tree-on-error" => {
if dump_tree.replace(DumpSolverProofTree::OnError).is_some() {
return false;
}
}
_ => return false,
}
}

*slot = Some(NextSolverConfig {
coherence: coherence || globally,
globally,
dump_tree: dump_tree.unwrap_or_default(),
});
*slot = Some(NextSolverConfig { coherence: coherence || globally, globally });
} else {
*slot = Some(NextSolverConfig {
coherence: true,
globally: true,
dump_tree: Default::default(),
});
*slot = Some(NextSolverConfig { coherence: true, globally: true });
}

true
Expand Down
27 changes: 5 additions & 22 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
use std::io::Write;
use std::ops::ControlFlow;

use rustc_data_structures::stack::ensure_sufficient_stack;
use rustc_hir::def_id::DefId;
use rustc_infer::infer::at::ToTrace;
Expand All @@ -20,10 +17,10 @@ use rustc_middle::ty::{
self, InferCtxtLike, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable,
TypeVisitable, TypeVisitableExt, TypeVisitor,
};
use rustc_session::config::DumpSolverProofTree;
use rustc_span::DUMMY_SP;
use rustc_type_ir::{self as ir, CanonicalVarValues, Interner};
use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
use std::ops::ControlFlow;

use crate::traits::coherence;
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
Expand Down Expand Up @@ -135,8 +132,7 @@ impl<I: Interner> NestedGoals<I> {
#[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
pub enum GenerateProofTree {
Yes,
IfEnabled,
Never,
No,
}

#[extension(pub trait InferCtxtEvalExt<'tcx>)]
Expand Down Expand Up @@ -182,7 +178,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
infcx,
search_graph: &mut search_graph,
nested_goals: NestedGoals::new(),
inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),

// Only relevant when canonicalizing the response,
// which we don't do within this evaluation context.
Expand All @@ -197,23 +193,14 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
};
let result = f(&mut ecx);

let tree = ecx.inspect.finalize();
if let (Some(tree), DumpSolverProofTree::Always) = (
&tree,
infcx.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default(),
) {
let mut lock = std::io::stdout().lock();
let _ = lock.write_fmt(format_args!("{tree:?}\n"));
let _ = lock.flush();
}

let proof_tree = ecx.inspect.finalize();
assert!(
ecx.nested_goals.is_empty(),
"root `EvalCtxt` should not have any goals added to it"
);

assert!(search_graph.is_empty());
(result, tree)
(result, proof_tree)
}

/// Creates a nested evaluation context that shares the same search graph as the
Expand Down Expand Up @@ -483,7 +470,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
// the certainty of all the goals.
#[instrument(level = "trace", skip(self))]
pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
self.inspect.start_evaluate_added_goals();
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
Expand All @@ -501,8 +487,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
}
}

self.inspect.evaluate_added_goals_result(response);

if response.is_err() {
self.tainted = Err(NoSolution);
}
Expand All @@ -515,7 +499,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
/// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
let tcx = self.tcx();
self.inspect.start_evaluate_added_goals_step();
let mut goals = core::mem::take(&mut self.nested_goals);

// If this loop did not result in any progress, what's our final certainty.
Expand Down
6 changes: 3 additions & 3 deletions compiler/rustc_trait_selection/src/solve/fulfill.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ impl<'tcx> ObligationStorage<'tcx> {
// change.
self.overflowed.extend(self.pending.extract_if(|o| {
let goal = o.clone().into();
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::Never).0;
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
match result {
Ok((has_changed, _)) => has_changed,
_ => false,
Expand Down Expand Up @@ -159,7 +159,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
let mut has_changed = false;
for obligation in self.obligations.unstalled_for_select() {
let goal = obligation.clone().into();
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
self.inspect_evaluated_obligation(infcx, &obligation, &result);
let (changed, certainty) = match result {
Ok(result) => result,
Expand Down Expand Up @@ -246,7 +246,7 @@ fn fulfillment_error_for_stalled<'tcx>(
root_obligation: PredicateObligation<'tcx>,
) -> FulfillmentError<'tcx> {
let (code, refine_obligation) = infcx.probe(|_| {
match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::Never).0 {
match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::No).0 {
Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
(FulfillmentErrorCode::Ambiguity { overflow: None }, true)
}
Expand Down
13 changes: 2 additions & 11 deletions compiler/rustc_trait_selection/src/solve/inspect/analyse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -317,7 +317,6 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
inspect::ProbeStep::RecordImplArgs { impl_args: i } => {
assert_eq!(impl_args.replace(i), None);
}
inspect::ProbeStep::EvaluateGoals(_) => (),
}
}

Expand Down Expand Up @@ -359,13 +358,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
warn!("unexpected root evaluation: {:?}", self.evaluation_kind);
return vec![];
}
inspect::CanonicalGoalEvaluationKind::Evaluation { revisions } => {
if let Some(last) = revisions.last() {
last
} else {
return vec![];
}
}
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
};

let mut nested_goals = vec![];
Expand All @@ -392,9 +385,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
source: GoalSource,
) -> Self {
let inspect::GoalEvaluation { uncanonicalized_goal, kind, evaluation } = root;
let inspect::GoalEvaluationKind::Root { orig_values } = kind else { unreachable!() };

let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
let result = evaluation.result.and_then(|ok| {
if let Some(term_hack) = normalizes_to_term_hack {
infcx
Expand Down
Loading
Loading