Skip to content

Make predicate numbering more robust #1082

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Nadrieril merged 7 commits into from
Apr 2, 2026
Merged

Make predicate numbering more robust #1082

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
2a720de
Prepare
Nadrieril Mar 30, 2026
b4c3792
Add a global predicate id to each item clause
Nadrieril Mar 31, 2026
c7fb5be
Propagate these ids
Nadrieril Mar 31, 2026
de848ab
Use these ids to resolve trait clause references
Nadrieril Apr 2, 2026
0ef3bc0
Cleanup
Nadrieril Apr 2, 2026
a5bee94
Sanity-check the predicate->clause id mapping
Nadrieril Apr 2, 2026
08d37b9
`BoundPredicateOrigin` is now redundant
Nadrieril Apr 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 5 additions & 7 deletions charon/hax-frontend/src/traits.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ use crate::{id_table::hash_consing::HashConsed, prelude::*};
pub mod resolution;
mod utils;
pub use utils::{
Predicates, ToPolyTraitRef, erase_and_norm, erase_free_regions, implied_predicates, normalize,
predicates_defined_on, required_predicates, self_predicate,
ItemPredicate, ItemPredicateId, ItemPredicates, ToPolyTraitRef, erase_and_norm,
erase_free_regions, implied_predicates, normalize, required_predicates, self_predicate,
};

pub use resolution::PredicateSearcher;
Expand Down Expand Up @@ -76,9 +76,7 @@ pub enum ImplExprAtom {
Concrete(ItemRef),
/// A context-bound clause like `where T: Trait`.
LocalBound {
/// The nth (non-self) predicate found for this item. We use predicates from
/// `required_predicates` starting from the parentmost item.
index: usize,
id: GenericPredicateId,
r#trait: Binder<TraitRef>,
path: Vec<ImplExprPathChunk>,
},
Expand Down Expand Up @@ -282,13 +280,13 @@ pub fn solve_item_implied_traits<'tcx, S: UnderOwnerState<'tcx>>(
fn solve_item_traits_inner<'tcx, S: UnderOwnerState<'tcx>>(
s: &S,
generics: ty::GenericArgsRef<'tcx>,
predicates: utils::Predicates<'tcx>,
predicates: utils::ItemPredicates<'tcx>,
) -> Vec<ImplExpr> {
let tcx = s.base().tcx;
let typing_env = s.typing_env();
predicates
.iter()
.map(|(clause, _span)| *clause)
.map(|pred| pred.clause)
.filter_map(|clause| clause.as_trait_clause())
.map(|clause| clause.to_poly_trait_ref())
// Substitute the item generics
Expand Down
100 changes: 39 additions & 61 deletions charon/hax-frontend/src/traits/resolution.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
//! This module is independent from the rest of hax, in particular it doesn't use its
//! state-tracking machinery.

use crate::ItemPredicate;
use crate::options::BoundsOptions;
use itertools::{Either, Itertools};
use std::collections::{HashMap, hash_map::Entry};
Expand All @@ -12,6 +13,7 @@ use rustc_middle::traits::CodegenObligationError;
use rustc_middle::ty::{self, *};
use rustc_trait_selection::traits::ImplSource;

use super::ItemPredicateId;
use super::utils::{
self, ToPolyTraitRef, erase_and_norm, implied_predicates, normalize_bound_val,
required_predicates, self_predicate,
Expand Down Expand Up @@ -47,9 +49,7 @@ pub enum ImplExprAtom<'tcx> {
/// A context-bound clause like `where T: Trait`.
LocalBound {
predicate: Predicate<'tcx>,
/// The nth (non-self) predicate found for this item. We use predicates from
/// `required_predicates` starting from the parentmost item.
index: usize,
id: ItemPredicateId,
r#trait: PolyTraitRef<'tcx>,
path: Path<'tcx>,
},
Expand Down Expand Up @@ -117,21 +117,9 @@ pub struct ImplExpr<'tcx> {
pub r#impl: ImplExprAtom<'tcx>,
}

/// Items have various predicates in scope. `path_to` uses them as a starting point for trait
/// resolution. This tracks where each of them comes from.
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub enum BoundPredicateOrigin {
/// The `Self: Trait` predicate implicitly present within trait declarations (note: we
/// don't add it for trait implementations, should we?).
SelfPred,
/// The nth (non-self) predicate found for this item. We use predicates from
/// `required_predicates` starting from the parentmost item.
Item(usize),
}

#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct AnnotatedTraitPred<'tcx> {
pub origin: BoundPredicateOrigin,
pub struct ItemClause<'tcx> {
pub id: ItemPredicateId,
pub clause: PolyTraitPredicate<'tcx>,
}

Expand Down Expand Up @@ -160,23 +148,18 @@ fn local_bound_predicates<'tcx>(
tcx: TyCtxt<'tcx>,
def_id: rustc_span::def_id::DefId,
options: BoundsOptions,
) -> Vec<PolyTraitPredicate<'tcx>> {
) -> Vec<ItemPredicate<'tcx>> {
fn acc_predicates<'tcx>(
tcx: TyCtxt<'tcx>,
def_id: rustc_span::def_id::DefId,
options: BoundsOptions,
predicates: &mut Vec<PolyTraitPredicate<'tcx>>,
predicates: &mut Vec<ItemPredicate<'tcx>>,
) {
if crate::inherits_parent_clauses(tcx, def_id) {
let parent = tcx.parent(def_id);
acc_predicates(tcx, parent, options, predicates);
}
predicates.extend(
required_predicates(tcx, def_id, options)
.iter()
.map(|(clause, _span)| *clause)
.filter_map(|clause| clause.as_trait_clause()),
);
predicates.extend(required_predicates(tcx, def_id, options).iter());
}

