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

   1 //! Building proof trees incrementally during trait solving.
   2 //!
   3 //! This code is *a bit* of a mess and can hopefully be
   4 //! mostly ignored. For a general overview of how it works,
   5 //! see the comment on [ProofTreeBuilder].
   6 use rustc_middle::traits::query::NoSolution;
   7 use rustc_middle::traits::solve::{
   8     CanonicalInput, Certainty, Goal, IsNormalizesToHack, QueryInput, QueryResult,
   9 };
  10 use rustc_middle::ty::{self, TyCtxt};
  11 use rustc_session::config::DumpSolverProofTree;
  12
  13 use crate::solve::eval_ctxt::UseGlobalCache;
  14 use crate::solve::{self, inspect, EvalCtxt, GenerateProofTree};
  15
  16 /// The core data structure when building proof trees.
  17 ///
  18 /// In case the current evaluation does not generate a proof
  19 /// tree, `state` is simply `None` and we avoid any work.
  20 ///
  21 /// The possible states of the solver are represented via
  22 /// variants of [DebugSolver]. For any nested computation we call
  23 /// `ProofTreeBuilder::new_nested_computation_kind` which
  24 /// creates a new `ProofTreeBuilder` to temporarily replace the
  25 /// current one. Once that nested computation is done,
  26 /// `ProofTreeBuilder::nested_computation_kind` is called
  27 /// to add the finished nested evaluation to the parent.
  28 ///
  29 /// We provide additional information to the current state
  30 /// by calling methods such as `ProofTreeBuilder::probe_kind`.
  31 ///
  32 /// The actual structure closely mirrors the finished proof
  33 /// trees. At the end of trait solving `ProofTreeBuilder::finalize`
  34 /// is called to recursively convert the whole structure to a
  35 /// finished proof tree.
  36 pub(in crate::solve) struct ProofTreeBuilder<'tcx> {
  37     state: Option<Box<BuilderData<'tcx>>>,
  38 }
  39
  40 struct BuilderData<'tcx> {
  41     tree: DebugSolver<'tcx>,
  42     use_global_cache: UseGlobalCache,
  43 }
  44
  45 /// The current state of the proof tree builder, at most places
  46 /// in the code, only one or two variants are actually possible.
  47 ///
  48 /// We simply ICE in case that assumption is broken.
  49 #[derive(Debug)]
  50 enum DebugSolver<'tcx> {
  51     Root,
  52     GoalEvaluation(WipGoalEvaluation<'tcx>),
  53     CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<'tcx>),
  54     AddedGoalsEvaluation(WipAddedGoalsEvaluation<'tcx>),
  55     GoalEvaluationStep(WipGoalEvaluationStep<'tcx>),
  56     Probe(WipProbe<'tcx>),
  57 }
  58
  59 impl<'tcx> From<WipGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
  60     fn from(g: WipGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
  61         DebugSolver::GoalEvaluation(g)
  62     }
  63 }
  64
  65 impl<'tcx> From<WipCanonicalGoalEvaluation<'tcx>> for DebugSolver<'tcx> {
  66     fn from(g: WipCanonicalGoalEvaluation<'tcx>) -> DebugSolver<'tcx> {
  67         DebugSolver::CanonicalGoalEvaluation(g)
  68     }
  69 }
  70
  71 impl<'tcx> From<WipAddedGoalsEvaluation<'tcx>> for DebugSolver<'tcx> {
  72     fn from(g: WipAddedGoalsEvaluation<'tcx>) -> DebugSolver<'tcx> {
  73         DebugSolver::AddedGoalsEvaluation(g)
  74     }
  75 }
  76
  77 impl<'tcx> From<WipGoalEvaluationStep<'tcx>> for DebugSolver<'tcx> {
  78     fn from(g: WipGoalEvaluationStep<'tcx>) -> DebugSolver<'tcx> {
  79         DebugSolver::GoalEvaluationStep(g)
  80     }
  81 }
  82
  83 impl<'tcx> From<WipProbe<'tcx>> for DebugSolver<'tcx> {
  84     fn from(p: WipProbe<'tcx>) -> DebugSolver<'tcx> {
  85         DebugSolver::Probe(p)
  86     }
  87 }
  88
  89 #[derive(Eq, PartialEq, Debug)]
  90 struct WipGoalEvaluation<'tcx> {
  91     pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
  92     pub kind: WipGoalEvaluationKind<'tcx>,
  93     pub evaluation: Option<WipCanonicalGoalEvaluation<'tcx>>,
  94     pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
  95 }
  96
  97 impl<'tcx> WipGoalEvaluation<'tcx> {
  98     fn finalize(self) -> inspect::GoalEvaluation<'tcx> {
  99         inspect::GoalEvaluation {
 100             uncanonicalized_goal: self.uncanonicalized_goal,
 101             kind: match self.kind {
 102                 WipGoalEvaluationKind::Root { orig_values } => {
 103                     inspect::GoalEvaluationKind::Root { orig_values }
 104                 }
 105                 WipGoalEvaluationKind::Nested { is_normalizes_to_hack } => {
 106                     inspect::GoalEvaluationKind::Nested { is_normalizes_to_hack }
 107                 }
 108             },
 109             evaluation: self.evaluation.unwrap().finalize(),
 110             returned_goals: self.returned_goals,
 111         }
 112     }
 113 }
 114
 115 #[derive(Eq, PartialEq, Debug)]
 116 pub(in crate::solve) enum WipGoalEvaluationKind<'tcx> {
 117     Root { orig_values: Vec<ty::GenericArg<'tcx>> },
 118     Nested { is_normalizes_to_hack: IsNormalizesToHack },
 119 }
 120
 121 #[derive(Eq, PartialEq, Debug)]
 122 pub(in crate::solve) enum WipCanonicalGoalEvaluationKind {
 123     Overflow,
 124     CacheHit(inspect::CacheHit),
 125 }
 126
 127 #[derive(Eq, PartialEq, Debug)]
 128 struct WipCanonicalGoalEvaluation<'tcx> {
 129     goal: CanonicalInput<'tcx>,
 130     kind: Option<WipCanonicalGoalEvaluationKind>,
 131     revisions: Vec<WipGoalEvaluationStep<'tcx>>,
 132     result: Option<QueryResult<'tcx>>,
 133 }
 134
 135 impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
 136     fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
 137         let kind = match self.kind {
 138             Some(WipCanonicalGoalEvaluationKind::Overflow) => {
 139                 inspect::CanonicalGoalEvaluationKind::Overflow
 140             }
 141             Some(WipCanonicalGoalEvaluationKind::CacheHit(hit)) => {
 142                 inspect::CanonicalGoalEvaluationKind::CacheHit(hit)
 143             }
 144             None => inspect::CanonicalGoalEvaluationKind::Uncached {
 145                 revisions: self
 146                     .revisions
 147                     .into_iter()
 148                     .map(WipGoalEvaluationStep::finalize)
 149                     .collect(),
 150             },
 151         };
 152
 153         inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
 154     }
 155 }
 156
 157 #[derive(Eq, PartialEq, Debug)]
 158 struct WipAddedGoalsEvaluation<'tcx> {
 159     evaluations: Vec<Vec<WipGoalEvaluation<'tcx>>>,
 160     result: Option<Result<Certainty, NoSolution>>,
 161 }
 162
 163 impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
 164     fn finalize(self) -> inspect::AddedGoalsEvaluation<'tcx> {
 165         inspect::AddedGoalsEvaluation {
 166             evaluations: self
 167                 .evaluations
 168                 .into_iter()
 169                 .map(|evaluations| {
 170                     evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
 171                 })
 172                 .collect(),
 173             result: self.result.unwrap(),
 174         }
 175     }
 176 }
 177
 178 #[derive(Eq, PartialEq, Debug)]
 179 struct WipGoalEvaluationStep<'tcx> {
 180     instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
 181
 182     evaluation: WipProbe<'tcx>,
 183 }
 184
 185 impl<'tcx> WipGoalEvaluationStep<'tcx> {
 186     fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
 187         let evaluation = self.evaluation.finalize();
 188         match evaluation.kind {
 189             inspect::ProbeKind::Root { .. } => (),
 190             _ => unreachable!("unexpected root evaluation: {evaluation:?}"),
 191         }
 192         inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
 193     }
 194 }
 195
 196 #[derive(Eq, PartialEq, Debug)]
 197 struct WipProbe<'tcx> {
 198     pub steps: Vec<WipProbeStep<'tcx>>,
 199     pub kind: Option<inspect::ProbeKind<'tcx>>,
 200 }
 201
 202 impl<'tcx> WipProbe<'tcx> {
 203     fn finalize(self) -> inspect::Probe<'tcx> {
 204         inspect::Probe {
 205             steps: self.steps.into_iter().map(WipProbeStep::finalize).collect(),
 206             kind: self.kind.unwrap(),
 207         }
 208     }
 209 }
 210
 211 #[derive(Eq, PartialEq, Debug)]
 212 enum WipProbeStep<'tcx> {
 213     AddGoal(inspect::CanonicalState<'tcx, Goal<'tcx, ty::Predicate<'tcx>>>),
 214     EvaluateGoals(WipAddedGoalsEvaluation<'tcx>),
 215     NestedProbe(WipProbe<'tcx>),
 216 }
 217
 218 impl<'tcx> WipProbeStep<'tcx> {
 219     fn finalize(self) -> inspect::ProbeStep<'tcx> {
 220         match self {
 221             WipProbeStep::AddGoal(goal) => inspect::ProbeStep::AddGoal(goal),
 222             WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
 223             WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
 224         }
 225     }
 226 }
 227
 228 impl<'tcx> ProofTreeBuilder<'tcx> {
 229     fn new(
 230         state: impl Into<DebugSolver<'tcx>>,
 231         use_global_cache: UseGlobalCache,
 232     ) -> ProofTreeBuilder<'tcx> {
 233         ProofTreeBuilder {
 234             state: Some(Box::new(BuilderData { tree: state.into(), use_global_cache })),
 235         }
 236     }
 237
 238     fn nested<T: Into<DebugSolver<'tcx>>>(&self, state: impl FnOnce() -> T) -> Self {
 239         match &self.state {
 240             Some(prev_state) => Self {
 241                 state: Some(Box::new(BuilderData {
 242                     tree: state().into(),
 243                     use_global_cache: prev_state.use_global_cache,
 244                 })),
 245             },
 246             None => Self { state: None },
 247         }
 248     }
 249
 250     fn as_mut(&mut self) -> Option<&mut DebugSolver<'tcx>> {
 251         self.state.as_mut().map(|boxed| &mut boxed.tree)
 252     }
 253
 254     pub fn finalize(self) -> Option<inspect::GoalEvaluation<'tcx>> {
 255         match self.state?.tree {
 256             DebugSolver::GoalEvaluation(wip_goal_evaluation) => {
 257                 Some(wip_goal_evaluation.finalize())
 258             }
 259             root => unreachable!("unexpected proof tree builder root node: {:?}", root),
 260         }
 261     }
 262
 263     pub fn use_global_cache(&self) -> bool {
 264         self.state
 265             .as_ref()
 266             .map(|state| matches!(state.use_global_cache, UseGlobalCache::Yes))
 267             .unwrap_or(true)
 268     }
 269
 270     pub fn new_maybe_root(
 271         tcx: TyCtxt<'tcx>,
 272         generate_proof_tree: GenerateProofTree,
 273     ) -> ProofTreeBuilder<'tcx> {
 274         match generate_proof_tree {
 275             GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
 276             GenerateProofTree::IfEnabled => {
 277                 let opts = &tcx.sess.opts.unstable_opts;
 278                 match opts.dump_solver_proof_tree {
 279                     DumpSolverProofTree::Always => {
 280                         let use_cache = opts.dump_solver_proof_tree_use_cache.unwrap_or(true);
 281                         ProofTreeBuilder::new_root(UseGlobalCache::from_bool(use_cache))
 282                     }
 283                     // `OnError` is handled by reevaluating goals in error
 284                     // reporting with `GenerateProofTree::Yes`.
 285                     DumpSolverProofTree::OnError | DumpSolverProofTree::Never => {
 286                         ProofTreeBuilder::new_noop()
 287                     }
 288                 }
 289             }
 290             GenerateProofTree::Yes(use_cache) => ProofTreeBuilder::new_root(use_cache),
 291         }
 292     }
 293
 294     pub fn new_root(use_global_cache: UseGlobalCache) -> ProofTreeBuilder<'tcx> {
 295         ProofTreeBuilder::new(DebugSolver::Root, use_global_cache)
 296     }
 297
 298     pub fn new_noop() -> ProofTreeBuilder<'tcx> {
 299         ProofTreeBuilder { state: None }
 300     }
 301
 302     pub fn is_noop(&self) -> bool {
 303         self.state.is_none()
 304     }
 305
 306     pub(in crate::solve) fn new_goal_evaluation(
 307         &mut self,
 308         goal: Goal<'tcx, ty::Predicate<'tcx>>,
 309         orig_values: &[ty::GenericArg<'tcx>],
 310         kind: solve::GoalEvaluationKind,
 311     ) -> ProofTreeBuilder<'tcx> {
 312         self.nested(|| WipGoalEvaluation {
 313             uncanonicalized_goal: goal,
 314             kind: match kind {
 315                 solve::GoalEvaluationKind::Root => {
 316                     WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
 317                 }
 318                 solve::GoalEvaluationKind::Nested { is_normalizes_to_hack } => {
 319                     WipGoalEvaluationKind::Nested { is_normalizes_to_hack }
 320                 }
 321             },
 322             evaluation: None,
 323             returned_goals: vec![],
 324         })
 325     }
 326
 327     pub fn new_canonical_goal_evaluation(
 328         &mut self,
 329         goal: CanonicalInput<'tcx>,
 330     ) -> ProofTreeBuilder<'tcx> {
 331         self.nested(|| WipCanonicalGoalEvaluation {
 332             goal,
 333             kind: None,
 334             revisions: vec![],
 335             result: None,
 336         })
 337     }
 338
 339     pub fn canonical_goal_evaluation(&mut self, canonical_goal_evaluation: ProofTreeBuilder<'tcx>) {
 340         if let Some(this) = self.as_mut() {
 341             match (this, canonical_goal_evaluation.state.unwrap().tree) {
 342                 (
 343                     DebugSolver::GoalEvaluation(goal_evaluation),
 344                     DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation),
 345                 ) => goal_evaluation.evaluation = Some(canonical_goal_evaluation),
 346                 _ => unreachable!(),
 347             }
 348         }
 349     }
 350
 351     pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind) {
 352         if let Some(this) = self.as_mut() {
 353             match this {
 354                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
 355                     assert_eq!(canonical_goal_evaluation.kind.replace(kind), None);
 356                 }
 357                 _ => unreachable!(),
 358             };
 359         }
 360     }
 361
 362     pub fn returned_goals(&mut self, goals: &[Goal<'tcx, ty::Predicate<'tcx>>]) {
 363         if let Some(this) = self.as_mut() {
 364             match this {
 365                 DebugSolver::GoalEvaluation(evaluation) => {
 366                     assert!(evaluation.returned_goals.is_empty());
 367                     evaluation.returned_goals.extend(goals);
 368                 }
 369                 _ => unreachable!(),
 370             }
 371         }
 372     }
 373     pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<'tcx>) {
 374         if let Some(this) = self.as_mut() {
 375             match (this, goal_evaluation.state.unwrap().tree) {
 376                 (
 377                     DebugSolver::AddedGoalsEvaluation(WipAddedGoalsEvaluation {
 378                         evaluations, ..
 379                     }),
 380                     DebugSolver::GoalEvaluation(goal_evaluation),
 381                 ) => evaluations.last_mut().unwrap().push(goal_evaluation),
 382                 (this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
 383                 _ => unreachable!(),
 384             }
 385         }
 386     }
 387
 388     pub fn new_goal_evaluation_step(
 389         &mut self,
 390         instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
 391     ) -> ProofTreeBuilder<'tcx> {
 392         self.nested(|| WipGoalEvaluationStep {
 393             instantiated_goal,
 394             evaluation: WipProbe { steps: vec![], kind: None },
 395         })
 396     }
 397     pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
 398         if let Some(this) = self.as_mut() {
 399             match (this, goal_evaluation_step.state.unwrap().tree) {
 400                 (
 401                     DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
 402                     DebugSolver::GoalEvaluationStep(goal_evaluation_step),
 403                 ) => {
 404                     canonical_goal_evaluations.revisions.push(goal_evaluation_step);
 405                 }
 406                 _ => unreachable!(),
 407             }
 408         }
 409     }
 410
 411     pub fn new_probe(&mut self) -> ProofTreeBuilder<'tcx> {
 412         self.nested(|| WipProbe { steps: vec![], kind: None })
 413     }
 414
 415     pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<'tcx>) {
 416         if let Some(this) = self.as_mut() {
 417             match this {
 418                 DebugSolver::Probe(this) => {
 419                     assert_eq!(this.kind.replace(probe_kind), None)
 420                 }
 421                 _ => unreachable!(),
 422             }
 423         }
 424     }
 425
 426     pub fn add_goal(ecx: &mut EvalCtxt<'_, 'tcx>, goal: Goal<'tcx, ty::Predicate<'tcx>>) {
 427         // Can't use `if let Some(this) = ecx.inspect.as_mut()` here because
 428         // we have to immutably use the `EvalCtxt` for `make_canonical_state`.
 429         if ecx.inspect.is_noop() {
 430             return;
 431         }
 432
 433         let goal = Self::make_canonical_state(ecx, goal);
 434
 435         match ecx.inspect.as_mut().unwrap() {
 436             DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
 437                 evaluation: WipProbe { steps, .. },
 438                 ..
 439             })
 440             | DebugSolver::Probe(WipProbe { steps, .. }) => steps.push(WipProbeStep::AddGoal(goal)),
 441             s => unreachable!("tried to add {goal:?} to {s:?}"),
 442         }
 443     }
 444
 445     pub fn finish_probe(&mut self, probe: ProofTreeBuilder<'tcx>) {
 446         if let Some(this) = self.as_mut() {
 447             match (this, probe.state.unwrap().tree) {
 448                 (
 449                     DebugSolver::Probe(WipProbe { steps, .. })
 450                     | DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
 451                         evaluation: WipProbe { steps, .. },
 452                         ..
 453                     }),
 454                     DebugSolver::Probe(probe),
 455                 ) => steps.push(WipProbeStep::NestedProbe(probe)),
 456                 _ => unreachable!(),
 457             }
 458         }
 459     }
 460
 461     pub fn new_evaluate_added_goals(&mut self) -> ProofTreeBuilder<'tcx> {
 462         self.nested(|| WipAddedGoalsEvaluation { evaluations: vec![], result: None })
 463     }
 464
 465     pub fn evaluate_added_goals_loop_start(&mut self) {
 466         if let Some(this) = self.as_mut() {
 467             match this {
 468                 DebugSolver::AddedGoalsEvaluation(this) => {
 469                     this.evaluations.push(vec![]);
 470                 }
 471                 _ => unreachable!(),
 472             }
 473         }
 474     }
 475
 476     pub fn eval_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
 477         if let Some(this) = self.as_mut() {
 478             match this {
 479                 DebugSolver::AddedGoalsEvaluation(this) => {
 480                     assert_eq!(this.result.replace(result), None);
 481                 }
 482                 _ => unreachable!(),
 483             }
 484         }
 485     }
 486
 487     pub fn added_goals_evaluation(&mut self, added_goals_evaluation: ProofTreeBuilder<'tcx>) {
 488         if let Some(this) = self.as_mut() {
 489             match (this, added_goals_evaluation.state.unwrap().tree) {
 490                 (
 491                     DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
 492                         evaluation: WipProbe { steps, .. },
 493                         ..
 494                     })
 495                     | DebugSolver::Probe(WipProbe { steps, .. }),
 496                     DebugSolver::AddedGoalsEvaluation(added_goals_evaluation),
 497                 ) => steps.push(WipProbeStep::EvaluateGoals(added_goals_evaluation)),
 498                 _ => unreachable!(),
 499             }
 500         }
 501     }
 502
 503     pub fn query_result(&mut self, result: QueryResult<'tcx>) {
 504         if let Some(this) = self.as_mut() {
 505             match this {
 506                 DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
 507                     assert_eq!(canonical_goal_evaluation.result.replace(result), None);
 508                 }
 509                 DebugSolver::GoalEvaluationStep(evaluation_step) => {
 510                     assert_eq!(
 511                         evaluation_step
 512                             .evaluation
 513                             .kind
 514                             .replace(inspect::ProbeKind::Root { result }),
 515                         None
 516                     );
 517                 }
 518                 _ => unreachable!(),
 519             }
 520         }
 521     }
 522 }