Update hax

AeneasVerif · Oct 15, 2024 · 5ef01bb · 5ef01bb
1 parent 355ce1b
commit 5ef01bb
Show file tree

Hide file tree

Showing 6 changed files with 31 additions and 34 deletions.
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
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
@@ -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
@@ -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<AnyTransId>,
-    /// Cache the `hax::FullDef`s to compute them only once each.
-    pub cached_defs: HashMap<DefId, Arc<hax::FullDef>>,
     /// 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<DefId, Option<PathElem>>,
@@ -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<DefId>) -> Arc<hax::FullDef> {
         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
@@ -106,10 +106,9 @@ impl BodyTransCtx<'_, '_, '_> {
         };
         let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = 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<TraitItemName, Ty> = 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
@@ -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
@@ -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<const N: usize>()
+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