Rollup merge of rust-lang#113694 - BoxyUwU:proof_tree_dump_filtering, r=compiler-errors

Allow filtering what proof trees are dumped to stdout via a rustc attr

Adds a `#![rustc_filter_proof_tree_dump("...")]` attribute that can be placed on the crate root to filter the output of `-Zdump-solver-proof-tree=always`. It works by only generating proof trees if the debug output of the root goal's predicate is the same as the string. It doesn't feel ideal although I wasn't sure how else to make something like this work- actually trying to parse goal syntax seemed far harder.

Ideally this would also work for `=on_error` but i haven't made that work yet. I was hoping this could be used to generate proof trees in ui tests but the output still seems kinda huge and its not deduplicated at all (the stdout file i commited literaly has the exact same proof tree Twice...) I'm not sure its actually worth adding `-Zdump-solver-proof-tree` to ui tests yet.

Author: matthiaskrgr

compiler/rustc_feature/src/builtin_attrs.rs

@@ -801,6 +801,11 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
         rustc_doc_primitive, Normal, template!(NameValueStr: "primitive name"), ErrorFollowing,
         r#"`rustc_doc_primitive` is a rustc internal attribute"#,
     ),
+    rustc_attr!(
+        rustc_filter_proof_tree_dump, Normal, template!(List: "filter1, filter2, ..."), DuplicatesOk,
+        "the `#[rustc_filter_proof_tree_dump(...)]` attribute is used to filter out proof trees \
+        from `-Zdump-solver-proof-tree` output.",
+    ),
 
     // ==========================================================================
     // Internal attributes, Testing:

compiler/rustc_span/src/def_id.rs

@@ -388,6 +388,7 @@ pub struct LocalDefId {
 impl !Ord for LocalDefId {}
 impl !PartialOrd for LocalDefId {}
 
+/// The [`DefId`] for the local crate root.
 pub const CRATE_DEF_ID: LocalDefId = LocalDefId { local_def_index: CRATE_DEF_INDEX };
 
 impl Idx for LocalDefId {

compiler/rustc_span/src/symbol.rs

@@ -1287,6 +1287,7 @@ symbols! {
         rustc_error,
         rustc_evaluate_where_clauses,
         rustc_expected_cgu_reuse,
+        rustc_filter_proof_tree_dump,
         rustc_has_incoherent_inherent_impls,
         rustc_host,
         rustc_if_this_changed,

compiler/rustc_trait_selection/src/solve/eval_ctxt.rs

@@ -159,9 +159,12 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
         Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
         Option<inspect::GoalEvaluation<'tcx>>,
     ) {
-        EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
-            ecx.evaluate_goal(IsNormalizesToHack::No, goal)
-        })
+        EvalCtxt::enter_root(
+            self,
+            generate_proof_tree,
+            || format!("{:?}", goal.predicate),
+            |ecx| ecx.evaluate_goal(IsNormalizesToHack::No, goal),
+        )
     }
 }
 
@@ -176,6 +179,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
     fn enter_root<R>(
         infcx: &InferCtxt<'tcx>,
         generate_proof_tree: GenerateProofTree,
+        filter: impl FnOnce() -> String,
         f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> R,
     ) -> (R, Option<inspect::GoalEvaluation<'tcx>>) {
         let mode = if infcx.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
@@ -194,7 +198,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
             var_values: CanonicalVarValues::dummy(),
             nested_goals: NestedGoals::new(),
             tainted: Ok(()),
-            inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
+            inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree, filter),
         };
         let result = f(&mut ecx);
 

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

@@ -43,46 +43,51 @@ impl<'tcx> InferCtxtSelectExt<'tcx> for InferCtxt<'tcx> {
             self.instantiate_binder_with_placeholders(obligation.predicate),
         );
 