let mut predicates = vec![];
Expand All @@ -193,10 +176,9 @@ fn parents_trait_predicates<'tcx>(
let self_trait_ref = pred.to_poly_trait_ref();
implied_predicates(tcx, pred.def_id(), options)
.iter()
.map(|(clause, _span)| *clause)
// Substitute with the `self` args so that the clause makes sense in the
// outside context.
.map(|clause| clause.instantiate_supertrait(tcx, self_trait_ref))
.map(|pred| pred.clause.instantiate_supertrait(tcx, self_trait_ref))
.filter_map(|pred| pred.as_trait_clause())
.collect()
}
Expand All @@ -207,18 +189,20 @@ fn parents_trait_predicates<'tcx>(
struct Candidate<'tcx> {
path: Path<'tcx>,
pred: PolyTraitPredicate<'tcx>,
origin: AnnotatedTraitPred<'tcx>,
origin: ItemClause<'tcx>,
}

impl<'tcx> Candidate<'tcx> {
fn into_impl_expr(self, tcx: TyCtxt<'tcx>) -> ImplExprAtom<'tcx> {
fn into_impl_expr(self, tcx: TyCtxt<'tcx>, implicit_self_clause: bool) -> ImplExprAtom<'tcx> {
let path = self.path;
let r#trait = self.origin.clause.to_poly_trait_ref();
match self.origin.origin {
BoundPredicateOrigin::SelfPred => ImplExprAtom::SelfImpl { r#trait, path },
BoundPredicateOrigin::Item(index) => ImplExprAtom::LocalBound {
match self.origin.id {
ItemPredicateId::TraitSelf if implicit_self_clause => {
ImplExprAtom::SelfImpl { r#trait, path }
}
_ => ImplExprAtom::LocalBound {
predicate: self.origin.clause.upcast(tcx),
index,
id: self.origin.id,
r#trait,
path,
},
Expand All @@ -235,13 +219,15 @@ pub struct PredicateSearcher<'tcx> {
candidates: HashMap<PolyTraitPredicate<'tcx>, Candidate<'tcx>>,
/// Resolution options.
options: BoundsOptions,
/// Count the number of bound clauses in scope; used to identify clauses uniquely.
bound_clause_count: usize,
/// Whether we're in a trait declaration context where an implicit `Self: Trait` clause is
/// accessible.
implicit_self_clause: bool,
}

impl<'tcx> PredicateSearcher<'tcx> {
/// Initialize the elaborator with the predicates accessible within this item.
pub fn new_for_owner(tcx: TyCtxt<'tcx>, owner_id: DefId, options: BoundsOptions) -> Self {
let initial_self_pred = initial_self_pred(tcx, owner_id);
let mut out = Self {
tcx,
typing_env: TypingEnv {
Expand All @@ -250,14 +236,12 @@ impl<'tcx> PredicateSearcher<'tcx> {
},
candidates: Default::default(),
options,
bound_clause_count: 0,
implicit_self_clause: initial_self_pred.is_some(),
};
out.insert_predicates(
initial_self_pred(tcx, owner_id).map(|clause| AnnotatedTraitPred {
origin: BoundPredicateOrigin::SelfPred,
clause,
}),
);
out.insert_predicates(initial_self_pred.map(|clause| ItemClause {
id: ItemPredicateId::TraitSelf,
clause,
}));
out.insert_bound_predicates(local_bound_predicates(tcx, owner_id, options));
out
}
Expand All @@ -267,20 +251,14 @@ impl<'tcx> PredicateSearcher<'tcx> {
/// insertion order.
pub fn insert_bound_predicates(
&mut self,
clauses: impl IntoIterator<Item = PolyTraitPredicate<'tcx>>,
preds: impl IntoIterator<Item = ItemPredicate<'tcx>>,
) {
let mut count = usize::MAX;
// Swap to avoid borrow conflicts.
std::mem::swap(&mut count, &mut self.bound_clause_count);
self.insert_predicates(clauses.into_iter().map(|clause| {
let i = count;
count += 1;
AnnotatedTraitPred {
origin: BoundPredicateOrigin::Item(i),
self.insert_predicates(preds.into_iter().filter_map(|pred| {
pred.clause.as_trait_clause().map(|clause| ItemClause {
id: pred.id,
clause,
}
})
}));
std::mem::swap(&mut count, &mut self.bound_clause_count);
}

/// Override the param env; we use this when resolving `dyn` predicates to add more clauses to
Expand All @@ -291,7 +269,7 @@ impl<'tcx> PredicateSearcher<'tcx> {

/// Insert annotated predicates in the search context. Prefer inserting them all at once as
/// this will give priority to shorter resolution paths.
fn insert_predicates(&mut self, preds: impl IntoIterator<Item = AnnotatedTraitPred<'tcx>>) {
fn insert_predicates(&mut self, preds: impl IntoIterator<Item = ItemClause<'tcx>>) {
self.insert_candidates(preds.into_iter().map(|clause| Candidate {
path: vec![],
pred: clause.clause,
Expand Down Expand Up @@ -370,8 +348,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.options);
let item_bounds = item_bounds
.iter()
.map(|(clause, _span)| *clause)
.filter_map(|pred| pred.as_trait_clause())
.filter_map(|pred| pred.clause.as_trait_clause())
// Substitute the item generics
.map(|pred| EarlyBinder::bind(pred).instantiate(tcx, alias_ty.args))
.enumerate();
Expand Down Expand Up @@ -464,7 +441,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
},
Ok(ImplSource::Param(_)) => {
match self.resolve_local(erased_tref.upcast(self.tcx), warn)? {
Some(candidate) => candidate.into_impl_expr(tcx),
Some(candidate) => candidate.into_impl_expr(tcx, self.implicit_self_clause),
None => {
let msg = format!(
"Could not find a clause for `{tref:?}` in the item parameters"
Expand Down Expand Up @@ -552,7 +529,9 @@ impl<'tcx> PredicateSearcher<'tcx> {
// We've added `Destruct` impls on everything, we should be able to resolve
// it.
match self.resolve_local(erased_tref.upcast(self.tcx), warn)? {
Some(candidate) => Either::Right(candidate.into_impl_expr(tcx)),
Some(candidate) => Either::Right(
candidate.into_impl_expr(tcx, self.implicit_self_clause),
),
None => {
let msg = format!(
"Cannot find virtual `Destruct` clause: `{tref:?}`"
Expand Down Expand Up @@ -638,15 +617,14 @@ impl<'tcx> PredicateSearcher<'tcx> {
pub fn resolve_predicates(
&mut self,
generics: GenericArgsRef<'tcx>,
predicates: utils::Predicates<'tcx>,
predicates: utils::ItemPredicates<'tcx>,
// Call back into hax-related code to display a nice warning.
warn: &impl Fn(&str),
) -> Result<Vec<ImplExpr<'tcx>>, String> {
let tcx = self.tcx;
predicates
.iter()
.map(|(clause, _span)| *clause)
.filter_map(|clause| clause.as_trait_clause())
.filter_map(|pred| pred.clause.as_trait_clause())
.map(|trait_pred| trait_pred.map_bound(|p| p.trait_ref))
// Substitute the item generics
.map(|trait_ref| EarlyBinder::bind(trait_ref).instantiate(tcx, generics))
Expand Down
Loading
Loading