Skip to content
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.

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

Cache Name computation #310

Merged
merged 1 commit into from
Aug 14, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
9 changes: 8 additions & 1 deletion charon/src/bin/charon-driver/translate/translate_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<DefId, Option<PathElem>>,
/// Cache the names to compute them only once each.
pub cached_names: HashMap<DefId, Name>,
}

/// A translation context for type/global/function bodies.
Expand Down Expand Up @@ -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<Name, Error> {
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);
Expand Down Expand Up @@ -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<Name, Error> {
Expand Down