bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

allow caller to force proof tree generation

Browse source
This commit is contained in:
Boxy 2023-06-09 00:19:54 +01:00
parent 51090b962f
commit bb743f8635
2 changed files with 89 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

39
compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
View file

@ -9,7 +9,7 @@ use rustc_infer::infer::{
use rustc_infer::traits::query::NoSolution; use rustc_infer::traits::query::NoSolution;
use rustc_infer::traits::ObligationCause; use rustc_infer::traits::ObligationCause;
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind}; use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
use rustc_middle::traits::solve::inspect::CandidateKind; use rustc_middle::traits::solve::inspect::{self, CandidateKind};
use rustc_middle::traits::solve::{ use rustc_middle::traits::solve::{
CanonicalInput, CanonicalResponse, Certainty, MaybeCause, PredefinedOpaques, CanonicalInput, CanonicalResponse, Certainty, MaybeCause, PredefinedOpaques,
PredefinedOpaquesData, QueryResult, PredefinedOpaquesData, QueryResult,
@ -108,6 +108,12 @@ impl NestedGoals<'_> {
} }
} }
#[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
pub enum GenerateProofTree {
Yes,
No,
}
pub trait InferCtxtEvalExt<'tcx> { pub trait InferCtxtEvalExt<'tcx> {
/// Evaluates a goal from **outside** of the trait solver. /// Evaluates a goal from **outside** of the trait solver.
/// ///
@ -116,7 +122,11 @@ pub trait InferCtxtEvalExt<'tcx> {
fn evaluate_root_goal( fn evaluate_root_goal(
&self, &self,
goal: Goal<'tcx, ty::Predicate<'tcx>>, goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>; generate_proof_tree: GenerateProofTree,
) -> (
Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
Option<inspect::GoalEvaluation<'tcx>>,
);
} }
impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> { impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
@ -124,7 +134,11 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
fn evaluate_root_goal( fn evaluate_root_goal(
&self, &self,
goal: Goal<'tcx, ty::Predicate<'tcx>>, goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> { generate_proof_tree: GenerateProofTree,
) -> (
Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution>,
Option<inspect::GoalEvaluation<'tcx>>,
) {
let mode = if self.intercrate { SolverMode::Coherence } else { SolverMode::Normal }; let mode = if self.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
let mut search_graph = search_graph::SearchGraph::new(self.tcx, mode); let mut search_graph = search_graph::SearchGraph::new(self.tcx, mode);
@ -141,19 +155,16 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
var_values: CanonicalVarValues::dummy(), var_values: CanonicalVarValues::dummy(),
nested_goals: NestedGoals::new(), nested_goals: NestedGoals::new(),
tainted: Ok(()), tainted: Ok(()),
inspect: self inspect: (self.tcx.sess.opts.unstable_opts.dump_solver_proof_tree
.tcx || matches!(generate_proof_tree, GenerateProofTree::Yes))
.sess .then(ProofTreeBuilder::new_root)
.opts .unwrap_or_else(ProofTreeBuilder::new_noop),
.unstable_opts
.dump_solver_proof_tree
.then(ProofTreeBuilder::new_root)
.unwrap_or_else(ProofTreeBuilder::new_noop),
}; };
let result = ecx.evaluate_goal(IsNormalizesToHack::No, goal); let result = ecx.evaluate_goal(IsNormalizesToHack::No, goal);
if let Some(tree) = ecx.inspect.finalize() { let tree = ecx.inspect.finalize();
println!("{:?}", tree); if let Some(tree) = &tree {
debug!(?tree);
} }
assert!( assert!(
@ -162,7 +173,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
); );
assert!(search_graph.is_empty()); assert!(search_graph.is_empty());
result (result, tree)
} }
} }

122
compiler/rustc_trait_selection/src/solve/fulfill.rs
View file

