charon_lib/ast/
krate.rs

1use crate::ast::*;
2use crate::formatter::{FmtCtx, IntoFormatter};
3use crate::ids::Vector;
4use crate::pretty::FmtWithCtx;
5use derive_generic_visitor::{ControlFlow, Drive, DriveMut};
6use index_vec::Idx;
7use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
8use serde::{Deserialize, Serialize};
9use serde_map_to_array::HashMapToArray;
10use std::cmp::{Ord, PartialOrd};
11use std::collections::HashMap;
12use std::fmt;
13
14generate_index_type!(FunDeclId, "Fun");
15generate_index_type!(TypeDeclId, "Adt");
16generate_index_type!(GlobalDeclId, "Global");
17generate_index_type!(TraitDeclId, "TraitDecl");
18generate_index_type!(TraitImplId, "TraitImpl");
19
20/// The id of a translated item.
21#[derive(
22    Copy,
23    Clone,
24    Debug,
25    PartialOrd,
26    Ord,
27    PartialEq,
28    Eq,
29    Hash,
30    EnumIsA,
31    EnumAsGetters,
32    VariantName,
33    VariantIndexArity,
34    Serialize,
35    Deserialize,
36    Drive,
37    DriveMut,
38)]
39#[charon::variants_prefix("Id")]
40pub enum ItemId {
41    Type(TypeDeclId),
42    Fun(FunDeclId),
43    Global(GlobalDeclId),
44    TraitDecl(TraitDeclId),
45    TraitImpl(TraitImplId),
46}
47
48/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
49macro_rules! wrap_unwrap_enum {
50    ($enum:ident::$variant:ident($variant_ty:ident)) => {
51        impl TryFrom<$enum> for $variant_ty {
52            type Error = ();
53            fn try_from(x: $enum) -> Result<Self, Self::Error> {
54                match x {
55                    $enum::$variant(x) => Ok(x),
56                    _ => Err(()),
57                }
58            }
59        }
60
61        impl From<$variant_ty> for $enum {
62            fn from(x: $variant_ty) -> Self {
63                $enum::$variant(x)
64            }
65        }
66    };
67}
68
69wrap_unwrap_enum!(ItemId::Fun(FunDeclId));
70wrap_unwrap_enum!(ItemId::Global(GlobalDeclId));
71wrap_unwrap_enum!(ItemId::Type(TypeDeclId));
72wrap_unwrap_enum!(ItemId::TraitDecl(TraitDeclId));
73wrap_unwrap_enum!(ItemId::TraitImpl(TraitImplId));
74impl TryFrom<ItemId> for TypeId {
75    type Error = ();
76    fn try_from(x: ItemId) -> Result<Self, Self::Error> {
77        Ok(TypeId::Adt(x.try_into()?))
78    }
79}
80impl TryFrom<ItemId> for FunId {
81    type Error = ();
82    fn try_from(x: ItemId) -> Result<Self, Self::Error> {
83        Ok(FunId::Regular(x.try_into()?))
84    }
85}
86
87/// A translated item.
88#[derive(Debug, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity, Drive, DriveMut)]
89pub enum ItemByVal {
90    Type(TypeDecl),
91    Fun(FunDecl),
92    Global(GlobalDecl),
93    TraitDecl(TraitDecl),
94    TraitImpl(TraitImpl),
95}
96
97/// A reference to a translated item.
98#[derive(
99    Debug, Clone, Copy, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity, Drive, DriveMut,
100)]
101pub enum ItemRef<'ctx> {
102    Type(&'ctx TypeDecl),
103    Fun(&'ctx FunDecl),
104    Global(&'ctx GlobalDecl),
105    TraitDecl(&'ctx TraitDecl),
106    TraitImpl(&'ctx TraitImpl),
107}
108
109/// A mutable reference to a translated item.
110#[derive(Debug, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity, Drive, DriveMut)]
111pub enum ItemRefMut<'ctx> {
112    Type(&'ctx mut TypeDecl),
113    Fun(&'ctx mut FunDecl),
114    Global(&'ctx mut GlobalDecl),
115    TraitDecl(&'ctx mut TraitDecl),
116    TraitImpl(&'ctx mut TraitImpl),
117}
118
119/// A (group of) top-level declaration(s), properly reordered.
120/// "G" stands for "generic"
121#[derive(
122    Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize,
123)]
124#[charon::variants_suffix("Group")]
125pub enum GDeclarationGroup<Id> {
126    /// A non-recursive declaration
127    NonRec(Id),
128    /// A (group of mutually) recursive declaration(s)
129    Rec(Vec<Id>),
130}
131
132/// A (group of) top-level declaration(s), properly reordered.
133#[derive(
134    Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize,
135)]
136#[charon::variants_suffix("Group")]
137pub enum DeclarationGroup {
138    /// A type declaration group
139    Type(GDeclarationGroup<TypeDeclId>),
140    /// A function declaration group
141    Fun(GDeclarationGroup<FunDeclId>),
142    /// A global declaration group
143    Global(GDeclarationGroup<GlobalDeclId>),
144    ///
145    TraitDecl(GDeclarationGroup<TraitDeclId>),
146    ///
147    TraitImpl(GDeclarationGroup<TraitImplId>),
148    /// Anything that doesn't fit into these categories.
149    Mixed(GDeclarationGroup<ItemId>),
150}
151
152pub type DeclarationsGroups = Vec<DeclarationGroup>;
153
154#[derive(Default, Clone, Drive, DriveMut, Serialize, Deserialize)]
155pub struct TargetInfo {
156    /// The pointer size of the target in bytes.
157    pub target_pointer_size: types::ByteCount,
158    /// Whether the target platform uses little endian byte order.
159    pub is_little_endian: bool,
160}
161
162/// The data of a translated crate.
163#[derive(Default, Clone, Drive, DriveMut, Serialize, Deserialize)]
164pub struct TranslatedCrate {
165    /// The name of the crate.
166    #[drive(skip)]
167    pub crate_name: String,
168
169    /// The options used when calling Charon. It is useful for the applications
170    /// which consumed the serialized code, to check that Charon was called with
171    /// the proper options.
172    #[drive(skip)]
173    pub options: crate::options::CliOpts,
174
175    /// Information about the target platform for which rustc is called on for the crate.
176    #[drive(skip)]
177    pub target_information: TargetInfo,
178
179    /// The names of all registered items. Available so we can know the names even of items that
180    /// failed to translate.
181    /// Invariant: after translation, any existing `ItemId` must have an associated name, even
182    /// if the corresponding item wasn't translated.
183    #[serde(with = "HashMapToArray::<ItemId, Name>")]
184    pub item_names: HashMap<ItemId, Name>,
185    /// Short names, for items whose last PathElem is unique.
186    #[serde(with = "HashMapToArray::<ItemId, Name>")]
187    pub short_names: HashMap<ItemId, Name>,
188
189    /// The translated files.
190    #[drive(skip)]
191    pub files: Vector<FileId, File>,
192    /// The translated type definitions
193    pub type_decls: Vector<TypeDeclId, TypeDecl>,
194    /// The translated function definitions
195    pub fun_decls: Vector<FunDeclId, FunDecl>,
196    /// The translated global definitions
197    pub global_decls: Vector<GlobalDeclId, GlobalDecl>,
198    /// The translated trait declarations
199    pub trait_decls: Vector<TraitDeclId, TraitDecl>,
200    /// The translated trait declarations
201    pub trait_impls: Vector<TraitImplId, TraitImpl>,
202    /// A `const UNIT: () = ();` used whenever we make a thin pointer/reference to avoid creating a
203    /// local `let unit = ();` variable. It is always `Some`.
204    pub unit_metadata: Option<GlobalDeclRef>,
205    /// The re-ordered groups of declarations, initialized as empty.
206    #[drive(skip)]
207    pub ordered_decls: Option<DeclarationsGroups>,
208}
209
210impl TranslatedCrate {
211    pub fn item_name(&self, id: impl Into<ItemId>) -> Option<&Name> {
212        self.item_names.get(&id.into())
213    }
214
215    pub fn item_short_name(&self, id: impl Into<ItemId>) -> Option<&Name> {
216        let id = id.into();
217        self.short_names.get(&id).or_else(|| self.item_name(id))
218    }
219
220    pub fn get_item(&self, trans_id: impl Into<ItemId>) -> Option<ItemRef<'_>> {
221        match trans_id.into() {
222            ItemId::Type(id) => self.type_decls.get(id).map(ItemRef::Type),
223            ItemId::Fun(id) => self.fun_decls.get(id).map(ItemRef::Fun),
224            ItemId::Global(id) => self.global_decls.get(id).map(ItemRef::Global),
225            ItemId::TraitDecl(id) => self.trait_decls.get(id).map(ItemRef::TraitDecl),
226            ItemId::TraitImpl(id) => self.trait_impls.get(id).map(ItemRef::TraitImpl),
227        }
228    }
229    pub fn get_item_mut(&mut self, trans_id: ItemId) -> Option<ItemRefMut<'_>> {
230        match trans_id {
231            ItemId::Type(id) => self.type_decls.get_mut(id).map(ItemRefMut::Type),
232            ItemId::Fun(id) => self.fun_decls.get_mut(id).map(ItemRefMut::Fun),
233            ItemId::Global(id) => self.global_decls.get_mut(id).map(ItemRefMut::Global),
234            ItemId::TraitDecl(id) => self.trait_decls.get_mut(id).map(ItemRefMut::TraitDecl),
235            ItemId::TraitImpl(id) => self.trait_impls.get_mut(id).map(ItemRefMut::TraitImpl),
236        }
237    }
238    pub fn remove_item(&mut self, trans_id: ItemId) -> Option<ItemByVal> {
239        match trans_id {
240            ItemId::Type(id) => self.type_decls.remove(id).map(ItemByVal::Type),
241            ItemId::Fun(id) => self.fun_decls.remove(id).map(ItemByVal::Fun),
242            ItemId::Global(id) => self.global_decls.remove(id).map(ItemByVal::Global),
243            ItemId::TraitDecl(id) => self.trait_decls.remove(id).map(ItemByVal::TraitDecl),
244            ItemId::TraitImpl(id) => self.trait_impls.remove(id).map(ItemByVal::TraitImpl),
245        }
246    }
247    pub fn set_item_slot(&mut self, id: ItemId, item: ItemByVal) {
248        match item {
249            ItemByVal::Type(decl) => self.type_decls.set_slot(*id.as_type().unwrap(), decl),
250            ItemByVal::Fun(decl) => self.fun_decls.set_slot(*id.as_fun().unwrap(), decl),
251            ItemByVal::Global(decl) => self.global_decls.set_slot(*id.as_global().unwrap(), decl),
252            ItemByVal::TraitDecl(decl) => self
253                .trait_decls
254                .set_slot(*id.as_trait_decl().unwrap(), decl),
255            ItemByVal::TraitImpl(decl) => self
256                .trait_impls
257                .set_slot(*id.as_trait_impl().unwrap(), decl),
258        }
259    }
260
261    pub fn all_ids(&self) -> impl Iterator<Item = ItemId> + use<> {
262        self.type_decls
263            .all_indices()
264            .map(ItemId::Type)
265            .chain(self.trait_decls.all_indices().map(ItemId::TraitDecl))
266            .chain(self.trait_impls.all_indices().map(ItemId::TraitImpl))
267            .chain(self.global_decls.all_indices().map(ItemId::Global))
268            .chain(self.fun_decls.all_indices().map(ItemId::Fun))
269    }
270    pub fn all_items(&self) -> impl Iterator<Item = ItemRef<'_>> {
271        self.type_decls
272            .iter()
273            .map(ItemRef::Type)
274            .chain(self.trait_decls.iter().map(ItemRef::TraitDecl))
275            .chain(self.trait_impls.iter().map(ItemRef::TraitImpl))
276            .chain(self.global_decls.iter().map(ItemRef::Global))
277            .chain(self.fun_decls.iter().map(ItemRef::Fun))
278    }
279    pub fn all_items_mut(&mut self) -> impl Iterator<Item = ItemRefMut<'_>> {
280        self.type_decls
281            .iter_mut()
282            .map(ItemRefMut::Type)
283            .chain(self.trait_impls.iter_mut().map(ItemRefMut::TraitImpl))
284            .chain(self.trait_decls.iter_mut().map(ItemRefMut::TraitDecl))
285            .chain(self.fun_decls.iter_mut().map(ItemRefMut::Fun))
286            .chain(self.global_decls.iter_mut().map(ItemRefMut::Global))
287    }
288    pub fn all_items_with_ids(&self) -> impl Iterator<Item = (ItemId, ItemRef<'_>)> {
289        self.all_items().map(|item| (item.id(), item))
290    }
291}
292
293impl ItemByVal {
294    pub fn as_ref(&self) -> ItemRef<'_> {
295        match self {
296            Self::Type(d) => ItemRef::Type(d),
297            Self::Fun(d) => ItemRef::Fun(d),
298            Self::Global(d) => ItemRef::Global(d),
299            Self::TraitDecl(d) => ItemRef::TraitDecl(d),
300            Self::TraitImpl(d) => ItemRef::TraitImpl(d),
301        }
302    }
303    pub fn as_mut(&mut self) -> ItemRefMut<'_> {
304        match self {
305            Self::Type(d) => ItemRefMut::Type(d),
306            Self::Fun(d) => ItemRefMut::Fun(d),
307            Self::Global(d) => ItemRefMut::Global(d),
308            Self::TraitDecl(d) => ItemRefMut::TraitDecl(d),
309            Self::TraitImpl(d) => ItemRefMut::TraitImpl(d),
310        }
311    }
312}
313
314impl<'ctx> ItemRef<'ctx> {
315    pub fn id(&self) -> ItemId {
316        match self {
317            ItemRef::Type(d) => d.def_id.into(),
318            ItemRef::Fun(d) => d.def_id.into(),
319            ItemRef::Global(d) => d.def_id.into(),
320            ItemRef::TraitDecl(d) => d.def_id.into(),
321            ItemRef::TraitImpl(d) => d.def_id.into(),
322        }
323    }
324
325    pub fn clone(&self) -> ItemByVal {
326        match *self {
327            Self::Type(d) => ItemByVal::Type(d.clone()),
328            Self::Fun(d) => ItemByVal::Fun(d.clone()),
329            Self::Global(d) => ItemByVal::Global(d.clone()),
330            Self::TraitDecl(d) => ItemByVal::TraitDecl(d.clone()),
331            Self::TraitImpl(d) => ItemByVal::TraitImpl(d.clone()),
332        }
333    }
334
335    pub fn item_meta(&self) -> &'ctx ItemMeta {
336        match self {
337            Self::Type(d) => &d.item_meta,
338            Self::Fun(d) => &d.item_meta,
339            Self::Global(d) => &d.item_meta,
340            Self::TraitDecl(d) => &d.item_meta,
341            Self::TraitImpl(d) => &d.item_meta,
342        }
343    }
344    /// The generic parameters of this item.
345    pub fn generic_params(&self) -> &'ctx GenericParams {
346        match self {
347            ItemRef::Type(d) => &d.generics,
348            ItemRef::Fun(d) => &d.signature.generics,
349            ItemRef::Global(d) => &d.generics,
350            ItemRef::TraitDecl(d) => &d.generics,
351            ItemRef::TraitImpl(d) => &d.generics,
352        }
353    }
354
355    /// Get information about the parent of this item, if any.
356    pub fn parent_info(&self) -> &'ctx ItemSource {
357        match self {
358            ItemRef::Fun(d) => &d.src,
359            ItemRef::Global(d) => &d.src,
360            ItemRef::Type(_) | ItemRef::TraitDecl(_) | ItemRef::TraitImpl(_) => {
361                &ItemSource::TopLevel
362            }
363        }
364    }
365
366    /// See [`GenericParams::identity_args`].
367    pub fn identity_args(&self) -> GenericArgs {
368        self.generic_params().identity_args()
369    }
370
371    /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
372    /// `ItemRef` isn't contained in any of our types.
373    pub fn drive<V: VisitAst>(&self, visitor: &mut V) -> ControlFlow<V::Break> {
374        match *self {
375            ItemRef::Type(d) => visitor.visit(d),
376            ItemRef::Fun(d) => visitor.visit(d),
377            ItemRef::Global(d) => visitor.visit(d),
378            ItemRef::TraitDecl(d) => visitor.visit(d),
379            ItemRef::TraitImpl(d) => visitor.visit(d),
380        }
381    }
382
383    /// Visit all occurrences of that type inside `self`, in pre-order traversal.
384    pub fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
385        match *self {
386            ItemRef::Type(d) => d.dyn_visit(f),
387            ItemRef::Fun(d) => d.dyn_visit(f),
388            ItemRef::Global(d) => d.dyn_visit(f),
389            ItemRef::TraitDecl(d) => d.dyn_visit(f),
390            ItemRef::TraitImpl(d) => d.dyn_visit(f),
391        }
392    }
393}
394
395impl<'ctx> ItemRefMut<'ctx> {
396    pub fn as_ref(&self) -> ItemRef<'_> {
397        match self {
398            ItemRefMut::Type(d) => ItemRef::Type(d),
399            ItemRefMut::Fun(d) => ItemRef::Fun(d),
400            ItemRefMut::Global(d) => ItemRef::Global(d),
401            ItemRefMut::TraitDecl(d) => ItemRef::TraitDecl(d),
402            ItemRefMut::TraitImpl(d) => ItemRef::TraitImpl(d),
403        }
404    }
405    pub fn reborrow(&mut self) -> ItemRefMut<'_> {
406        match self {
407            ItemRefMut::Type(d) => ItemRefMut::Type(d),
408            ItemRefMut::Fun(d) => ItemRefMut::Fun(d),
409            ItemRefMut::Global(d) => ItemRefMut::Global(d),
410            ItemRefMut::TraitDecl(d) => ItemRefMut::TraitDecl(d),
411            ItemRefMut::TraitImpl(d) => ItemRefMut::TraitImpl(d),
412        }
413    }
414
415    pub fn set_id(&mut self, id: ItemId) {
416        match (self, id) {
417            (Self::Type(d), ItemId::Type(id)) => d.def_id = id,
418            (Self::Fun(d), ItemId::Fun(id)) => d.def_id = id,
419            (Self::Global(d), ItemId::Global(id)) => d.def_id = id,
420            (Self::TraitDecl(d), ItemId::TraitDecl(id)) => d.def_id = id,
421            (Self::TraitImpl(d), ItemId::TraitImpl(id)) => d.def_id = id,
422            _ => unreachable!(),
423        }
424    }
425
426    pub fn item_meta(&mut self) -> &mut ItemMeta {
427        match self {
428            Self::Type(d) => &mut d.item_meta,
429            Self::Fun(d) => &mut d.item_meta,
430            Self::Global(d) => &mut d.item_meta,
431            Self::TraitDecl(d) => &mut d.item_meta,
432            Self::TraitImpl(d) => &mut d.item_meta,
433        }
434    }
435    /// The generic parameters of this item.
436    pub fn generic_params(&mut self) -> &mut GenericParams {
437        match self {
438            ItemRefMut::Type(d) => &mut d.generics,
439            ItemRefMut::Fun(d) => &mut d.signature.generics,
440            ItemRefMut::Global(d) => &mut d.generics,
441            ItemRefMut::TraitDecl(d) => &mut d.generics,
442            ItemRefMut::TraitImpl(d) => &mut d.generics,
443        }
444    }
445
446    /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
447    /// `ItemRefMut` isn't contained in any of our types.
448    pub fn drive_mut<V: VisitAstMut>(&mut self, visitor: &mut V) -> ControlFlow<V::Break> {
449        match self {
450            ItemRefMut::Type(d) => visitor.visit(*d),
451            ItemRefMut::Fun(d) => visitor.visit(*d),
452            ItemRefMut::Global(d) => visitor.visit(*d),
453            ItemRefMut::TraitDecl(d) => visitor.visit(*d),
454            ItemRefMut::TraitImpl(d) => visitor.visit(*d),
455        }
456    }
457
458    /// Visit all occurrences of that type inside `self`, in pre-order traversal.
459    pub fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T)) {
460        match self {
461            ItemRefMut::Type(d) => d.dyn_visit_mut(f),
462            ItemRefMut::Fun(d) => d.dyn_visit_mut(f),
463            ItemRefMut::Global(d) => d.dyn_visit_mut(f),
464            ItemRefMut::TraitDecl(d) => d.dyn_visit_mut(f),
465            ItemRefMut::TraitImpl(d) => d.dyn_visit_mut(f),
466        }
467    }
468}
469
470impl fmt::Display for TranslatedCrate {
471    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
472        let fmt: &FmtCtx = &self.into_fmt();
473        match &self.ordered_decls {
474            None => {
475                // We do simple: types, globals, traits, functions
476                for d in &self.type_decls {
477                    writeln!(f, "{}\n", d.with_ctx(fmt))?
478                }
479                for d in &self.global_decls {
480                    writeln!(f, "{}\n", d.with_ctx(fmt))?
481                }
482                for d in &self.trait_decls {
483                    writeln!(f, "{}\n", d.with_ctx(fmt))?
484                }
485                for d in &self.trait_impls {
486                    writeln!(f, "{}\n", d.with_ctx(fmt))?
487                }
488                for d in &self.fun_decls {
489                    writeln!(f, "{}\n", d.with_ctx(fmt))?
490                }
491            }
492            Some(ordered_decls) => {
493                for gr in ordered_decls {
494                    for id in gr.get_ids() {
495                        writeln!(f, "{}\n", fmt.format_decl_id(id))?
496                    }
497                }
498            }
499        }
500        fmt::Result::Ok(())
501    }
502}
503
504impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate {
505    type C = FmtCtx<'a>;
506
507    fn into_fmt(self) -> Self::C {
508        FmtCtx {
509            translated: Some(self),
510            ..Default::default()
511        }
512    }
513}
514
515pub trait HasVectorOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
516    fn get_vector(&self) -> &Vector<Id, Self::Output>;
517    fn get_vector_mut(&mut self) -> &mut Vector<Id, Self::Output>;
518}
519
520/// Delegate `Index` implementations to subfields.
521macro_rules! mk_index_impls {
522    ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
523        impl std::ops::Index<$idx> for $ty {
524            type Output = $output;
525            fn index(&self, index: $idx) -> &Self::Output {
526                &self.$field[index]
527            }
528        }
529        impl std::ops::IndexMut<$idx> for $ty {
530            fn index_mut(&mut self, index: $idx) -> &mut Self::Output {
531                &mut self.$field[index]
532            }
533        }
534        impl HasVectorOf<$idx> for $ty {
535            fn get_vector(&self) -> &Vector<$idx, Self::Output> {
536                &self.$field
537            }
538            fn get_vector_mut(&mut self) -> &mut Vector<$idx, Self::Output> {
539                &mut self.$field
540            }
541        }
542    };
543}
544pub(crate) use mk_index_impls;
545
546mk_index_impls!(TranslatedCrate.type_decls[TypeDeclId]: TypeDecl);
547mk_index_impls!(TranslatedCrate.fun_decls[FunDeclId]: FunDecl);
548mk_index_impls!(TranslatedCrate.global_decls[GlobalDeclId]: GlobalDecl);
549mk_index_impls!(TranslatedCrate.trait_decls[TraitDeclId]: TraitDecl);
550mk_index_impls!(TranslatedCrate.trait_impls[TraitImplId]: TraitImpl);
charon_lib/ast/krate.rs

charon_lib/ast/
krate.rs
