From f552d5008a88cc592f53992680668437688132f6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 25 Jul 2024 18:09:15 +0200 Subject: [PATCH] Make breadth-first in path_to consider all starting points to avoid infinite loop. --- frontend/exporter/src/traits.rs | 140 +++++++++--------- .../toolchain__traits into-fstar.snap | 16 ++ tests/traits/src/lib.rs | 11 ++ 3 files changed, 99 insertions(+), 68 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 13aae48d1..7c2cf91e2 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -199,79 +199,90 @@ pub mod rustc { }) .collect() } + } - #[tracing::instrument(level = "trace", skip(s, param_env))] - fn path_to( - self, - s: &S, - target: PolyTraitRef<'tcx>, - param_env: rustc_middle::ty::ParamEnv<'tcx>, - ) -> Option> { - let tcx = s.base().tcx; + #[tracing::instrument(level = "trace", skip(s, param_env))] + pub fn path_to<'tcx, S: UnderOwnerState<'tcx>>( + starting_points: Vec>, + s: &S, + target: PolyTraitRef<'tcx>, + param_env: rustc_middle::ty::ParamEnv<'tcx>, + ) -> Option<(Path<'tcx>, AnnotatedPredicate<'tcx>)> { + let tcx = s.base().tcx; - /// A candidate projects `self` along a path reaching some - /// predicate. A candidate is selected when its predicate - /// is the one expected, aka `target`. - #[derive(Debug)] - struct Candidate<'tcx> { - path: Path<'tcx>, - pred: PolyTraitPredicate<'tcx>, - } + /// A candidate projects `self` along a path reaching some + /// predicate. A candidate is selected when its predicate + /// is the one expected, aka `target`. + #[derive(Debug)] + struct Candidate<'tcx> { + path: Path<'tcx>, + pred: PolyTraitPredicate<'tcx>, + origin: AnnotatedPredicate<'tcx>, + } - use std::collections::VecDeque; - let mut candidates: VecDeque> = vec![Candidate { - path: vec![], - pred: self, - }] - .into(); - - let target_pred = target.upcast(tcx); - let mut seen = std::collections::HashSet::new(); - - while let Some(candidate) = candidates.pop_front() { - { - // If a predicate was already seen, we know it is - // not the one we are looking for: we skip it. - if seen.contains(&candidate.pred) { - continue; - } - seen.insert(candidate.pred.clone()); - } + use std::collections::VecDeque; + let mut candidates: VecDeque> = starting_points + .into_iter() + .map(|pred| { + let clause = pred.predicate.as_trait_clause(); + clause.map(|clause| Candidate { + path: vec![], + pred: clause, + origin: pred.clone(), + }) + }) + .filter(|candidate| candidate.is_some()) + .map(|candidate| candidate.unwrap()) + .collect(); + + let target_pred = target.upcast(tcx); + let mut seen = std::collections::HashSet::new(); - // if the candidate equals the target, let's return its path - if predicate_equality(candidate.pred.upcast(tcx), target_pred, param_env, s) { - return Some(candidate.path); + while let Some(candidate) = candidates.pop_front() { + { + // If a predicate was already seen, we know it is + // not the one we are looking for: we skip it. + if seen.contains(&candidate.pred) { + continue; } + seen.insert(candidate.pred.clone()); + } + + // if the candidate equals the target, let's return its path + if predicate_equality(candidate.pred.upcast(tcx), target_pred, param_env, s) { + return Some((candidate.path, candidate.origin)); + } - // otherwise, we add to the queue all paths reachable from the candidate - for (index, parent_pred) in candidate.pred.parents_trait_predicates(s) { + // otherwise, we add to the queue all paths reachable from the candidate + for (index, parent_pred) in candidate.pred.parents_trait_predicates(s) { + let mut path = candidate.path.clone(); + path.push(PathChunk::Parent { + predicate: parent_pred.clone(), + index, + }); + candidates.push_back(Candidate { + pred: parent_pred.clone(), + path, + origin: candidate.origin.clone(), + }); + } + for (item, binder) in candidate.pred.associated_items_trait_predicates(s) { + for (index, parent_pred) in binder.skip_binder().into_iter() { let mut path = candidate.path.clone(); - path.push(PathChunk::Parent { + path.push(PathChunk::AssocItem { + item, predicate: parent_pred.clone(), index, }); candidates.push_back(Candidate { pred: parent_pred.clone(), path, + origin: candidate.origin.clone(), }); } - for (item, binder) in candidate.pred.associated_items_trait_predicates(s) { - for (index, parent_pred) in binder.skip_binder().into_iter() { - let mut path = candidate.path.clone(); - path.push(PathChunk::AssocItem { - item, - predicate: parent_pred.clone(), - index, - }); - candidates.push_back(Candidate { - pred: parent_pred.clone(), - path, - }); - } - } } - None } + None } } @@ -347,23 +358,16 @@ pub mod rustc { } .with_args(impl_exprs(s, &nested), trait_ref), ImplSource::Param(nested) => { - use search_clause::TraitPredicateExt; let tcx = s.base().tcx; - let predicates = &tcx.predicates_defined_on_or_above(s.owner_id()); - let Some((apred, path)) = predicates.into_iter().find_map(|apred| { - apred - .predicate - .as_trait_clause() - .map(|poly_trait_predicate| poly_trait_predicate) - .and_then(|poly_trait_predicate| { - poly_trait_predicate.path_to(s, self.clone(), param_env) - }) - .map(|path| (apred, path)) - }) else { + let predicates = tcx.predicates_defined_on_or_above(s.owner_id()); + let Some((path, apred)) = + search_clause::path_to(predicates.clone(), s, self.clone(), param_env) + else { supposely_unreachable_fatal!(s, "ImplExprPredNotFound"; { self, nested, predicates, trait_ref }) }; + use rustc_middle::ty::ToPolyTraitRef; let r#trait = apred .predicate diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index d2f3d6240..210e8a0f0 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -446,6 +446,22 @@ let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0) : t_Foo v_SelfType type t_Bar (v_FooConst: usize) (v_FooType: Type0) = | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType ''' +"Traits.Recursive_trait_with_assoc_type.fst" = ''' +module Traits.Recursive_trait_with_assoc_type +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class t_Trait1 (v_Self: Type0) = { + f_T:Type0; + f_T_10748091164337312478:t_Trait1 f_T +} + +class t_Trait2 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4567617955834163411:t_Trait1 v_Self; + f_U:Type0 +} +''' "Traits.Type_alias_bounds_issue_707_.fst" = ''' module Traits.Type_alias_bounds_issue_707_ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index a81df90d3..ad42cac56 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -265,3 +265,14 @@ mod block_size { fn proc_block(block: Vec<::BlockSize>); } } + +// issue 692 +mod recursive_trait_with_assoc_type { + pub trait Trait1 { + type T: Trait1; + } + + pub trait Trait2: Trait1 { + type U; + } +}