Minimize rustc dependencies in the main crate

charon/src/ast/gast.rs

@@ -12,14 +12,14 @@ 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};
 
 generate_index_type!(FunDeclId, "Fun");
 generate_index_type!(BodyId, "Body");
 
 /// For use when deserializing.
-fn dummy_def_id() -> rustc_hir::def_id::DefId {
-    use rustc_hir::def_id::*;
+fn dummy_def_id() -> DefId {
     DefId {
         krate: CrateNum::MAX,
         index: DefIndex::MAX,
@@ -145,7 +145,7 @@ pub struct FunDecl {
     #[serde(skip)]
     #[drive(skip)]
     #[serde(default = "dummy_def_id")]
-    pub rust_id: rustc_hir::def_id::DefId,
+    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.
@@ -167,7 +167,7 @@ pub struct GlobalDecl {
     #[serde(skip)]
     #[drive(skip)]
     #[serde(default = "dummy_def_id")]
-    pub rust_id: rustc_hir::def_id::DefId,
+    pub rust_id: DefId,
     /// The meta data associated with the declaration.
     pub item_meta: ItemMeta,
     pub generics: GenericParams,

charon/src/ast/krate.rs

@@ -7,7 +7,7 @@ use crate::types::*;
 use derive_visitor::{Drive, DriveMut};
 use linked_hash_set::LinkedHashSet;
 use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
-use rustc_hir::def_id::DefId;
+use rustc_span::def_id::DefId;
 use serde::{Deserialize, Serialize};
 use std::cmp::{Ord, PartialOrd};
 use std::collections::HashMap;

charon/src/ast/meta_utils.rs

@@ -1,21 +1,10 @@
 //! This file groups everything which is linked to implementations about [crate::meta]
 use crate::meta::*;
 use crate::names::{Disambiguator, Name, PathElem};
-use rustc_ast::{AttrArgs, NormalAttr};
-use rustc_hir::def_id::DefId;
-use rustc_middle::ty::TyCtxt;
 use rustc_span::source_map::SourceMap;
 use std::cmp::Ordering;
 use std::iter::Iterator;
 
-/// Retrieve the Rust span from a def id.
-///
-/// Rem.: we use [TyCtxt::def_span], not [TyCtxt::def_ident_span] to retrieve
-/// the span.
-pub fn get_rspan_from_def_id(ctx: TyCtxt, def_id: DefId) -> rustc_span::Span {
-    ctx.def_span(def_id)
-}
-
 impl Loc {
     fn min(l0: &Loc, l1: &Loc) -> Loc {
         match l0.line.cmp(&l1.line) {
@@ -131,36 +120,14 @@ pub fn span_to_string(source_map: &SourceMap, span: rustc_span::Span) -> String
 }
 
 impl Attribute {
-    pub fn parse(normal_attr: &NormalAttr, span: rustc_span::Span) -> Result<Self, String> {
-        // We use `pprust` to render the attribute somewhat like it is written in the source.
-        // WARNING: this can change whitespace, and sometimes even adds newlines. Maybe we
-        // should use spans and SourceMap info instead.
-        use rustc_ast_pretty::pprust::PrintState;
-
-        // If the attribute path has two components, the first of which is `charon` or `aeneas`, we
-        // try to parse it. Otherwise we return `Unknown`.
-        let attr_name = if let [path_start, attr_name] = normal_attr.item.path.segments.as_slice()
-            && let path_start = path_start.ident.as_str()
-            && (path_start == "charon" || path_start == "aeneas")
-        {
-            attr_name.ident.as_str()
-        } else {
-            let full_attr = rustc_ast_pretty::pprust::State::to_string(|s| {
-                s.print_attr_item(&normal_attr.item, span)
-            });
-            return Ok(Self::Unknown(full_attr));
-        };
-
-        let args = match &normal_attr.item.args {
-            AttrArgs::Empty => None,
-            AttrArgs::Delimited(args) => Some(rustc_ast_pretty::pprust::State::to_string(|s| {
-                s.print_tts(&args.tokens, false)
-            })),
-            AttrArgs::Eq(..) => unimplemented!("`#[charon::foo = val]` syntax is unsupported"),
-        };
-        match attr_name {
+    /// Parse a `charon::*` or `aeneas::*` attribute.
+    pub fn parse_special_attr(
+        attr_name: &str,
+        args: Option<String>,
+    ) -> Result<Option<Self>, String> {
+        let parsed = match attr_name {
             // `#[charon::opaque]`
-            "opaque" if args.is_none() => Ok(Self::Opaque),
+            "opaque" if args.is_none() => Self::Opaque,
             // `#[charon::rename("new_name")]`
             "rename" if let Some(attr) = args => {
                 let Some(attr) = attr
@@ -185,7 +152,7 @@ impl Attribute {
                     ));
                 }
 
-                Ok(Self::Rename(attr.to_string()))
+                Self::Rename(attr.to_string())
             }
             // `#[charon::variants_prefix("T")]`
             "variants_prefix" if let Some(attr) = args => {
@@ -198,7 +165,7 @@ impl Attribute {
                     ));
                 };
 
-                Ok(Self::VariantsPrefix(attr.to_string()))
+                Self::VariantsPrefix(attr.to_string())
             }
             // `#[charon::variants_suffix("T")]`
             "variants_suffix" if let Some(attr) = args => {
@@ -211,15 +178,11 @@ impl Attribute {
                     ));
                 };
 
-                Ok(Self::VariantsSuffix(attr.to_string()))
-            }
-            _ => {
-                let full_attr = rustc_ast_pretty::pprust::State::to_string(|s| {
-                    s.print_attr_item(&normal_attr.item, span)
-                });
-                Err(format!("Unrecognized attribute: `{full_attr}`"))
+                Self::VariantsSuffix(attr.to_string())
             }
-        }
+            _ => return Ok(None),
+        };
+        Ok(Some(parsed))
     }
 }
 

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -10,6 +10,8 @@ use charon_lib::ullbc_ast as ast;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::SInto;
 use macros::VariantIndexArity;
+use rustc_ast::AttrArgs;
+use rustc_ast_pretty::pprust;
 use rustc_error_messages::MultiSpan;
 use rustc_hir::def_id::DefId;
 use rustc_hir::Node as HirNode;
@@ -456,8 +458,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
 
     /// Compute the span information for a Rust definition identified by its id.
     pub(crate) fn translate_span_from_rid(&mut self, def_id: DefId) -> Span {
-        // Retrieve the span from the def id
-        let rspan = meta::get_rspan_from_def_id(self.tcx, def_id);
+        // Retrieve the span from the def id.
+        // Rem.: we use [TyCtxt::def_span], not [TyCtxt::def_ident_span] to retrieve the span.
+        let rspan = self.tcx.def_span(def_id);
         let rspan = rspan.sinto(&self.hax_state);
         self.translate_span_from_rspan(rspan)
     }
@@ -650,12 +653,54 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             .unwrap_or_default()
     }
 
+    /// Parse an attribute to recognize our special `charon::*` and `aeneas::*` attributes.
+    pub(crate) fn parse_attribute(
+        &mut self,
+        normal_attr: &rustc_ast::NormalAttr,
+        span: rustc_span::Span,
+    ) -> Result<Attribute, String> {
+        // We use `pprust` to render the attribute somewhat like it is written in the source.
+        // WARNING: this can change whitespace, and sometimes even adds newlines. Maybe we
+        // should use spans and SourceMap info instead.
+        use pprust::PrintState;
+
+        // If the attribute path has two components, the first of which is `charon` or `aeneas`, we
+        // try to parse it. Otherwise we return `Unknown`.
+        let attr_name = if let [path_start, attr_name] = normal_attr.item.path.segments.as_slice()
+            && let path_start = path_start.ident.as_str()
+            && (path_start == "charon" || path_start == "aeneas")
+        {
+            attr_name.ident.as_str()
+        } else {
+            let full_attr =
+                pprust::State::to_string(|s| s.print_attr_item(&normal_attr.item, span));
+            return Ok(Attribute::Unknown(full_attr));
+        };
+
+        let args = match &normal_attr.item.args {
+            AttrArgs::Empty => None,
+            AttrArgs::Delimited(args) => Some(rustc_ast_pretty::pprust::State::to_string(|s| {
+                s.print_tts(&args.tokens, false)
+            })),
+            AttrArgs::Eq(..) => unimplemented!("`#[charon::foo = val]` syntax is unsupported"),
+        };
+        match Attribute::parse_special_attr(attr_name, args)? {
+            Some(parsed) => Ok(parsed),
+            None => {
+                let full_attr = rustc_ast_pretty::pprust::State::to_string(|s| {
+                    s.print_attr_item(&normal_attr.item, span)
+                });
+                Err(format!("Unrecognized attribute: `{full_attr}`"))
+            }
+        }
+    }
+
     /// 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: &rustc_ast::Attribute) -> Option<Attribute> {
         use rustc_ast::ast::AttrKind;
         match &attr.kind {
-            AttrKind::Normal(normal_attr) => match Attribute::parse(&normal_attr, attr.span) {
+            AttrKind::Normal(normal_attr) => match self.parse_attribute(&normal_attr, attr.span) {
                 Ok(a) => Some(a),
                 Err(msg) => {
                     self.span_err(attr.span, &format!("Error parsing attribute: {msg}"));

charon/src/deps_errors.rs

@@ -4,7 +4,7 @@ use petgraph::algo::dijkstra::dijkstra;
 use petgraph::graphmap::DiGraphMap;
 use rustc_error_messages::MultiSpan;
 use rustc_errors::DiagCtxtHandle;
-use rustc_hir::def_id::DefId;
+use rustc_span::def_id::DefId;
 use std::cmp::{Ord, PartialOrd};
 use std::collections::{HashMap, HashSet};
 

charon/src/lib.rs

@@ -25,13 +25,9 @@
 // For when we use charon on itself :3
 #![register_tool(charon)]
 
-extern crate rustc_ast;
-extern crate rustc_ast_pretty;
 extern crate rustc_driver;
 extern crate rustc_error_messages;
 extern crate rustc_errors;
-extern crate rustc_hir;
-extern crate rustc_middle;
 extern crate rustc_span;
 
 #[macro_use]

charon/src/transform/ctx.rs

@@ -7,7 +7,7 @@ use crate::llbc_ast;
 use crate::pretty::FmtWithCtx;
 use crate::ullbc_ast;
 use rustc_error_messages::MultiSpan;
-use rustc_hir::def_id::DefId;
+use rustc_span::def_id::DefId;
 use std::fmt;
 
 /// Simpler context used for rustc-independent code transformation. This only depends on rustc for