From 6cf96c5903f3dafea83f3569fcb3c6403e74e8b1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Oct 2024 15:55:23 +0200 Subject: [PATCH 1/9] Use our own `Span` throughout translation --- .../translate/translate_constants.rs | 6 +- .../translate/translate_crate_to_ullbc.rs | 4 +- .../charon-driver/translate/translate_ctx.rs | 51 +++++------ .../translate/translate_functions_to_ullbc.rs | 86 +++++++------------ .../translate/translate_predicates.rs | 24 +++--- .../translate/translate_traits.rs | 17 ++-- .../translate/translate_types.rs | 33 ++++--- charon/src/errors.rs | 10 ++- charon/src/transform/reconstruct_boxes.rs | 6 +- .../src/transform/remove_read_discriminant.rs | 8 +- .../ui/issue-369-mismatched-genericparams.out | 2 +- charon/tests/ui/issue-393-shallowinitbox.out | 2 +- .../unsupported/advanced-const-generics.out | 2 +- 13 files changed, 108 insertions(+), 143 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs index 9bd3bedf1..a0aac3c35 100644 --- a/charon/src/bin/charon-driver/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -75,7 +75,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// update hax. pub(crate) fn translate_constant_expr_to_constant_expr( &mut self, - span: rustc_span::Span, + span: Span, v: &hax::ConstantExpr, ) -> Result { use hax::ConstantExprKind; @@ -202,7 +202,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// the default span (i.e., it is useless), hence the additional span argument. pub(crate) fn translate_constant_expr_to_const_generic( &mut self, - span: rustc_span::Span, + span: Span, v: &hax::ConstantExpr, ) -> Result { // Remark: we can't user globals as constant generics (meaning @@ -237,7 +237,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// the default span (i.e., it is useless), hence the additional span argument. pub(crate) fn translate_constant_to_constant_expr( &mut self, - span: rustc_span::Span, + span: Span, v: &hax::Constant, ) -> Result { self.translate_constant_expr_to_constant_expr(span, &v.const_.constant_kind) 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 68b5467ba..6d66a31ff 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 @@ -257,7 +257,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { return; } self.with_def_id(rust_id, |mut ctx| { - let span = ctx.tcx.def_span(rust_id); + let span = ctx.def_span(rust_id); // Catch cycles let res = if ctx.translate_stack.contains(&trans_id) { ctx.span_err( @@ -354,7 +354,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { self.translate_item(rust_id, id); if self.errors.ignored_failed_decls.contains(&rust_id) { - let span = self.tcx.def_span(rust_id); + let span = self.def_span(rust_id); error_or_panic!(self, span, format!("Failed to translate item {id:?}.")) } Ok(self.translated.get_item(id).unwrap()) diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 56830a0ee..3137767b5 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -298,7 +298,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub fn def_id_to_path_elem( &mut self, - span: rustc_span::Span, + span: Span, def_id: DefId, ) -> Result, Error> { if let Some(path_elem) = self.cached_path_elems.get(&def_id) { @@ -404,7 +404,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } trace!("{:?}", def_id); let tcx = self.tcx; - let span = tcx.def_span(def_id); + let span = &tcx.def_span(def_id); + let span = self.translate_span_from_hax(span.sinto(&self.hax_state)); // We have to be a bit careful when retrieving names from def ids. For instance, // due to reexports, [`TyCtxt::def_path_str`](TyCtxt::def_path_str) might give @@ -507,8 +508,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned(); let rename = renames.next(); if renames.next().is_some() { + let span = self.translate_span_from_hax(def.span.clone()); self.span_err( - def.span.rust_span_data.unwrap().span(), + span, "There should be at most one `charon::rename(\"...\")` \ or `aeneas::rename(\"...\")` attribute per declaration", ); @@ -670,6 +672,11 @@ 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); + self.translate_span_from_hax(span) + } + /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc /// encodes them as attributes). For now we use `String`s for `Attributes`. pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option { @@ -692,10 +699,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { match Attribute::parse_from_raw(raw_attr) { Ok(a) => Some(a), Err(msg) => { - self.span_err( - attr.span.rust_span_data.unwrap().span(), - &format!("Error parsing attribute: {msg}"), - ); + let span = self.translate_span_from_hax(attr.span.clone()); + self.span_err(span, &format!("Error parsing attribute: {msg}")); None } } @@ -896,7 +901,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.t_ctx.continue_on_failure() } - pub fn span_err(&mut self, span: rustc_span::Span, msg: &str) { + pub fn span_err(&mut self, span: Span, msg: &str) { self.t_ctx.span_err(span, msg) } @@ -904,6 +909,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.t_ctx.translate_span_from_hax(rspan) } + pub(crate) fn def_span(&mut self, def_id: impl Into) -> Span { + self.t_ctx.def_span(def_id) + } + pub(crate) fn get_local(&self, local: &hax::Local) -> Option { use rustc_index::Idx; self.vars_map.get(&local.index()).copied() @@ -914,27 +923,19 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.blocks_map.get(&rid) } - pub(crate) fn register_type_decl_id( - &mut self, - span: rustc_span::Span, - id: impl Into, - ) -> TypeDeclId { + pub(crate) fn register_type_decl_id(&mut self, span: Span, id: impl Into) -> TypeDeclId { let src = self.make_dep_source(span); self.t_ctx.register_type_decl_id(&src, id.into()) } - pub(crate) fn register_fun_decl_id( - &mut self, - span: rustc_span::Span, - id: impl Into, - ) -> FunDeclId { + pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: impl Into) -> FunDeclId { let src = self.make_dep_source(span); self.t_ctx.register_fun_decl_id(&src, id.into()) } pub(crate) fn register_global_decl_id( &mut self, - span: rustc_span::Span, + span: Span, id: impl Into, ) -> GlobalDeclId { let src = self.make_dep_source(span); @@ -945,7 +946,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// like [core::marker::Sized] or [core::marker::Sync]. pub(crate) fn register_trait_decl_id( &mut self, - span: rustc_span::Span, + span: Span, id: impl Into, ) -> TraitDeclId { let src = self.make_dep_source(span); @@ -956,7 +957,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// like [core::marker::Sized] or [core::marker::Sync]. pub(crate) fn register_trait_impl_id( &mut self, - span: rustc_span::Span, + span: Span, id: impl Into, ) -> TraitImplId { let src = self.make_dep_source(span); @@ -979,7 +980,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Translate a binder of regions by appending the stored reguions to the given vector. pub(crate) fn translate_region_binder( &mut self, - span: rustc_span::Span, + span: Span, binder: hax::Binder<()>, region_vars: &mut Vector, ) -> Result, Error> { @@ -1010,7 +1011,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Set the first bound regions group pub(crate) fn set_first_bound_regions_group( &mut self, - span: rustc_span::Span, + span: Span, binder: hax::Binder<()>, ) -> Result<(), Error> { assert!(self.bound_region_vars.is_empty()); @@ -1031,7 +1032,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// it contains universally quantified regions). pub(crate) fn with_locally_bound_regions_group( &mut self, - span: rustc_span::Span, + span: Span, binder: hax::Binder<()>, f: F, ) -> Result @@ -1090,7 +1091,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.blocks.insert(id, block); } - pub(crate) fn make_dep_source(&self, span: rustc_span::Span) -> Option { + pub(crate) fn make_dep_source(&self, span: Span) -> Option { DepSource::make(self.def_id, span) } } 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 1dc2104f0..18fd5036a 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 @@ -64,11 +64,7 @@ fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp { } impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { - fn translate_binaryop_kind( - &mut self, - span: rustc_span::Span, - binop: hax::BinOp, - ) -> Result { + fn translate_binaryop_kind(&mut self, span: Span, binop: hax::BinOp) -> Result { Ok(match binop { hax::BinOp::BitXor => BinOp::BitXor, hax::BinOp::BitAnd => BinOp::BitAnd, @@ -184,7 +180,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Translate the type let erase_regions = true; - let span = var.source_info.span.rust_span_data.unwrap().span(); + let span = self.translate_span_from_hax(var.source_info.span.clone()); let ty = self.translate_ty(span, erase_regions, &var.ty)?; // Add the variable to the environment @@ -268,7 +264,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Translate a place and return its type fn translate_place_with_type( &mut self, - span: rustc_span::Span, + span: Span, place: &hax::Place, ) -> Result<(Place, Ty), Error> { let erase_regions = true; @@ -278,11 +274,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } /// Translate a place - fn translate_place( - &mut self, - span: rustc_span::Span, - place: &hax::Place, - ) -> Result { + fn translate_place(&mut self, span: Span, place: &hax::Place) -> Result { Ok(self.translate_place_with_type(span, place)?.0) } @@ -291,7 +283,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// update our representation of places to match the Hax representation. fn translate_projection( &mut self, - span: rustc_span::Span, + span: Span, place: &hax::Place, ) -> Result<(VarId, Projection), Error> { let erase_regions = true; @@ -432,7 +424,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Translate an operand with its type fn translate_operand_with_type( &mut self, - span: rustc_span::Span, + span: Span, operand: &hax::Operand, ) -> Result<(Operand, Ty), Error> { trace!(); @@ -454,21 +446,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } /// Translate an operand - fn translate_operand( - &mut self, - span: rustc_span::Span, - operand: &hax::Operand, - ) -> Result { + fn translate_operand(&mut self, span: Span, operand: &hax::Operand) -> Result { trace!(); Ok(self.translate_operand_with_type(span, operand)?.0) } /// Translate an rvalue - fn translate_rvalue( - &mut self, - span: rustc_span::Span, - rvalue: &hax::Rvalue, - ) -> Result { + fn translate_rvalue(&mut self, span: Span, rvalue: &hax::Rvalue) -> Result { let erase_regions = true; match rvalue { hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)), @@ -783,7 +767,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { #[allow(clippy::too_many_arguments)] pub(crate) fn translate_fun_decl_id_with_args( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, def_id: &hax::DefId, substs: &Vec, @@ -898,7 +882,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { statement: &hax::Statement, ) -> Result, Error> { trace!("About to translate statement (MIR) {:?}", statement); - let span = statement.source_info.span.rust_span_data.unwrap().span(); + let span = self + .t_ctx + .translate_span_from_source_info(&body.source_scopes, &statement.source_info); use hax::StatementKind; let t_statement: Option = match &*statement.kind { @@ -963,16 +949,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { }; // Add the span information - match t_statement { - None => Ok(None), - Some(t_statement) => { - let span = self - .t_ctx - .translate_span_from_source_info(&body.source_scopes, &statement.source_info); - - Ok(Some(Statement::new(span, t_statement))) - } - } + Ok(t_statement.map(|kind| Statement::new(span, kind))) } /// Translate a terminator @@ -983,8 +960,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { statements: &mut Vec, ) -> Result { trace!("About to translate terminator (MIR) {:?}", terminator); - let rustc_span = terminator.source_info.span.rust_span_data.unwrap().span(); - // Compute the span information beforehand (we might need it to introduce // intermediate statements - we desugar some terminators) let span = self @@ -1000,7 +975,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } TerminatorKind::SwitchInt { discr, targets } => { // Translate the operand which gives the discriminant - let (discr, discr_ty) = self.translate_operand_with_type(rustc_span, discr)?; + let (discr, discr_ty) = self.translate_operand_with_type(span, discr)?; // Translate the switch targets let targets = self.translate_switch_targets(&discr_ty, targets)?; @@ -1010,10 +985,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { TerminatorKind::UnwindResume => { // This is used to correctly unwind. We shouldn't get there: if // we panic, the state gets stuck. - error_or_panic!(self, rustc_span, "Unexpected terminator: UnwindResume"); + error_or_panic!(self, span, "Unexpected terminator: UnwindResume"); } TerminatorKind::UnwindTerminate { .. } => { - error_or_panic!(self, rustc_span, "Unexpected terminator: UnwindTerminate") + error_or_panic!(self, span, "Unexpected terminator: UnwindTerminate") } TerminatorKind::Return => RawTerminator::Return, // A MIR `Unreachable` terminator indicates undefined behavior of the rust abstract @@ -1025,7 +1000,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { unwind: _, // We consider that panic is an error, and don't model unwinding replace: _, } => { - let place = self.translate_place(rustc_span, place)?; + let place = self.translate_place(span, place)?; statements.push(Statement { span, content: RawStatement::Drop(place), @@ -1047,7 +1022,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } => self.translate_function_call( statements, span, - rustc_span, fun, generics, args, @@ -1064,7 +1038,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { unwind: _, // We model unwinding as an effet, we don't represent it in control flow } => { let assert = Assert { - cond: self.translate_operand(rustc_span, cond)?, + cond: self.translate_operand(span, cond)?, expected: *expected, }; statements.push(Statement { @@ -1102,14 +1076,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { RawTerminator::Goto { target } } TerminatorKind::InlineAsm { .. } => { - error_or_panic!(self, rustc_span, "Inline assembly is not supported"); + error_or_panic!(self, span, "Inline assembly is not supported"); } TerminatorKind::CoroutineDrop | TerminatorKind::TailCall { .. } | TerminatorKind::Yield { .. } => { error_or_panic!( self, - rustc_span, + span, format!("Unsupported terminator: {:?}", terminator.kind) ); } @@ -1156,8 +1130,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { fn translate_function_call( &mut self, statements: &mut Vec, - terminator_span: Span, - span: rustc_span::Span, + span: Span, fun: &hax::FunOperand, generics: &Vec, args: &Vec>, @@ -1227,7 +1200,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { dest: lval, }; statements.push(Statement { - span: terminator_span, + span, content: RawStatement::Call(call), }); Ok(match next_block { @@ -1240,7 +1213,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// values. fn translate_arguments( &mut self, - span: rustc_span::Span, + span: Span, args: &Vec>, ) -> Result, Error> { let mut t_args: Vec = Vec::new(); @@ -1311,8 +1284,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Translation error Ok(Err(e)) => Err(e), Err(_) => { - let span = item_meta.span.rust_span(); - error_or_panic!(self, span, "Thread panicked when extracting body."); + error_or_panic!( + self, + item_meta.span, + "Thread panicked when extracting body." + ); } } } @@ -1385,7 +1361,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { def: &hax::FullDef, ) -> Result { let erase_regions = false; - let span = item_meta.span.rust_span(); + let span = item_meta.span; let generics = self.translate_def_generics(span, def)?; @@ -1486,7 +1462,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { def: &hax::FullDef, ) -> Result { trace!("About to translate function:\n{:?}", rust_id); - let def_span = item_meta.span.rust_span(); + let def_span = item_meta.span; // Initialize the body translation context let mut bt_ctx = BodyTransCtx::new(rust_id, self); @@ -1540,7 +1516,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { def: &hax::FullDef, ) -> Result { trace!("About to translate global:\n{:?}", rust_id); - let span = item_meta.span.rust_span(); + let span = item_meta.span; // Initialize the body translation context let mut bt_ctx = BodyTransCtx::new(rust_id, self); diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 84b17ddde..70eac1162 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -1,9 +1,8 @@ use super::translate_ctx::*; use super::translate_traits::PredicateLocation; +use charon_lib::ast::*; use charon_lib::common::*; -use charon_lib::gast::*; use charon_lib::ids::Vector; -use charon_lib::types::*; use hax_frontend_exporter as hax; impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { @@ -85,7 +84,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// auto traits like [core::marker::Sized] and [core::marker::Sync]. pub(crate) fn translate_trait_decl_ref( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, bound_trait_ref: &hax::Binder, ) -> Result, Error> { @@ -115,14 +114,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// `origin` is where this clause comes from. pub(crate) fn register_trait_clause( &mut self, - hspan: &hax::Span, + span: Span, trait_pred: &hax::TraitPredicate, origin: PredicateOrigin, location: &PredicateLocation, ) -> Result, Error> { - let span = self.translate_span_from_hax(hspan.clone()); - - let trait_decl_ref = self.translate_trait_predicate(hspan, trait_pred)?; + let trait_decl_ref = self.translate_trait_predicate(span, trait_pred)?; let poly_trait_ref = RegionBinder { // We're under the binder of `hax::Predicate`, we re-wrap it here. regions: self.region_vars[0].clone(), @@ -148,12 +145,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub(crate) fn translate_trait_predicate( &mut self, - hspan: &hax::Span, + span: Span, trait_pred: &hax::TraitPredicate, ) -> Result { // Note sure what this is about assert!(trait_pred.is_positive); - let span = hspan.rust_span_data.unwrap().span(); // We translate trait clauses for signatures, etc. so we do not erase the regions let erase_regions = false; @@ -180,7 +176,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Predicates are always used in signatures/type definitions, etc. // For this reason, we do not erase the regions. let erase_regions = false; - let span = hspan.rust_span_data.unwrap().span(); + let span = self.translate_span_from_hax(hspan.clone()); let binder = pred.kind.rebind(()); self.with_locally_bound_regions_group(span, binder, move |ctx| { @@ -193,7 +189,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let regions = ctx.region_vars[0].clone(); match kind { ClauseKind::Trait(trait_pred) => { - ctx.register_trait_clause(hspan, trait_pred, origin, location)?; + ctx.register_trait_clause(span, trait_pred, origin, location)?; } ClauseKind::RegionOutlives(p) => { // TODO: we're under a binder, we should re-bind @@ -271,7 +267,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub(crate) fn translate_trait_impl_exprs( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, impl_sources: &[hax::ImplExpr], ) -> Result, Error> { @@ -287,7 +283,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { #[tracing::instrument(skip(self, span, erase_regions))] pub(crate) fn translate_trait_impl_expr( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, impl_expr: &hax::ImplExpr, ) -> Result, Error> { @@ -321,7 +317,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub(crate) fn translate_trait_impl_expr_aux( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, impl_source: &hax::ImplExpr, trait_decl_ref: PolyTraitDeclRef, diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index f5801d0dd..55da2c763 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -43,7 +43,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { ); let tcx = self.t_ctx.tcx; - let span = tcx.def_span(trait_impl_def_id); + let span = self.def_span(trait_impl_def_id); // Lookup the trait clauses and substitute - TODO: not sure about the substitution let subst = rust_impl_trait_ref.args; @@ -94,7 +94,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { trace!("About to translate trait decl:\n{:?}", rust_id); trace!("Trait decl id:\n{:?}", def_id); - let span = item_meta.span.rust_span(); + let span = item_meta.span; let erase_regions = false; let mut bt_ctx = BodyTransCtx::new(rust_id, self); @@ -132,7 +132,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let mut provided_methods = Vec::new(); for (item_name, hax_item, hax_def) in &items { let rust_item_id = DefId::from(&hax_item.def_id); - let item_span = bt_ctx.t_ctx.tcx.def_span(rust_item_id); + let item_span = bt_ctx.def_span(rust_item_id); match &hax_def.kind { hax::FullDefKind::AssocFn { .. } => { let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id); @@ -228,7 +228,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { trace!("Trait impl id:\n{:?}", def_id); let tcx = self.tcx; - let span = item_meta.span.rust_span(); + let span = item_meta.span; let erase_regions = false; let mut bt_ctx = BodyTransCtx::new(rust_id, self); @@ -315,18 +315,17 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { for item in impl_items { let name = TraitItemName(item.name.clone()); - let rust_item_id = DefId::from(&item.def_id); - let item_span = tcx.def_span(rust_item_id); + let item_span = bt_ctx.def_span(&item.def_id); match &item.kind { hax::AssocKind::Fn => { - let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id); + let fun_id = bt_ctx.register_fun_decl_id(item_span, &item.def_id); methods.insert(name, fun_id); } hax::AssocKind::Const => { // The parameters of the constant are the same as those of the item that // declares them. let gref = GlobalDeclRef { - id: bt_ctx.register_global_decl_id(item_span, rust_item_id), + id: bt_ctx.register_global_decl_id(item_span, &item.def_id), generics: generics.identity_args(), }; consts.insert(name, gref); @@ -361,7 +360,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { for decl_item in decl_items { let item_def_id = (&decl_item.def_id).into(); - let item_span = tcx.def_span(item_def_id); + let item_span = bt_ctx.def_span(item_def_id); 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 ea45f5cfd..f302b2351 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -10,7 +10,6 @@ use charon_lib::pretty::FmtWithCtx; use core::convert::*; use hax::Visibility; use hax_frontend_exporter as hax; -use hax_frontend_exporter::SInto; use rustc_hir::def_id::DefId; /// Small helper: we ignore some region names (when they are equal to "'_") @@ -58,7 +57,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Translate a region pub(crate) fn translate_region( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, region: &hax::Region, ) -> Result { @@ -120,7 +119,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { #[tracing::instrument(skip(self, span, erase_regions))] pub(crate) fn translate_ty( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, ty: &hax::Ty, ) -> Result { @@ -353,7 +352,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { #[allow(clippy::type_complexity)] pub fn translate_substs( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, used_params: Option>, substs: &[hax::GenericArg], @@ -403,7 +402,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub fn translate_substs_and_trait_refs( &mut self, - span: rustc_span::Span, + span: Span, erase_regions: bool, used_params: Option>, substs: &[hax::GenericArg], @@ -436,7 +435,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Translate a type def id pub(crate) fn translate_type_id( &mut self, - span: rustc_span::Span, + span: Span, def_id: &hax::DefId, ) -> Result { trace!("{:?}", def_id); @@ -455,7 +454,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { fn translate_adt_def( &mut self, trans_id: TypeDeclId, - def_span: rustc_span::Span, + def_span: Span, item_meta: &ItemMeta, adt: &hax::AdtDef, ) -> Result { @@ -504,9 +503,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { for (j, field_def) in var_def.fields.iter().enumerate() { trace!("variant {i}: field {j}: {field_def:?}"); let field_span = self.t_ctx.translate_span_from_hax(field_def.span.clone()); - let field_rspan = field_span.span.rust_span_data.span(); // Translate the field type - let ty = self.translate_ty(field_rspan, erase_regions, &field_def.ty)?; + let ty = self.translate_ty(field_span, erase_regions, &field_def.ty)?; let field_full_def = self.t_ctx.hax_def(&field_def.did); let field_attrs = self.t_ctx.translate_attr_info(&field_full_def); @@ -521,7 +519,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } } Some(b) => { - error_assert!(self, field_rspan, *b == field_name.is_some()); + error_assert!(self, field_span, *b == field_name.is_some()); } }; @@ -586,7 +584,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { fn translate_discriminant( &mut self, - def_span: rustc_span::Span, + def_span: Span, discr: &hax::DiscriminantValue, ) -> Result { let ty = self.translate_ty(def_span, true, &discr.ty)?; @@ -618,7 +616,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Translate the generics and predicates of this item and its parents. pub(crate) fn translate_def_generics( &mut self, - span: rustc_span::Span, + span: Span, def: &hax::FullDef, ) -> Result { self.push_generics_for_def(span, def, false)?; @@ -644,7 +642,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Add the generics and predicates of this item and its parents to the current context. fn push_generics_for_def( &mut self, - span: rustc_span::Span, + span: Span, def: &hax::FullDef, is_parent: bool, ) -> Result<(), Error> { @@ -672,8 +670,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } | FullDefKind::Trait { self_predicate, .. } => { self.register_trait_decl_id(span, &self_predicate.trait_ref.def_id); - let hax_span = span.sinto(&self.t_ctx.hax_state); - let _ = self.translate_trait_predicate(&hax_span, self_predicate)?; + let _ = self.translate_trait_predicate(span, self_predicate)?; } _ => {} } @@ -754,7 +751,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub(crate) fn push_generic_params( &mut self, - span: rustc_span::Span, + span: Span, generics: &hax::TyGenerics, ) -> Result<(), Error> { for param in &generics.params { @@ -765,7 +762,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub(crate) fn push_generic_param( &mut self, - span: rustc_span::Span, + span: Span, param: &hax::GenericParamDef, ) -> Result<(), Error> { match ¶m.kind { @@ -811,7 +808,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let mut bt_ctx = BodyTransCtx::new(rust_id, self); let erase_regions = false; - let span = item_meta.span.rust_span(); + let span = item_meta.span; // Translate generics and predicates let generics = bt_ctx.translate_def_generics(span, def)?; diff --git a/charon/src/errors.rs b/charon/src/errors.rs index d2c2d71b7..d2daebc0d 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -1,4 +1,5 @@ //! Utilities to generate error reports about the external dependencies. +use crate::ast::Span; use macros::VariantIndexArity; use petgraph::algo::dijkstra::dijkstra; use petgraph::graphmap::DiGraphMap; @@ -25,7 +26,7 @@ macro_rules! error_or_panic { ($ctx:expr, $span:expr, $msg:expr) => {{ $crate::errors::register_error_or_panic!($ctx, $span, $msg); let e = $crate::common::Error { - span: $span, + span: $span.into(), msg: $msg.to_string(), }; return Err(e); @@ -80,8 +81,11 @@ impl Ord for DepSource { } impl DepSource { - pub fn make(src_id: DefId, span: rustc_span::Span) -> Option { - Some(DepSource { src_id, span }) + pub fn make(src_id: DefId, span: Span) -> Option { + Some(DepSource { + src_id, + span: span.rust_span(), + }) } } diff --git a/charon/src/transform/reconstruct_boxes.rs b/charon/src/transform/reconstruct_boxes.rs index 5b175ea75..e94cde0ad 100644 --- a/charon/src/transform/reconstruct_boxes.rs +++ b/charon/src/transform/reconstruct_boxes.rs @@ -115,11 +115,7 @@ impl UllbcPass for Transform { // Make sure we got all the `ShallowInitBox`es. b.body.drive(&mut visitor_enter_fn(|rvalue: &Rvalue| { if rvalue.is_shallow_init_box() { - register_error_or_panic!( - ctx, - b.span.span.rust_span_data.span(), - "Unexpected `ShallowInitBox`" - ); + register_error_or_panic!(ctx, b.span, "Unexpected `ShallowInitBox`"); } })); } diff --git a/charon/src/transform/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs index 6924d49c5..23a558a17 100644 --- a/charon/src/transform/remove_read_discriminant.rs +++ b/charon/src/transform/remove_read_discriminant.rs @@ -39,11 +39,7 @@ impl Transform { | TypeDeclKind::Opaque | TypeDeclKind::Alias(..) => { // We shouldn't get there - register_error_or_panic!( - ctx, - block.span.span.rust_span_data.span(), - "Unreachable case" - ); + register_error_or_panic!(ctx, block.span, "Unreachable case"); None } TypeDeclKind::Error(_) => None, @@ -92,7 +88,7 @@ impl Transform { discr_to_id.get(&discr).or_else(|| { register_error_or_panic!( ctx, - block.span.span.rust_span_data.span(), + block.span, "Found incorrect discriminant {discr} for enum {adt_id}" ); None diff --git a/charon/tests/ui/issue-369-mismatched-genericparams.out b/charon/tests/ui/issue-369-mismatched-genericparams.out index 39af822b1..034150d78 100644 --- a/charon/tests/ui/issue-369-mismatched-genericparams.out +++ b/charon/tests/ui/issue-369-mismatched-genericparams.out @@ -1,5 +1,5 @@ error: Mismatched generics: - expected: GenericParams { regions: [], types: [Some(TypeVar { index: 0, name: "T" })], const_generics: [], trait_clauses: [Some(TraitClause { clause_id: 0, span: Some(Span { span: RawSpan { file_id: 3, beg: Loc { line: 2498, col: 5 }, end: Loc { line: 2498, col: 6 }, rust_span_data: /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2498:6: 2498:7 (#0) }, generated_from_span: None }), origin: WhereClauseOnImpl, trait_: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })], regions_outlive: [], types_outlive: [], trait_type_constraints: [] } + expected: GenericParams { regions: [], types: [Some(TypeVar { index: 0, name: "T" })], const_generics: [], trait_clauses: [Some(TraitClause { clause_id: 0, span: Some(Span { span: RawSpan { file_id: 1, beg: Loc { line: 2498, col: 5 }, end: Loc { line: 2498, col: 6 }, rust_span_data: /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2498:6: 2498:7 (#0) }, generated_from_span: None }), origin: WhereClauseOnImpl, trait_: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })], regions_outlive: [], types_outlive: [], trait_type_constraints: [] } got: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } }), Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })] } --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2479:1 diff --git a/charon/tests/ui/issue-393-shallowinitbox.out b/charon/tests/ui/issue-393-shallowinitbox.out index a9ef0d39f..d3209d5cd 100644 --- a/charon/tests/ui/issue-393-shallowinitbox.out +++ b/charon/tests/ui/issue-393-shallowinitbox.out @@ -7,7 +7,7 @@ error: Unexpected `ShallowInitBox` | |_^ error: Mismatched generics: - expected: GenericParams { regions: [], types: [Some(TypeVar { index: 0, name: "T" })], const_generics: [], trait_clauses: [Some(TraitClause { clause_id: 0, span: Some(Span { span: RawSpan { file_id: 8, beg: Loc { line: 2498, col: 5 }, end: Loc { line: 2498, col: 6 }, rust_span_data: /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2498:6: 2498:7 (#0) }, generated_from_span: None }), origin: WhereClauseOnImpl, trait_: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })], regions_outlive: [], types_outlive: [], trait_type_constraints: [] } + expected: GenericParams { regions: [], types: [Some(TypeVar { index: 0, name: "T" })], const_generics: [], trait_clauses: [Some(TraitClause { clause_id: 0, span: Some(Span { span: RawSpan { file_id: 5, beg: Loc { line: 2498, col: 5 }, end: Loc { line: 2498, col: 6 }, rust_span_data: /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2498:6: 2498:7 (#0) }, generated_from_span: None }), origin: WhereClauseOnImpl, trait_: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })], regions_outlive: [], types_outlive: [], trait_type_constraints: [] } got: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } }), Some(TraitRef { kind: Clause(0), trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { trait_id: 0, generics: GenericArgs { regions: [], types: [Some(TypeVar(0))], const_generics: [], trait_refs: [] } } } })] } --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:2479:1 diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out index 773ed5176..9d885d74a 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:788:42: +thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:785: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`. From 1a77cc63d98ef350fb3cfbcb91f14e0ed822126d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Oct 2024 16:24:33 +0200 Subject: [PATCH 2/9] Use our own `Span` in error reporting --- charon/src/ast/meta_utils.rs | 24 +++++++++++++++++++ .../charon-driver/translate/translate_ctx.rs | 5 ++-- charon/src/common.rs | 2 +- charon/src/errors.rs | 15 +++++------- charon/src/transform/ctx.rs | 3 +-- 5 files changed, 34 insertions(+), 15 deletions(-) diff --git a/charon/src/ast/meta_utils.rs b/charon/src/ast/meta_utils.rs index beca57f43..bd56c116c 100644 --- a/charon/src/ast/meta_utils.rs +++ b/charon/src/ast/meta_utils.rs @@ -6,6 +6,10 @@ use std::cmp::Ordering; use std::iter::Iterator; impl Loc { + fn dummy() -> Self { + Loc { line: 0, col: 0 } + } + fn min(l0: &Loc, l1: &Loc) -> Loc { match l0.line.cmp(&l1.line) { Ordering::Equal => Loc { @@ -29,6 +33,26 @@ impl Loc { } } +impl RawSpan { + pub fn dummy() -> Self { + RawSpan { + file_id: FileId::from_raw(0), + beg: Loc::dummy(), + end: Loc::dummy(), + rust_span_data: rustc_span::DUMMY_SP.data(), + } + } +} + +impl Span { + pub fn dummy() -> Self { + Span { + span: RawSpan::dummy(), + generated_from_span: None, + } + } +} + /// Combine some span information (useful when we need to compute the /// span-information of, say, a sequence). pub fn combine_span(m0: &Span, m1: &Span) -> Span { diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 3137767b5..5a8651443 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -11,7 +11,6 @@ use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; use itertools::Itertools; use macros::VariantIndexArity; -use rustc_error_messages::MultiSpan; use rustc_hir::def_id::DefId; use rustc_hir::Node as HirNode; use rustc_middle::ty::TyCtxt; @@ -58,7 +57,7 @@ impl TranslateOptions { Ok(p) => Ok(p), Err(e) => { let msg = format!("failed to parse pattern `{s}` ({e})"); - error_or_panic!(error_ctx, rustc_span::DUMMY_SP, msg) + error_or_panic!(error_ctx, Span::dummy(), msg) } }; @@ -279,7 +278,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } /// Span an error and register the error. - pub fn span_err>(&mut self, span: S, msg: &str) { + pub fn span_err(&mut self, span: Span, msg: &str) { self.errors.span_err(span, msg) } diff --git a/charon/src/common.rs b/charon/src/common.rs index f8e480d35..423c126d6 100644 --- a/charon/src/common.rs +++ b/charon/src/common.rs @@ -3,7 +3,7 @@ pub static TAB_INCR: &str = " "; /// Common error used during the translation. #[derive(Debug)] pub struct Error { - pub span: rustc_span::Span, + pub span: crate::ast::Span, pub msg: String, } diff --git a/charon/src/errors.rs b/charon/src/errors.rs index d2daebc0d..15ba0a30b 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -26,7 +26,7 @@ macro_rules! error_or_panic { ($ctx:expr, $span:expr, $msg:expr) => {{ $crate::errors::register_error_or_panic!($ctx, $span, $msg); let e = $crate::common::Error { - span: $span.into(), + span: $span, msg: $msg.to_string(), }; return Err(e); @@ -58,7 +58,7 @@ pub use error_assert; #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] pub struct DepSource { pub src_id: DefId, - pub span: rustc_span::Span, + pub span: Span, } impl DepSource { @@ -82,10 +82,7 @@ impl Ord for DepSource { impl DepSource { pub fn make(src_id: DefId, span: Span) -> Option { - Some(DepSource { - src_id, - span: span.rust_span(), - }) + Some(DepSource { src_id, span }) } } @@ -129,7 +126,7 @@ impl ErrorCtx<'_> { } /// Report and register an error. - pub fn span_err>(&mut self, span: S, msg: &str) { + pub fn span_err(&mut self, span: Span, msg: &str) { self.span_err_no_register(span, msg); self.error_count += 1; if let Some(id) = self.def_id { @@ -163,7 +160,7 @@ impl ErrorCtx<'_> { enum Node { External(DefId), /// We use the span information only for local references - Local(DefId, rustc_span::Span), + Local(DefId, Span), } impl Node { @@ -271,7 +268,7 @@ impl ErrorCtx<'_> { .iter() .filter_map(|(n, _)| match n { Node::External(_) => None, - Node::Local(_, span) => Some(*span), + Node::Local(_, span) => Some(span.rust_span()), }) .collect(); diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 1522c0fcd..0c7dc4c48 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -6,7 +6,6 @@ use crate::llbc_ast; use crate::name_matcher::NamePattern; use crate::pretty::FmtWithCtx; use crate::ullbc_ast; -use rustc_error_messages::MultiSpan; use rustc_span::def_id::DefId; use std::fmt; @@ -199,7 +198,7 @@ impl<'ctx> TransformCtx<'ctx> { } /// Span an error and register the error. - pub(crate) fn span_err>(&mut self, span: S, msg: &str) { + pub(crate) fn span_err(&mut self, span: Span, msg: &str) { self.errors.span_err(span, msg) } From 12e4f0d5125fbac4fcb89f797d3f4a9bea52dce3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Oct 2024 16:53:31 +0200 Subject: [PATCH 3/9] Move `Error` to the `errors` module --- charon/src/ast/mod.rs | 1 + .../bin/charon-driver/translate/translate_constants.rs | 1 - .../charon-driver/translate/translate_crate_to_ullbc.rs | 3 +-- charon/src/bin/charon-driver/translate/translate_ctx.rs | 1 - .../bin/charon-driver/translate/translate_predicates.rs | 1 - .../src/bin/charon-driver/translate/translate_traits.rs | 4 +--- .../src/bin/charon-driver/translate/translate_types.rs | 1 - charon/src/common.rs | 7 ------- charon/src/errors.rs | 9 ++++++++- charon/src/transform/update_closure_signatures.rs | 1 - charon/tests/ui/unsupported/advanced-const-generics.out | 2 +- 11 files changed, 12 insertions(+), 19 deletions(-) diff --git a/charon/src/ast/mod.rs b/charon/src/ast/mod.rs index f61b8a364..e35864825 100644 --- a/charon/src/ast/mod.rs +++ b/charon/src/ast/mod.rs @@ -18,6 +18,7 @@ pub mod values; pub mod values_utils; // Re-export everything except llbc/ullbc, for convenience. +pub use crate::errors::Error; pub use builtins::*; pub use expressions::*; pub use gast::*; diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs index a0aac3c35..3f4a221d8 100644 --- a/charon/src/bin/charon-driver/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -1,7 +1,6 @@ //! Functions to translate constants to LLBC. use super::translate_ctx::*; use charon_lib::ast::*; -use charon_lib::common::*; use hax_frontend_exporter as hax; impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { 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 6d66a31ff..f4d2f1d84 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 @@ -1,8 +1,7 @@ use super::get_mir::extract_constants_at_top_level; use super::translate_ctx::*; -use charon_lib::ast::krate::*; use charon_lib::ast::meta::FileName; -use charon_lib::common::*; +use charon_lib::ast::*; use charon_lib::options::CliOpts; use charon_lib::transform::ctx::TransformOptions; use charon_lib::transform::TransformCtx; diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 5a8651443..9914bd1e4 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -1,7 +1,6 @@ //! The translation contexts. use super::translate_types::translate_bound_region_kind_name; use charon_lib::ast::*; -use charon_lib::common::*; use charon_lib::formatter::{FmtCtx, IntoFormatter}; use charon_lib::ids::{MapGenerator, Vector}; use charon_lib::name_matcher::NamePattern; diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 70eac1162..03826195b 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -1,7 +1,6 @@ use super::translate_ctx::*; use super::translate_traits::PredicateLocation; use charon_lib::ast::*; -use charon_lib::common::*; use charon_lib::ids::Vector; use hax_frontend_exporter as hax; diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index 55da2c763..fb6fd93bb 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -1,11 +1,9 @@ use super::translate_ctx::*; -use charon_lib::common::*; +use charon_lib::ast::*; use charon_lib::formatter::IntoFormatter; -use charon_lib::gast::*; use charon_lib::ids::Vector; use charon_lib::meta::ItemMeta; use charon_lib::pretty::FmtWithCtx; -use charon_lib::types::*; use charon_lib::ullbc_ast as ast; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index f302b2351..c59c0a3db 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -3,7 +3,6 @@ use crate::translate::translate_traits::PredicateLocation; use super::translate_ctx::*; use charon_lib::ast::*; use charon_lib::builtins; -use charon_lib::common::*; use charon_lib::formatter::IntoFormatter; use charon_lib::ids::Vector; use charon_lib::pretty::FmtWithCtx; diff --git a/charon/src/common.rs b/charon/src/common.rs index 423c126d6..9cf2ca43e 100644 --- a/charon/src/common.rs +++ b/charon/src/common.rs @@ -1,12 +1,5 @@ pub static TAB_INCR: &str = " "; -/// Common error used during the translation. -#[derive(Debug)] -pub struct Error { - pub span: crate::ast::Span, - pub msg: String, -} - /// Custom function to pretty-print elements from an iterator /// The output format is: /// ```text diff --git a/charon/src/errors.rs b/charon/src/errors.rs index 15ba0a30b..54729e942 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -9,6 +9,13 @@ use rustc_span::def_id::DefId; use std::cmp::{Ord, PartialOrd}; use std::collections::{HashMap, HashSet}; +/// Common error used during the translation. +#[derive(Debug)] +pub struct Error { + pub span: Span, + pub msg: String, +} + #[macro_export] macro_rules! register_error_or_panic { ($ctx:expr, $span: expr, $msg: expr) => {{ @@ -25,7 +32,7 @@ pub use register_error_or_panic; macro_rules! error_or_panic { ($ctx:expr, $span:expr, $msg:expr) => {{ $crate::errors::register_error_or_panic!($ctx, $span, $msg); - let e = $crate::common::Error { + let e = $crate::errors::Error { span: $span, msg: $msg.to_string(), }; diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index ea8111e9b..58cf9b1db 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -3,7 +3,6 @@ //! which ignores this first variable. This micro-pass updates this. use derive_visitor::{visitor_enter_fn_mut, DriveMut, VisitorMut}; -use crate::common::*; use crate::ids::Vector; use crate::transform::TransformCtx; use crate::ullbc_ast::*; diff --git a/charon/tests/ui/unsupported/advanced-const-generics.out b/charon/tests/ui/unsupported/advanced-const-generics.out index 9d885d74a..11d2459bc 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:785:42: +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`. From b9a634ecf8f2ee05ef11f024b2e072bbd39b49f0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Oct 2024 19:30:15 +0200 Subject: [PATCH 4/9] Factor out `BodyTransCtx::new` calls --- .../translate/translate_crate_to_ullbc.rs | 15 ++-- .../translate/translate_functions_to_ullbc.rs | 42 ++++------ .../translate/translate_traits.rs | 82 +++++++++---------- .../translate/translate_types.rs | 18 ++-- 4 files changed, 72 insertions(+), 85 deletions(-) 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 f4d2f1d84..53a658fda 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 @@ -309,6 +309,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { rust_id: DefId, trans_id: AnyTransId, ) -> Result<(), Error> { + // Translate the meta information let name = self.def_id_to_name(rust_id)?; self.translated.item_names.insert(trans_id, name.clone()); let opacity = self.opacity_for_name(&name); @@ -316,28 +317,30 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Don't even start translating the item. In particular don't call `hax_def` on it. return Ok(()); } - // Translate the meta information let def: Arc = self.hax_def(rust_id); let item_meta = self.translate_item_meta(&def, name, opacity)?; + + // Initialize the body translation context + let bt_ctx = BodyTransCtx::new(rust_id, self); match trans_id { AnyTransId::Type(id) => { - let ty = self.translate_type(id, rust_id, item_meta, &def)?; + let ty = bt_ctx.translate_type(id, item_meta, &def)?; self.translated.type_decls.set_slot(id, ty); } AnyTransId::Fun(id) => { - let fun_decl = self.translate_function(id, rust_id, item_meta, &def)?; + let fun_decl = bt_ctx.translate_function(id, rust_id, item_meta, &def)?; self.translated.fun_decls.set_slot(id, fun_decl); } AnyTransId::Global(id) => { - let global_decl = self.translate_global(id, rust_id, item_meta, &def)?; + let global_decl = bt_ctx.translate_global(id, rust_id, item_meta, &def)?; self.translated.global_decls.set_slot(id, global_decl); } AnyTransId::TraitDecl(id) => { - let trait_decl = self.translate_trait_decl(id, rust_id, item_meta, &def)?; + let trait_decl = bt_ctx.translate_trait_decl(id, rust_id, item_meta, &def)?; self.translated.trait_decls.set_slot(id, trait_decl); } AnyTransId::TraitImpl(id) => { - let trait_impl = self.translate_trait_impl(id, rust_id, item_meta, &def)?; + let trait_impl = bt_ctx.translate_trait_impl(id, rust_id, item_meta, &def)?; self.translated.trait_impls.set_slot(id, trait_impl); } } 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 18fd5036a..558d52b97 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 @@ -1270,13 +1270,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Translate a function body if we can (it has MIR) and we want to (we don't translate bodies /// declared opaque, and only translate non-local bodies if `extract_opaque_bodies` is set). fn translate_body( - mut self, + &mut self, rust_id: DefId, 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 mut this = panic::AssertUnwindSafe(&mut *self); let res = panic::catch_unwind(move || this.translate_body_aux(rust_id, arg_count, item_meta)); match res { @@ -1451,11 +1451,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } } -impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { +impl BodyTransCtx<'_, '_, '_> { /// Translate one function. #[tracing::instrument(skip(self, rust_id, item_meta))] pub fn translate_function( - &mut self, + mut self, def_id: FunDeclId, rust_id: DefId, item_meta: ItemMeta, @@ -1464,14 +1464,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { trace!("About to translate function:\n{:?}", rust_id); let def_span = item_meta.span; - // Initialize the body translation context - let mut bt_ctx = BodyTransCtx::new(rust_id, self); - // Check whether this function is a method declaration for a trait definition. // If this is the case, it shouldn't contain a body. - let kind = bt_ctx + let kind = self .t_ctx - .get_item_kind(&DepSource::make(rust_id, def_span), def)?; + .get_item_kind(&self.make_dep_source(def_span), def)?; let is_trait_method_decl_without_default = match &kind { ItemKind::Regular | ItemKind::TraitImpl { .. } => false, ItemKind::TraitDecl { has_default, .. } => !has_default, @@ -1479,18 +1476,18 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Translate the function signature trace!("Translating function signature"); - let signature = bt_ctx.translate_function_signature(rust_id, &item_meta, def)?; + let signature = self.translate_function_signature(rust_id, &item_meta, def)?; 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 bt_ctx.translate_body(rust_id, signature.inputs.len(), &item_meta) { - Ok(Ok(body)) => Ok(self.translated.bodies.push(body)), + match self.translate_body(rust_id, signature.inputs.len(), &item_meta) { + Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)), // Opaque declaration Ok(Err(Opaque)) => Err(Opaque), // Translation error. We reserve a slot and leave it empty. // FIXME: handle error cases more explicitly. - Err(_) => Ok(self.translated.bodies.reserve_slot()), + Err(_) => Ok(self.t_ctx.translated.bodies.reserve_slot()), } } else { Err(Opaque) @@ -1509,7 +1506,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Translate one global. #[tracing::instrument(skip(self, rust_id, item_meta))] pub fn translate_global( - &mut self, + mut self, def_id: GlobalDeclId, rust_id: DefId, item_meta: ItemMeta, @@ -1518,13 +1515,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { trace!("About to translate global:\n{:?}", rust_id); let span = item_meta.span; - // Initialize the body translation context - let mut bt_ctx = BodyTransCtx::new(rust_id, self); - // Retrieve the kind - let global_kind = bt_ctx - .t_ctx - .get_item_kind(&DepSource::make(rust_id, span), &def)?; + let global_kind = self.t_ctx.get_item_kind(&self.make_dep_source(span), def)?; // Translate the generics and predicates - globals *can* have generics // Ex.: @@ -1533,7 +1525,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // const LEN : usize = N; // } // ``` - let generics = bt_ctx.translate_def_generics(span, def)?; + let generics = self.translate_def_generics(span, def)?; trace!("Translating global type"); let ty = match &def.kind { @@ -1543,17 +1535,17 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { _ => panic!("Unexpected def for constant: {def:?}"), }; let erase_regions = false; // This doesn't matter: there shouldn't be any regions - let ty = bt_ctx.translate_ty(span, erase_regions, ty)?; + let ty = self.translate_ty(span, erase_regions, ty)?; // 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 bt_ctx.translate_body(rust_id, 0, &item_meta) { - Ok(Ok(body)) => Ok(self.translated.bodies.push(body)), + let body_id = match self.translate_body(rust_id, 0, &item_meta) { + Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)), // Opaque declaration Ok(Err(Opaque)) => Err(Opaque), // Translation error. We reserve a slot and leave it empty. // FIXME: handle error cases more explicitly. - Err(_) => Ok(self.translated.bodies.reserve_slot()), + Err(_) => Ok(self.t_ctx.translated.bodies.reserve_slot()), }; Ok(GlobalDecl { diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index fb6fd93bb..9efbad85d 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -80,10 +80,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { assert!(id.is_zero()); Ok(TraitItemName(name.to_string())) } +} +impl BodyTransCtx<'_, '_, '_> { #[tracing::instrument(skip(self, rust_id, item_meta))] pub fn translate_trait_decl( - &mut self, + mut self, def_id: TraitDeclId, rust_id: DefId, item_meta: ItemMeta, @@ -94,7 +96,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let span = item_meta.span; let erase_regions = false; - let mut bt_ctx = BodyTransCtx::new(rust_id, self); if let hax::FullDefKind::TraitAlias { .. } = def.kind() { error_or_panic!(self, span, &format!("Trait aliases are not supported")); @@ -107,7 +108,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { .iter() .map(|item| { let name = TraitItemName(item.name.clone()); - let def = bt_ctx.t_ctx.hax_def(&item.def_id); + let def = self.t_ctx.hax_def(&item.def_id); (name, item, def) }) .collect_vec(); @@ -115,9 +116,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Translate the generics // Note that in the generics returned by [translate_def_generics], the trait refs only // contain the local trait clauses. The parent clauses are stored in - // `bt_ctx.parent_trait_clauses`. + // `self.parent_trait_clauses`. // TODO: Distinguish between required and implied trait clauses? - let generics = bt_ctx.translate_def_generics(span, def)?; + let generics = self.translate_def_generics(span, def)?; // Translate the associated items // We do something subtle here: TODO: explain @@ -130,10 +131,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let mut provided_methods = Vec::new(); for (item_name, hax_item, hax_def) in &items { let rust_item_id = DefId::from(&hax_item.def_id); - let item_span = bt_ctx.def_span(rust_item_id); + let item_span = self.def_span(rust_item_id); match &hax_def.kind { hax::FullDefKind::AssocFn { .. } => { - let fun_id = bt_ctx.register_fun_decl_id(item_span, rust_item_id); + let fun_id = self.register_fun_decl_id(item_span, rust_item_id); if hax_item.has_value { // This is a provided method, provided_methods.push((item_name.clone(), fun_id)); @@ -148,21 +149,21 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // The parameters of the constant are the same as those of the item that // declares them. let gref = GlobalDeclRef { - id: bt_ctx.register_global_decl_id(item_span, rust_item_id), + id: self.register_global_decl_id(item_span, rust_item_id), generics: generics.identity_args(), }; const_defaults.insert(item_name.clone(), gref); }; - let ty = bt_ctx.translate_ty(item_span, erase_regions, ty)?; + let ty = self.translate_ty(item_span, erase_regions, ty)?; consts.push((item_name.clone(), ty)); } hax::FullDefKind::AssocTy { value, .. } => { // TODO: handle generics (i.e. GATs). - if let Some(clauses) = bt_ctx.item_trait_clauses.get(item_name) { + if let Some(clauses) = self.item_trait_clauses.get(item_name) { type_clauses.push((item_name.clone(), clauses.clone())); } if let Some(ty) = value { - let ty = bt_ctx.translate_ty(item_span, erase_regions, &ty)?; + let ty = self.translate_ty(item_span, erase_regions, &ty)?; type_defaults.insert(item_name.clone(), ty); }; types.push(item_name.clone()); @@ -173,7 +174,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Debugging: { - let ctx = bt_ctx.into_fmt(); + let ctx = self.into_fmt(); let generic_clauses = generics .trait_clauses .iter() @@ -187,8 +188,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { ); } if item_meta.opacity.is_opaque() { - let ctx = bt_ctx.into_fmt(); - bt_ctx.t_ctx.errors.dcx.span_warn( + let ctx = self.into_fmt(); + self.t_ctx.errors.dcx.span_warn( item_meta.span, format!( "Trait declarations cannot be \"opaque\"; the trait `{}` will be translated as normal.", @@ -203,7 +204,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { def_id, item_meta, generics, - parent_clauses: bt_ctx.parent_trait_clauses, + parent_clauses: self.parent_trait_clauses, type_clauses, consts, const_defaults, @@ -216,7 +217,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { #[tracing::instrument(skip(self, rust_id, item_meta))] pub fn translate_trait_impl( - &mut self, + mut self, def_id: TraitImplId, rust_id: DefId, item_meta: ItemMeta, @@ -225,12 +226,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { trace!("About to translate trait impl:\n{:?}", rust_id); trace!("Trait impl id:\n{:?}", def_id); - let tcx = self.tcx; + let tcx = self.t_ctx.tcx; let span = item_meta.span; let erase_regions = false; - let mut bt_ctx = BodyTransCtx::new(rust_id, self); - let generics = bt_ctx.translate_def_generics(span, def)?; + let generics = self.translate_def_generics(span, def)?; let hax::FullDefKind::Impl { impl_subject: hax::ImplSubject::Trait(trait_pred), @@ -241,7 +241,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { unreachable!() }; let implemented_trait_id = &trait_pred.trait_ref.def_id; - let trait_def = bt_ctx.t_ctx.hax_def(implemented_trait_id); + let trait_def = self.t_ctx.hax_def(implemented_trait_id); let hax::FullDefKind::Trait { items: decl_items, .. } = trait_def.kind() @@ -250,15 +250,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { }; // Retrieve the information about the implemented trait. - let trait_id = bt_ctx.register_trait_decl_id(span, implemented_trait_id); + let trait_id = self.register_trait_decl_id(span, implemented_trait_id); let implemented_trait = { let implemented_trait = &trait_pred.trait_ref; - let (regions, types, const_generics) = bt_ctx.translate_substs( - span, - erase_regions, - None, - &implemented_trait.generic_args, - )?; + let (regions, types, const_generics) = + self.translate_substs(span, erase_regions, None, &implemented_trait.generic_args)?; let generics = GenericArgs { regions, types, @@ -282,20 +278,20 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { unreachable!() }; let parent_trait_refs = hax::solve_item_traits( - &bt_ctx.hax_state, + &self.hax_state, rust_trait_ref.def_id, rust_trait_ref.args, None, ); let parent_trait_refs = - bt_ctx.translate_trait_impl_exprs(span, erase_regions, &parent_trait_refs)?; + self.translate_trait_impl_exprs(span, erase_regions, &parent_trait_refs)?; (rust_trait_ref, parent_trait_refs) }; { // Debugging - let ctx = bt_ctx.into_fmt(); + let ctx = self.into_fmt(); let refs = parent_trait_refs .iter() .map(|c| c.fmt_with_ctx(&ctx)) @@ -306,24 +302,24 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Explore the associated items // We do something subtle here: TODO - let tcx = bt_ctx.t_ctx.tcx; + let tcx = self.t_ctx.tcx; let mut consts = HashMap::new(); let mut types: HashMap = HashMap::new(); let mut methods = HashMap::new(); for item in impl_items { let name = TraitItemName(item.name.clone()); - let item_span = bt_ctx.def_span(&item.def_id); + let item_span = self.def_span(&item.def_id); match &item.kind { hax::AssocKind::Fn => { - let fun_id = bt_ctx.register_fun_decl_id(item_span, &item.def_id); + let fun_id = self.register_fun_decl_id(item_span, &item.def_id); methods.insert(name, fun_id); } hax::AssocKind::Const => { // The parameters of the constant are the same as those of the item that // declares them. let gref = GlobalDeclRef { - id: bt_ctx.register_global_decl_id(item_span, &item.def_id), + id: self.register_global_decl_id(item_span, &item.def_id), generics: generics.identity_args(), }; consts.insert(name, gref); @@ -332,14 +328,14 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // 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 = bt_ctx.t_ctx.hax_def(&item.def_id); + 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 = bt_ctx.translate_ty(item_span, erase_regions, ty)?; + let ty = self.translate_ty(item_span, erase_regions, ty)?; types.insert(name, ty); } } @@ -358,7 +354,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { for decl_item in decl_items { let item_def_id = (&decl_item.def_id).into(); - let item_span = bt_ctx.def_span(item_def_id); + let item_span = self.def_span(item_def_id); let name = TraitItemName(decl_item.name.to_string()); match &decl_item.kind { hax::AssocKind::Fn => { @@ -383,7 +379,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // The parameters of the constant are the same as those of the item // that declares them. GlobalDeclRef { - id: bt_ctx.register_global_decl_id(item_span, item_def_id), + id: self.register_global_decl_id(item_span, item_def_id), generics: implemented_trait.generics.clone(), } } @@ -400,14 +396,14 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let ty = tcx .type_of(item_def_id) .instantiate(tcx, rust_implemented_trait_ref.args) - .sinto(&bt_ctx.hax_state); - bt_ctx.translate_ty(item_span, erase_regions, &ty)? + .sinto(&self.hax_state); + self.translate_ty(item_span, erase_regions, &ty)? } }; types.push((name.clone(), ty)); // Retrieve the trait refs - let trait_refs = bt_ctx.translate_trait_refs_from_impl_trait_item( + let trait_refs = self.translate_trait_refs_from_impl_trait_item( rust_id, &rust_implemented_trait_ref, item_def_id, @@ -417,8 +413,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } } if item_meta.opacity.is_opaque() { - let ctx = bt_ctx.into_fmt(); - bt_ctx.t_ctx.errors.dcx.span_warn( + let ctx = self.into_fmt(); + self.t_ctx.errors.dcx.span_warn( item_meta.span, format!( "Trait implementations cannot be \"opaque\"; the impl `{}` will be translated as normal.", diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index c59c0a3db..4d87730ca 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -790,27 +790,24 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } } -impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { +impl BodyTransCtx<'_, '_, '_> { /// Translate a type definition. /// /// Note that we translate the types one by one: we don't need to take into /// account the fact that some types are mutually recursive at this point /// (we will need to take that into account when generating the code in a file). - #[tracing::instrument(skip(self, rust_id, item_meta))] + #[tracing::instrument(skip(self, item_meta))] pub fn translate_type( - &mut self, + mut self, trans_id: TypeDeclId, - rust_id: DefId, item_meta: ItemMeta, def: &hax::FullDef, ) -> Result { - let mut bt_ctx = BodyTransCtx::new(rust_id, self); - let erase_regions = false; let span = item_meta.span; // Translate generics and predicates - let generics = bt_ctx.translate_def_generics(span, def)?; + let generics = self.translate_def_generics(span, def)?; // Translate type body let kind = match &def.kind { @@ -818,17 +815,16 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque), hax::FullDefKind::TyAlias { ty, .. } => { // Don't error on missing trait refs. - bt_ctx.error_on_impl_expr_error = false; + self.error_on_impl_expr_error = false; // We only translate crate-local type aliases so the `unwrap` is ok. let ty = ty.as_ref().unwrap(); - bt_ctx - .translate_ty(span, erase_regions, ty) + self.translate_ty(span, erase_regions, ty) .map(TypeDeclKind::Alias) } hax::FullDefKind::Struct { def, .. } | hax::FullDefKind::Enum { def, .. } | hax::FullDefKind::Union { def, .. } => { - bt_ctx.translate_adt_def(trans_id, span, &item_meta, def) + self.translate_adt_def(trans_id, span, &item_meta, def) } _ => panic!("Unexpected item when translating types: {def:?}"), }; From 8c6f95c7c930180682046b683aae6d8d23565ec6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Oct 2024 21:10:50 +0200 Subject: [PATCH 5/9] Add test --- charon/tests/ui/error-dependencies.out | 21 +++++++++++++++++++++ charon/tests/ui/error-dependencies.rs | 18 ++++++++++++++++++ 2 files changed, 39 insertions(+) create mode 100644 charon/tests/ui/error-dependencies.out create mode 100644 charon/tests/ui/error-dependencies.rs diff --git a/charon/tests/ui/error-dependencies.out b/charon/tests/ui/error-dependencies.out new file mode 100644 index 000000000..b70f78262 --- /dev/null +++ b/charon/tests/ui/error-dependencies.out @@ -0,0 +1,21 @@ +error: Trait aliases are not supported + --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/ptr/metadata.rs:81:1 + +error: Ignoring the following item due to an error: core::ptr::metadata::Thin + --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/ptr/metadata.rs:81:1 + +error: The external definition `core::ptr::metadata::Thin` triggered errors. It is (transitively) used at the following location(s): + --> tests/ui/error-dependencies.rs:8:13 + | +8 | let _ = core::ptr::null::(); + | ^^^^^^^^^^^^^^^^^^^^^^^ +... +15 | let _ = custom_null::(); + | ^^^^^^^^^^^^^^^^^^^ +16 | } +17 | fn custom_null() {} + | ^^^^^^^^^^^^^^^ + +error: aborting due to 3 previous errors + +Error: Charon driver exited with code 101 diff --git a/charon/tests/ui/error-dependencies.rs b/charon/tests/ui/error-dependencies.rs new file mode 100644 index 000000000..b0ab6aa87 --- /dev/null +++ b/charon/tests/ui/error-dependencies.rs @@ -0,0 +1,18 @@ +//@ known-failure +//! This file tests the error messages that indicates why we attempte to translate a given +//! definition. +#![feature(register_tool)] +#![register_tool(charon)] + +fn main() { + let _ = core::ptr::null::(); + let _ = opaque::other_error(); +} + +#[charon::opaque] +mod opaque { + pub fn other_error() { + let _ = custom_null::(); + } + fn custom_null() {} +} From 902ead1757996269f1d6cd329978c92417906846 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Oct 2024 21:35:03 +0200 Subject: [PATCH 6/9] Remove all calls to `DefId::is_local` from charon_lib --- .../translate/translate_crate_to_ullbc.rs | 5 +- .../charon-driver/translate/translate_ctx.rs | 19 +++- charon/src/errors.rs | 95 ++++++++----------- charon/src/transform/ctx.rs | 9 +- 4 files changed, 63 insertions(+), 65 deletions(-) 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 53a658fda..d76a70be0 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 @@ -416,10 +416,11 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC continue_on_failure: !options.abort_on_error, errors_as_warnings: options.errors_as_warnings, dcx: tcx.dcx(), - decls_with_errors: HashSet::new(), + external_decls_with_errors: HashSet::new(), ignored_failed_decls: HashSet::new(), - dep_sources: HashMap::new(), + external_dep_sources: HashMap::new(), def_id: None, + def_id_is_local: false, error_count: 0, }; let translate_options = TranslateOptions::new(&mut error_ctx, options); diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 9914bd1e4..e90318132 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -747,7 +747,15 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Register the fact that `id` is a dependency of `src` (if `src` is not `None`). pub(crate) fn register_dep_source(&mut self, src: &Option, id: DefId) { - self.errors.register_dep_source(src, id) + if let Some(src) = src { + if src.src_id != id && !id.is_local() { + self.errors + .external_dep_sources + .entry(id) + .or_default() + .insert(*src); + } + } } pub(crate) fn register_id(&mut self, src: &Option, id: OrdRustId) -> AnyTransId { @@ -863,9 +871,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { F: FnOnce(&mut Self) -> T, { let current_def_id = self.errors.def_id; + let current_def_id_is_local = self.errors.def_id_is_local; self.errors.def_id = Some(def_id); + self.errors.def_id_is_local = def_id.is_local(); let ret = f(self); self.errors.def_id = current_def_id; + self.errors.def_id_is_local = current_def_id_is_local; ret } } @@ -1090,7 +1101,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } pub(crate) fn make_dep_source(&self, span: Span) -> Option { - DepSource::make(self.def_id, span) + let src_id = self.def_id; + Some(DepSource { + src_id, + span: src_id.is_local().then_some(span), + }) } } diff --git a/charon/src/errors.rs b/charon/src/errors.rs index 54729e942..f3ec4d46e 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -65,7 +65,9 @@ pub use error_assert; #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] pub struct DepSource { pub src_id: DefId, - pub span: Span, + /// The location where the id was referred to. We store `None` for external dependencies as we + /// don't want to show these to the users. + pub span: Option, } impl DepSource { @@ -87,12 +89,6 @@ impl Ord for DepSource { } } -impl DepSource { - pub fn make(src_id: DefId, span: Span) -> Option { - Some(DepSource { src_id, span }) - } -} - /// The context for tracking and reporting errors. pub struct ErrorCtx<'ctx> { /// If true, do not abort on the first error and attempt to extract as much as possible. @@ -102,14 +98,16 @@ pub struct ErrorCtx<'ctx> { /// The compiler session, used for displaying errors. pub dcx: DiagCtxtHandle<'ctx>, - /// The ids of the declarations for which extraction we encountered errors. - pub decls_with_errors: HashSet, + /// The ids of the external_declarations for which extraction we encountered errors. + pub external_decls_with_errors: HashSet, /// The ids of the declarations we completely failed to extract and had to ignore. pub ignored_failed_decls: HashSet, - /// Dependency graph with sources. See [DepSource]. - pub dep_sources: HashMap>, + /// For each external item, a list of locations that point to it. See [DepSource]. + pub external_dep_sources: HashMap>, /// The id of the definition we are exploring, used to track the source of errors. pub def_id: Option, + /// Whether the definition being explored is local to the crate or not. + pub def_id_is_local: bool, /// The number of errors encountered so far. pub error_count: usize, } @@ -136,24 +134,10 @@ impl ErrorCtx<'_> { pub fn span_err(&mut self, span: Span, msg: &str) { self.span_err_no_register(span, msg); self.error_count += 1; - if let Some(id) = self.def_id { - let _ = self.decls_with_errors.insert(id); - } - } - - /// Register the fact that `id` is a dependency of `src` (if `src` is not `None`). - pub fn register_dep_source(&mut self, src: &Option, id: DefId) { - if let Some(src) = src { - if src.src_id != id { - match self.dep_sources.get_mut(&id) { - None => { - let _ = self.dep_sources.insert(id, HashSet::from([*src])); - } - Some(srcs) => { - let _ = srcs.insert(*src); - } - } - } + if let Some(id) = self.def_id + && !self.def_id_is_local + { + let _ = self.external_decls_with_errors.insert(id); } } @@ -245,20 +229,17 @@ impl ErrorCtx<'_> { // - from local def to external def let mut graph = Graph::new(); - trace!("dep_sources:\n{:?}", self.dep_sources); - for (id, srcs) in &self.dep_sources { - // Only insert dependencies from external defs - if !id.is_local() { - let node = Node::External(*id); - graph.insert_node(node); + trace!("dep_sources:\n{:?}", self.external_dep_sources); + for (id, srcs) in &self.external_dep_sources { + let src_node = Node::External(*id); + graph.insert_node(src_node); - for src in srcs { - if src.src_id.is_local() { - graph.insert_edge(node, Node::Local(src.src_id, src.span)); - } else { - graph.insert_edge(node, Node::External(src.src_id)); - } - } + for src in srcs { + let tgt_node = match src.span { + Some(span) => Node::Local(src.src_id, span), + None => Node::External(src.src_id), + }; + graph.insert_edge(src_node, tgt_node) } } trace!("Graph:\n{}", graph); @@ -266,26 +247,24 @@ impl ErrorCtx<'_> { // We need to compute the reachability graph. An easy way is simply // to use Dijkstra on every external definition which triggered an // error. - for id in &self.decls_with_errors { - if !id.is_local() { - let reachable = dijkstra(&graph.dgraph, Node::External(*id), None, &mut |_| 1); - trace!("id: {:?}\nreachable:\n{:?}", id, reachable); + for id in &self.external_decls_with_errors { + let reachable = dijkstra(&graph.dgraph, Node::External(*id), None, &mut |_| 1); + trace!("id: {:?}\nreachable:\n{:?}", id, reachable); - let reachable: Vec = reachable - .iter() - .filter_map(|(n, _)| match n { - Node::External(_) => None, - Node::Local(_, span) => Some(span.rust_span()), - }) - .collect(); + let reachable: Vec = reachable + .iter() + .filter_map(|(n, _)| match n { + Node::External(_) => None, + Node::Local(_, span) => Some(span.rust_span()), + }) + .collect(); - // Display the error message - let span = MultiSpan::from_spans(reachable); - let msg = format!("The external definition `{:?}` triggered errors. It is (transitively) used at the following location(s):", + // Display the error message + let span = MultiSpan::from_spans(reachable); + let msg = format!("The external definition `{:?}` triggered errors. It is (transitively) used at the following location(s):", *id, ); - self.span_err_no_register(span, &msg); - } + self.span_err_no_register(span, &msg); } } } diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 0c7dc4c48..b9eef3ee3 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -202,14 +202,17 @@ impl<'ctx> TransformCtx<'ctx> { self.errors.span_err(span, msg) } - pub(crate) fn with_def_id(&mut self, def_id: DefId, f: F) -> T + pub(crate) fn with_def_id(&mut self, def_id: DefId, def_id_is_local: bool, f: F) -> T where F: FnOnce(&mut Self) -> T, { let current_def_id = self.errors.def_id; + let current_def_id_is_local = self.errors.def_id_is_local; self.errors.def_id = Some(def_id); + self.errors.def_id_is_local = def_id_is_local; let ret = f(self); self.errors.def_id = current_def_id; + self.errors.def_id_is_local = current_def_id_is_local; ret } @@ -279,7 +282,7 @@ impl<'ctx> TransformCtx<'ctx> { } Err(Opaque) => Err(Opaque), }; - ctx.with_def_id(decl.rust_id, |ctx| { + ctx.with_def_id(decl.rust_id, decl.item_meta.is_local, |ctx| { f(ctx, decl, body); }) } @@ -305,7 +308,7 @@ impl<'ctx> TransformCtx<'ctx> { } Err(Opaque) => Err(Opaque), }; - ctx.with_def_id(decl.rust_id, |ctx| { + ctx.with_def_id(decl.rust_id, decl.item_meta.is_local, |ctx| { f(ctx, decl, body); }) } From 98ca26a6aacb968d486ad8b283588bbf7f8be12b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 5 Oct 2024 16:31:10 +0200 Subject: [PATCH 7/9] Use `AnyDeclId` to track error dependencies --- charon/src/ast/meta.rs | 30 +++++++- charon/src/ast/meta_utils.rs | 17 +++++ charon/src/bin/charon-driver/driver.rs | 3 +- .../translate/translate_crate_to_ullbc.rs | 10 +-- .../charon-driver/translate/translate_ctx.rs | 40 ++++++---- charon/src/errors.rs | 74 +++++-------------- charon/src/transform/ctx.rs | 14 ++-- charon/tests/ui/error-dependencies.out | 2 +- 8 files changed, 106 insertions(+), 84 deletions(-) diff --git a/charon/src/ast/meta.rs b/charon/src/ast/meta.rs index 3e2f1cb1a..e4655f990 100644 --- a/charon/src/ast/meta.rs +++ b/charon/src/ast/meta.rs @@ -9,7 +9,20 @@ use std::path::PathBuf; generate_index_type!(FileId); -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] +#[derive( + Debug, + Copy, + Clone, + PartialEq, + Eq, + PartialOrd, + Ord, + Hash, + Serialize, + Deserialize, + Drive, + DriveMut, +)] pub struct Loc { /// The (1-based) line number. pub line: usize, @@ -47,7 +60,20 @@ impl From for rustc_error_messages::MultiSpan { } /// Meta information about a piece of code (block, statement, etc.) -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] +#[derive( + Debug, + Copy, + Clone, + PartialEq, + Eq, + PartialOrd, + Ord, + Hash, + Serialize, + Deserialize, + Drive, + DriveMut, +)] pub struct Span { /// The source code span. /// diff --git a/charon/src/ast/meta_utils.rs b/charon/src/ast/meta_utils.rs index bd56c116c..c724c7858 100644 --- a/charon/src/ast/meta_utils.rs +++ b/charon/src/ast/meta_utils.rs @@ -42,6 +42,23 @@ impl RawSpan { rust_span_data: rustc_span::DUMMY_SP.data(), } } + + /// Value with which we order `RawSpans`s. + fn sort_key(&self) -> impl Ord { + (self.file_id, self.beg, self.end) + } +} + +/// Manual impls because `SpanData` is not orderable. +impl PartialOrd for RawSpan { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} +impl Ord for RawSpan { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.sort_key().cmp(&other.sort_key()) + } } impl Span { diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index 412160c00..79879c1a2 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -1,5 +1,6 @@ use crate::translate::translate_crate_to_ullbc; use charon_lib::export; +use charon_lib::formatter::IntoFormatter; use charon_lib::options; use charon_lib::reorder_decls::compute_reordered_decls; use charon_lib::transform::{LLBC_PASSES, ULLBC_PASSES}; @@ -271,7 +272,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa } // Display an error report about the external dependencies, if necessary - ctx.errors.report_external_deps_errors(); + ctx.errors.report_external_deps_errors(ctx.into_fmt()); } trace!("Done"); 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 d76a70be0..834beb1ad 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 @@ -250,12 +250,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } pub(crate) fn translate_item(&mut self, rust_id: DefId, trans_id: AnyTransId) { - if self.errors.ignored_failed_decls.contains(&rust_id) + if self.errors.ignored_failed_decls.contains(&trans_id) || self.translated.get_item(trans_id).is_some() { return; } - self.with_def_id(rust_id, |mut ctx| { + self.with_def_id(rust_id, trans_id, |mut ctx| { let span = ctx.def_span(rust_id); // Catch cycles let res = if ctx.translate_stack.contains(&trans_id) { @@ -299,7 +299,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { span, &format!("Ignoring the following item due to an error: {rust_id:?}"), ); - ctx.errors.ignore_failed_decl(rust_id); + ctx.errors.ignore_failed_decl(trans_id); } }) } @@ -321,7 +321,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { let item_meta = self.translate_item_meta(&def, name, opacity)?; // Initialize the body translation context - let bt_ctx = BodyTransCtx::new(rust_id, self); + let bt_ctx = BodyTransCtx::new(rust_id, Some(trans_id), self); match trans_id { AnyTransId::Type(id) => { let ty = bt_ctx.translate_type(id, item_meta, &def)?; @@ -355,7 +355,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Translate if not already translated. self.translate_item(rust_id, id); - if self.errors.ignored_failed_decls.contains(&rust_id) { + if self.errors.ignored_failed_decls.contains(&id) { let span = self.def_span(rust_id); error_or_panic!(self, span, format!("Failed to translate item {id:?}.")) } diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index e90318132..8bdf9825c 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -200,8 +200,10 @@ pub struct TranslateCtx<'tcx, 'ctx> { /// us to use those collections. pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// The definition we are currently extracting. - /// TODO: this duplicates the field of [TranslateCtx] + /// TODO: this duplicates the field of [ErrorCtx] pub def_id: DefId, + /// The id of the definition we are currently extracting, if there is one. + pub item_id: Option, /// The translation context containing the top-level definitions/ids. pub t_ctx: &'ctx mut TranslateCtx<'tcx, 'ctx1>, /// A hax state with an owner id @@ -346,7 +348,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // We need to convert the type, which may contain quantified // substs and bounds. In order to properly do so, we introduce // a body translation context. - let mut bt_ctx = BodyTransCtx::new(def_id, self); + let mut bt_ctx = BodyTransCtx::new(def_id, None, self); let generics = bt_ctx.translate_def_generics(span, &def)?; let ty = bt_ctx.translate_ty(span, erase_regions, &ty)?; ImplElem::Ty(generics, ty) @@ -746,12 +748,17 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } /// Register the fact that `id` is a dependency of `src` (if `src` is not `None`). - pub(crate) fn register_dep_source(&mut self, src: &Option, id: DefId) { + pub(crate) fn register_dep_source( + &mut self, + src: &Option, + def_id: DefId, + item_id: AnyTransId, + ) { if let Some(src) = src { - if src.src_id != id && !id.is_local() { + if src.src_id != item_id && !def_id.is_local() { self.errors .external_dep_sources - .entry(id) + .entry(item_id) .or_default() .insert(*src); } @@ -760,8 +767,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub(crate) fn register_id(&mut self, src: &Option, id: OrdRustId) -> AnyTransId { let rust_id = id.get_id(); - self.register_dep_source(src, rust_id); - match self.translated.id_map.get(&rust_id) { + let item_id = match self.translated.id_map.get(&rust_id) { Some(tid) => *tid, None => { let trans_id = match id { @@ -795,7 +801,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } trans_id } - } + }; + self.register_dep_source(src, rust_id, item_id); + item_id } pub(crate) fn register_type_decl_id( @@ -866,13 +874,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { .unwrap() } - pub(crate) fn with_def_id(&mut self, def_id: DefId, f: F) -> T + pub(crate) fn with_def_id(&mut self, def_id: DefId, item_id: AnyTransId, f: F) -> T where F: FnOnce(&mut Self) -> T, { let current_def_id = self.errors.def_id; let current_def_id_is_local = self.errors.def_id_is_local; - self.errors.def_id = Some(def_id); + self.errors.def_id = Some(item_id); self.errors.def_id_is_local = def_id.is_local(); let ret = f(self); self.errors.def_id = current_def_id; @@ -883,10 +891,15 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { /// Create a new `ExecContext`. - pub(crate) fn new(def_id: DefId, t_ctx: &'ctx mut TranslateCtx<'tcx, 'ctx1>) -> Self { + pub(crate) fn new( + def_id: DefId, + item_id: Option, + t_ctx: &'ctx mut TranslateCtx<'tcx, 'ctx1>, + ) -> Self { let hax_state = hax::State::new_from_state_and_id(&t_ctx.hax_state, def_id); BodyTransCtx { def_id, + item_id, t_ctx, hax_state, error_on_impl_expr_error: true, @@ -1101,10 +1114,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } pub(crate) fn make_dep_source(&self, span: Span) -> Option { - let src_id = self.def_id; Some(DepSource { - src_id, - span: src_id.is_local().then_some(span), + src_id: self.item_id?, + span: self.def_id.is_local().then_some(span), }) } } diff --git a/charon/src/errors.rs b/charon/src/errors.rs index f3ec4d46e..d093bd4a2 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -1,11 +1,11 @@ //! Utilities to generate error reports about the external dependencies. -use crate::ast::Span; +use crate::ast::{AnyTransId, Span}; +use crate::formatter::{FmtCtx, Formatter}; use macros::VariantIndexArity; use petgraph::algo::dijkstra::dijkstra; use petgraph::graphmap::DiGraphMap; use rustc_error_messages::MultiSpan; use rustc_errors::DiagCtxtHandle; -use rustc_span::def_id::DefId; use std::cmp::{Ord, PartialOrd}; use std::collections::{HashMap, HashSet}; @@ -62,33 +62,14 @@ pub use error_assert; /// dependencies, especially if some external dependencies don't extract: /// we use this information to tell the user what is the code which /// (transitively) lead to the extraction of those problematic dependencies. -#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)] pub struct DepSource { - pub src_id: DefId, + pub src_id: AnyTransId, /// The location where the id was referred to. We store `None` for external dependencies as we /// don't want to show these to the users. pub span: Option, } -impl DepSource { - /// Value with which we order `DepSource`s. - fn sort_key(&self) -> impl Ord { - (self.src_id.index, self.src_id.krate) - } -} - -/// Manual impls because `DefId` is not orderable. -impl PartialOrd for DepSource { - fn partial_cmp(&self, other: &Self) -> Option { - Some(self.cmp(other)) - } -} -impl Ord for DepSource { - fn cmp(&self, other: &Self) -> std::cmp::Ordering { - self.sort_key().cmp(&other.sort_key()) - } -} - /// The context for tracking and reporting errors. pub struct ErrorCtx<'ctx> { /// If true, do not abort on the first error and attempt to extract as much as possible. @@ -99,13 +80,13 @@ pub struct ErrorCtx<'ctx> { /// The compiler session, used for displaying errors. pub dcx: DiagCtxtHandle<'ctx>, /// The ids of the external_declarations for which extraction we encountered errors. - pub external_decls_with_errors: HashSet, + pub external_decls_with_errors: HashSet, /// The ids of the declarations we completely failed to extract and had to ignore. - pub ignored_failed_decls: HashSet, + pub ignored_failed_decls: HashSet, /// For each external item, a list of locations that point to it. See [DepSource]. - pub external_dep_sources: HashMap>, + pub external_dep_sources: HashMap>, /// The id of the definition we are exploring, used to track the source of errors. - pub def_id: Option, + pub def_id: Option, /// Whether the definition being explored is local to the crate or not. pub def_id_is_local: bool, /// The number of errors encountered so far. @@ -141,38 +122,17 @@ impl ErrorCtx<'_> { } } - pub fn ignore_failed_decl(&mut self, id: DefId) { + pub fn ignore_failed_decl(&mut self, id: AnyTransId) { self.ignored_failed_decls.insert(id); } } /// For tracing error dependencies. -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, VariantIndexArity)] +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)] enum Node { - External(DefId), + External(AnyTransId), /// We use the span information only for local references - Local(DefId, Span), -} - -impl Node { - /// Value with which we order `Node`s. - fn sort_key(&self) -> impl Ord { - let (variant_index, _) = self.variant_index_arity(); - let (Self::External(def_id) | Self::Local(def_id, _)) = self; - (variant_index, def_id.index, def_id.krate) - } -} - -/// Manual impls because `DefId` is not orderable. -impl PartialOrd for Node { - fn partial_cmp(&self, other: &Self) -> Option { - Some(self.cmp(other)) - } -} -impl Ord for Node { - fn cmp(&self, other: &Self) -> std::cmp::Ordering { - self.sort_key().cmp(&other.sort_key()) - } + Local(AnyTransId, Span), } struct Graph { @@ -216,7 +176,7 @@ impl ErrorCtx<'_> { /// the external dependencies, print a detailed report to explain /// to the user which dependencies were problematic, and where they /// are used in the code. - pub fn report_external_deps_errors(&self) { + pub fn report_external_deps_errors(&self, f: FmtCtx<'_>) { if !self.has_errors() { return; } @@ -261,9 +221,11 @@ impl ErrorCtx<'_> { // Display the error message let span = MultiSpan::from_spans(reachable); - let msg = format!("The external definition `{:?}` triggered errors. It is (transitively) used at the following location(s):", - *id, - ); + let msg = format!( + "The external definition `{}` triggered errors. \ + It is (transitively) used at the following location(s):", + f.format_object(*id) + ); self.span_err_no_register(span, &msg); } } diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index b9eef3ee3..cb12cf06d 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -6,7 +6,6 @@ use crate::llbc_ast; use crate::name_matcher::NamePattern; use crate::pretty::FmtWithCtx; use crate::ullbc_ast; -use rustc_span::def_id::DefId; use std::fmt; /// The options that control transformation. @@ -202,13 +201,18 @@ impl<'ctx> TransformCtx<'ctx> { self.errors.span_err(span, msg) } - pub(crate) fn with_def_id(&mut self, def_id: DefId, def_id_is_local: bool, f: F) -> T + pub(crate) fn with_def_id( + &mut self, + def_id: impl Into, + def_id_is_local: bool, + f: F, + ) -> T where F: FnOnce(&mut Self) -> T, { let current_def_id = self.errors.def_id; let current_def_id_is_local = self.errors.def_id_is_local; - self.errors.def_id = Some(def_id); + self.errors.def_id = Some(def_id.into()); self.errors.def_id_is_local = def_id_is_local; let ret = f(self); self.errors.def_id = current_def_id; @@ -282,7 +286,7 @@ impl<'ctx> TransformCtx<'ctx> { } Err(Opaque) => Err(Opaque), }; - ctx.with_def_id(decl.rust_id, decl.item_meta.is_local, |ctx| { + ctx.with_def_id(decl.def_id, decl.item_meta.is_local, |ctx| { f(ctx, decl, body); }) } @@ -308,7 +312,7 @@ impl<'ctx> TransformCtx<'ctx> { } Err(Opaque) => Err(Opaque), }; - ctx.with_def_id(decl.rust_id, decl.item_meta.is_local, |ctx| { + ctx.with_def_id(decl.def_id, decl.item_meta.is_local, |ctx| { f(ctx, decl, body); }) } diff --git a/charon/tests/ui/error-dependencies.out b/charon/tests/ui/error-dependencies.out index b70f78262..5dfec2cfd 100644 --- a/charon/tests/ui/error-dependencies.out +++ b/charon/tests/ui/error-dependencies.out @@ -4,7 +4,7 @@ error: Trait aliases are not supported error: Ignoring the following item due to an error: core::ptr::metadata::Thin --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/ptr/metadata.rs:81:1 -error: The external definition `core::ptr::metadata::Thin` triggered errors. It is (transitively) used at the following location(s): +error: The external definition `@TraitDecl0` triggered errors. It is (transitively) used at the following location(s): --> tests/ui/error-dependencies.rs:8:13 | 8 | let _ = core::ptr::null::(); From 5e78f21d6bf303e50ce63c9a233a234e5230c334 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 5 Oct 2024 16:38:04 +0200 Subject: [PATCH 8/9] Improve the printing of missing items --- charon/src/pretty/fmt_with_ctx.rs | 13 +++++ charon/src/pretty/formatter.rs | 68 +++++++------------------- charon/tests/ui/error-dependencies.out | 2 +- charon/tests/ui/opacity.out | 2 +- charon/tests/ui/unsafe.out | 6 +-- 5 files changed, 37 insertions(+), 54 deletions(-) diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 46623ab83..2e0bf951c 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1542,6 +1542,19 @@ impl FmtWithCtx for Variant { } } +impl std::fmt::Display for AnyTransId { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { + let s = match self { + AnyTransId::Type(x) => x.to_pretty_string(), + AnyTransId::Fun(x) => x.to_pretty_string(), + AnyTransId::Global(x) => x.to_pretty_string(), + AnyTransId::TraitDecl(x) => x.to_pretty_string(), + AnyTransId::TraitImpl(x) => x.to_pretty_string(), + }; + f.write_str(&s) + } +} + impl std::fmt::Display for BinOp { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { match self { diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 04bea2c82..7a706cebb 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -211,84 +211,54 @@ impl<'a> FmtCtx<'a> { impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: TypeDeclId) -> String { - match &self.translated { - None => id.to_pretty_string(), - Some(translated) => match translated.type_decls.get(id) { - None => id.to_pretty_string(), - Some(d) => d.item_meta.name.fmt_with_ctx(self), - }, - } + self.format_object(AnyTransId::from(id)) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: GlobalDeclId) -> String { - match &self.translated { - None => id.to_pretty_string(), - Some(translated) => match translated.global_decls.get(id) { - None => id.to_pretty_string(), - Some(d) => d.item_meta.name.fmt_with_ctx(self), - }, - } + self.format_object(AnyTransId::from(id)) } } -impl<'a> Formatter for FmtCtx<'a> { +impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: ast::FunDeclId) -> String { - match &self.translated { - None => id.to_pretty_string(), - Some(translated) => match translated.fun_decls.get(id) { - None => id.to_pretty_string(), - Some(d) => d.item_meta.name.fmt_with_ctx(self), - }, - } + self.format_object(AnyTransId::from(id)) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: BodyId) -> String { - match &self.translated { + match self + .translated + .and_then(|translated| translated.bodies.get(id)) + { None => "".to_owned(), - Some(translated) => match translated.bodies.get(id) { - None => "".to_owned(), - Some(d) => d.fmt_with_ctx(self), - }, + Some(d) => d.fmt_with_ctx(self), } } } -impl<'a> Formatter for FmtCtx<'a> { +impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: ast::TraitDeclId) -> String { - match &self.translated { - None => id.to_pretty_string(), - Some(translated) => match translated.trait_decls.get(id) { - None => id.to_pretty_string(), - Some(d) => d.item_meta.name.fmt_with_ctx(self), - }, - } + self.format_object(AnyTransId::from(id)) } } -impl<'a> Formatter for FmtCtx<'a> { +impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: ast::TraitImplId) -> String { - match &self.translated { - None => id.to_pretty_string(), - Some(translated) => match translated.trait_impls.get(id) { - None => id.to_pretty_string(), - Some(d) => d.item_meta.name.fmt_with_ctx(self), - }, - } + self.format_object(AnyTransId::from(id)) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, id: AnyTransId) -> String { - match id { - AnyTransId::Type(x) => self.format_object(x), - AnyTransId::Fun(x) => self.format_object(x), - AnyTransId::Global(x) => self.format_object(x), - AnyTransId::TraitDecl(x) => self.format_object(x), - AnyTransId::TraitImpl(x) => self.format_object(x), + match self + .translated + .and_then(|translated| translated.item_names.get(&id)) + { + None => id.to_string(), + Some(name) => name.fmt_with_ctx(self), } } } diff --git a/charon/tests/ui/error-dependencies.out b/charon/tests/ui/error-dependencies.out index 5dfec2cfd..b70f78262 100644 --- a/charon/tests/ui/error-dependencies.out +++ b/charon/tests/ui/error-dependencies.out @@ -4,7 +4,7 @@ error: Trait aliases are not supported error: Ignoring the following item due to an error: core::ptr::metadata::Thin --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/ptr/metadata.rs:81:1 -error: The external definition `@TraitDecl0` triggered errors. It is (transitively) used at the following location(s): +error: The external definition `core::ptr::metadata::Thin` triggered errors. It is (transitively) used at the following location(s): --> tests/ui/error-dependencies.rs:8:13 | 8 | let _ = core::ptr::null::(); diff --git a/charon/tests/ui/opacity.out b/charon/tests/ui/opacity.out index 2209958f8..8d4e18047 100644 --- a/charon/tests/ui/opacity.out +++ b/charon/tests/ui/opacity.out @@ -114,7 +114,7 @@ fn test_crate::foo() @8 := const (0 : i32) @7 := &@8 @6 := &*(@7) - @5 := @Fun4[core::marker::Sized](move (@6)) + @5 := core::slice::raw::from_ref[core::marker::Sized](move (@6)) drop @6 @fake_read(@5) drop @8 diff --git a/charon/tests/ui/unsafe.out b/charon/tests/ui/unsafe.out index d9fb88f37..6edaa16dd 100644 --- a/charon/tests/ui/unsafe.out +++ b/charon/tests/ui/unsafe.out @@ -2,7 +2,7 @@ fn core::ptr::null() -> *const T where - [@TraitClause0]: @TraitDecl1, + [@TraitClause0]: core::ptr::metadata::Thin, trait core::marker::Sized @@ -18,7 +18,7 @@ fn test_crate::call_unsafe_fn() let @3: *const u32; // anonymous local let @4: (); // anonymous local - x@1 := core::ptr::null[@TraitDecl1]() + x@1 := core::ptr::null[core::ptr::metadata::Thin]() @fake_read(x@1) @3 := copy (x@1) @2 := core::ptr::const_ptr::{*const T}::read[core::marker::Sized](move (@3)) @@ -39,7 +39,7 @@ fn test_crate::deref_raw_ptr() let @2: u32; // anonymous local let @3: (); // anonymous local - x@1 := core::ptr::null[@TraitDecl1]() + x@1 := core::ptr::null[core::ptr::metadata::Thin]() @fake_read(x@1) @2 := copy (*(x@1)) @fake_read(@2) From 8a80793e440b256611baf747483a1b24613a043e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 5 Oct 2024 16:51:08 +0200 Subject: [PATCH 9/9] Remove all references to `DefId` from charon-lib --- charon/src/ast/gast.rs | 17 ----------------- charon/src/ast/krate.rs | 11 ----------- .../translate/translate_crate_to_ullbc.rs | 4 +++- .../charon-driver/translate/translate_ctx.rs | 11 ++++++++--- .../translate/translate_functions_to_ullbc.rs | 2 -- charon/src/transform/reorder_decls.rs | 16 +++++----------- 6 files changed, 16 insertions(+), 45 deletions(-) diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 7812c4ff6..4b51f95b0 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -12,21 +12,12 @@ use crate::values::*; use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use macros::EnumIsA; use macros::EnumToGetters; -use rustc_span::def_id::{CrateNum, DefId, DefIndex}; use serde::{Deserialize, Serialize}; use std::collections::HashMap; generate_index_type!(FunDeclId, "Fun"); generate_index_type!(BodyId, "Body"); -/// For use when deserializing. -fn dummy_def_id() -> DefId { - DefId { - krate: CrateNum::MAX, - index: DefIndex::MAX, - } -} - /// A variable #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)] pub struct Var { @@ -153,10 +144,6 @@ pub enum ItemKind { pub struct FunDecl { #[drive(skip)] pub def_id: FunDeclId, - #[serde(skip)] - #[drive(skip)] - #[serde(default = "dummy_def_id")] - pub rust_id: DefId, /// The meta data associated with the declaration. pub item_meta: ItemMeta, /// The signature contains the inputs/output types *with* non-erased regions. @@ -175,10 +162,6 @@ pub struct FunDecl { pub struct GlobalDecl { #[drive(skip)] pub def_id: GlobalDeclId, - #[serde(skip)] - #[drive(skip)] - #[serde(default = "dummy_def_id")] - pub rust_id: DefId, /// The meta data associated with the declaration. pub item_meta: ItemMeta, pub generics: GenericParams, diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 66367c0f4..3a17f79f0 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -5,7 +5,6 @@ use crate::reorder_decls::DeclarationsGroups; use derive_visitor::{Drive, DriveMut}; use hashlink::LinkedHashSet; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; -use rustc_span::def_id::DefId; use serde::{Deserialize, Serialize}; use serde_map_to_array::HashMapToArray; use std::cmp::{Ord, PartialOrd}; @@ -110,16 +109,6 @@ pub struct TranslatedCrate { /// failed to translate. #[serde(with = "HashMapToArray::")] pub item_names: HashMap, - /// The map from rustc id to translated id. - #[drive(skip)] - #[serde(skip)] - #[charon::opaque] - pub id_map: HashMap, - /// The reverse map of ids. - #[drive(skip)] - #[serde(skip)] - #[charon::opaque] - pub reverse_id_map: HashMap, /// The translated type definitions pub type_decls: Vector, 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 834beb1ad..d1494d42b 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 @@ -351,7 +351,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// translated version of this item. #[allow(dead_code)] pub(crate) fn get_or_translate(&mut self, id: AnyTransId) -> Result, Error> { - let rust_id = *self.translated.reverse_id_map.get(&id).unwrap(); + let rust_id = *self.reverse_id_map.get(&id).unwrap(); // Translate if not already translated. self.translate_item(rust_id, id); @@ -434,6 +434,8 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC real_crate_name, ..TranslatedCrate::default() }, + id_map: Default::default(), + reverse_id_map: Default::default(), priority_queue: Default::default(), translate_stack: Default::default(), cached_defs: 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 8bdf9825c..646af82b1 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -172,6 +172,11 @@ pub struct TranslateCtx<'tcx, 'ctx> { /// The translated data. pub translated: TranslatedCrate, + /// The map from rustc id to translated id. + pub id_map: HashMap, + /// The reverse map of ids. + pub reverse_id_map: HashMap, + /// Context for tracking and reporting errors. pub errors: ErrorCtx<'ctx>, /// The declarations we came accross and which we haven't translated yet. @@ -767,7 +772,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub(crate) fn register_id(&mut self, src: &Option, id: OrdRustId) -> AnyTransId { let rust_id = id.get_id(); - let item_id = match self.translated.id_map.get(&rust_id) { + let item_id = match self.id_map.get(&rust_id) { Some(tid) => *tid, None => { let trans_id = match id { @@ -789,8 +794,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { }; // Add the id to the queue of declarations to translate self.priority_queue.insert(id, trans_id); - self.translated.id_map.insert(id.get_id(), trans_id); - self.translated.reverse_id_map.insert(trans_id, id.get_id()); + self.id_map.insert(id.get_id(), trans_id); + self.reverse_id_map.insert(trans_id, id.get_id()); self.translated.all_ids.insert(trans_id); // Store the name early so the name matcher can identify paths. We can't to it for // trait impls because they register themselves when computing their name. 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 558d52b97..32977c588 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 @@ -1495,7 +1495,6 @@ impl BodyTransCtx<'_, '_, '_> { Ok(FunDecl { def_id, - rust_id, item_meta, signature, kind, @@ -1550,7 +1549,6 @@ impl BodyTransCtx<'_, '_, '_> { Ok(GlobalDecl { def_id, - rust_id, item_meta, generics, ty, diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs index 37ce81273..916ac85d2 100644 --- a/charon/src/transform/reorder_decls.rs +++ b/charon/src/transform/reorder_decls.rs @@ -95,23 +95,17 @@ pub struct DeclInfo { pub type DeclarationsGroups = Vec; -/// We use the [Debug] trait instead of [Display] for the identifiers, because -/// the rustc [DefId] doesn't implement [Display]... -impl Display for GDeclarationGroup { +impl Display for GDeclarationGroup { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), Error> { match self { - GDeclarationGroup::NonRec(id) => write!(f, "non-rec: {id:?}"), - GDeclarationGroup::Rec(ids) => write!( - f, - "rec: {}", - vec_to_string(&|id| format!(" {id:?}"), ids) - ), + GDeclarationGroup::NonRec(id) => write!(f, "non-rec: {id}"), + GDeclarationGroup::Rec(ids) => { + write!(f, "rec: {}", vec_to_string(&|id| format!(" {id}"), ids)) + } } } } -/// We use the [Debug] trait instead of [Display] for the identifiers, because -/// the rustc [DefId] doesn't implement [Display]... impl Display for DeclarationGroup { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), Error> { match self {