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..2094222e 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,13 +129,13 @@ 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 { - let def_id = (&item.def_id).into(); + for (item, item_def) in items { + let def_id = item_def.rust_def_id(); // Match on the impl item kind match &item.kind { hax::AssocKind::Const => { @@ -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..b9871464 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 { @@ -542,14 +536,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { name: Name, opacity: ItemOpacity, ) -> Result { - let def_id: DefId = (&def.def_id).into(); - // TODO: upstream to hax - let span = def_id - .as_local() - .map(|local_def_id| self.tcx.source_span(local_def_id)) - .unwrap_or(def.span.rust_span_data.unwrap().span()); - let source_text = self.tcx.sess.source_map().span_to_snippet(span.into()).ok(); - let span = self.translate_span_from_hax(&span.sinto(&self.hax_state)); + let def_id = def.rust_def_id(); + let span = def.source_span.as_ref().unwrap_or(&def.span); + let span = self.translate_span_from_hax(span); let attr_info = self.translate_attr_info(def); let is_local = def.def_id.is_local; @@ -565,7 +554,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { Ok(ItemMeta { name, span, - source_text, + source_text: def.source_text.clone(), attr_info, is_local, opacity, @@ -685,7 +674,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } pub(crate) fn def_span(&mut self, def_id: impl Into) -> Span { - let span = self.tcx.def_span(def_id.into()).sinto(&self.hax_state); + let span = &self.hax_def(def_id).span; self.translate_span_from_hax(&span) } @@ -859,7 +848,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_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index 63a6a3d2..3f9ca8a4 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -733,19 +733,17 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } /// Checks whether the given id corresponds to a built-in function. - fn recognize_builtin_fun(&mut self, def_id: &hax::DefId) -> Result, Error> { - use rustc_hir::lang_items::LangItem; - let tcx = self.t_ctx.tcx; - let rust_id = DefId::from(def_id); - let name = self.t_ctx.hax_def_id_to_name(def_id)?; - - let panic_lang_items = &[LangItem::Panic, LangItem::PanicFmt, LangItem::BeginPanic]; + fn recognize_builtin_fun(&mut self, def: &hax::FullDef) -> Result, Error> { + let name = self.t_ctx.hax_def_id_to_name(&def.def_id)?; + let panic_lang_items = &["panic", "panic_fmt", "begin_panic"]; let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME]; - if tcx.is_diagnostic_item(rustc_span::sym::box_new, rust_id) { + + if def.diagnostic_item.as_deref() == Some("box_new") { Ok(Some(BuiltinFun::BoxNew)) - } else if panic_lang_items - .iter() - .any(|i| tcx.is_lang_item(rust_id, *i)) + } else if def + .lang_item + .as_deref() + .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it)) || panic_names.iter().any(|panic| name.equals_ref_name(panic)) { Ok(Some(BuiltinFun::Panic)) @@ -775,7 +773,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { trait_refs: &Vec, trait_info: &Option, ) -> Result { - let builtin_fun = self.recognize_builtin_fun(def_id)?; + let fun_def = self.t_ctx.hax_def(def_id); + let builtin_fun = self.recognize_builtin_fun(&fun_def)?; if matches!(builtin_fun, Some(BuiltinFun::Panic)) { let name = self.t_ctx.hax_def_id_to_name(def_id)?; return Ok(SubstFunIdOrPanic::Panic(name)); @@ -1226,12 +1225,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } /// Gather all the lines that start with `//` inside the given span. - fn translate_body_comments(&mut self, charon_span: Span) -> Vec<(usize, Vec)> { - let rust_span = charon_span.rust_span(); - let source_map = self.t_ctx.tcx.sess.source_map(); - if rust_span.ctxt().is_root() - && let Ok(body_text) = source_map.span_to_snippet(rust_span.into()) - { + fn translate_body_comments( + &mut self, + def: &hax::FullDef, + charon_span: Span, + ) -> Vec<(usize, Vec)> { + if let Some(body_text) = &def.source_text { let mut comments = body_text .lines() // Iter through the lines of this body in reverse order. @@ -1271,14 +1270,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// declared opaque, and only translate non-local bodies if `extract_opaque_bodies` is set). fn translate_body( &mut self, - rust_id: DefId, + def: &hax::FullDef, arg_count: usize, item_meta: &ItemMeta, ) -> Result, Error> { // Stopgap measure because there are still many panics in charon and hax. let mut this = panic::AssertUnwindSafe(&mut *self); - let res = - panic::catch_unwind(move || this.translate_body_aux(rust_id, arg_count, item_meta)); + let res = panic::catch_unwind(move || this.translate_body_aux(def, arg_count, item_meta)); match res { Ok(Ok(body)) => Ok(body), // Translation error @@ -1295,7 +1293,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { fn translate_body_aux( &mut self, - rust_id: DefId, + def: &hax::FullDef, arg_count: usize, item_meta: &ItemMeta, ) -> Result, Error> { @@ -1305,6 +1303,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } // Retrieve the body + let rust_id = def.rust_def_id(); let Some(body) = get_mir_for_def_id_and_level(self.t_ctx.tcx, rust_id, self.t_ctx.options.mir_level) else { @@ -1346,7 +1345,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { span, arg_count, locals: mem::take(&mut self.vars), - comments: self.translate_body_comments(span), + comments: self.translate_body_comments(def, span), body: blocks, }))) } @@ -1481,7 +1480,7 @@ impl BodyTransCtx<'_, '_, '_> { let body_id = if !is_trait_method_decl_without_default { // Translate the body. This doesn't store anything if we can't/decide not to translate // this body. - match self.translate_body(rust_id, signature.inputs.len(), &item_meta) { + match self.translate_body(def, signature.inputs.len(), &item_meta) { Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)), // Opaque declaration Ok(Err(Opaque)) => Err(Opaque), @@ -1538,7 +1537,7 @@ impl BodyTransCtx<'_, '_, '_> { // Translate its body like the body of a function. This returns `Opaque if we can't/decide // not to translate this body. - let body_id = match self.translate_body(rust_id, 0, &item_meta) { + let body_id = match self.translate_body(def, 0, &item_meta) { Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)), // Opaque declaration Ok(Err(Opaque)) => Err(Opaque), diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index 9efbad85..1c6f4342 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,9 +347,9 @@ impl BodyTransCtx<'_, '_, '_> { let mut required_methods = Vec::new(); let mut provided_methods = Vec::new(); - for decl_item in decl_items { - let item_def_id = (&decl_item.def_id).into(); - let item_span = self.def_span(item_def_id); + for (decl_item, decl_item_def) in decl_items { + let item_def_id = decl_item_def.rust_def_id(); + let item_span = self.translate_span_from_hax(&decl_item_def.span); let name = TraitItemName(decl_item.name.to_string()); match &decl_item.kind { hax::AssocKind::Fn => { diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 6429b941..95539cd8 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -9,7 +9,6 @@ use charon_lib::pretty::FmtWithCtx; use core::convert::*; use hax::Visibility; use hax_frontend_exporter as hax; -use rustc_hir::def_id::DefId; /// Small helper: we ignore some region names (when they are equal to "'_") fn check_region_name(s: Option) -> Option { @@ -420,10 +419,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Checks whether the given id corresponds to a built-in type. fn recognize_builtin_type(&mut self, def_id: &hax::DefId) -> Result, Error> { - use rustc_hir::lang_items::LangItem; - let tcx = self.t_ctx.tcx; - let rust_id = DefId::from(def_id); - let ty = if tcx.is_lang_item(rust_id, LangItem::OwnedBox) { + let def = self.t_ctx.hax_def(def_id); + let ty = if def.lang_item.as_deref() == Some("owned_box") { Some(BuiltinTy::Box) } else { None @@ -664,7 +661,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 +710,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..f56b3f0c 100644 --- a/charon/tests/ui/unsupported/advanced-const-generics.out +++ b/charon/tests/ui/unsupported/advanced-const-generics.out @@ -1,18 +1,3 @@ -thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:784: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`. - --> tests/ui/unsupported/advanced-const-generics.rs:14:1 - | -14 | fn foo() -> Foo { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -error: Ignoring the following item due to an error: test_crate::foo - --> tests/ui/unsupported/advanced-const-generics.rs:14:1 - | -14 | fn foo() -> Foo { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - disabled backtrace error[E9999]: Supposely unreachable place in the Rust AST. The label is "TranslateUneval". This error report happend because some assumption about the Rust AST was broken. @@ -25,26 +10,31 @@ 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)! - -error: Thread panicked when extracting item `test_crate::bar`. --> 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: Ignoring the following item due to an error: test_crate::bar - --> tests/ui/unsupported/advanced-const-generics.rs:18:1 +thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:784: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`. + --> tests/ui/unsupported/advanced-const-generics.rs:14:1 | -18 | / fn bar() -19 | | where -20 | | [(); N + 1]:, - | |_________________^ +14 | fn foo() -> Foo { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: Ignoring the following item due to an error: test_crate::foo + --> tests/ui/unsupported/advanced-const-generics.rs:14:1 + | +14 | fn foo() -> Foo { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -error: aborting due to 5 previous errors +error: aborting due to 3 previous errors Error: Charon driver exited with code 101