Skip to content

Commit

Permalink
Merge pull request #398 from Nadrieril/translate-generics
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Oct 2, 2024
2 parents c139608 + e3795a9 commit 5b8851f
Show file tree
Hide file tree
Showing 10 changed files with 730 additions and 246 deletions.
52 changes: 2 additions & 50 deletions charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,36 +94,7 @@ impl TranslateOptions {
opacities.push((pat.to_string(), Invisible));
}

// Hide some methods that have signatures we don't handle yet.
// TODO: handle these signatures.
let tricky_iterator_methods = &[
"filter",
"find",
"inspect",
"is_sorted_by",
"map_windows",
"max_by",
"max_by_key",
"min_by",
"min_by_key",
"partition",
"partition_in_place",
"rposition",
"scan",
"skip_while",
"take_while",
"try_find",
];
for method in tricky_iterator_methods {
opacities.push((
format!("core::iter::traits::iterator::Iterator::{method}"),
Invisible,
));
}
opacities.push((
format!("core::iter::traits::double_ended::DoubleEndedIterator::rfind"),
Invisible,
));
// We always hide this trait.
opacities.push((format!("core::alloc::Allocator"), Invisible));
opacities.push((
format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
Expand Down Expand Up @@ -378,10 +349,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
// substs and bounds. In order to properly do so, we introduce
// a body translation context.
let mut bt_ctx = BodyTransCtx::new(def_id, self);

bt_ctx.push_generics_for_def(span, &def)?;
let generics = bt_ctx.get_generics();

let generics = bt_ctx.translate_def_generics(span, &def)?;
let ty = bt_ctx.translate_ty(span, erase_regions, &ty)?;
ImplElem::Ty(generics, ty)
}
Expand Down Expand Up @@ -1122,22 +1090,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
self.blocks.insert(id, block);
}

pub(crate) fn get_generics(&mut self) -> GenericParams {
// Sanity checks
self.check_generics();
assert!(self.region_vars.len() == 1);
let mut generic_params = self.generic_params.clone();
assert!(generic_params.regions.is_empty());
generic_params.regions = self.region_vars[0].clone();
assert!(generic_params
.trait_clauses
.iter()
.enumerate()
.all(|(i, c)| c.clause_id.index() == i));
trace!("Translated generics: {generic_params:?}");
generic_params
}

pub(crate) fn make_dep_source(&self, span: rustc_span::Span) -> Option<DepSource> {
DepSource::make(self.def_id, span)
}
Expand Down
24 changes: 3 additions & 21 deletions charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1387,32 +1387,15 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let erase_regions = false;
let span = item_meta.span.rust_span();

let generics = self.translate_def_generics(span, def)?;

let signature = match &def.kind {
hax::FullDefKind::Closure { args, .. } => &args.sig,
hax::FullDefKind::Fn { sig, .. } => sig,
hax::FullDefKind::AssocFn { sig, .. } => sig,
_ => panic!("Unexpected definition for function: {def:?}"),
};

// The parameters (and in particular the lifetimes) are split between
// early bound and late bound parameters. See those blog posts for explanations:
// https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
// https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
// Note that only lifetimes can be late bound.
//
// [TyCtxt.generics_of] gives us the early-bound parameters
// The late-bounds parameters are bound in the [Binder] returned by
// [TyCtxt.type_of].

// Add the early bound parameters and predicates.
self.push_generics_for_def(span, &def)?;

// Add the *late-bound* parameters (bound in the signature, can only be lifetimes).
let binder = signature.rebind(());
self.set_first_bound_regions_group(span, binder)?;

let generics = self.get_generics();

// Translate the signature
trace!("signature of {def_id:?}:\n{:?}", signature.value);
let inputs: Vec<Ty> = signature
Expand Down Expand Up @@ -1574,8 +1557,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
// const LEN : usize = N;
// }
// ```
bt_ctx.push_generics_for_def(span, def)?;
let generics = bt_ctx.get_generics();
let generics = bt_ctx.translate_def_generics(span, def)?;

