From 5ef01bbed86371eaeea8814a2d735470eea4b9de Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 08:55:09 +0200 Subject: [PATCH] Update hax --- charon/Cargo.lock | 6 +++--- .../translate/translate_crate_to_ullbc.rs | 5 ++--- .../charon-driver/translate/translate_ctx.rs | 14 ++++---------- .../charon-driver/translate/translate_traits.rs | 17 ++++++----------- .../charon-driver/translate/translate_types.rs | 9 ++++++--- .../ui/unsupported/advanced-const-generics.out | 14 ++++++++++---- 6 files changed, 31 insertions(+), 34 deletions(-) diff --git a/charon/Cargo.lock b/charon/Cargo.lock index cc7143cb..4e725d9e 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -506,7 +506,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#ce9ea56e1d785a465331e609cf99dcc56142dc7a" +source = "git+https://github.com/hacspec/hax?branch=main#e2734c854c286eed2405967c7940d934c1fcd72e" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -517,7 +517,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#ce9ea56e1d785a465331e609cf99dcc56142dc7a" +source = "git+https://github.com/hacspec/hax?branch=main#e2734c854c286eed2405967c7940d934c1fcd72e" dependencies = [ "bincode", "extension-traits", @@ -535,7 +535,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#ce9ea56e1d785a465331e609cf99dcc56142dc7a" +source = "git+https://github.com/hacspec/hax?branch=main#e2734c854c286eed2405967c7940d934c1fcd72e" dependencies = [ "bincode", "hax-adt-into", diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index 492305e6..d4c4e45a 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -129,12 +129,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { }; // If this is a trait implementation, register it - if let hax::ImplSubject::Trait(..) = impl_subject { + if let hax::ImplSubject::Trait { .. } = impl_subject { let _ = self.register_trait_impl_id(&None, def_id); } // Explore the items - for item in items { + for (item, _) in items { let def_id = (&item.def_id).into(); // Match on the impl item kind match &item.kind { @@ -410,7 +410,6 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC reverse_id_map: Default::default(), priority_queue: Default::default(), translate_stack: Default::default(), - cached_defs: Default::default(), cached_path_elems: Default::default(), cached_names: Default::default(), }; diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 89d8fe6e..c50360c9 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -186,8 +186,6 @@ pub struct TranslateCtx<'tcx, 'ctx> { /// Stack of the translations currently happening. Used to avoid cycles where items need to /// translate themselves transitively. pub translate_stack: Vec, - /// Cache the `hax::FullDef`s to compute them only once each. - pub cached_defs: HashMap>, /// Cache the `PathElem`s to compute them only once each. It's an `Option` because some /// `DefId`s (e.g. `extern {}` blocks) don't appear in the `Name`. pub cached_path_elems: HashMap>, @@ -364,7 +362,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { ImplElem::Ty(generics, ty) } // Trait implementation - hax::ImplSubject::Trait(..) => { + hax::ImplSubject::Trait { .. } => { let impl_id = self.register_trait_impl_id(&None, def_id); ImplElem::Trait(impl_id) } @@ -495,12 +493,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub fn hax_def(&mut self, def_id: impl Into) -> Arc { let def_id: DefId = def_id.into(); - // We return an `Arc` because keeping a borrow would prevent us from doing anything useful - // with `self`. - self.cached_defs - .entry(def_id) - .or_insert_with(|| Arc::new(def_id.sinto(&self.hax_state))) - .clone() + // Hax takes care of caching the translation. + def_id.sinto(&self.hax_state) } pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo { @@ -859,7 +853,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { { let def = self.hax_def(id); let hax::FullDefKind::Impl { - impl_subject: hax::ImplSubject::Trait(trait_pred), + impl_subject: hax::ImplSubject::Trait { trait_pred, .. }, .. } = def.kind() else { diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index 9efbad85..00e0db91 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -106,10 +106,9 @@ impl BodyTransCtx<'_, '_, '_> { }; let items: Vec<(TraitItemName, &hax::AssocItem, Arc)> = items .iter() - .map(|item| { + .map(|(item, def)| { let name = TraitItemName(item.name.clone()); - let def = self.t_ctx.hax_def(&item.def_id); - (name, item, def) + (name, item, def.clone()) }) .collect_vec(); @@ -233,7 +232,7 @@ impl BodyTransCtx<'_, '_, '_> { let generics = self.translate_def_generics(span, def)?; let hax::FullDefKind::Impl { - impl_subject: hax::ImplSubject::Trait(trait_pred), + impl_subject: hax::ImplSubject::Trait { trait_pred, .. }, items: impl_items, .. } = &def.kind @@ -307,7 +306,7 @@ impl BodyTransCtx<'_, '_, '_> { let mut types: HashMap = HashMap::new(); let mut methods = HashMap::new(); - for item in impl_items { + for (item, item_def) in impl_items { let name = TraitItemName(item.name.clone()); let item_span = self.def_span(&item.def_id); match &item.kind { @@ -325,17 +324,13 @@ impl BodyTransCtx<'_, '_, '_> { consts.insert(name, gref); } hax::AssocKind::Type => { - // Warning: don't call `hax_def` on associated functions because this triggers - // hax crashes on functions with higher-kinded predicates like - // `Iterator::scan`. - let item_def = self.t_ctx.hax_def(&item.def_id); let hax::FullDefKind::AssocTy { value: Some(ty), .. } = item_def.kind() else { unreachable!() }; - let ty = self.translate_ty(item_span, erase_regions, ty)?; + let ty = self.translate_ty(item_span, erase_regions, &ty)?; types.insert(name, ty); } } @@ -352,7 +347,7 @@ impl BodyTransCtx<'_, '_, '_> { let mut required_methods = Vec::new(); let mut provided_methods = Vec::new(); - for decl_item in decl_items { + for (decl_item, _) in decl_items { let item_def_id = (&decl_item.def_id).into(); let item_span = self.def_span(item_def_id); let name = TraitItemName(decl_item.name.to_string()); diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 6429b941..6d3afe30 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -664,7 +664,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Add the self trait clause. match &def.kind { FullDefKind::Impl { - impl_subject: hax::ImplSubject::Trait(self_predicate), + impl_subject: + hax::ImplSubject::Trait { + trait_pred: self_predicate, + .. + }, .. } | FullDefKind::Trait { self_predicate, .. } => { @@ -709,8 +713,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { 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); + for (item, item_def) in items { if let hax::FullDefKind::AssocTy { predicates, .. } = &item_def.kind { let name = TraitItemName(item.name.clone()); self.register_predicates( diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out index 11d2459b..1d24e5e4 100644 --- a/charon/tests/ui/unsupported/advanced-const-generics.out +++ b/charon/tests/ui/unsupported/advanced-const-generics.out @@ -1,4 +1,4 @@ -thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:784:42: +thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:787:42: called `Option::unwrap()` on a `None` value note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace error: Thread panicked when extracting item `test_crate::foo`. @@ -25,9 +25,15 @@ error[E9999]: Supposely unreachable place in the Rust AST. The label is "Transla N/#0, ], } - | - = note: ⚠️ This is a bug in Hax's frontend. - Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! + --> tests/ui/unsupported/advanced-const-generics.rs:18:1 + | +18 | / fn bar() +19 | | where +20 | | [(); N + 1]:, + | |_________________^ + | + = note: ⚠️ This is a bug in Hax's frontend. + Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! error: Thread panicked when extracting item `test_crate::bar`. --> tests/ui/unsupported/advanced-const-generics.rs:18:1