Rollup merge of rust-lang#125510 - lcnr:change-proof-trees-to-be-shal…

…low, r=compiler-errors

remove proof tree formatting, make em shallow

Debugging via tracing `RUSTC_LOG=rustc_trait_selection::solve=debug` is now imo slightly more readable then the actual proof tree formatter. Removing everything that's not needed for the `analyse` visitor allows us to remove a bunch of code.

I personally believe that we should continue to use tracing over proof trees for debugging:
- it eagerly prints, allowing us to debug ICEs
- the proof tree builder ends up going out of sync with the actual runtime behavior, which is confusing
- using shallow proof trees is a lot more performant as we frequently do not recurse into all nested goals when using an analyse visitor
- this allows us to clean up the implementation and remove some code

r? `@compiler-errors`

compiler/rustc_interface/src/tests.rs

@@ -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);

compiler/rustc_middle/src/arena.rs

@@ -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,

compiler/rustc_middle/src/traits/solve/cache.rs

@@ -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,
 }
@@ -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>>,
@@ -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`.

compiler/rustc_middle/src/ty/context.rs

@@ -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>>;

compiler/rustc_session/src/config.rs

@@ -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)]

compiler/rustc_session/src/options.rs

@@ -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 =
@@ -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

compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs

@@ -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;
@@ -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};
@@ -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>)]
@@ -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.
@@ -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
@@ -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
@@ -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);
  }
@@ -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.

compiler/rustc_trait_selection/src/solve/fulfill.rs

@@ -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,
@@ -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,
@@ -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)
  }

compiler/rustc_trait_selection/src/solve/inspect/analyse.rs

@@ -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(_) => (),
  }
  }
 
@@ -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![];
@@ -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