@ -10,6 +10,7 @@ use rustc_infer::traits::{
use rustc_middle::ty; use rustc_middle::ty;
use rustc_middle::ty::error::{ExpectedFound, TypeError}; use rustc_middle::ty::error::{ExpectedFound, TypeError};
use super::eval_ctxt::GenerateProofTree;
use super::{Certainty, InferCtxtEvalExt}; use super::{Certainty, InferCtxtEvalExt};
/// A trait engine using the new trait solver. /// A trait engine using the new trait solver.
@ -46,8 +47,11 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
self.obligations self.obligations
.drain(..) .drain(..)
.map(|obligation| { .map(|obligation| {
let code = let code = infcx.probe(|_| {
infcx.probe(|_| match infcx.evaluate_root_goal(obligation.clone().into()) { match infcx
.evaluate_root_goal(obligation.clone().into(), GenerateProofTree::No)
.0
{
Ok((_, Certainty::Maybe(MaybeCause::Ambiguity), _)) => { Ok((_, Certainty::Maybe(MaybeCause::Ambiguity), _)) => {
FulfillmentErrorCode::CodeAmbiguity { overflow: false } FulfillmentErrorCode::CodeAmbiguity { overflow: false }
} }
@ -60,7 +64,8 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
Err(_) => { Err(_) => {
bug!("did not expect selection error when collecting ambiguity errors") bug!("did not expect selection error when collecting ambiguity errors")
} }
}); }
});
FulfillmentError { FulfillmentError {
obligation: obligation.clone(), obligation: obligation.clone(),
@ -81,61 +86,62 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
let mut has_changed = false; let mut has_changed = false;
for obligation in mem::take(&mut self.obligations) { for obligation in mem::take(&mut self.obligations) {
let goal = obligation.clone().into(); let goal = obligation.clone().into();
let (changed, certainty, nested_goals) = match infcx.evaluate_root_goal(goal) { let (changed, certainty, nested_goals) =
Ok(result) => result, match infcx.evaluate_root_goal(goal, GenerateProofTree::No).0 {
Err(NoSolution) => { Ok(result) => result,
errors.push(FulfillmentError { Err(NoSolution) => {
obligation: obligation.clone(), errors.push(FulfillmentError {
code: match goal.predicate.kind().skip_binder() { obligation: obligation.clone(),
ty::PredicateKind::Clause(ty::Clause::Projection(_)) => { code: match goal.predicate.kind().skip_binder() {
FulfillmentErrorCode::CodeProjectionError( ty::PredicateKind::Clause(ty::Clause::Projection(_)) => {
// FIXME: This could be a `Sorts` if the term is a type FulfillmentErrorCode::CodeProjectionError(
MismatchedProjectionTypes { err: TypeError::Mismatch }, // FIXME: This could be a `Sorts` if the term is a type
) MismatchedProjectionTypes { err: TypeError::Mismatch },
} )
ty::PredicateKind::AliasRelate(_, _, _) => { }
FulfillmentErrorCode::CodeProjectionError( ty::PredicateKind::AliasRelate(_, _, _) => {
MismatchedProjectionTypes { err: TypeError::Mismatch }, FulfillmentErrorCode::CodeProjectionError(
) MismatchedProjectionTypes { err: TypeError::Mismatch },
} )
ty::PredicateKind::Subtype(pred) => { }
let (a, b) = infcx.instantiate_binder_with_placeholders( ty::PredicateKind::Subtype(pred) => {
goal.predicate.kind().rebind((pred.a, pred.b)), let (a, b) = infcx.instantiate_binder_with_placeholders(
); goal.predicate.kind().rebind((pred.a, pred.b)),
let expected_found = ExpectedFound::new(true, a, b); );
FulfillmentErrorCode::CodeSubtypeError( let expected_found = ExpectedFound::new(true, a, b);
expected_found, FulfillmentErrorCode::CodeSubtypeError(
TypeError::Sorts(expected_found), expected_found,
) TypeError::Sorts(expected_found),
} )
ty::PredicateKind::Coerce(pred) => { }
let (a, b) = infcx.instantiate_binder_with_placeholders( ty::PredicateKind::Coerce(pred) => {
goal.predicate.kind().rebind((pred.a, pred.b)), let (a, b) = infcx.instantiate_binder_with_placeholders(
); goal.predicate.kind().rebind((pred.a, pred.b)),
let expected_found = ExpectedFound::new(false, a, b); );
FulfillmentErrorCode::CodeSubtypeError( let expected_found = ExpectedFound::new(false, a, b);
expected_found, FulfillmentErrorCode::CodeSubtypeError(
TypeError::Sorts(expected_found), expected_found,
) TypeError::Sorts(expected_found),
} )
ty::PredicateKind::Clause(_) }
| ty::PredicateKind::ObjectSafe(_) ty::PredicateKind::Clause(_)
| ty::PredicateKind::ClosureKind(_, _, _) | ty::PredicateKind::ObjectSafe(_)
| ty::PredicateKind::Ambiguous => { | ty::PredicateKind::ClosureKind(_, _, _)
FulfillmentErrorCode::CodeSelectionError( | ty::PredicateKind::Ambiguous => {
SelectionError::Unimplemented, FulfillmentErrorCode::CodeSelectionError(
) SelectionError::Unimplemented,
} )
ty::PredicateKind::ConstEquate(..) }
| ty::PredicateKind::TypeWellFormedFromEnv(_) => { ty::PredicateKind::ConstEquate(..)
bug!("unexpected goal: {goal:?}") | ty::PredicateKind::TypeWellFormedFromEnv(_) => {
} bug!("unexpected goal: {goal:?}")
}, }
root_obligation: obligation, },
}); root_obligation: obligation,
continue; });
} continue;
}; }
};
// Push any nested goals that we get from unifying our canonical response // Push any nested goals that we get from unifying our canonical response
// with our obligation onto the fulfillment context. // with our obligation onto the fulfillment context.
self.obligations.extend(nested_goals.into_iter().map(|goal| { self.obligations.extend(nested_goals.into_iter().map(|goal| {