mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Take into account trait predicate coinductiveness

Browse Source
This commit is contained in:
Jack Huey 2022-06-26 18:59:29 -04:00
parent e16dbb5076
commit bd298adcd4
1 changed files with 36 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
compiler/rustc_trait_selection/src/traits/select/mod.rs
View File

@ -512,13 +512,36 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
let cache = previous_stack.cache;
let dfn = cache.next_dfn();
for stack_arg in previous_stack.cache.wf_tys.borrow().iter().rev() {
for stack_arg in previous_stack.cache.wf_args.borrow().iter().rev() {
if stack_arg.0 != arg {
continue;
}
debug!("WellFormed({:?}) on stack", arg);
if let Some(stack) = previous_stack.head {
stack.update_reached_depth(stack_arg.1);
// Okay, let's imagine we have two different stacks:
// `T: NonAutoTrait -> WF(T) -> T: NonAutoTrait`
// `WF(T) -> T: NonAutoTrait -> WF(T)`
// Because of this, we need to check that all
// predicates between the WF goals are coinductive.
// Otherwise, we can say that `T: NonAutoTrait` is
// true.
// Let's imagine we have a predicate stack like
// `Foo: Bar -> WF(T) -> T: NonAutoTrait -> T: Auto
// depth ^1 ^2 ^3
// and the current predicate is `WF(T)`. `wf_args`
// would contain `(T, 1)`. We want to check all
// trait predicates greater than `1`. The previous
// stack would be `T: Auto`.
let cycle = stack.iter().take_while(|s| s.depth > stack_arg.1);
let tcx = self.tcx();
let cycle =
cycle.map(|stack| stack.obligation.predicate.to_predicate(tcx));
if self.coinductive_match(cycle) {
stack.update_reached_depth(stack_arg.1);
return Ok(EvaluatedToOk);
} else {
return Ok(EvaluatedToRecur);
}
}
return Ok(EvaluatedToOk);
}
@ -534,10 +557,10 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
Some(mut obligations) => {
self.add_depth(obligations.iter_mut(), obligation.recursion_depth);
cache.wf_tys.borrow_mut().push((arg, previous_stack.depth()));
cache.wf_args.borrow_mut().push((arg, previous_stack.depth()));
let result =
self.evaluate_predicates_recursively(previous_stack, obligations);
cache.wf_tys.borrow_mut().pop();
cache.wf_args.borrow_mut().pop();
let result = result?;
@ -2465,7 +2488,14 @@ struct ProvisionalEvaluationCache<'tcx> {
/// means the cached value for `F`.
map: RefCell<FxHashMap<ty::PolyTraitPredicate<'tcx>, ProvisionalEvaluation>>,
wf_tys: RefCell<Vec<(ty::GenericArg<'tcx>, usize)>>,
/// The stack of args that we assume to be true because a `WF(arg)` predicate
/// is on the stack above (and because of wellformedness is coinductive).
/// In an "ideal" world, this would share a stack with trait predicates in
/// `TraitObligationStack`. However, trait predicates are *much* hotter than
/// `WellFormed` predicates, and it's very likely that the additional matches
/// will have a perf effect. The value here is the well-formed `GenericArg`
/// and the depth of the trait predicate *above* that well-formed predicate.
wf_args: RefCell<Vec<(ty::GenericArg<'tcx>, usize)>>,
}
/// A cache value for the provisional cache: contains the depth-first
@ -2479,7 +2509,7 @@ struct ProvisionalEvaluation {
impl<'tcx> Default for ProvisionalEvaluationCache<'tcx> {
fn default() -> Self {
Self { dfn: Cell::new(0), map: Default::default(), wf_tys: Default::default() }
Self { dfn: Cell::new(0), map: Default::default(), wf_args: Default::default() }
}
}