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