trace!("Translating global type");
let ty = match &def.kind {
Expand Down
92 changes: 21 additions & 71 deletions charon/src/bin/charon-driver/translate/translate_traits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
item_meta: ItemMeta,
def: &hax::FullDef,
) -> Result<TraitDecl, Error> {
use hax::AssocKind;
trace!("About to translate trait decl:\n{:?}", rust_id);
trace!("Trait decl id:\n{:?}", def_id);

Expand All @@ -106,95 +105,47 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let hax::FullDefKind::Trait { items, .. } = &def.kind else {
error_or_panic!(self, span, &format!("Unexpected definition: {def:?}"));
};
let items: Vec<(TraitItemName, &hax::AssocItem, Option<Arc<hax::FullDef>>)> = items
let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
.iter()
.map(|item| {
let name = TraitItemName(item.name.clone());
// Warning: don't call `hax_def` on associated functions because this triggers
// hax crashes on functions with higher-kinded predicates like
// `Iterator::scan`.
let def = if matches!(item.kind, AssocKind::Type | AssocKind::Const) {
let def = bt_ctx.t_ctx.hax_def(&item.def_id);
Some(def)
} else {
None
};
let def = bt_ctx.t_ctx.hax_def(&item.def_id);
(name, item, def)
})
.collect_vec();

// Translate the generics
bt_ctx.push_generics_for_def(span, def)?;

// Gather the associated type clauses
let mut type_clauses = Vec::new();
for (name, item, def) in &items {
match &item.kind {
AssocKind::Type => {
let hax::FullDefKind::AssocTy { predicates, .. } =
&def.as_deref().unwrap().kind
else {
unreachable!()
};
// TODO: handle generics (i.e. GATs).
// Register the trait clauses as item trait clauses
bt_ctx.register_predicates(
&predicates,
PredicateOrigin::TraitItem(name.clone()),
&PredicateLocation::Item(name.clone()),
)?;
if let Some(clauses) = bt_ctx.item_trait_clauses.get(name) {
type_clauses.push((name.clone(), clauses.clone()));
}
}
AssocKind::Fn => {}
AssocKind::Const => {}
}
}

// Note that in the generics returned by [get_generics], the trait refs only contain the
// local trait clauses. The parent clauses are stored in `bt_ctx.parent_trait_clauses`.
// Note that in the generics returned by [translate_def_generics], the trait refs only
// contain the local trait clauses. The parent clauses are stored in
// `bt_ctx.parent_trait_clauses`.
// TODO: Distinguish between required and implied trait clauses?
let generics = bt_ctx.get_generics();
let generics = bt_ctx.translate_def_generics(span, def)?;

// Translate the associated items
// We do something subtle here: TODO: explain
let mut consts = Vec::new();
let mut const_defaults = HashMap::new();
let mut types = Vec::new();
let mut type_clauses = Vec::new();
let mut type_defaults = HashMap::new();
let mut required_methods = Vec::new();
let mut provided_methods = Vec::new();
for (item_name, hax_item, opt_hax_def) in &items {
for (item_name, hax_item, hax_def) in &items {
let rust_item_id = DefId::from(&hax_item.def_id);
let item_span = bt_ctx.t_ctx.tcx.def_span(rust_item_id);
match &hax_item.kind {
AssocKind::Fn => {
match &hax_def.kind {
hax::FullDefKind::AssocFn { .. } => {
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
if hax_item.has_value {
// This is a *provided* method,
// Hack: To avoid having a trait that lists methods that aren't translated,
// we filter out invisible methods early. FIXME: remove this once we can
// translate all `Iterator` method signatures.
let fun_name = bt_ctx.t_ctx.def_id_to_name(rust_item_id)?;
if !bt_ctx.t_ctx.opacity_for_name(&fun_name).is_invisible() {
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
provided_methods.push((item_name.clone(), fun_id));
}
// This is a provided method,
provided_methods.push((item_name.clone(), fun_id));
} else {
// This is a required method (no default implementation)
let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id);
required_methods.push((item_name.clone(), fun_id));
}
}
AssocKind::Const => {
hax::FullDefKind::AssocConst { ty, .. } => {
// Check if the constant has a value (i.e., a body).
// We are handling a trait *declaration* so we need to
// check whether the constant has a default value.
let hax::FullDefKind::AssocConst { ty, .. } =
&opt_hax_def.as_deref().unwrap().kind
else {
unreachable!()
};
if hax_item.has_value {
// The parameters of the constant are the same as those of the item that
// declares them.
Expand All @@ -207,18 +158,18 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let ty = bt_ctx.translate_ty(item_span, erase_regions, ty)?;
consts.push((item_name.clone(), ty));
}
AssocKind::Type => {
let hax::FullDefKind::AssocTy { value, .. } =
&opt_hax_def.as_deref().unwrap().kind
else {
unreachable!()
};
hax::FullDefKind::AssocTy { value, .. } => {
// TODO: handle generics (i.e. GATs).
if let Some(clauses) = bt_ctx.item_trait_clauses.get(item_name) {
type_clauses.push((item_name.clone(), clauses.clone()));
}
if let Some(ty) = value {
let ty = bt_ctx.translate_ty(item_span, erase_regions, &ty)?;
type_defaults.insert(item_name.clone(), ty);
};
types.push(item_name.clone());
}
_ => panic!("Unexpected definition for trait item: {hax_def:?}"),
}
}

Expand Down Expand Up @@ -281,8 +232,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let erase_regions = false;
let mut bt_ctx = BodyTransCtx::new(rust_id, self);

bt_ctx.push_generics_for_def(span, def)?;
let generics = bt_ctx.get_generics();
let generics = bt_ctx.translate_def_generics(span, def)?;

let hax::FullDefKind::Impl {
impl_subject: hax::ImplSubject::Trait(trait_pred),
Expand Down
74 changes: 70 additions & 4 deletions charon/src/bin/charon-driver/translate/translate_types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -615,11 +615,38 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}
}

/// Translate the generics and predicates of this item and its parents.
pub(crate) fn translate_def_generics(
&mut self,
span: rustc_span::Span,
def: &hax::FullDef,
) -> Result<GenericParams, Error> {
self.push_generics_for_def(span, def, false)?;
let mut generic_params = self.generic_params.clone();

// Sanity checks
self.check_generics();
assert!(generic_params
.trait_clauses
.iter()
.enumerate()
.all(|(i, c)| c.clause_id.index() == i));

// The regons were tracked separately, we add them back here.
assert!(generic_params.regions.is_empty());
assert!(self.region_vars.len() == 1);
generic_params.regions = self.region_vars[0].clone();

trace!("Translated generics: {generic_params:?}");
Ok(generic_params)
}

/// Add the generics and predicates of this item and its parents to the current context.
pub(crate) fn push_generics_for_def(
fn push_generics_for_def(
&mut self,
span: rustc_span::Span,
def: &hax::FullDef,
is_parent: bool,
) -> Result<(), Error> {
use hax::FullDefKind;
// Add generics from the parent item, recursively (recursivity is useful for closures, as
Expand All @@ -630,7 +657,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
| FullDefKind::AssocConst { parent, .. }
| FullDefKind::Closure { parent, .. } => {
let parent_def = self.t_ctx.hax_def(parent);
self.push_generics_for_def(span, &parent_def)?;
self.push_generics_for_def(span, &parent_def, true)?;
}
_ => {}
}
Expand Down Expand Up @@ -681,7 +708,47 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
_ => panic!("Unexpected def: {def:?}"),
};
self.register_predicates(predicates, origin, &location)?;

// Also add the predicates on associated types.
if let hax::FullDefKind::Trait { items, .. } = &def.kind
&& !is_parent
{
for item in items {
let item_def = self.t_ctx.hax_def(&item.def_id);
if let hax::FullDefKind::AssocTy { predicates, .. } = &item_def.kind {
let name = TraitItemName(item.name.clone());
self.register_predicates(
&predicates,
PredicateOrigin::TraitItem(name.clone()),
&PredicateLocation::Item(name),
)?;
}
}
}
}

// The parameters (and in particular the lifetimes) are split between
// early bound and late bound parameters. See those blog posts for explanations:
// https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
// https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
// Note that only lifetimes can be late bound.
//
// [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
// parameters here.
let signature = match &def.kind {
hax::FullDefKind::Closure { args, .. } => Some(&args.sig),
hax::FullDefKind::Fn { sig, .. } => Some(sig),
hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
_ => None,
};
// We don't want the late-bound parameters of the parent, only early-bound ones.
if let Some(signature) = signature
&& !is_parent
{
let binder = signature.rebind(());
self.set_first_bound_regions_group(span, binder)?;
}

Ok(())
}

Expand Down Expand Up @@ -747,8 +814,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let span = item_meta.span.rust_span();

// Translate generics and predicates
bt_ctx.push_generics_for_def(span, def)?;
let generics = bt_ctx.get_generics();
let generics = bt_ctx.translate_def_generics(span, def)?;

// Translate type body
let kind = match &def.kind {
Expand Down
Loading

0 comments on commit 5b8851f

Please sign in to comment.