Skip to content

Commit

Permalink
remove proof tree formatter, make em shallow
Browse files Browse the repository at this point in the history
  • Loading branch information
lcnr committed May 24, 2024
1 parent 213ad10 commit ebd9f35
Show file tree
Hide file tree
Showing 16 changed files with 135 additions and 505 deletions.
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

0 comments on commit ebd9f35

Please sign in to comment.