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 1961502b2..49c74e448 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 @@ -391,6 +391,7 @@ pub fn translate<'tcx, 'ctx>( translate_stack: Default::default(), cached_defs: Default::default(), cached_path_elems: Default::default(), + cached_names: Default::default(), }; // First push all the items in the stack of items to translate. diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 8ecc705b7..768e3a711 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -101,6 +101,8 @@ pub struct TranslateCtx<'tcx, 'ctx> { /// 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>, + /// Cache the names to compute them only once each. + pub cached_names: HashMap, } /// A translation context for type/global/function bodies. @@ -342,6 +344,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Retrieve an item name from a [DefId]. pub fn def_id_to_name(&mut self, def_id: DefId) -> Result { + if let Some(name) = self.cached_names.get(&def_id) { + return Ok(name.clone()); + } trace!("{:?}", def_id); let tcx = self.tcx; let span = tcx.def_span(def_id); @@ -411,9 +416,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { name.push(PathElem::Ident(crate_name, Disambiguator::new(0))); name.reverse(); + let name = Name { name }; trace!("{:?}", name); - Ok(Name { name }) + self.cached_names.insert(def_id, name.clone()); + Ok(name) } pub fn hax_def_id_to_name(&mut self, def_id: &hax::DefId) -> Result {