Merge pull request #407 from Nadrieril/detangle-rustc

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,

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::<AnyTransId, Name>")]
     pub item_names: HashMap<AnyTransId, Name>,
-    /// The map from rustc id to translated id.
-    #[drive(skip)]
-    #[serde(skip)]
-    #[charon::opaque]
-    pub id_map: HashMap<DefId, AnyTransId>,
-    /// The reverse map of ids.
-    #[drive(skip)]
-    #[serde(skip)]
-    #[charon::opaque]
-    pub reverse_id_map: HashMap<AnyTransId, DefId>,
 
     /// The translated type definitions
     pub type_decls: Vector<TypeDeclId, TypeDecl>,

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<RawSpan> 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.
     ///

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,43 @@ 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(),
+        }
+    }
+
+    /// 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<std::cmp::Ordering> {
+        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 {
+    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 {

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::*;

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");

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> {
@@ -75,7 +74,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<ConstantExpr, Error> {
         use hax::ConstantExprKind;
@@ -202,7 +201,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<ConstGeneric, Error> {
         // Remark: we can't user globals as constant generics (meaning
@@ -237,7 +236,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<ConstantExpr, Error> {
         self.translate_constant_expr_to_constant_expr(span, &v.const_.constant_kind)

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;
@@ -251,13 +250,13 @@ 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| {
-            let span = ctx.tcx.def_span(rust_id);
+        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) {
                 ctx.span_err(
@@ -300,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);
             }
         })
     }
@@ -310,35 +309,38 @@ 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);
         if opacity.is_invisible() {
             // 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<hax::FullDef> = 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, Some(trans_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);
             }
         }
@@ -349,12 +351,12 @@ 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<AnyTransItem<'_>, 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);
 
-        if self.errors.ignored_failed_decls.contains(&rust_id) {
-            let span = self.tcx.def_span(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:?}."))
         }
         Ok(self.translated.get_item(id).unwrap())
@@ -414,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);
@@ -431,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(),