-        let (result, _) = EvalCtxt::enter_root(self, GenerateProofTree::Never, |ecx| {
-            let goal = Goal::new(ecx.tcx(), trait_goal.param_env, trait_goal.predicate);
-            let (orig_values, canonical_goal) = ecx.canonicalize_goal(goal);
-            let mut candidates = ecx.compute_canonical_trait_candidates(canonical_goal);
-
-            // pseudo-winnow
-            if candidates.len() == 0 {
-                return Err(SelectionError::Unimplemented);
-            } else if candidates.len() > 1 {
-                let mut i = 0;
-                while i < candidates.len() {
-                    let should_drop_i = (0..candidates.len()).filter(|&j| i != j).any(|j| {
-                        candidate_should_be_dropped_in_favor_of(
-                            ecx.tcx(),
-                            &candidates[i],
-                            &candidates[j],
-                        )
-                    });
-                    if should_drop_i {
-                        candidates.swap_remove(i);
-                    } else {
-                        i += 1;
-                        if i > 1 {
-                            return Ok(None);
+        let (result, _) = EvalCtxt::enter_root(
+            self,
+            GenerateProofTree::Never,
+            || unreachable!("proof trees cannot be generated for selection"),
+            |ecx| {
+                let goal = Goal::new(ecx.tcx(), trait_goal.param_env, trait_goal.predicate);
+                let (orig_values, canonical_goal) = ecx.canonicalize_goal(goal);
+                let mut candidates = ecx.compute_canonical_trait_candidates(canonical_goal);
+
+                // pseudo-winnow
+                if candidates.len() == 0 {
+                    return Err(SelectionError::Unimplemented);
+                } else if candidates.len() > 1 {
+                    let mut i = 0;
+                    while i < candidates.len() {
+                        let should_drop_i = (0..candidates.len()).filter(|&j| i != j).any(|j| {
+                            candidate_should_be_dropped_in_favor_of(
+                                ecx.tcx(),
+                                &candidates[i],
+                                &candidates[j],
+                            )
+                        });
+                        if should_drop_i {
+                            candidates.swap_remove(i);
+                        } else {
+                            i += 1;
+                            if i > 1 {
+                                return Ok(None);
+                            }
                         }
                     }
                 }
-            }
 
-            let candidate = candidates.pop().unwrap();
-            let (certainty, nested_goals) = ecx
-                .instantiate_and_apply_query_response(
-                    trait_goal.param_env,
-                    orig_values,
-                    candidate.result,
-                )
-                .map_err(|_| SelectionError::Unimplemented)?;
+                let candidate = candidates.pop().unwrap();
+                let (certainty, nested_goals) = ecx
+                    .instantiate_and_apply_query_response(
+                        trait_goal.param_env,
+                        orig_values,
+                        candidate.result,
+                    )
+                    .map_err(|_| SelectionError::Unimplemented)?;
 
-            Ok(Some((candidate, certainty, nested_goals)))
-        });
+                Ok(Some((candidate, certainty, nested_goals)))
+            },
+        );
 
         let (candidate, certainty, nested_goals) = match result {
             Ok(Some((candidate, certainty, nested_goals))) => (candidate, certainty, nested_goals),

compiler/rustc_trait_selection/src/solve/inspect.rs

@@ -5,6 +5,7 @@ use rustc_middle::traits::solve::{
 };
 use rustc_middle::ty::{self, TyCtxt};
 use rustc_session::config::DumpSolverProofTree;
+use rustc_span::def_id::CRATE_DEF_ID;
 
 use super::eval_ctxt::UseGlobalCache;
 use super::GenerateProofTree;
@@ -199,15 +200,53 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
     pub fn new_maybe_root(
         tcx: TyCtxt<'tcx>,
         generate_proof_tree: GenerateProofTree,
+        filter: impl FnOnce() -> String,
     ) -> ProofTreeBuilder<'tcx> {
         match generate_proof_tree {
             GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
             GenerateProofTree::IfEnabled => {
                 let opts = &tcx.sess.opts.unstable_opts;
                 match opts.dump_solver_proof_tree {
                     DumpSolverProofTree::Always => {
-                        let use_cache = opts.dump_solver_proof_tree_use_cache.unwrap_or(true);
-                        ProofTreeBuilder::new_root(UseGlobalCache::from_bool(use_cache))
+                        let should_generate = if tcx
+                            .get_attrs(CRATE_DEF_ID, rustc_span::sym::rustc_filter_proof_tree_dump)
+                            .next()
+                            .is_some()
+                        {
+                            // dont do the filtering behaviour if there are no attributes anywhere
+                            let goal = filter();
+                            tcx
+                            .get_attrs(CRATE_DEF_ID, rustc_span::sym::rustc_filter_proof_tree_dump)
+                            .flat_map(|attr| {
+                                let meta = attr.meta_kind().unwrap();
+                                match meta {
+                                    rustc_ast::MetaItemKind::Word
+                                    | rustc_ast::MetaItemKind::NameValue(_) => {
+                                        bug!("wrong attribute kind for `rustc_filter_proof_tree_dump`")
+                                    }
+                                    rustc_ast::MetaItemKind::List(nested_meta) => {
+                                        nested_meta.into_iter().map(|nested_meta| {
+                                            match nested_meta {
+                                                rustc_ast::NestedMetaItem::MetaItem(_) => unreachable!("only string literals are supported in `rustc_filter_proof_tree_dump`"),
+                                                rustc_ast::NestedMetaItem::Lit(lit) => match lit.kind {
+                                                    rustc_ast::LitKind::Str(sym, _) => sym,
+                                                    _ => unreachable!("only string literals are supported in `rustc_filter_proof_tree_dump`"),
+                                                },
+                                            }
+                                        })
+                                    }
+                                }
+                            }).any(|sym| goal.as_str() == sym.as_str())
+                        } else {
+                            true
+                        };
+
+                        if should_generate {
+                            let use_cache = opts.dump_solver_proof_tree_use_cache.unwrap_or(true);
+                            ProofTreeBuilder::new_root(UseGlobalCache::from_bool(use_cache))
+                        } else {
+                            ProofTreeBuilder::new_noop()
+                        }
                     }
                     // `OnError` is handled by reevaluating goals in error
                     // reporting with `GenerateProofTree::Yes`.

tests/ui/traits/new-solver/alias_eq_simple.rs

@@ -1,5 +1,12 @@
 // check-pass
 // compile-flags: -Ztrait-solver=next
+// compile-flags: -Zdump-solver-proof-tree=always
+// compile-flags: -Zdump-solver-proof-tree-use-cache=no
+
+#![feature(rustc_attrs)]
+#![rustc_filter_proof_tree_dump(
+    "Binder { value: TraitPredicate(<(i32, u32) as TraitA>, polarity:Positive), bound_vars: [] }"
+)]
 
 // test that the new solver can handle `alias-eq(<i32 as TraitB>::Assoc, u32)`