charon_lib/ast/
krate.rs

1use crate::ast::*;
2use crate::formatter::{FmtCtx, IntoFormatter};
3use crate::ids::Vector;
4use crate::pretty::FmtWithCtx;
5use crate::reorder_decls::DeclarationsGroups;
6use derive_generic_visitor::{ControlFlow, Drive, DriveMut};
7use index_vec::Idx;
8use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
9use serde::{Deserialize, Serialize};
10use serde_map_to_array::HashMapToArray;
11use std::cmp::{Ord, PartialOrd};
12use std::collections::HashMap;
13use std::fmt;
14
15generate_index_type!(FunDeclId, "Fun");
16generate_index_type!(TypeDeclId, "Adt");
17generate_index_type!(GlobalDeclId, "Global");
18generate_index_type!(TraitDeclId, "TraitDecl");
19generate_index_type!(TraitImplId, "TraitImpl");
20
21/// The id of a translated item.
22#[derive(
23    Copy,
24    Clone,
25    Debug,
26    PartialOrd,
27    Ord,
28    PartialEq,
29    Eq,
30    Hash,
31    EnumIsA,
32    EnumAsGetters,
33    VariantName,
34    VariantIndexArity,
35    Serialize,
36    Deserialize,
37    Drive,
38    DriveMut,
39)]
40#[charon::rename("AnyDeclId")]
41#[charon::variants_prefix("Id")]
42pub enum AnyTransId {
43    Type(TypeDeclId),
44    Fun(FunDeclId),
45    Global(GlobalDeclId),
46    TraitDecl(TraitDeclId),
47    TraitImpl(TraitImplId),
48}
49
50/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
51macro_rules! wrap_unwrap_enum {
52    ($enum:ident::$variant:ident($variant_ty:ident)) => {
53        impl TryFrom<$enum> for $variant_ty {
54            type Error = ();
55            fn try_from(x: $enum) -> Result<Self, Self::Error> {
56                match x {
57                    $enum::$variant(x) => Ok(x),
58                    _ => Err(()),
59                }
60            }
61        }
62
63        impl From<$variant_ty> for $enum {
64            fn from(x: $variant_ty) -> Self {
65                $enum::$variant(x)
66            }
67        }
68    };
69}
70
71wrap_unwrap_enum!(AnyTransId::Fun(FunDeclId));
72wrap_unwrap_enum!(AnyTransId::Global(GlobalDeclId));
73wrap_unwrap_enum!(AnyTransId::Type(TypeDeclId));
74wrap_unwrap_enum!(AnyTransId::TraitDecl(TraitDeclId));
75wrap_unwrap_enum!(AnyTransId::TraitImpl(TraitImplId));
76
77/// A reference to a translated item.
78#[derive(
79    Debug, Clone, Copy, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity, Drive, DriveMut,
80)]
81pub enum AnyTransItem<'ctx> {
82    Type(&'ctx TypeDecl),
83    Fun(&'ctx FunDecl),
84    Global(&'ctx GlobalDecl),
85    TraitDecl(&'ctx TraitDecl),
86    TraitImpl(&'ctx TraitImpl),
87}
88
89/// A mutable reference to a translated item.
90#[derive(Debug, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity, Drive, DriveMut)]
91pub enum AnyTransItemMut<'ctx> {
92    Type(&'ctx mut TypeDecl),
93    Fun(&'ctx mut FunDecl),
94    Global(&'ctx mut GlobalDecl),
95    TraitDecl(&'ctx mut TraitDecl),
96    TraitImpl(&'ctx mut TraitImpl),
97}
98
99#[derive(Default, Clone, Drive, DriveMut, Serialize, Deserialize)]
100pub struct TargetInfo {
101    /// The pointer size of the target in bytes.
102    pub target_pointer_size: types::ByteCount,
103    /// Whether the target platform uses little endian byte order.
104    pub is_little_endian: bool,
105}
106
107/// The data of a translated crate.
108#[derive(Default, Clone, Drive, DriveMut, Serialize, Deserialize)]
109pub struct TranslatedCrate {
110    /// The name of the crate.
111    #[drive(skip)]
112    pub crate_name: String,
113
114    /// The options used when calling Charon. It is useful for the applications
115    /// which consumed the serialized code, to check that Charon was called with
116    /// the proper options.
117    #[drive(skip)]
118    pub options: crate::options::CliOpts,
119
120    /// Information about the target platform for which rustc is called on for the crate.
121    #[drive(skip)]
122    pub target_information: TargetInfo,
123
124    /// The names of all registered items. Available so we can know the names even of items that
125    /// failed to translate.
126    /// Invariant: after translation, any existing `AnyTransId` must have an associated name, even
127    /// if the corresponding item wasn't translated.
128    #[serde(with = "HashMapToArray::<AnyTransId, Name>")]
129    pub item_names: HashMap<AnyTransId, Name>,
130    /// Short names, for items whose last PathElem is unique.
131    #[serde(with = "HashMapToArray::<AnyTransId, Name>")]
132    pub short_names: HashMap<AnyTransId, Name>,
133
134    /// The translated files.
135    #[drive(skip)]
136    pub files: Vector<FileId, File>,
137    /// The translated type definitions
138    pub type_decls: Vector<TypeDeclId, TypeDecl>,
139    /// The translated function definitions
140    pub fun_decls: Vector<FunDeclId, FunDecl>,
141    /// The translated global definitions
142    pub global_decls: Vector<GlobalDeclId, GlobalDecl>,
143    /// The translated trait declarations
144    pub trait_decls: Vector<TraitDeclId, TraitDecl>,
145    /// The translated trait declarations
146    pub trait_impls: Vector<TraitImplId, TraitImpl>,
147    /// The re-ordered groups of declarations, initialized as empty.
148    #[drive(skip)]
149    pub ordered_decls: Option<DeclarationsGroups>,
150}
151
152impl TranslatedCrate {
153    pub fn item_name(&self, id: impl Into<AnyTransId>) -> Option<&Name> {
154        self.item_names.get(&id.into())
155    }
156
157    pub fn item_short_name(&self, id: impl Into<AnyTransId>) -> Option<&Name> {
158        let id = id.into();
159        self.short_names.get(&id).or_else(|| self.item_name(id))
160    }
161
162    pub fn get_item(&self, trans_id: impl Into<AnyTransId>) -> Option<AnyTransItem<'_>> {
163        match trans_id.into() {
164            AnyTransId::Type(id) => self.type_decls.get(id).map(AnyTransItem::Type),
165            AnyTransId::Fun(id) => self.fun_decls.get(id).map(AnyTransItem::Fun),
166            AnyTransId::Global(id) => self.global_decls.get(id).map(AnyTransItem::Global),
167            AnyTransId::TraitDecl(id) => self.trait_decls.get(id).map(AnyTransItem::TraitDecl),
168            AnyTransId::TraitImpl(id) => self.trait_impls.get(id).map(AnyTransItem::TraitImpl),
169        }
170    }
171
172    pub fn get_item_mut(&mut self, trans_id: AnyTransId) -> Option<AnyTransItemMut<'_>> {
173        match trans_id {
174            AnyTransId::Type(id) => self.type_decls.get_mut(id).map(AnyTransItemMut::Type),
175            AnyTransId::Fun(id) => self.fun_decls.get_mut(id).map(AnyTransItemMut::Fun),
176            AnyTransId::Global(id) => self.global_decls.get_mut(id).map(AnyTransItemMut::Global),
177            AnyTransId::TraitDecl(id) => {
178                self.trait_decls.get_mut(id).map(AnyTransItemMut::TraitDecl)
179            }
180            AnyTransId::TraitImpl(id) => {
181                self.trait_impls.get_mut(id).map(AnyTransItemMut::TraitImpl)
182            }
183        }
184    }
185
186    pub fn all_ids(&self) -> impl Iterator<Item = AnyTransId> + use<> {
187        self.type_decls
188            .all_indices()
189            .map(AnyTransId::Type)
190            .chain(self.trait_decls.all_indices().map(AnyTransId::TraitDecl))
191            .chain(self.trait_impls.all_indices().map(AnyTransId::TraitImpl))
192            .chain(self.global_decls.all_indices().map(AnyTransId::Global))
193            .chain(self.fun_decls.all_indices().map(AnyTransId::Fun))
194    }
195    pub fn all_items(&self) -> impl Iterator<Item = AnyTransItem<'_>> {
196        self.type_decls
197            .iter()
198            .map(AnyTransItem::Type)
199            .chain(self.trait_decls.iter().map(AnyTransItem::TraitDecl))
200            .chain(self.trait_impls.iter().map(AnyTransItem::TraitImpl))
201            .chain(self.global_decls.iter().map(AnyTransItem::Global))
202            .chain(self.fun_decls.iter().map(AnyTransItem::Fun))
203    }
204    pub fn all_items_mut(&mut self) -> impl Iterator<Item = AnyTransItemMut<'_>> {
205        self.type_decls
206            .iter_mut()
207            .map(AnyTransItemMut::Type)
208            .chain(self.trait_impls.iter_mut().map(AnyTransItemMut::TraitImpl))
209            .chain(self.trait_decls.iter_mut().map(AnyTransItemMut::TraitDecl))
210            .chain(self.fun_decls.iter_mut().map(AnyTransItemMut::Fun))
211            .chain(self.global_decls.iter_mut().map(AnyTransItemMut::Global))
212    }
213    pub fn all_items_with_ids(&self) -> impl Iterator<Item = (AnyTransId, AnyTransItem<'_>)> {
214        self.all_items().map(|item| (item.id(), item))
215    }
216}
217
218impl<'ctx> AnyTransItem<'ctx> {
219    pub fn id(&self) -> AnyTransId {
220        match self {
221            AnyTransItem::Type(d) => d.def_id.into(),
222            AnyTransItem::Fun(d) => d.def_id.into(),
223            AnyTransItem::Global(d) => d.def_id.into(),
224            AnyTransItem::TraitDecl(d) => d.def_id.into(),
225            AnyTransItem::TraitImpl(d) => d.def_id.into(),
226        }
227    }
228
229    pub fn item_meta(&self) -> &'ctx ItemMeta {
230        match self {
231            AnyTransItem::Type(d) => &d.item_meta,
232            AnyTransItem::Fun(d) => &d.item_meta,
233            AnyTransItem::Global(d) => &d.item_meta,
234            AnyTransItem::TraitDecl(d) => &d.item_meta,
235            AnyTransItem::TraitImpl(d) => &d.item_meta,
236        }
237    }
238
239    /// The generic parameters of this item.
240    pub fn generic_params(&self) -> &'ctx GenericParams {
241        match self {
242            AnyTransItem::Type(d) => &d.generics,
243            AnyTransItem::Fun(d) => &d.signature.generics,
244            AnyTransItem::Global(d) => &d.generics,
245            AnyTransItem::TraitDecl(d) => &d.generics,
246            AnyTransItem::TraitImpl(d) => &d.generics,
247        }
248    }
249
250    /// Get information about the parent of this item, if any.
251    pub fn parent_info(&self) -> &'ctx ItemKind {
252        match self {
253            AnyTransItem::Fun(d) => &d.kind,
254            AnyTransItem::Global(d) => &d.kind,
255            AnyTransItem::Type(_) | AnyTransItem::TraitDecl(_) | AnyTransItem::TraitImpl(_) => {
256                &ItemKind::TopLevel
257            }
258        }
259    }
260
261    /// See [`GenericParams::identity_args`].
262    pub fn identity_args(&self) -> GenericArgs {
263        self.generic_params().identity_args()
264    }
265
266    /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
267    /// `AnyTransItem` isn't contained in any of our types.
268    pub fn drive<V: VisitAst>(&self, visitor: &mut V) -> ControlFlow<V::Break> {
269        match *self {
270            AnyTransItem::Type(d) => visitor.visit(d),
271            AnyTransItem::Fun(d) => visitor.visit(d),
272            AnyTransItem::Global(d) => visitor.visit(d),
273            AnyTransItem::TraitDecl(d) => visitor.visit(d),
274            AnyTransItem::TraitImpl(d) => visitor.visit(d),
275        }
276    }
277
278    /// Visit all occurrences of that type inside `self`, in pre-order traversal.
279    pub fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
280        match *self {
281            AnyTransItem::Type(d) => d.dyn_visit(f),
282            AnyTransItem::Fun(d) => d.dyn_visit(f),
283            AnyTransItem::Global(d) => d.dyn_visit(f),
284            AnyTransItem::TraitDecl(d) => d.dyn_visit(f),
285            AnyTransItem::TraitImpl(d) => d.dyn_visit(f),
286        }
287    }
288}
289
290impl<'ctx> AnyTransItemMut<'ctx> {
291    pub fn as_ref(&self) -> AnyTransItem<'_> {
292        match self {
293            AnyTransItemMut::Type(d) => AnyTransItem::Type(d),
294            AnyTransItemMut::Fun(d) => AnyTransItem::Fun(d),
295            AnyTransItemMut::Global(d) => AnyTransItem::Global(d),
296            AnyTransItemMut::TraitDecl(d) => AnyTransItem::TraitDecl(d),
297            AnyTransItemMut::TraitImpl(d) => AnyTransItem::TraitImpl(d),
298        }
299    }
300
301    /// The generic parameters of this item.
302    pub fn generic_params(&mut self) -> &mut GenericParams {
303        match self {
304            AnyTransItemMut::Type(d) => &mut d.generics,
305            AnyTransItemMut::Fun(d) => &mut d.signature.generics,
306            AnyTransItemMut::Global(d) => &mut d.generics,
307            AnyTransItemMut::TraitDecl(d) => &mut d.generics,
308            AnyTransItemMut::TraitImpl(d) => &mut d.generics,
309        }
310    }
311
312    /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
313    /// `AnyTransItemMut` isn't contained in any of our types.
314    pub fn drive_mut<V: VisitAstMut>(&mut self, visitor: &mut V) -> ControlFlow<V::Break> {
315        match self {
316            AnyTransItemMut::Type(d) => visitor.visit(*d),
317            AnyTransItemMut::Fun(d) => visitor.visit(*d),
318            AnyTransItemMut::Global(d) => visitor.visit(*d),
319            AnyTransItemMut::TraitDecl(d) => visitor.visit(*d),
320            AnyTransItemMut::TraitImpl(d) => visitor.visit(*d),
321        }
322    }
323
324    /// Visit all occurrences of that type inside `self`, in pre-order traversal.
325    pub fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T)) {
326        match self {
327            AnyTransItemMut::Type(d) => d.dyn_visit_mut(f),
328            AnyTransItemMut::Fun(d) => d.dyn_visit_mut(f),
329            AnyTransItemMut::Global(d) => d.dyn_visit_mut(f),
330            AnyTransItemMut::TraitDecl(d) => d.dyn_visit_mut(f),
331            AnyTransItemMut::TraitImpl(d) => d.dyn_visit_mut(f),
332        }
333    }
334}
335
336impl fmt::Display for TranslatedCrate {
337    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
338        let fmt: &FmtCtx = &self.into_fmt();
339        match &self.ordered_decls {
340            None => {
341                // We do simple: types, globals, traits, functions
342                for d in &self.type_decls {
343                    writeln!(f, "{}\n", d.with_ctx(fmt))?
344                }
345                for d in &self.global_decls {
346                    writeln!(f, "{}\n", d.with_ctx(fmt))?
347                }
348                for d in &self.trait_decls {
349                    writeln!(f, "{}\n", d.with_ctx(fmt))?
350                }
351                for d in &self.trait_impls {
352                    writeln!(f, "{}\n", d.with_ctx(fmt))?
353                }
354                for d in &self.fun_decls {
355                    writeln!(f, "{}\n", d.with_ctx(fmt))?
356                }
357            }
358            Some(ordered_decls) => {
359                for gr in ordered_decls {
360                    for id in gr.get_ids() {
361                        writeln!(f, "{}\n", fmt.format_decl_id(id))?
362                    }
363                }
364            }
365        }
366        fmt::Result::Ok(())
367    }
368}
369
370impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate {
371    type C = FmtCtx<'a>;
372
373    fn into_fmt(self) -> Self::C {
374        FmtCtx {
375            translated: Some(self),
376            ..Default::default()
377        }
378    }
379}
380
381pub trait HasVectorOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
382    fn get_vector(&self) -> &Vector<Id, Self::Output>;
383    fn get_vector_mut(&mut self) -> &mut Vector<Id, Self::Output>;
384}
385
386/// Delegate `Index` implementations to subfields.
387macro_rules! mk_index_impls {
388    ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
389        impl std::ops::Index<$idx> for $ty {
390            type Output = $output;
391            fn index(&self, index: $idx) -> &Self::Output {
392                &self.$field[index]
393            }
394        }
395        impl std::ops::IndexMut<$idx> for $ty {
396            fn index_mut(&mut self, index: $idx) -> &mut Self::Output {
397                &mut self.$field[index]
398            }
399        }
400        impl HasVectorOf<$idx> for $ty {
401            fn get_vector(&self) -> &Vector<$idx, Self::Output> {
402                &self.$field
403            }
404            fn get_vector_mut(&mut self) -> &mut Vector<$idx, Self::Output> {
405                &mut self.$field
406            }
407        }
408    };
409}
410pub(crate) use mk_index_impls;
411
412mk_index_impls!(TranslatedCrate.type_decls[TypeDeclId]: TypeDecl);
413mk_index_impls!(TranslatedCrate.fun_decls[FunDeclId]: FunDecl);
414mk_index_impls!(TranslatedCrate.global_decls[GlobalDeclId]: GlobalDecl);
415mk_index_impls!(TranslatedCrate.trait_decls[TraitDeclId]: TraitDecl);
416mk_index_impls!(TranslatedCrate.trait_impls[TraitImplId]: TraitImpl);
charon_lib/ast/krate.rs

charon_lib/ast/
krate.rs
